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