1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub enum AtomicFact {
6 NormalAtomicFact(NormalAtomicFact),
7 EqualFact(EqualFact),
8 LessFact(LessFact),
9 GreaterFact(GreaterFact),
10 LessEqualFact(LessEqualFact),
11 GreaterEqualFact(GreaterEqualFact),
12 IsSetFact(IsSetFact),
13 IsNonemptySetFact(IsNonemptySetFact),
14 IsFiniteSetFact(IsFiniteSetFact),
15 InFact(InFact),
16 IsCartFact(IsCartFact),
17 IsTupleFact(IsTupleFact),
18 SubsetFact(SubsetFact),
19 SupersetFact(SupersetFact),
20 RestrictFact(RestrictFact),
21 NotRestrictFact(NotRestrictFact),
22 NotNormalAtomicFact(NotNormalAtomicFact),
23 NotEqualFact(NotEqualFact),
24 NotLessFact(NotLessFact),
25 NotGreaterFact(NotGreaterFact),
26 NotLessEqualFact(NotLessEqualFact),
27 NotGreaterEqualFact(NotGreaterEqualFact),
28 NotIsSetFact(NotIsSetFact),
29 NotIsNonemptySetFact(NotIsNonemptySetFact),
30 NotIsFiniteSetFact(NotIsFiniteSetFact),
31 NotInFact(NotInFact),
32 NotIsCartFact(NotIsCartFact),
33 NotIsTupleFact(NotIsTupleFact),
34 NotSubsetFact(NotSubsetFact),
35 NotSupersetFact(NotSupersetFact),
36}
37
38#[derive(Clone)]
39pub struct RestrictFact {
40 pub obj: Obj,
41 pub obj_can_restrict_to_fn_set: Obj,
42 pub line_file: LineFile,
43}
44
45#[derive(Clone)]
46pub struct NotRestrictFact {
47 pub obj: Obj,
48 pub obj_cannot_restrict_to_fn_set: Obj,
49 pub line_file: LineFile,
50}
51
52#[derive(Clone)]
53pub struct SupersetFact {
54 pub left: Obj,
55 pub right: Obj,
56 pub line_file: LineFile,
57}
58
59#[derive(Clone)]
60pub struct NotSupersetFact {
61 pub left: Obj,
62 pub right: Obj,
63 pub line_file: LineFile,
64}
65
66#[derive(Clone)]
67pub struct SubsetFact {
68 pub left: Obj,
69 pub right: Obj,
70 pub line_file: LineFile,
71}
72
73#[derive(Clone)]
74pub struct NotSubsetFact {
75 pub left: Obj,
76 pub right: Obj,
77 pub line_file: LineFile,
78}
79
80#[derive(Clone)]
81pub struct IsTupleFact {
82 pub set: Obj,
83 pub line_file: LineFile,
84}
85
86#[derive(Clone)]
87pub struct NotIsTupleFact {
88 pub set: Obj,
89 pub line_file: LineFile,
90}
91
92#[derive(Clone)]
93pub struct IsCartFact {
94 pub set: Obj,
95 pub line_file: LineFile,
96}
97
98#[derive(Clone)]
99pub struct NotIsCartFact {
100 pub set: Obj,
101 pub line_file: LineFile,
102}
103
104#[derive(Clone)]
105pub struct InFact {
106 pub element: Obj,
107 pub set: Obj,
108 pub line_file: LineFile,
109}
110
111#[derive(Clone)]
112pub struct NotInFact {
113 pub element: Obj,
114 pub set: Obj,
115 pub line_file: LineFile,
116}
117
118#[derive(Clone)]
119pub struct NormalAtomicFact {
120 pub predicate: IdentifierOrIdentifierWithMod,
121 pub body: Vec<Obj>,
122 pub line_file: LineFile,
123}
124
125#[derive(Clone)]
126pub struct NotNormalAtomicFact {
127 pub predicate: IdentifierOrIdentifierWithMod,
128 pub body: Vec<Obj>,
129 pub line_file: LineFile,
130}
131
132#[derive(Clone)]
133pub struct EqualFact {
134 pub left: Obj,
135 pub right: Obj,
136 pub line_file: LineFile,
137}
138
139#[derive(Clone)]
140pub struct NotEqualFact {
141 pub left: Obj,
142 pub right: Obj,
143 pub line_file: LineFile,
144}
145
146#[derive(Clone)]
147pub struct LessFact {
148 pub left: Obj,
149 pub right: Obj,
150 pub line_file: LineFile,
151}
152
153#[derive(Clone)]
154pub struct NotLessFact {
155 pub left: Obj,
156 pub right: Obj,
157 pub line_file: LineFile,
158}
159
160#[derive(Clone)]
161pub struct GreaterFact {
162 pub left: Obj,
163 pub right: Obj,
164 pub line_file: LineFile,
165}
166
167#[derive(Clone)]
168pub struct NotGreaterFact {
169 pub left: Obj,
170 pub right: Obj,
171 pub line_file: LineFile,
172}
173
174#[derive(Clone)]
175pub struct LessEqualFact {
176 pub left: Obj,
177 pub right: Obj,
178 pub line_file: LineFile,
179}
180
181#[derive(Clone)]
182pub struct NotLessEqualFact {
183 pub left: Obj,
184 pub right: Obj,
185 pub line_file: LineFile,
186}
187
188#[derive(Clone)]
189pub struct GreaterEqualFact {
190 pub left: Obj,
191 pub right: Obj,
192 pub line_file: LineFile,
193}
194
195#[derive(Clone)]
196pub struct NotGreaterEqualFact {
197 pub left: Obj,
198 pub right: Obj,
199 pub line_file: LineFile,
200}
201
202#[derive(Clone)]
203pub struct IsSetFact {
204 pub set: Obj,
205 pub line_file: LineFile,
206}
207
208#[derive(Clone)]
209pub struct NotIsSetFact {
210 pub set: Obj,
211 pub line_file: LineFile,
212}
213
214#[derive(Clone)]
215pub struct IsNonemptySetFact {
216 pub set: Obj,
217 pub line_file: LineFile,
218}
219
220#[derive(Clone)]
221pub struct NotIsNonemptySetFact {
222 pub set: Obj,
223 pub line_file: LineFile,
224}
225
226#[derive(Clone)]
227pub struct IsFiniteSetFact {
228 pub set: Obj,
229 pub line_file: LineFile,
230}
231
232#[derive(Clone)]
233pub struct NotIsFiniteSetFact {
234 pub set: Obj,
235 pub line_file: LineFile,
236}
237
238impl SubsetFact {
239 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
240 SubsetFact {
241 left,
242 right,
243 line_file,
244 }
245 }
246}
247
248impl NotSubsetFact {
249 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
250 NotSubsetFact {
251 left,
252 right,
253 line_file,
254 }
255 }
256}
257
258impl NormalAtomicFact {
259 pub fn new(
260 predicate: IdentifierOrIdentifierWithMod,
261 body: Vec<Obj>,
262 line_file: LineFile,
263 ) -> Self {
264 NormalAtomicFact {
265 predicate,
266 body,
267 line_file,
268 }
269 }
270}
271
272impl NotNormalAtomicFact {
273 pub fn new(
274 predicate: IdentifierOrIdentifierWithMod,
275 body: Vec<Obj>,
276 line_file: LineFile,
277 ) -> Self {
278 NotNormalAtomicFact {
279 predicate,
280 body,
281 line_file,
282 }
283 }
284}
285
286impl EqualFact {
287 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
288 EqualFact {
289 left,
290 right,
291 line_file,
292 }
293 }
294}
295
296impl NotEqualFact {
297 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
298 NotEqualFact {
299 left,
300 right,
301 line_file,
302 }
303 }
304}
305
306impl LessFact {
307 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
308 LessFact {
309 left,
310 right,
311 line_file,
312 }
313 }
314}
315
316impl NotLessFact {
317 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
318 NotLessFact {
319 left,
320 right,
321 line_file,
322 }
323 }
324}
325
326impl GreaterFact {
327 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
328 GreaterFact {
329 left,
330 right,
331 line_file,
332 }
333 }
334}
335
336impl NotGreaterFact {
337 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
338 NotGreaterFact {
339 left,
340 right,
341 line_file,
342 }
343 }
344}
345
346impl LessEqualFact {
347 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
348 LessEqualFact {
349 left,
350 right,
351 line_file,
352 }
353 }
354}
355
356impl NotLessEqualFact {
357 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
358 NotLessEqualFact {
359 left,
360 right,
361 line_file,
362 }
363 }
364}
365
366impl GreaterEqualFact {
367 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
368 GreaterEqualFact {
369 left,
370 right,
371 line_file,
372 }
373 }
374}
375
376impl NotGreaterEqualFact {
377 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
378 NotGreaterEqualFact {
379 left,
380 right,
381 line_file,
382 }
383 }
384}
385
386impl IsSetFact {
387 pub fn new(set: Obj, line_file: LineFile) -> Self {
388 IsSetFact { set, line_file }
389 }
390}
391
392impl NotIsSetFact {
393 pub fn new(set: Obj, line_file: LineFile) -> Self {
394 NotIsSetFact { set, line_file }
395 }
396}
397
398impl IsNonemptySetFact {
399 pub fn new(set: Obj, line_file: LineFile) -> Self {
400 IsNonemptySetFact { set, line_file }
401 }
402}
403
404impl NotIsNonemptySetFact {
405 pub fn new(set: Obj, line_file: LineFile) -> Self {
406 NotIsNonemptySetFact { set, line_file }
407 }
408}
409
410impl IsFiniteSetFact {
411 pub fn new(set: Obj, line_file: LineFile) -> Self {
412 IsFiniteSetFact { set, line_file }
413 }
414}
415
416impl NotIsFiniteSetFact {
417 pub fn new(set: Obj, line_file: LineFile) -> Self {
418 NotIsFiniteSetFact { set, line_file }
419 }
420}
421
422impl InFact {
423 pub fn new(element: Obj, set: Obj, line_file: LineFile) -> Self {
424 InFact {
425 element,
426 set,
427 line_file,
428 }
429 }
430}
431
432impl NotInFact {
433 pub fn new(element: Obj, set: Obj, line_file: LineFile) -> Self {
434 NotInFact {
435 element,
436 set,
437 line_file,
438 }
439 }
440}
441
442impl IsCartFact {
443 pub fn new(set: Obj, line_file: LineFile) -> Self {
444 IsCartFact { set, line_file }
445 }
446}
447
448impl NotIsCartFact {
449 pub fn new(set: Obj, line_file: LineFile) -> Self {
450 NotIsCartFact { set, line_file }
451 }
452}
453
454impl IsTupleFact {
455 pub fn new(tuple: Obj, line_file: LineFile) -> Self {
456 IsTupleFact {
457 set: tuple,
458 line_file,
459 }
460 }
461}
462
463impl NotIsTupleFact {
464 pub fn new(tuple: Obj, line_file: LineFile) -> Self {
465 NotIsTupleFact {
466 set: tuple,
467 line_file,
468 }
469 }
470}
471
472impl SupersetFact {
473 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
474 SupersetFact {
475 left,
476 right,
477 line_file,
478 }
479 }
480}
481
482impl NotSupersetFact {
483 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
484 NotSupersetFact {
485 left,
486 right,
487 line_file,
488 }
489 }
490}
491
492impl fmt::Display for AtomicFact {
493 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
494 match self {
495 AtomicFact::NormalAtomicFact(x) => write!(f, "{}", x),
496 AtomicFact::EqualFact(x) => write!(f, "{}", x),
497 AtomicFact::LessFact(x) => write!(f, "{}", x),
498 AtomicFact::GreaterFact(x) => write!(f, "{}", x),
499 AtomicFact::LessEqualFact(x) => write!(f, "{}", x),
500 AtomicFact::GreaterEqualFact(x) => write!(f, "{}", x),
501 AtomicFact::IsSetFact(x) => write!(f, "{}", x),
502 AtomicFact::IsNonemptySetFact(x) => write!(f, "{}", x),
503 AtomicFact::IsFiniteSetFact(x) => write!(f, "{}", x),
504 AtomicFact::NotNormalAtomicFact(x) => write!(f, "{}", x),
505 AtomicFact::NotEqualFact(x) => write!(f, "{}", x),
506 AtomicFact::NotLessFact(x) => write!(f, "{}", x),
507 AtomicFact::NotGreaterFact(x) => write!(f, "{}", x),
508 AtomicFact::NotLessEqualFact(x) => write!(f, "{}", x),
509 AtomicFact::NotGreaterEqualFact(x) => write!(f, "{}", x),
510 AtomicFact::NotIsSetFact(x) => write!(f, "{}", x),
511 AtomicFact::NotIsNonemptySetFact(x) => write!(f, "{}", x),
512 AtomicFact::NotIsFiniteSetFact(x) => write!(f, "{}", x),
513 AtomicFact::InFact(x) => write!(f, "{}", x),
514 AtomicFact::NotInFact(x) => write!(f, "{}", x),
515 AtomicFact::IsCartFact(x) => write!(f, "{}", x),
516 AtomicFact::NotIsCartFact(x) => write!(f, "{}", x),
517 AtomicFact::IsTupleFact(x) => write!(f, "{}", x),
518 AtomicFact::NotIsTupleFact(x) => write!(f, "{}", x),
519 AtomicFact::SubsetFact(x) => write!(f, "{}", x),
520 AtomicFact::NotSubsetFact(x) => write!(f, "{}", x),
521 AtomicFact::SupersetFact(x) => write!(f, "{}", x),
522 AtomicFact::NotSupersetFact(x) => write!(f, "{}", x),
523 AtomicFact::RestrictFact(x) => write!(f, "{}", x),
524 AtomicFact::NotRestrictFact(x) => write!(f, "{}", x),
525 }
526 }
527}
528
529impl fmt::Display for SupersetFact {
530 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
531 write!(
532 f,
533 "{} {}{} {}",
534 self.left, FACT_PREFIX, SUPERSET, self.right
535 )
536 }
537}
538
539impl fmt::Display for NotSupersetFact {
540 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
541 write!(
542 f,
543 "{} {} {}{} {}",
544 NOT, self.left, FACT_PREFIX, SUPERSET, self.right
545 )
546 }
547}
548
549impl fmt::Display for SubsetFact {
550 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
551 write!(f, "{} {}{} {}", self.left, FACT_PREFIX, SUBSET, self.right)
552 }
553}
554
555impl fmt::Display for NotSubsetFact {
556 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
557 write!(
558 f,
559 "{} {} {}{} {}",
560 NOT, self.left, FACT_PREFIX, SUBSET, self.right
561 )
562 }
563}
564
565impl fmt::Display for InFact {
566 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
567 write!(f, "{} {}{} {}", self.element, FACT_PREFIX, IN, self.set)
568 }
569}
570
571impl fmt::Display for NotInFact {
572 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
573 write!(
574 f,
575 "{} {} {}{} {}",
576 NOT, self.element, FACT_PREFIX, IN, self.set
577 )
578 }
579}
580
581impl fmt::Display for IsCartFact {
582 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
583 write!(f, "{}{}{}", FACT_PREFIX, IS_CART, braced_string(&self.set))
584 }
585}
586
587impl fmt::Display for NotIsCartFact {
588 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
589 write!(
590 f,
591 "{} {}{}{}",
592 NOT,
593 FACT_PREFIX,
594 IS_CART,
595 braced_string(&self.set)
596 )
597 }
598}
599
600impl fmt::Display for IsTupleFact {
601 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
602 write!(f, "{}{}{}", FACT_PREFIX, IS_TUPLE, braced_string(&self.set))
603 }
604}
605
606impl fmt::Display for NotIsTupleFact {
607 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
608 write!(
609 f,
610 "{} {}{}{}",
611 NOT,
612 FACT_PREFIX,
613 IS_TUPLE,
614 braced_string(&self.set)
615 )
616 }
617}
618
619impl fmt::Display for NormalAtomicFact {
620 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
621 write!(
622 f,
623 "{}{}{}",
624 FACT_PREFIX,
625 self.predicate,
626 braced_vec_to_string(&self.body)
627 )
628 }
629}
630
631impl fmt::Display for NotNormalAtomicFact {
632 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
633 write!(
634 f,
635 "{} {}{}{}",
636 NOT,
637 FACT_PREFIX,
638 self.predicate,
639 braced_vec_to_string(&self.body)
640 )
641 }
642}
643
644impl fmt::Display for EqualFact {
645 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
646 write!(f, "{} {} {}", self.left, EQUAL, self.right)
647 }
648}
649
650impl fmt::Display for NotEqualFact {
651 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
652 write!(f, "{} {} {}", self.left, NOT_EQUAL, self.right)
653 }
654}
655
656impl fmt::Display for LessFact {
657 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
658 write!(f, "{} {} {}", self.left, LESS, self.right)
659 }
660}
661
662impl fmt::Display for NotLessFact {
663 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
664 write!(f, "{} {} {} {}", NOT, self.left, LESS, self.right)
665 }
666}
667
668impl fmt::Display for GreaterFact {
669 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
670 write!(f, "{} {} {}", self.left, GREATER, self.right)
671 }
672}
673
674impl fmt::Display for NotGreaterFact {
675 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
676 write!(f, "{} {} {} {}", NOT, self.left, GREATER, self.right)
677 }
678}
679
680impl fmt::Display for LessEqualFact {
681 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
682 write!(f, "{} {} {}", self.left, LESS_EQUAL, self.right)
683 }
684}
685
686impl fmt::Display for NotLessEqualFact {
687 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
688 write!(f, "{} {} {} {}", NOT, self.left, LESS_EQUAL, self.right)
689 }
690}
691
692impl fmt::Display for GreaterEqualFact {
693 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
694 write!(f, "{} {} {}", self.left, GREATER_EQUAL, self.right)
695 }
696}
697
698impl fmt::Display for NotGreaterEqualFact {
699 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
700 write!(f, "{} {} {} {}", NOT, self.left, GREATER_EQUAL, self.right)
701 }
702}
703
704impl fmt::Display for IsSetFact {
705 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
706 write!(f, "{}{}{}", FACT_PREFIX, IS_SET, braced_string(&self.set))
707 }
708}
709
710impl fmt::Display for NotIsSetFact {
711 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
712 write!(
713 f,
714 "{} {}{}{}",
715 NOT,
716 FACT_PREFIX,
717 IS_SET,
718 braced_string(&self.set)
719 )
720 }
721}
722
723impl fmt::Display for IsNonemptySetFact {
724 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
725 write!(
726 f,
727 "{}{}{}",
728 FACT_PREFIX,
729 IS_NONEMPTY_SET,
730 braced_string(&self.set)
731 )
732 }
733}
734
735impl fmt::Display for NotIsNonemptySetFact {
736 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
737 write!(
738 f,
739 "{} {}{}{}",
740 NOT,
741 FACT_PREFIX,
742 IS_NONEMPTY_SET,
743 braced_string(&self.set)
744 )
745 }
746}
747
748impl fmt::Display for IsFiniteSetFact {
749 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
750 write!(
751 f,
752 "{}{}{}",
753 FACT_PREFIX,
754 IS_FINITE_SET,
755 braced_string(&self.set)
756 )
757 }
758}
759
760impl fmt::Display for NotIsFiniteSetFact {
761 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
762 write!(
763 f,
764 "{} {}{}{}",
765 NOT,
766 FACT_PREFIX,
767 IS_FINITE_SET,
768 braced_string(&self.set)
769 )
770 }
771}
772
773impl AtomicFact {
774 pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
775 if from == to {
776 return self;
777 }
778 fn r(o: Obj, from: &str, to: &str) -> Obj {
779 Obj::replace_bound_identifier(o, from, to)
780 }
781 match self {
782 AtomicFact::NormalAtomicFact(x) => NormalAtomicFact::new(
783 x.predicate,
784 x.body.into_iter().map(|o| r(o, from, to)).collect(),
785 x.line_file,
786 )
787 .into(),
788 AtomicFact::EqualFact(x) => {
789 EqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
790 }
791 AtomicFact::LessFact(x) => {
792 LessFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
793 }
794 AtomicFact::GreaterFact(x) => {
795 GreaterFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
796 }
797 AtomicFact::LessEqualFact(x) => {
798 LessEqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
799 }
800 AtomicFact::GreaterEqualFact(x) => {
801 GreaterEqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
802 }
803 AtomicFact::IsSetFact(x) => IsSetFact::new(r(x.set, from, to), x.line_file).into(),
804 AtomicFact::IsNonemptySetFact(x) => {
805 IsNonemptySetFact::new(r(x.set, from, to), x.line_file).into()
806 }
807 AtomicFact::IsFiniteSetFact(x) => {
808 IsFiniteSetFact::new(r(x.set, from, to), x.line_file).into()
809 }
810 AtomicFact::InFact(x) => {
811 InFact::new(r(x.element, from, to), r(x.set, from, to), x.line_file).into()
812 }
813 AtomicFact::IsCartFact(x) => IsCartFact::new(r(x.set, from, to), x.line_file).into(),
814 AtomicFact::IsTupleFact(x) => IsTupleFact::new(r(x.set, from, to), x.line_file).into(),
815 AtomicFact::SubsetFact(x) => {
816 SubsetFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
817 }
818 AtomicFact::SupersetFact(x) => {
819 SupersetFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
820 }
821 AtomicFact::RestrictFact(x) => RestrictFact::new(
822 r(x.obj, from, to),
823 r(x.obj_can_restrict_to_fn_set, from, to),
824 x.line_file,
825 )
826 .into(),
827 AtomicFact::NotRestrictFact(x) => NotRestrictFact::new(
828 r(x.obj, from, to),
829 r(x.obj_cannot_restrict_to_fn_set, from, to),
830 x.line_file,
831 )
832 .into(),
833 AtomicFact::NotNormalAtomicFact(x) => NotNormalAtomicFact::new(
834 x.predicate,
835 x.body.into_iter().map(|o| r(o, from, to)).collect(),
836 x.line_file,
837 )
838 .into(),
839 AtomicFact::NotEqualFact(x) => {
840 NotEqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
841 }
842 AtomicFact::NotLessFact(x) => {
843 NotLessFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
844 }
845 AtomicFact::NotGreaterFact(x) => {
846 NotGreaterFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
847 }
848 AtomicFact::NotLessEqualFact(x) => {
849 NotLessEqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
850 }
851 AtomicFact::NotGreaterEqualFact(x) => {
852 NotGreaterEqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file)
853 .into()
854 }
855 AtomicFact::NotIsSetFact(x) => {
856 NotIsSetFact::new(r(x.set, from, to), x.line_file).into()
857 }
858 AtomicFact::NotIsNonemptySetFact(x) => {
859 NotIsNonemptySetFact::new(r(x.set, from, to), x.line_file).into()
860 }
861 AtomicFact::NotIsFiniteSetFact(x) => {
862 NotIsFiniteSetFact::new(r(x.set, from, to), x.line_file).into()
863 }
864 AtomicFact::NotInFact(x) => {
865 NotInFact::new(r(x.element, from, to), r(x.set, from, to), x.line_file).into()
866 }
867 AtomicFact::NotIsCartFact(x) => {
868 NotIsCartFact::new(r(x.set, from, to), x.line_file).into()
869 }
870 AtomicFact::NotIsTupleFact(x) => {
871 NotIsTupleFact::new(r(x.set, from, to), x.line_file).into()
872 }
873 AtomicFact::NotSubsetFact(x) => {
874 NotSubsetFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
875 }
876 AtomicFact::NotSupersetFact(x) => {
877 NotSupersetFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file).into()
878 }
879 }
880 }
881}
882
883impl AtomicFact {
884 fn predicate_string(&self) -> String {
885 match self {
886 AtomicFact::NormalAtomicFact(x) => x.predicate.to_string(),
887 AtomicFact::EqualFact(_) => EQUAL.to_string(),
888 AtomicFact::LessFact(_) => LESS.to_string(),
889 AtomicFact::GreaterFact(_) => GREATER.to_string(),
890 AtomicFact::LessEqualFact(_) => LESS_EQUAL.to_string(),
891 AtomicFact::GreaterEqualFact(_) => GREATER_EQUAL.to_string(),
892 AtomicFact::IsSetFact(_) => IS_SET.to_string(),
893 AtomicFact::IsNonemptySetFact(_) => IS_NONEMPTY_SET.to_string(),
894 AtomicFact::IsFiniteSetFact(_) => IS_FINITE_SET.to_string(),
895 AtomicFact::InFact(_) => IN.to_string(),
896 AtomicFact::IsCartFact(_) => IS_CART.to_string(),
897 AtomicFact::IsTupleFact(_) => IS_TUPLE.to_string(),
898 AtomicFact::SubsetFact(_) => SUBSET.to_string(),
899 AtomicFact::SupersetFact(_) => SUPERSET.to_string(),
900 AtomicFact::NotNormalAtomicFact(x) => x.predicate.to_string(),
901 AtomicFact::NotEqualFact(_) => EQUAL.to_string(),
902 AtomicFact::NotLessFact(_) => LESS.to_string(),
903 AtomicFact::NotGreaterFact(_) => GREATER.to_string(),
904 AtomicFact::NotLessEqualFact(_) => LESS_EQUAL.to_string(),
905 AtomicFact::NotGreaterEqualFact(_) => GREATER_EQUAL.to_string(),
906 AtomicFact::NotIsSetFact(_) => IS_SET.to_string(),
907 AtomicFact::NotIsNonemptySetFact(_) => IS_NONEMPTY_SET.to_string(),
908 AtomicFact::NotIsFiniteSetFact(_) => IS_FINITE_SET.to_string(),
909 AtomicFact::NotInFact(_) => IN.to_string(),
910 AtomicFact::NotIsCartFact(_) => IS_CART.to_string(),
911 AtomicFact::NotIsTupleFact(_) => IS_TUPLE.to_string(),
912 AtomicFact::NotSubsetFact(_) => SUBSET.to_string(),
913 AtomicFact::NotSupersetFact(_) => SUPERSET.to_string(),
914 AtomicFact::RestrictFact(_) => RESTRICT.to_string(),
915 AtomicFact::NotRestrictFact(_) => RESTRICT.to_string(),
916 }
917 }
918
919 pub fn is_true(&self) -> bool {
920 match self {
921 AtomicFact::NormalAtomicFact(_) => true,
922 AtomicFact::EqualFact(_) => true,
923 AtomicFact::LessFact(_) => true,
924 AtomicFact::GreaterFact(_) => true,
925 AtomicFact::LessEqualFact(_) => true,
926 AtomicFact::GreaterEqualFact(_) => true,
927 AtomicFact::IsSetFact(_) => true,
928 AtomicFact::IsNonemptySetFact(_) => true,
929 AtomicFact::IsFiniteSetFact(_) => true,
930 AtomicFact::InFact(_) => true,
931 AtomicFact::IsCartFact(_) => true,
932 AtomicFact::IsTupleFact(_) => true,
933 AtomicFact::SubsetFact(_) => true,
934 AtomicFact::SupersetFact(_) => true,
935 AtomicFact::RestrictFact(_) => true,
936 AtomicFact::NotNormalAtomicFact(_) => false,
937 AtomicFact::NotEqualFact(_) => false,
938 AtomicFact::NotLessFact(_) => false,
939 AtomicFact::NotGreaterFact(_) => false,
940 AtomicFact::NotLessEqualFact(_) => false,
941 AtomicFact::NotGreaterEqualFact(_) => false,
942 AtomicFact::NotIsSetFact(_) => false,
943 AtomicFact::NotIsNonemptySetFact(_) => false,
944 AtomicFact::NotIsFiniteSetFact(_) => false,
945 AtomicFact::NotInFact(_) => false,
946 AtomicFact::NotIsCartFact(_) => false,
947 AtomicFact::NotIsTupleFact(_) => false,
948 AtomicFact::NotSubsetFact(_) => false,
949 AtomicFact::NotSupersetFact(_) => false,
950 AtomicFact::NotRestrictFact(_) => false,
951 }
952 }
953
954 pub fn key(&self) -> String {
955 return self.predicate_string();
956 }
957
958 pub fn transposed_binary_order_equivalent(&self) -> Option<Self> {
959 match self {
960 AtomicFact::LessFact(f) => {
961 Some(GreaterFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()).into())
962 }
963 AtomicFact::GreaterFact(f) => {
964 Some(LessFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()).into())
965 }
966 AtomicFact::LessEqualFact(f) => Some(AtomicFact::GreaterEqualFact(
967 GreaterEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
968 )),
969 AtomicFact::GreaterEqualFact(f) => Some(
970 LessEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()).into(),
971 ),
972 AtomicFact::NotLessFact(f) => Some(
973 NotGreaterFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()).into(),
974 ),
975 AtomicFact::NotGreaterFact(f) => {
976 Some(NotLessFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()).into())
977 }
978 AtomicFact::NotLessEqualFact(f) => Some(AtomicFact::NotGreaterEqualFact(
979 NotGreaterEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
980 )),
981 AtomicFact::NotGreaterEqualFact(f) => Some(AtomicFact::NotLessEqualFact(
982 NotLessEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
983 )),
984 _ => None,
985 }
986 }
987}
988
989impl AtomicFact {
990 pub fn to_atomic_fact(
991 prop_name: IdentifierOrIdentifierWithMod,
992 is_true: bool,
993 args: Vec<Obj>,
994 line_file: LineFile,
995 ) -> Result<AtomicFact, RuntimeError> {
996 let prop_name_as_string = prop_name.to_string();
997 match prop_name_as_string.as_str() {
998 EQUAL => {
999 if args.len() != 2 {
1000 let msg = format!("{} requires 2 arguments, but got {}", EQUAL, args.len());
1001 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1002 None,
1003 msg,
1004 line_file.clone(),
1005 None,
1006 vec![],
1007 ))
1008 .into());
1009 }
1010 let mut args = args;
1011 let a0 = args.remove(0);
1012 let a1 = args.remove(0);
1013 if is_true {
1014 Ok(EqualFact::new(a0, a1, line_file).into())
1015 } else {
1016 Ok(NotEqualFact::new(a0, a1, line_file).into())
1017 }
1018 }
1019 NOT_EQUAL => {
1020 if args.len() != 2 {
1021 let msg = format!("{} requires 2 arguments, but got {}", NOT_EQUAL, args.len());
1022 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1023 None,
1024 msg,
1025 line_file.clone(),
1026 None,
1027 vec![],
1028 ))
1029 .into());
1030 }
1031 let mut args = args;
1032 let a0 = args.remove(0);
1033 let a1 = args.remove(0);
1034 if is_true {
1035 Ok(NotEqualFact::new(a0, a1, line_file).into())
1036 } else {
1037 Ok(EqualFact::new(a0, a1, line_file).into())
1038 }
1039 }
1040 LESS => {
1041 if args.len() != 2 {
1042 let msg = format!("{} requires 2 arguments, but got {}", LESS, args.len());
1043 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1044 None,
1045 msg,
1046 line_file.clone(),
1047 None,
1048 vec![],
1049 ))
1050 .into());
1051 }
1052 let mut args = args;
1053 let a0 = args.remove(0);
1054 let a1 = args.remove(0);
1055 if is_true {
1056 Ok(LessFact::new(a0, a1, line_file).into())
1057 } else {
1058 Ok(NotLessFact::new(a0, a1, line_file).into())
1059 }
1060 }
1061 GREATER => {
1062 if args.len() != 2 {
1063 let msg = format!("{} requires 2 arguments, but got {}", GREATER, args.len());
1064 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1065 None,
1066 msg,
1067 line_file.clone(),
1068 None,
1069 vec![],
1070 ))
1071 .into());
1072 }
1073 let mut args = args;
1074 let a0 = args.remove(0);
1075 let a1 = args.remove(0);
1076 if is_true {
1077 Ok(GreaterFact::new(a0, a1, line_file).into())
1078 } else {
1079 Ok(NotGreaterFact::new(a0, a1, line_file).into())
1080 }
1081 }
1082 LESS_EQUAL => {
1083 if args.len() != 2 {
1084 let msg = format!(
1085 "{} requires 2 arguments, but got {}",
1086 LESS_EQUAL,
1087 args.len()
1088 );
1089 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1090 None,
1091 msg,
1092 line_file.clone(),
1093 None,
1094 vec![],
1095 ))
1096 .into());
1097 }
1098 let mut args = args;
1099 let a0 = args.remove(0);
1100 let a1 = args.remove(0);
1101 if is_true {
1102 Ok(LessEqualFact::new(a0, a1, line_file).into())
1103 } else {
1104 Ok(NotLessEqualFact::new(a0, a1, line_file).into())
1105 }
1106 }
1107 GREATER_EQUAL => {
1108 if args.len() != 2 {
1109 let msg = format!(
1110 "{} requires 2 arguments, but got {}",
1111 GREATER_EQUAL,
1112 args.len()
1113 );
1114 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1115 None,
1116 msg,
1117 line_file.clone(),
1118 None,
1119 vec![],
1120 ))
1121 .into());
1122 }
1123 let mut args = args;
1124 let a0 = args.remove(0);
1125 let a1 = args.remove(0);
1126 if is_true {
1127 Ok(GreaterEqualFact::new(a0, a1, line_file).into())
1128 } else {
1129 Ok(NotGreaterEqualFact::new(a0, a1, line_file).into())
1130 }
1131 }
1132 IS_SET => {
1133 if args.len() != 1 {
1134 let msg = format!("{} requires 1 argument, but got {}", IS_SET, args.len());
1135 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1136 None,
1137 msg,
1138 line_file.clone(),
1139 None,
1140 vec![],
1141 ))
1142 .into());
1143 }
1144 let mut args = args;
1145 let a0 = args.remove(0);
1146 if is_true {
1147 Ok(IsSetFact::new(a0, line_file).into())
1148 } else {
1149 Ok(NotIsSetFact::new(a0, line_file).into())
1150 }
1151 }
1152 IS_NONEMPTY_SET => {
1153 if args.len() != 1 {
1154 let msg = format!(
1155 "{} requires 1 argument, but got {}",
1156 IS_NONEMPTY_SET,
1157 args.len()
1158 );
1159 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1160 None,
1161 msg,
1162 line_file.clone(),
1163 None,
1164 vec![],
1165 ))
1166 .into());
1167 }
1168 let mut args = args;
1169 let a0 = args.remove(0);
1170 if is_true {
1171 Ok(IsNonemptySetFact::new(a0, line_file).into())
1172 } else {
1173 Ok(NotIsNonemptySetFact::new(a0, line_file).into())
1174 }
1175 }
1176 IS_FINITE_SET => {
1177 if args.len() != 1 {
1178 let msg = format!(
1179 "{} requires 1 argument, but got {}",
1180 IS_FINITE_SET,
1181 args.len()
1182 );
1183 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1184 None,
1185 msg,
1186 line_file.clone(),
1187 None,
1188 vec![],
1189 ))
1190 .into());
1191 }
1192 let mut args = args;
1193 let a0 = args.remove(0);
1194 if is_true {
1195 Ok(IsFiniteSetFact::new(a0, line_file).into())
1196 } else {
1197 Ok(NotIsFiniteSetFact::new(a0, line_file).into())
1198 }
1199 }
1200 IN => {
1201 if args.len() != 2 {
1202 let msg = format!("{} requires 2 arguments, but got {}", IN, args.len());
1203 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1204 None,
1205 msg,
1206 line_file.clone(),
1207 None,
1208 vec![],
1209 ))
1210 .into());
1211 }
1212 let mut args = args;
1213 let a0 = args.remove(0);
1214 let a1 = args.remove(0);
1215 if is_true {
1216 Ok(InFact::new(a0, a1, line_file).into())
1217 } else {
1218 Ok(NotInFact::new(a0, a1, line_file).into())
1219 }
1220 }
1221 IS_CART => {
1222 if args.len() != 1 {
1223 let msg = format!("{} requires 1 argument, but got {}", IS_CART, args.len());
1224 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1225 None,
1226 msg,
1227 line_file.clone(),
1228 None,
1229 vec![],
1230 ))
1231 .into());
1232 }
1233 let mut args = args;
1234 let a0 = args.remove(0);
1235 if is_true {
1236 Ok(IsCartFact::new(a0, line_file).into())
1237 } else {
1238 Ok(NotIsCartFact::new(a0, line_file).into())
1239 }
1240 }
1241 IS_TUPLE => {
1242 if args.len() != 1 {
1243 let msg = format!("{} requires 1 argument, but got {}", IS_TUPLE, args.len());
1244 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1245 None,
1246 msg,
1247 line_file.clone(),
1248 None,
1249 vec![],
1250 ))
1251 .into());
1252 }
1253 let mut args = args;
1254 let a0 = args.remove(0);
1255 if is_true {
1256 Ok(IsTupleFact::new(a0, line_file).into())
1257 } else {
1258 Ok(NotIsTupleFact::new(a0, line_file).into())
1259 }
1260 }
1261 SUBSET => {
1262 if args.len() != 2 {
1263 let msg = format!("{} requires 2 arguments, but got {}", SUBSET, args.len());
1264 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1265 None,
1266 msg,
1267 line_file.clone(),
1268 None,
1269 vec![],
1270 ))
1271 .into());
1272 }
1273 let mut args = args;
1274 let a0 = args.remove(0);
1275 let a1 = args.remove(0);
1276 if is_true {
1277 Ok(SubsetFact::new(a0, a1, line_file).into())
1278 } else {
1279 Ok(NotSubsetFact::new(a0, a1, line_file).into())
1280 }
1281 }
1282 SUPERSET => {
1283 if args.len() != 2 {
1284 let msg = format!("{} requires 2 arguments, but got {}", SUPERSET, args.len());
1285 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1286 None,
1287 msg,
1288 line_file.clone(),
1289 None,
1290 vec![],
1291 ))
1292 .into());
1293 }
1294 let mut args = args;
1295 let a0 = args.remove(0);
1296 let a1 = args.remove(0);
1297 if is_true {
1298 Ok(SupersetFact::new(a0, a1, line_file).into())
1299 } else {
1300 Ok(NotSupersetFact::new(a0, a1, line_file).into())
1301 }
1302 }
1303 RESTRICT => {
1304 if args.len() != 2 {
1305 let msg = format!("{} requires 2 arguments, but got {}", RESTRICT, args.len());
1306 return Err(NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
1307 None,
1308 msg,
1309 line_file.clone(),
1310 None,
1311 vec![],
1312 ))
1313 .into());
1314 }
1315 let mut args = args;
1316 let a0 = args.remove(0);
1317 let a1 = args.remove(0);
1318 if is_true {
1319 Ok(RestrictFact::new(a0, a1, line_file).into())
1320 } else {
1321 Ok(NotRestrictFact::new(a0, a1, line_file).into())
1322 }
1323 }
1324 _ => {
1325 if is_true {
1326 Ok(NormalAtomicFact::new(prop_name, args, line_file).into())
1327 } else {
1328 Ok(NotNormalAtomicFact::new(prop_name, args, line_file).into())
1329 }
1330 }
1331 }
1332 }
1333}
1334
1335impl AtomicFact {
1336 pub fn args(&self) -> Vec<Obj> {
1337 match self {
1338 AtomicFact::NormalAtomicFact(normal_atomic_fact) => normal_atomic_fact.body.clone(),
1339 AtomicFact::EqualFact(equal_fact) => {
1340 vec![equal_fact.left.clone(), equal_fact.right.clone()]
1341 }
1342 AtomicFact::LessFact(less_fact) => {
1343 vec![less_fact.left.clone(), less_fact.right.clone()]
1344 }
1345 AtomicFact::GreaterFact(greater_fact) => {
1346 vec![greater_fact.left.clone(), greater_fact.right.clone()]
1347 }
1348 AtomicFact::LessEqualFact(less_equal_fact) => {
1349 vec![less_equal_fact.left.clone(), less_equal_fact.right.clone()]
1350 }
1351 AtomicFact::GreaterEqualFact(greater_equal_fact) => vec![
1352 greater_equal_fact.left.clone(),
1353 greater_equal_fact.right.clone(),
1354 ],
1355 AtomicFact::IsSetFact(is_set_fact) => vec![is_set_fact.set.clone()],
1356 AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => {
1357 vec![is_nonempty_set_fact.set.clone()]
1358 }
1359 AtomicFact::IsFiniteSetFact(is_finite_set_fact) => vec![is_finite_set_fact.set.clone()],
1360 AtomicFact::InFact(in_fact) => vec![in_fact.element.clone(), in_fact.set.clone()],
1361 AtomicFact::IsCartFact(is_cart_fact) => vec![is_cart_fact.set.clone()],
1362 AtomicFact::IsTupleFact(is_tuple_fact) => vec![is_tuple_fact.set.clone()],
1363 AtomicFact::SubsetFact(subset_fact) => {
1364 vec![subset_fact.left.clone(), subset_fact.right.clone()]
1365 }
1366 AtomicFact::SupersetFact(superset_fact) => {
1367 vec![superset_fact.left.clone(), superset_fact.right.clone()]
1368 }
1369 AtomicFact::NotNormalAtomicFact(not_normal_atomic_fact) => {
1370 not_normal_atomic_fact.body.clone()
1371 }
1372 AtomicFact::NotEqualFact(not_equal_fact) => {
1373 vec![not_equal_fact.left.clone(), not_equal_fact.right.clone()]
1374 }
1375 AtomicFact::NotLessFact(not_less_fact) => {
1376 vec![not_less_fact.left.clone(), not_less_fact.right.clone()]
1377 }
1378 AtomicFact::NotGreaterFact(not_greater_fact) => vec![
1379 not_greater_fact.left.clone(),
1380 not_greater_fact.right.clone(),
1381 ],
1382 AtomicFact::NotLessEqualFact(not_less_equal_fact) => vec![
1383 not_less_equal_fact.left.clone(),
1384 not_less_equal_fact.right.clone(),
1385 ],
1386 AtomicFact::NotGreaterEqualFact(not_greater_equal_fact) => vec![
1387 not_greater_equal_fact.left.clone(),
1388 not_greater_equal_fact.right.clone(),
1389 ],
1390 AtomicFact::NotIsSetFact(not_is_set_fact) => vec![not_is_set_fact.set.clone()],
1391 AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => {
1392 vec![not_is_nonempty_set_fact.set.clone()]
1393 }
1394 AtomicFact::NotIsFiniteSetFact(not_is_finite_set_fact) => {
1395 vec![not_is_finite_set_fact.set.clone()]
1396 }
1397 AtomicFact::NotInFact(not_in_fact) => {
1398 vec![not_in_fact.element.clone(), not_in_fact.set.clone()]
1399 }
1400 AtomicFact::NotIsCartFact(not_is_cart_fact) => vec![not_is_cart_fact.set.clone()],
1401 AtomicFact::NotIsTupleFact(not_is_tuple_fact) => vec![not_is_tuple_fact.set.clone()],
1402 AtomicFact::NotSubsetFact(not_subset_fact) => {
1403 vec![not_subset_fact.left.clone(), not_subset_fact.right.clone()]
1404 }
1405 AtomicFact::NotSupersetFact(not_superset_fact) => vec![
1406 not_superset_fact.left.clone(),
1407 not_superset_fact.right.clone(),
1408 ],
1409 AtomicFact::RestrictFact(restrict_fact) => vec![
1410 restrict_fact.obj.clone(),
1411 restrict_fact.obj_can_restrict_to_fn_set.clone().into(),
1412 ],
1413 AtomicFact::NotRestrictFact(not_restrict_fact) => vec![
1414 not_restrict_fact.obj.clone(),
1415 not_restrict_fact.obj_cannot_restrict_to_fn_set.clone(),
1416 ],
1417 }
1418 }
1419}
1420
1421impl AtomicFact {
1423 pub fn is_builtin_predicate_and_return_expected_args_len(&self) -> usize {
1424 match self {
1425 AtomicFact::EqualFact(_) => 2,
1426 AtomicFact::LessFact(_) => 2,
1427 AtomicFact::GreaterFact(_) => 2,
1428 AtomicFact::LessEqualFact(_) => 2,
1429 AtomicFact::GreaterEqualFact(_) => 2,
1430 AtomicFact::IsSetFact(_) => 1,
1431 AtomicFact::IsNonemptySetFact(_) => 1,
1432 AtomicFact::IsFiniteSetFact(_) => 1,
1433 AtomicFact::InFact(_) => 2,
1434 AtomicFact::IsCartFact(_) => 1,
1435 AtomicFact::IsTupleFact(_) => 1,
1436 AtomicFact::SubsetFact(_) => 2,
1437 AtomicFact::SupersetFact(_) => 2,
1438 AtomicFact::NotEqualFact(_) => 2,
1439 AtomicFact::NotLessFact(_) => 2,
1440 AtomicFact::NotGreaterFact(_) => 2,
1441 AtomicFact::NotLessEqualFact(_) => 2,
1442 AtomicFact::NotGreaterEqualFact(_) => 2,
1443 AtomicFact::NotIsSetFact(_) => 1,
1444 AtomicFact::NotIsNonemptySetFact(_) => 1,
1445 AtomicFact::NotIsFiniteSetFact(_) => 1,
1446 AtomicFact::NotInFact(_) => 2,
1447 AtomicFact::NotIsCartFact(_) => 1,
1448 AtomicFact::NotIsTupleFact(_) => 1,
1449 AtomicFact::NotSubsetFact(_) => 2,
1450 AtomicFact::NotSupersetFact(_) => 2,
1451 AtomicFact::RestrictFact(_) => 2,
1452 AtomicFact::NotRestrictFact(_) => 2,
1453 _ => unreachable!("其他情况不是builtin predicate"),
1454 }
1455 }
1456}
1457
1458impl AtomicFact {
1459 pub fn number_of_args(&self) -> usize {
1460 match self {
1461 AtomicFact::EqualFact(_) => 2,
1462 AtomicFact::LessFact(_) => 2,
1463 AtomicFact::GreaterFact(_) => 2,
1464 AtomicFact::LessEqualFact(_) => 2,
1465 AtomicFact::GreaterEqualFact(_) => 2,
1466 AtomicFact::IsSetFact(_) => 1,
1467 AtomicFact::IsNonemptySetFact(_) => 1,
1468 AtomicFact::IsFiniteSetFact(_) => 1,
1469 AtomicFact::InFact(_) => 2,
1470 AtomicFact::IsCartFact(_) => 1,
1471 AtomicFact::IsTupleFact(_) => 1,
1472 AtomicFact::SubsetFact(_) => 2,
1473 AtomicFact::SupersetFact(_) => 2,
1474 AtomicFact::NotEqualFact(_) => 2,
1475 AtomicFact::NotLessFact(_) => 2,
1476 AtomicFact::NotGreaterFact(_) => 2,
1477 AtomicFact::NotLessEqualFact(_) => 2,
1478 AtomicFact::NotGreaterEqualFact(_) => 2,
1479 AtomicFact::NotIsSetFact(_) => 1,
1480 AtomicFact::NotIsNonemptySetFact(_) => 1,
1481 AtomicFact::NotIsFiniteSetFact(_) => 1,
1482 AtomicFact::NotInFact(_) => 2,
1483 AtomicFact::NotIsCartFact(_) => 1,
1484 AtomicFact::NotIsTupleFact(_) => 1,
1485 AtomicFact::NotSubsetFact(_) => 2,
1486 AtomicFact::NotSupersetFact(_) => 2,
1487 AtomicFact::NormalAtomicFact(a) => a.body.len(),
1488 AtomicFact::NotNormalAtomicFact(a) => a.body.len(),
1489 AtomicFact::RestrictFact(_) => 2,
1490 AtomicFact::NotRestrictFact(_) => 2,
1491 }
1492 }
1493
1494 pub fn line_file(&self) -> LineFile {
1495 match self {
1496 AtomicFact::EqualFact(a) => a.line_file.clone(),
1497 AtomicFact::LessFact(a) => a.line_file.clone(),
1498 AtomicFact::GreaterFact(a) => a.line_file.clone(),
1499 AtomicFact::LessEqualFact(a) => a.line_file.clone(),
1500 AtomicFact::GreaterEqualFact(a) => a.line_file.clone(),
1501 AtomicFact::IsSetFact(a) => a.line_file.clone(),
1502 AtomicFact::IsNonemptySetFact(a) => a.line_file.clone(),
1503 AtomicFact::IsFiniteSetFact(a) => a.line_file.clone(),
1504 AtomicFact::InFact(a) => a.line_file.clone(),
1505 AtomicFact::IsCartFact(a) => a.line_file.clone(),
1506 AtomicFact::IsTupleFact(a) => a.line_file.clone(),
1507 AtomicFact::SubsetFact(a) => a.line_file.clone(),
1508 AtomicFact::SupersetFact(a) => a.line_file.clone(),
1509 AtomicFact::NormalAtomicFact(a) => a.line_file.clone(),
1510 AtomicFact::NotNormalAtomicFact(a) => a.line_file.clone(),
1511 AtomicFact::NotEqualFact(a) => a.line_file.clone(),
1512 AtomicFact::NotLessFact(a) => a.line_file.clone(),
1513 AtomicFact::NotGreaterFact(a) => a.line_file.clone(),
1514 AtomicFact::NotLessEqualFact(a) => a.line_file.clone(),
1515 AtomicFact::NotGreaterEqualFact(a) => a.line_file.clone(),
1516 AtomicFact::NotIsSetFact(a) => a.line_file.clone(),
1517 AtomicFact::NotIsNonemptySetFact(a) => a.line_file.clone(),
1518 AtomicFact::NotIsFiniteSetFact(a) => a.line_file.clone(),
1519 AtomicFact::NotInFact(a) => a.line_file.clone(),
1520 AtomicFact::NotIsCartFact(a) => a.line_file.clone(),
1521 AtomicFact::NotIsTupleFact(a) => a.line_file.clone(),
1522 AtomicFact::NotSubsetFact(a) => a.line_file.clone(),
1523 AtomicFact::NotSupersetFact(a) => a.line_file.clone(),
1524 AtomicFact::RestrictFact(a) => a.line_file.clone(),
1525 AtomicFact::NotRestrictFact(a) => a.line_file.clone(),
1526 }
1527 }
1528
1529 pub fn with_new_line_file(self, line_file: LineFile) -> Self {
1530 match self {
1531 AtomicFact::EqualFact(x) => EqualFact::new(x.left, x.right, line_file).into(),
1532 AtomicFact::LessFact(x) => LessFact::new(x.left, x.right, line_file).into(),
1533 AtomicFact::GreaterFact(x) => GreaterFact::new(x.left, x.right, line_file).into(),
1534 AtomicFact::LessEqualFact(x) => LessEqualFact::new(x.left, x.right, line_file).into(),
1535 AtomicFact::GreaterEqualFact(x) => {
1536 GreaterEqualFact::new(x.left, x.right, line_file).into()
1537 }
1538 AtomicFact::IsSetFact(x) => IsSetFact::new(x.set, line_file).into(),
1539 AtomicFact::IsNonemptySetFact(x) => IsNonemptySetFact::new(x.set, line_file).into(),
1540 AtomicFact::IsFiniteSetFact(x) => IsFiniteSetFact::new(x.set, line_file).into(),
1541 AtomicFact::InFact(x) => InFact::new(x.element, x.set, line_file).into(),
1542 AtomicFact::IsCartFact(x) => IsCartFact::new(x.set, line_file).into(),
1543 AtomicFact::IsTupleFact(x) => IsTupleFact::new(x.set, line_file).into(),
1544 AtomicFact::SubsetFact(x) => SubsetFact::new(x.left, x.right, line_file).into(),
1545 AtomicFact::SupersetFact(x) => SupersetFact::new(x.left, x.right, line_file).into(),
1546 AtomicFact::NormalAtomicFact(x) => {
1547 NormalAtomicFact::new(x.predicate, x.body, line_file).into()
1548 }
1549 AtomicFact::NotNormalAtomicFact(x) => AtomicFact::NotNormalAtomicFact(
1550 NotNormalAtomicFact::new(x.predicate, x.body, line_file),
1551 ),
1552 AtomicFact::NotEqualFact(x) => NotEqualFact::new(x.left, x.right, line_file).into(),
1553 AtomicFact::NotLessFact(x) => NotLessFact::new(x.left, x.right, line_file).into(),
1554 AtomicFact::NotGreaterFact(x) => NotGreaterFact::new(x.left, x.right, line_file).into(),
1555 AtomicFact::NotLessEqualFact(x) => {
1556 NotLessEqualFact::new(x.left, x.right, line_file).into()
1557 }
1558 AtomicFact::NotGreaterEqualFact(x) => AtomicFact::NotGreaterEqualFact(
1559 NotGreaterEqualFact::new(x.left, x.right, line_file),
1560 ),
1561 AtomicFact::NotIsSetFact(x) => NotIsSetFact::new(x.set, line_file).into(),
1562 AtomicFact::NotIsNonemptySetFact(x) => {
1563 NotIsNonemptySetFact::new(x.set, line_file).into()
1564 }
1565 AtomicFact::NotIsFiniteSetFact(x) => NotIsFiniteSetFact::new(x.set, line_file).into(),
1566 AtomicFact::NotInFact(x) => NotInFact::new(x.element, x.set, line_file).into(),
1567 AtomicFact::NotIsCartFact(x) => NotIsCartFact::new(x.set, line_file).into(),
1568 AtomicFact::NotIsTupleFact(x) => NotIsTupleFact::new(x.set, line_file).into(),
1569 AtomicFact::NotSubsetFact(x) => NotSubsetFact::new(x.left, x.right, line_file).into(),
1570 AtomicFact::NotSupersetFact(x) => {
1571 NotSupersetFact::new(x.left, x.right, line_file).into()
1572 }
1573 AtomicFact::RestrictFact(x) => {
1574 RestrictFact::new(x.obj, x.obj_can_restrict_to_fn_set, line_file).into()
1575 }
1576 AtomicFact::NotRestrictFact(x) => {
1577 NotRestrictFact::new(x.obj, x.obj_cannot_restrict_to_fn_set, line_file).into()
1578 }
1579 }
1580 }
1581}
1582
1583impl RestrictFact {
1584 pub fn new(obj: Obj, obj_can_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1585 RestrictFact {
1586 obj,
1587 obj_can_restrict_to_fn_set,
1588 line_file,
1589 }
1590 }
1591}
1592
1593impl NotRestrictFact {
1594 pub fn new(obj: Obj, obj_cannot_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1595 NotRestrictFact {
1596 obj,
1597 obj_cannot_restrict_to_fn_set,
1598 line_file,
1599 }
1600 }
1601}
1602
1603impl fmt::Display for RestrictFact {
1604 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1605 write!(
1606 f,
1607 "{} {}{} {}",
1608 self.obj, FACT_PREFIX, RESTRICT, self.obj_can_restrict_to_fn_set
1609 )
1610 }
1611}
1612
1613impl fmt::Display for NotRestrictFact {
1614 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1615 write!(
1616 f,
1617 "{} {} {}{} {}",
1618 NOT, self.obj, FACT_PREFIX, RESTRICT, self.obj_cannot_restrict_to_fn_set
1619 )
1620 }
1621}
1622
1623impl AtomicFact {
1624 pub fn get_args_from_fact(&self) -> Vec<Obj> {
1625 self.args()
1626 }
1627}
1628
1629impl AtomicFact {
1630 pub fn make_reversed(&self) -> AtomicFact {
1631 match self {
1632 AtomicFact::NormalAtomicFact(a) => AtomicFact::NotNormalAtomicFact(
1633 NotNormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1634 ),
1635 AtomicFact::NotNormalAtomicFact(a) => AtomicFact::NormalAtomicFact(
1636 NormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1637 ),
1638 AtomicFact::EqualFact(a) => {
1639 NotEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1640 }
1641 AtomicFact::LessFact(a) => {
1642 NotLessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1643 }
1644 AtomicFact::GreaterFact(a) => {
1645 NotGreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1646 }
1647 AtomicFact::LessEqualFact(a) => {
1648 NotLessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1649 }
1650 AtomicFact::GreaterEqualFact(a) => AtomicFact::NotGreaterEqualFact(
1651 NotGreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1652 ),
1653 AtomicFact::IsSetFact(a) => {
1654 NotIsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1655 }
1656 AtomicFact::IsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1657 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1658 ),
1659 AtomicFact::IsFiniteSetFact(a) => AtomicFact::NotIsFiniteSetFact(
1660 NotIsFiniteSetFact::new(a.set.clone(), a.line_file.clone()),
1661 ),
1662 AtomicFact::InFact(a) => {
1663 NotInFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1664 }
1665 AtomicFact::IsCartFact(a) => {
1666 NotIsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1667 }
1668 AtomicFact::IsTupleFact(a) => {
1669 NotIsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1670 }
1671 AtomicFact::SubsetFact(a) => {
1672 NotSubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1673 }
1674 AtomicFact::SupersetFact(a) => {
1675 NotSupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1676 }
1677 AtomicFact::RestrictFact(a) => NotRestrictFact::new(
1678 a.obj.clone(),
1679 a.obj_can_restrict_to_fn_set.clone(),
1680 a.line_file.clone(),
1681 )
1682 .into(),
1683 AtomicFact::NotEqualFact(a) => {
1684 EqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1685 }
1686 AtomicFact::NotLessFact(a) => {
1687 LessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1688 }
1689 AtomicFact::NotGreaterFact(a) => {
1690 GreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1691 }
1692 AtomicFact::NotLessEqualFact(a) => {
1693 LessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1694 }
1695 AtomicFact::NotGreaterEqualFact(a) => AtomicFact::GreaterEqualFact(
1696 GreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1697 ),
1698 AtomicFact::NotIsSetFact(a) => {
1699 IsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1700 }
1701 AtomicFact::NotIsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1702 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1703 ),
1704 AtomicFact::NotIsFiniteSetFact(a) => {
1705 IsFiniteSetFact::new(a.set.clone(), a.line_file.clone()).into()
1706 }
1707 AtomicFact::NotInFact(a) => {
1708 InFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1709 }
1710 AtomicFact::NotIsCartFact(a) => {
1711 IsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1712 }
1713 AtomicFact::NotIsTupleFact(a) => {
1714 IsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1715 }
1716 AtomicFact::NotSubsetFact(a) => {
1717 SubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1718 }
1719 AtomicFact::NotSupersetFact(a) => {
1720 SupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1721 }
1722 AtomicFact::NotRestrictFact(a) => RestrictFact::new(
1723 a.obj.clone(),
1724 a.obj_cannot_restrict_to_fn_set.clone(),
1725 a.line_file.clone(),
1726 )
1727 .into(),
1728 }
1729 }
1730}
1731
1732impl AtomicFact {
1733 fn body_vec_after_calculate_each_calculable_arg(original_body: &Vec<Obj>) -> Vec<Obj> {
1734 let mut next_body = Vec::new();
1735 for obj in original_body {
1736 next_body.push(obj.replace_with_numeric_result_if_can_be_calculated().0);
1737 }
1738 next_body
1739 }
1740
1741 pub fn calculate_args(&self) -> (AtomicFact, bool) {
1742 let calculated_atomic_fact: AtomicFact = match self {
1743 AtomicFact::NormalAtomicFact(inner) => NormalAtomicFact::new(
1744 inner.predicate.clone(),
1745 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1746 inner.line_file.clone(),
1747 )
1748 .into(),
1749 AtomicFact::NotNormalAtomicFact(inner) => NotNormalAtomicFact::new(
1750 inner.predicate.clone(),
1751 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1752 inner.line_file.clone(),
1753 )
1754 .into(),
1755 AtomicFact::EqualFact(inner) => EqualFact::new(
1756 inner
1757 .left
1758 .replace_with_numeric_result_if_can_be_calculated()
1759 .0,
1760 inner
1761 .right
1762 .replace_with_numeric_result_if_can_be_calculated()
1763 .0,
1764 inner.line_file.clone(),
1765 )
1766 .into(),
1767 AtomicFact::NotEqualFact(inner) => NotEqualFact::new(
1768 inner
1769 .left
1770 .replace_with_numeric_result_if_can_be_calculated()
1771 .0,
1772 inner
1773 .right
1774 .replace_with_numeric_result_if_can_be_calculated()
1775 .0,
1776 inner.line_file.clone(),
1777 )
1778 .into(),
1779 AtomicFact::LessFact(inner) => LessFact::new(
1780 inner
1781 .left
1782 .replace_with_numeric_result_if_can_be_calculated()
1783 .0,
1784 inner
1785 .right
1786 .replace_with_numeric_result_if_can_be_calculated()
1787 .0,
1788 inner.line_file.clone(),
1789 )
1790 .into(),
1791 AtomicFact::NotLessFact(inner) => NotLessFact::new(
1792 inner
1793 .left
1794 .replace_with_numeric_result_if_can_be_calculated()
1795 .0,
1796 inner
1797 .right
1798 .replace_with_numeric_result_if_can_be_calculated()
1799 .0,
1800 inner.line_file.clone(),
1801 )
1802 .into(),
1803 AtomicFact::GreaterFact(inner) => GreaterFact::new(
1804 inner
1805 .left
1806 .replace_with_numeric_result_if_can_be_calculated()
1807 .0,
1808 inner
1809 .right
1810 .replace_with_numeric_result_if_can_be_calculated()
1811 .0,
1812 inner.line_file.clone(),
1813 )
1814 .into(),
1815 AtomicFact::NotGreaterFact(inner) => NotGreaterFact::new(
1816 inner
1817 .left
1818 .replace_with_numeric_result_if_can_be_calculated()
1819 .0,
1820 inner
1821 .right
1822 .replace_with_numeric_result_if_can_be_calculated()
1823 .0,
1824 inner.line_file.clone(),
1825 )
1826 .into(),
1827 AtomicFact::LessEqualFact(inner) => LessEqualFact::new(
1828 inner
1829 .left
1830 .replace_with_numeric_result_if_can_be_calculated()
1831 .0,
1832 inner
1833 .right
1834 .replace_with_numeric_result_if_can_be_calculated()
1835 .0,
1836 inner.line_file.clone(),
1837 )
1838 .into(),
1839 AtomicFact::NotLessEqualFact(inner) => NotLessEqualFact::new(
1840 inner
1841 .left
1842 .replace_with_numeric_result_if_can_be_calculated()
1843 .0,
1844 inner
1845 .right
1846 .replace_with_numeric_result_if_can_be_calculated()
1847 .0,
1848 inner.line_file.clone(),
1849 )
1850 .into(),
1851 AtomicFact::GreaterEqualFact(inner) => GreaterEqualFact::new(
1852 inner
1853 .left
1854 .replace_with_numeric_result_if_can_be_calculated()
1855 .0,
1856 inner
1857 .right
1858 .replace_with_numeric_result_if_can_be_calculated()
1859 .0,
1860 inner.line_file.clone(),
1861 )
1862 .into(),
1863 AtomicFact::NotGreaterEqualFact(inner) => NotGreaterEqualFact::new(
1864 inner
1865 .left
1866 .replace_with_numeric_result_if_can_be_calculated()
1867 .0,
1868 inner
1869 .right
1870 .replace_with_numeric_result_if_can_be_calculated()
1871 .0,
1872 inner.line_file.clone(),
1873 )
1874 .into(),
1875 AtomicFact::IsSetFact(inner) => IsSetFact::new(
1876 inner
1877 .set
1878 .replace_with_numeric_result_if_can_be_calculated()
1879 .0,
1880 inner.line_file.clone(),
1881 )
1882 .into(),
1883 AtomicFact::NotIsSetFact(inner) => NotIsSetFact::new(
1884 inner
1885 .set
1886 .replace_with_numeric_result_if_can_be_calculated()
1887 .0,
1888 inner.line_file.clone(),
1889 )
1890 .into(),
1891 AtomicFact::IsNonemptySetFact(inner) => IsNonemptySetFact::new(
1892 inner
1893 .set
1894 .replace_with_numeric_result_if_can_be_calculated()
1895 .0,
1896 inner.line_file.clone(),
1897 )
1898 .into(),
1899 AtomicFact::NotIsNonemptySetFact(inner) => NotIsNonemptySetFact::new(
1900 inner
1901 .set
1902 .replace_with_numeric_result_if_can_be_calculated()
1903 .0,
1904 inner.line_file.clone(),
1905 )
1906 .into(),
1907 AtomicFact::IsFiniteSetFact(inner) => IsFiniteSetFact::new(
1908 inner
1909 .set
1910 .replace_with_numeric_result_if_can_be_calculated()
1911 .0,
1912 inner.line_file.clone(),
1913 )
1914 .into(),
1915 AtomicFact::NotIsFiniteSetFact(inner) => NotIsFiniteSetFact::new(
1916 inner
1917 .set
1918 .replace_with_numeric_result_if_can_be_calculated()
1919 .0,
1920 inner.line_file.clone(),
1921 )
1922 .into(),
1923 AtomicFact::InFact(inner) => InFact::new(
1924 inner
1925 .element
1926 .replace_with_numeric_result_if_can_be_calculated()
1927 .0,
1928 inner
1929 .set
1930 .replace_with_numeric_result_if_can_be_calculated()
1931 .0,
1932 inner.line_file.clone(),
1933 )
1934 .into(),
1935 AtomicFact::NotInFact(inner) => NotInFact::new(
1936 inner
1937 .element
1938 .replace_with_numeric_result_if_can_be_calculated()
1939 .0,
1940 inner
1941 .set
1942 .replace_with_numeric_result_if_can_be_calculated()
1943 .0,
1944 inner.line_file.clone(),
1945 )
1946 .into(),
1947 AtomicFact::IsCartFact(inner) => IsCartFact::new(
1948 inner
1949 .set
1950 .replace_with_numeric_result_if_can_be_calculated()
1951 .0,
1952 inner.line_file.clone(),
1953 )
1954 .into(),
1955 AtomicFact::NotIsCartFact(inner) => NotIsCartFact::new(
1956 inner
1957 .set
1958 .replace_with_numeric_result_if_can_be_calculated()
1959 .0,
1960 inner.line_file.clone(),
1961 )
1962 .into(),
1963 AtomicFact::IsTupleFact(inner) => IsTupleFact::new(
1964 inner
1965 .set
1966 .replace_with_numeric_result_if_can_be_calculated()
1967 .0,
1968 inner.line_file.clone(),
1969 )
1970 .into(),
1971 AtomicFact::NotIsTupleFact(inner) => NotIsTupleFact::new(
1972 inner
1973 .set
1974 .replace_with_numeric_result_if_can_be_calculated()
1975 .0,
1976 inner.line_file.clone(),
1977 )
1978 .into(),
1979 AtomicFact::SubsetFact(inner) => SubsetFact::new(
1980 inner
1981 .left
1982 .replace_with_numeric_result_if_can_be_calculated()
1983 .0,
1984 inner
1985 .right
1986 .replace_with_numeric_result_if_can_be_calculated()
1987 .0,
1988 inner.line_file.clone(),
1989 )
1990 .into(),
1991 AtomicFact::NotSubsetFact(inner) => NotSubsetFact::new(
1992 inner
1993 .left
1994 .replace_with_numeric_result_if_can_be_calculated()
1995 .0,
1996 inner
1997 .right
1998 .replace_with_numeric_result_if_can_be_calculated()
1999 .0,
2000 inner.line_file.clone(),
2001 )
2002 .into(),
2003 AtomicFact::SupersetFact(inner) => SupersetFact::new(
2004 inner
2005 .left
2006 .replace_with_numeric_result_if_can_be_calculated()
2007 .0,
2008 inner
2009 .right
2010 .replace_with_numeric_result_if_can_be_calculated()
2011 .0,
2012 inner.line_file.clone(),
2013 )
2014 .into(),
2015 AtomicFact::NotSupersetFact(inner) => NotSupersetFact::new(
2016 inner
2017 .left
2018 .replace_with_numeric_result_if_can_be_calculated()
2019 .0,
2020 inner
2021 .right
2022 .replace_with_numeric_result_if_can_be_calculated()
2023 .0,
2024 inner.line_file.clone(),
2025 )
2026 .into(),
2027 AtomicFact::RestrictFact(inner) => RestrictFact::new(
2028 inner
2029 .obj
2030 .replace_with_numeric_result_if_can_be_calculated()
2031 .0,
2032 inner
2033 .obj_can_restrict_to_fn_set
2034 .replace_with_numeric_result_if_can_be_calculated()
2035 .0,
2036 inner.line_file.clone(),
2037 )
2038 .into(),
2039 AtomicFact::NotRestrictFact(inner) => NotRestrictFact::new(
2040 inner
2041 .obj
2042 .replace_with_numeric_result_if_can_be_calculated()
2043 .0,
2044 inner
2045 .obj_cannot_restrict_to_fn_set
2046 .replace_with_numeric_result_if_can_be_calculated()
2047 .0,
2048 inner.line_file.clone(),
2049 )
2050 .into(),
2051 };
2052 let any_argument_replaced = calculated_atomic_fact.to_string() != self.to_string();
2053 (calculated_atomic_fact, any_argument_replaced)
2054 }
2055}
2056
2057impl From<NormalAtomicFact> for AtomicFact {
2058 fn from(f: NormalAtomicFact) -> Self {
2059 AtomicFact::NormalAtomicFact(f)
2060 }
2061}
2062
2063impl From<EqualFact> for AtomicFact {
2064 fn from(f: EqualFact) -> Self {
2065 AtomicFact::EqualFact(f)
2066 }
2067}
2068
2069impl From<LessFact> for AtomicFact {
2070 fn from(f: LessFact) -> Self {
2071 AtomicFact::LessFact(f)
2072 }
2073}
2074
2075impl From<GreaterFact> for AtomicFact {
2076 fn from(f: GreaterFact) -> Self {
2077 AtomicFact::GreaterFact(f)
2078 }
2079}
2080
2081impl From<LessEqualFact> for AtomicFact {
2082 fn from(f: LessEqualFact) -> Self {
2083 AtomicFact::LessEqualFact(f)
2084 }
2085}
2086
2087impl From<GreaterEqualFact> for AtomicFact {
2088 fn from(f: GreaterEqualFact) -> Self {
2089 AtomicFact::GreaterEqualFact(f)
2090 }
2091}
2092
2093impl From<IsSetFact> for AtomicFact {
2094 fn from(f: IsSetFact) -> Self {
2095 AtomicFact::IsSetFact(f)
2096 }
2097}
2098
2099impl From<IsNonemptySetFact> for AtomicFact {
2100 fn from(f: IsNonemptySetFact) -> Self {
2101 AtomicFact::IsNonemptySetFact(f)
2102 }
2103}
2104
2105impl From<IsFiniteSetFact> for AtomicFact {
2106 fn from(f: IsFiniteSetFact) -> Self {
2107 AtomicFact::IsFiniteSetFact(f)
2108 }
2109}
2110
2111impl From<InFact> for AtomicFact {
2112 fn from(f: InFact) -> Self {
2113 AtomicFact::InFact(f)
2114 }
2115}
2116
2117impl From<IsCartFact> for AtomicFact {
2118 fn from(f: IsCartFact) -> Self {
2119 AtomicFact::IsCartFact(f)
2120 }
2121}
2122
2123impl From<IsTupleFact> for AtomicFact {
2124 fn from(f: IsTupleFact) -> Self {
2125 AtomicFact::IsTupleFact(f)
2126 }
2127}
2128
2129impl From<SubsetFact> for AtomicFact {
2130 fn from(f: SubsetFact) -> Self {
2131 AtomicFact::SubsetFact(f)
2132 }
2133}
2134
2135impl From<SupersetFact> for AtomicFact {
2136 fn from(f: SupersetFact) -> Self {
2137 AtomicFact::SupersetFact(f)
2138 }
2139}
2140
2141impl From<RestrictFact> for AtomicFact {
2142 fn from(f: RestrictFact) -> Self {
2143 AtomicFact::RestrictFact(f)
2144 }
2145}
2146
2147impl From<NotRestrictFact> for AtomicFact {
2148 fn from(f: NotRestrictFact) -> Self {
2149 AtomicFact::NotRestrictFact(f)
2150 }
2151}
2152
2153impl From<NotNormalAtomicFact> for AtomicFact {
2154 fn from(f: NotNormalAtomicFact) -> Self {
2155 AtomicFact::NotNormalAtomicFact(f)
2156 }
2157}
2158
2159impl From<NotEqualFact> for AtomicFact {
2160 fn from(f: NotEqualFact) -> Self {
2161 AtomicFact::NotEqualFact(f)
2162 }
2163}
2164
2165impl From<NotLessFact> for AtomicFact {
2166 fn from(f: NotLessFact) -> Self {
2167 AtomicFact::NotLessFact(f)
2168 }
2169}
2170
2171impl From<NotGreaterFact> for AtomicFact {
2172 fn from(f: NotGreaterFact) -> Self {
2173 AtomicFact::NotGreaterFact(f)
2174 }
2175}
2176
2177impl From<NotLessEqualFact> for AtomicFact {
2178 fn from(f: NotLessEqualFact) -> Self {
2179 AtomicFact::NotLessEqualFact(f)
2180 }
2181}
2182
2183impl From<NotGreaterEqualFact> for AtomicFact {
2184 fn from(f: NotGreaterEqualFact) -> Self {
2185 AtomicFact::NotGreaterEqualFact(f)
2186 }
2187}
2188
2189impl From<NotIsSetFact> for AtomicFact {
2190 fn from(f: NotIsSetFact) -> Self {
2191 AtomicFact::NotIsSetFact(f)
2192 }
2193}
2194
2195impl From<NotIsNonemptySetFact> for AtomicFact {
2196 fn from(f: NotIsNonemptySetFact) -> Self {
2197 AtomicFact::NotIsNonemptySetFact(f)
2198 }
2199}
2200
2201impl From<NotIsFiniteSetFact> for AtomicFact {
2202 fn from(f: NotIsFiniteSetFact) -> Self {
2203 AtomicFact::NotIsFiniteSetFact(f)
2204 }
2205}
2206
2207impl From<NotInFact> for AtomicFact {
2208 fn from(f: NotInFact) -> Self {
2209 AtomicFact::NotInFact(f)
2210 }
2211}
2212
2213impl From<NotIsCartFact> for AtomicFact {
2214 fn from(f: NotIsCartFact) -> Self {
2215 AtomicFact::NotIsCartFact(f)
2216 }
2217}
2218
2219impl From<NotIsTupleFact> for AtomicFact {
2220 fn from(f: NotIsTupleFact) -> Self {
2221 AtomicFact::NotIsTupleFact(f)
2222 }
2223}
2224
2225impl From<NotSubsetFact> for AtomicFact {
2226 fn from(f: NotSubsetFact) -> Self {
2227 AtomicFact::NotSubsetFact(f)
2228 }
2229}
2230
2231impl From<NotSupersetFact> for AtomicFact {
2232 fn from(f: NotSupersetFact) -> Self {
2233 AtomicFact::NotSupersetFact(f)
2234 }
2235}
2236
2237impl From<NormalAtomicFact> for Fact {
2238 fn from(f: NormalAtomicFact) -> Self {
2239 Fact::AtomicFact(f.into())
2240 }
2241}
2242
2243impl From<EqualFact> for Fact {
2244 fn from(f: EqualFact) -> Self {
2245 Fact::AtomicFact(f.into())
2246 }
2247}
2248
2249impl From<LessFact> for Fact {
2250 fn from(f: LessFact) -> Self {
2251 Fact::AtomicFact(f.into())
2252 }
2253}
2254
2255impl From<GreaterFact> for Fact {
2256 fn from(f: GreaterFact) -> Self {
2257 Fact::AtomicFact(f.into())
2258 }
2259}
2260
2261impl From<LessEqualFact> for Fact {
2262 fn from(f: LessEqualFact) -> Self {
2263 Fact::AtomicFact(f.into())
2264 }
2265}
2266
2267impl From<GreaterEqualFact> for Fact {
2268 fn from(f: GreaterEqualFact) -> Self {
2269 Fact::AtomicFact(f.into())
2270 }
2271}
2272
2273impl From<IsSetFact> for Fact {
2274 fn from(f: IsSetFact) -> Self {
2275 Fact::AtomicFact(f.into())
2276 }
2277}
2278
2279impl From<IsNonemptySetFact> for Fact {
2280 fn from(f: IsNonemptySetFact) -> Self {
2281 Fact::AtomicFact(f.into())
2282 }
2283}
2284
2285impl From<IsFiniteSetFact> for Fact {
2286 fn from(f: IsFiniteSetFact) -> Self {
2287 Fact::AtomicFact(f.into())
2288 }
2289}
2290
2291impl From<InFact> for Fact {
2292 fn from(f: InFact) -> Self {
2293 Fact::AtomicFact(f.into())
2294 }
2295}
2296
2297impl From<IsCartFact> for Fact {
2298 fn from(f: IsCartFact) -> Self {
2299 Fact::AtomicFact(f.into())
2300 }
2301}
2302
2303impl From<IsTupleFact> for Fact {
2304 fn from(f: IsTupleFact) -> Self {
2305 Fact::AtomicFact(f.into())
2306 }
2307}
2308
2309impl From<SubsetFact> for Fact {
2310 fn from(f: SubsetFact) -> Self {
2311 Fact::AtomicFact(f.into())
2312 }
2313}
2314
2315impl From<SupersetFact> for Fact {
2316 fn from(f: SupersetFact) -> Self {
2317 Fact::AtomicFact(f.into())
2318 }
2319}
2320
2321impl From<RestrictFact> for Fact {
2322 fn from(f: RestrictFact) -> Self {
2323 Fact::AtomicFact(f.into())
2324 }
2325}
2326
2327impl From<NotRestrictFact> for Fact {
2328 fn from(f: NotRestrictFact) -> Self {
2329 Fact::AtomicFact(f.into())
2330 }
2331}
2332
2333impl From<NotNormalAtomicFact> for Fact {
2334 fn from(f: NotNormalAtomicFact) -> Self {
2335 Fact::AtomicFact(f.into())
2336 }
2337}
2338
2339impl From<NotEqualFact> for Fact {
2340 fn from(f: NotEqualFact) -> Self {
2341 Fact::AtomicFact(f.into())
2342 }
2343}
2344
2345impl From<NotLessFact> for Fact {
2346 fn from(f: NotLessFact) -> Self {
2347 Fact::AtomicFact(f.into())
2348 }
2349}
2350
2351impl From<NotGreaterFact> for Fact {
2352 fn from(f: NotGreaterFact) -> Self {
2353 Fact::AtomicFact(f.into())
2354 }
2355}
2356
2357impl From<NotLessEqualFact> for Fact {
2358 fn from(f: NotLessEqualFact) -> Self {
2359 Fact::AtomicFact(f.into())
2360 }
2361}
2362
2363impl From<NotGreaterEqualFact> for Fact {
2364 fn from(f: NotGreaterEqualFact) -> Self {
2365 Fact::AtomicFact(f.into())
2366 }
2367}
2368
2369impl From<NotIsSetFact> for Fact {
2370 fn from(f: NotIsSetFact) -> Self {
2371 Fact::AtomicFact(f.into())
2372 }
2373}
2374
2375impl From<NotIsNonemptySetFact> for Fact {
2376 fn from(f: NotIsNonemptySetFact) -> Self {
2377 Fact::AtomicFact(f.into())
2378 }
2379}
2380
2381impl From<NotIsFiniteSetFact> for Fact {
2382 fn from(f: NotIsFiniteSetFact) -> Self {
2383 Fact::AtomicFact(f.into())
2384 }
2385}
2386
2387impl From<NotInFact> for Fact {
2388 fn from(f: NotInFact) -> Self {
2389 Fact::AtomicFact(f.into())
2390 }
2391}
2392
2393impl From<NotIsCartFact> for Fact {
2394 fn from(f: NotIsCartFact) -> Self {
2395 Fact::AtomicFact(f.into())
2396 }
2397}
2398
2399impl From<NotIsTupleFact> for Fact {
2400 fn from(f: NotIsTupleFact) -> Self {
2401 Fact::AtomicFact(f.into())
2402 }
2403}
2404
2405impl From<NotSubsetFact> for Fact {
2406 fn from(f: NotSubsetFact) -> Self {
2407 Fact::AtomicFact(f.into())
2408 }
2409}
2410
2411impl From<NotSupersetFact> for Fact {
2412 fn from(f: NotSupersetFact) -> Self {
2413 Fact::AtomicFact(f.into())
2414 }
2415}