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 pub fn commutative_reordered_args(&self, gather: &[usize]) -> Option<Self> {
1063 match self {
1064 AtomicFact::NormalAtomicFact(f) => {
1065 let n = f.body.len();
1066 if gather.len() != n || n < 2 {
1067 return None;
1068 }
1069 let mut seen = vec![false; n];
1070 for &i in gather {
1071 if i >= n || seen[i] {
1072 return None;
1073 }
1074 seen[i] = true;
1075 }
1076 let new_body: Vec<Obj> = gather.iter().map(|&i| f.body[i].clone()).collect();
1077 Some(
1078 NormalAtomicFact::new(f.predicate.clone(), new_body, f.line_file.clone())
1079 .into(),
1080 )
1081 }
1082 _ => None,
1083 }
1084 }
1085}
1086
1087impl AtomicFact {
1088 pub fn to_atomic_fact(
1089 prop_name: AtomicName,
1090 is_true: bool,
1091 args: Vec<Obj>,
1092 line_file: LineFile,
1093 ) -> Result<AtomicFact, RuntimeError> {
1094 let prop_name_as_string = prop_name.to_string();
1095 match prop_name_as_string.as_str() {
1096 EQUAL => {
1097 if args.len() != 2 {
1098 let msg = format!("{} requires 2 arguments, but got {}", EQUAL, args.len());
1099 return Err(NewFactRuntimeError(
1100 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1101 )
1102 .into());
1103 }
1104 let mut args = args;
1105 let a0 = args.remove(0);
1106 let a1 = args.remove(0);
1107 if is_true {
1108 Ok(EqualFact::new(a0, a1, line_file).into())
1109 } else {
1110 Ok(NotEqualFact::new(a0, a1, line_file).into())
1111 }
1112 }
1113 NOT_EQUAL => {
1114 if args.len() != 2 {
1115 let msg = format!("{} requires 2 arguments, but got {}", NOT_EQUAL, args.len());
1116 return Err(NewFactRuntimeError(
1117 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1118 )
1119 .into());
1120 }
1121 let mut args = args;
1122 let a0 = args.remove(0);
1123 let a1 = args.remove(0);
1124 if is_true {
1125 Ok(NotEqualFact::new(a0, a1, line_file).into())
1126 } else {
1127 Ok(EqualFact::new(a0, a1, line_file).into())
1128 }
1129 }
1130 LESS => {
1131 if args.len() != 2 {
1132 let msg = format!("{} requires 2 arguments, but got {}", LESS, args.len());
1133 return Err(NewFactRuntimeError(
1134 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1135 )
1136 .into());
1137 }
1138 let mut args = args;
1139 let a0 = args.remove(0);
1140 let a1 = args.remove(0);
1141 if is_true {
1142 Ok(LessFact::new(a0, a1, line_file).into())
1143 } else {
1144 Ok(NotLessFact::new(a0, a1, line_file).into())
1145 }
1146 }
1147 GREATER => {
1148 if args.len() != 2 {
1149 let msg = format!("{} requires 2 arguments, but got {}", GREATER, args.len());
1150 return Err(NewFactRuntimeError(
1151 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1152 )
1153 .into());
1154 }
1155 let mut args = args;
1156 let a0 = args.remove(0);
1157 let a1 = args.remove(0);
1158 if is_true {
1159 Ok(GreaterFact::new(a0, a1, line_file).into())
1160 } else {
1161 Ok(NotGreaterFact::new(a0, a1, line_file).into())
1162 }
1163 }
1164 LESS_EQUAL => {
1165 if args.len() != 2 {
1166 let msg = format!(
1167 "{} requires 2 arguments, but got {}",
1168 LESS_EQUAL,
1169 args.len()
1170 );
1171 return Err(NewFactRuntimeError(
1172 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1173 )
1174 .into());
1175 }
1176 let mut args = args;
1177 let a0 = args.remove(0);
1178 let a1 = args.remove(0);
1179 if is_true {
1180 Ok(LessEqualFact::new(a0, a1, line_file).into())
1181 } else {
1182 Ok(NotLessEqualFact::new(a0, a1, line_file).into())
1183 }
1184 }
1185 GREATER_EQUAL => {
1186 if args.len() != 2 {
1187 let msg = format!(
1188 "{} requires 2 arguments, but got {}",
1189 GREATER_EQUAL,
1190 args.len()
1191 );
1192 return Err(NewFactRuntimeError(
1193 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1194 )
1195 .into());
1196 }
1197 let mut args = args;
1198 let a0 = args.remove(0);
1199 let a1 = args.remove(0);
1200 if is_true {
1201 Ok(GreaterEqualFact::new(a0, a1, line_file).into())
1202 } else {
1203 Ok(NotGreaterEqualFact::new(a0, a1, line_file).into())
1204 }
1205 }
1206 IS_SET => {
1207 if args.len() != 1 {
1208 let msg = format!("{} requires 1 argument, but got {}", IS_SET, args.len());
1209 return Err(NewFactRuntimeError(
1210 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1211 )
1212 .into());
1213 }
1214 let mut args = args;
1215 let a0 = args.remove(0);
1216 if is_true {
1217 Ok(IsSetFact::new(a0, line_file).into())
1218 } else {
1219 Ok(NotIsSetFact::new(a0, line_file).into())
1220 }
1221 }
1222 IS_NONEMPTY_SET => {
1223 if args.len() != 1 {
1224 let msg = format!(
1225 "{} requires 1 argument, but got {}",
1226 IS_NONEMPTY_SET,
1227 args.len()
1228 );
1229 return Err(NewFactRuntimeError(
1230 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1231 )
1232 .into());
1233 }
1234 let mut args = args;
1235 let a0 = args.remove(0);
1236 if is_true {
1237 Ok(IsNonemptySetFact::new(a0, line_file).into())
1238 } else {
1239 Ok(NotIsNonemptySetFact::new(a0, line_file).into())
1240 }
1241 }
1242 IS_FINITE_SET => {
1243 if args.len() != 1 {
1244 let msg = format!(
1245 "{} requires 1 argument, but got {}",
1246 IS_FINITE_SET,
1247 args.len()
1248 );
1249 return Err(NewFactRuntimeError(
1250 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1251 )
1252 .into());
1253 }
1254 let mut args = args;
1255 let a0 = args.remove(0);
1256 if is_true {
1257 Ok(IsFiniteSetFact::new(a0, line_file).into())
1258 } else {
1259 Ok(NotIsFiniteSetFact::new(a0, line_file).into())
1260 }
1261 }
1262 IN => {
1263 if args.len() != 2 {
1264 let msg = format!("{} requires 2 arguments, but got {}", IN, args.len());
1265 return Err(NewFactRuntimeError(
1266 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1267 )
1268 .into());
1269 }
1270 let mut args = args;
1271 let a0 = args.remove(0);
1272 let a1 = args.remove(0);
1273 if is_true {
1274 Ok(InFact::new(a0, a1, line_file).into())
1275 } else {
1276 Ok(NotInFact::new(a0, a1, line_file).into())
1277 }
1278 }
1279 IS_CART => {
1280 if args.len() != 1 {
1281 let msg = format!("{} requires 1 argument, but got {}", IS_CART, args.len());
1282 return Err(NewFactRuntimeError(
1283 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1284 )
1285 .into());
1286 }
1287 let mut args = args;
1288 let a0 = args.remove(0);
1289 if is_true {
1290 Ok(IsCartFact::new(a0, line_file).into())
1291 } else {
1292 Ok(NotIsCartFact::new(a0, line_file).into())
1293 }
1294 }
1295 IS_TUPLE => {
1296 if args.len() != 1 {
1297 let msg = format!("{} requires 1 argument, but got {}", IS_TUPLE, args.len());
1298 return Err(NewFactRuntimeError(
1299 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1300 )
1301 .into());
1302 }
1303 let mut args = args;
1304 let a0 = args.remove(0);
1305 if is_true {
1306 Ok(IsTupleFact::new(a0, line_file).into())
1307 } else {
1308 Ok(NotIsTupleFact::new(a0, line_file).into())
1309 }
1310 }
1311 SUBSET => {
1312 if args.len() != 2 {
1313 let msg = format!("{} requires 2 arguments, but got {}", SUBSET, args.len());
1314 return Err(NewFactRuntimeError(
1315 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1316 )
1317 .into());
1318 }
1319 let mut args = args;
1320 let a0 = args.remove(0);
1321 let a1 = args.remove(0);
1322 if is_true {
1323 Ok(SubsetFact::new(a0, a1, line_file).into())
1324 } else {
1325 Ok(NotSubsetFact::new(a0, a1, line_file).into())
1326 }
1327 }
1328 SUPERSET => {
1329 if args.len() != 2 {
1330 let msg = format!("{} requires 2 arguments, but got {}", SUPERSET, args.len());
1331 return Err(NewFactRuntimeError(
1332 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1333 )
1334 .into());
1335 }
1336 let mut args = args;
1337 let a0 = args.remove(0);
1338 let a1 = args.remove(0);
1339 if is_true {
1340 Ok(SupersetFact::new(a0, a1, line_file).into())
1341 } else {
1342 Ok(NotSupersetFact::new(a0, a1, line_file).into())
1343 }
1344 }
1345 RESTRICT_FN_IN => {
1346 if args.len() != 2 {
1347 let msg = format!(
1348 "{} requires 2 arguments, but got {}",
1349 RESTRICT_FN_IN,
1350 args.len()
1351 );
1352 return Err(NewFactRuntimeError(
1353 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1354 )
1355 .into());
1356 }
1357 let mut args = args;
1358 let a0 = args.remove(0);
1359 let a1 = args.remove(0);
1360 if is_true {
1361 Ok(RestrictFact::new(a0, a1, line_file).into())
1362 } else {
1363 Ok(NotRestrictFact::new(a0, a1, line_file).into())
1364 }
1365 }
1366 FN_EQ_IN => {
1367 if !is_true {
1368 let msg = format!("{} does not support `not`", FN_EQ_IN);
1369 return Err(NewFactRuntimeError(
1370 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1371 )
1372 .into());
1373 }
1374 if args.len() != 3 {
1375 let msg = format!(
1376 "{} requires 3 arguments (f, g, set), but got {}",
1377 FN_EQ_IN,
1378 args.len()
1379 );
1380 return Err(NewFactRuntimeError(
1381 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1382 )
1383 .into());
1384 }
1385 let mut args = args;
1386 let a0 = args.remove(0);
1387 let a1 = args.remove(0);
1388 let a2 = args.remove(0);
1389 Ok(FnEqualInFact::new(a0, a1, a2, line_file).into())
1390 }
1391 FN_EQ => {
1392 if !is_true {
1393 let msg = format!("{} does not support `not`", FN_EQ);
1394 return Err(NewFactRuntimeError(
1395 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1396 )
1397 .into());
1398 }
1399 if args.len() != 2 {
1400 let msg = format!(
1401 "{} requires 2 arguments (f, g), but got {}",
1402 FN_EQ,
1403 args.len()
1404 );
1405 return Err(NewFactRuntimeError(
1406 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1407 )
1408 .into());
1409 }
1410 let mut args = args;
1411 let a0 = args.remove(0);
1412 let a1 = args.remove(0);
1413 Ok(FnEqualFact::new(a0, a1, line_file).into())
1414 }
1415 _ => {
1416 if is_true {
1417 Ok(NormalAtomicFact::new(prop_name, args, line_file).into())
1418 } else {
1419 Ok(NotNormalAtomicFact::new(prop_name, args, line_file).into())
1420 }
1421 }
1422 }
1423 }
1424}
1425
1426impl AtomicFact {
1427 pub fn args(&self) -> Vec<Obj> {
1428 match self {
1429 AtomicFact::NormalAtomicFact(normal_atomic_fact) => normal_atomic_fact.body.clone(),
1430 AtomicFact::EqualFact(equal_fact) => {
1431 vec![equal_fact.left.clone(), equal_fact.right.clone()]
1432 }
1433 AtomicFact::LessFact(less_fact) => {
1434 vec![less_fact.left.clone(), less_fact.right.clone()]
1435 }
1436 AtomicFact::GreaterFact(greater_fact) => {
1437 vec![greater_fact.left.clone(), greater_fact.right.clone()]
1438 }
1439 AtomicFact::LessEqualFact(less_equal_fact) => {
1440 vec![less_equal_fact.left.clone(), less_equal_fact.right.clone()]
1441 }
1442 AtomicFact::GreaterEqualFact(greater_equal_fact) => vec![
1443 greater_equal_fact.left.clone(),
1444 greater_equal_fact.right.clone(),
1445 ],
1446 AtomicFact::IsSetFact(is_set_fact) => vec![is_set_fact.set.clone()],
1447 AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => {
1448 vec![is_nonempty_set_fact.set.clone()]
1449 }
1450 AtomicFact::IsFiniteSetFact(is_finite_set_fact) => vec![is_finite_set_fact.set.clone()],
1451 AtomicFact::InFact(in_fact) => vec![in_fact.element.clone(), in_fact.set.clone()],
1452 AtomicFact::IsCartFact(is_cart_fact) => vec![is_cart_fact.set.clone()],
1453 AtomicFact::IsTupleFact(is_tuple_fact) => vec![is_tuple_fact.set.clone()],
1454 AtomicFact::SubsetFact(subset_fact) => {
1455 vec![subset_fact.left.clone(), subset_fact.right.clone()]
1456 }
1457 AtomicFact::SupersetFact(superset_fact) => {
1458 vec![superset_fact.left.clone(), superset_fact.right.clone()]
1459 }
1460 AtomicFact::NotNormalAtomicFact(not_normal_atomic_fact) => {
1461 not_normal_atomic_fact.body.clone()
1462 }
1463 AtomicFact::NotEqualFact(not_equal_fact) => {
1464 vec![not_equal_fact.left.clone(), not_equal_fact.right.clone()]
1465 }
1466 AtomicFact::NotLessFact(not_less_fact) => {
1467 vec![not_less_fact.left.clone(), not_less_fact.right.clone()]
1468 }
1469 AtomicFact::NotGreaterFact(not_greater_fact) => vec![
1470 not_greater_fact.left.clone(),
1471 not_greater_fact.right.clone(),
1472 ],
1473 AtomicFact::NotLessEqualFact(not_less_equal_fact) => vec![
1474 not_less_equal_fact.left.clone(),
1475 not_less_equal_fact.right.clone(),
1476 ],
1477 AtomicFact::NotGreaterEqualFact(not_greater_equal_fact) => vec![
1478 not_greater_equal_fact.left.clone(),
1479 not_greater_equal_fact.right.clone(),
1480 ],
1481 AtomicFact::NotIsSetFact(not_is_set_fact) => vec![not_is_set_fact.set.clone()],
1482 AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => {
1483 vec![not_is_nonempty_set_fact.set.clone()]
1484 }
1485 AtomicFact::NotIsFiniteSetFact(not_is_finite_set_fact) => {
1486 vec![not_is_finite_set_fact.set.clone()]
1487 }
1488 AtomicFact::NotInFact(not_in_fact) => {
1489 vec![not_in_fact.element.clone(), not_in_fact.set.clone()]
1490 }
1491 AtomicFact::NotIsCartFact(not_is_cart_fact) => vec![not_is_cart_fact.set.clone()],
1492 AtomicFact::NotIsTupleFact(not_is_tuple_fact) => vec![not_is_tuple_fact.set.clone()],
1493 AtomicFact::NotSubsetFact(not_subset_fact) => {
1494 vec![not_subset_fact.left.clone(), not_subset_fact.right.clone()]
1495 }
1496 AtomicFact::NotSupersetFact(not_superset_fact) => vec![
1497 not_superset_fact.left.clone(),
1498 not_superset_fact.right.clone(),
1499 ],
1500 AtomicFact::RestrictFact(restrict_fact) => vec![
1501 restrict_fact.obj.clone(),
1502 restrict_fact.obj_can_restrict_to_fn_set.clone().into(),
1503 ],
1504 AtomicFact::NotRestrictFact(not_restrict_fact) => vec![
1505 not_restrict_fact.obj.clone(),
1506 not_restrict_fact.obj_cannot_restrict_to_fn_set.clone(),
1507 ],
1508 AtomicFact::FnEqualInFact(f) => {
1509 vec![f.left.clone(), f.right.clone(), f.set.clone()]
1510 }
1511 AtomicFact::FnEqualFact(f) => vec![f.left.clone(), f.right.clone()],
1512 }
1513 }
1514}
1515
1516impl AtomicFact {
1518 pub fn is_builtin_predicate_and_return_expected_args_len(&self) -> usize {
1519 match self {
1520 AtomicFact::EqualFact(_) => 2,
1521 AtomicFact::LessFact(_) => 2,
1522 AtomicFact::GreaterFact(_) => 2,
1523 AtomicFact::LessEqualFact(_) => 2,
1524 AtomicFact::GreaterEqualFact(_) => 2,
1525 AtomicFact::IsSetFact(_) => 1,
1526 AtomicFact::IsNonemptySetFact(_) => 1,
1527 AtomicFact::IsFiniteSetFact(_) => 1,
1528 AtomicFact::InFact(_) => 2,
1529 AtomicFact::IsCartFact(_) => 1,
1530 AtomicFact::IsTupleFact(_) => 1,
1531 AtomicFact::SubsetFact(_) => 2,
1532 AtomicFact::SupersetFact(_) => 2,
1533 AtomicFact::NotEqualFact(_) => 2,
1534 AtomicFact::NotLessFact(_) => 2,
1535 AtomicFact::NotGreaterFact(_) => 2,
1536 AtomicFact::NotLessEqualFact(_) => 2,
1537 AtomicFact::NotGreaterEqualFact(_) => 2,
1538 AtomicFact::NotIsSetFact(_) => 1,
1539 AtomicFact::NotIsNonemptySetFact(_) => 1,
1540 AtomicFact::NotIsFiniteSetFact(_) => 1,
1541 AtomicFact::NotInFact(_) => 2,
1542 AtomicFact::NotIsCartFact(_) => 1,
1543 AtomicFact::NotIsTupleFact(_) => 1,
1544 AtomicFact::NotSubsetFact(_) => 2,
1545 AtomicFact::NotSupersetFact(_) => 2,
1546 AtomicFact::RestrictFact(_) => 2,
1547 AtomicFact::NotRestrictFact(_) => 2,
1548 AtomicFact::FnEqualInFact(_) => 3,
1549 AtomicFact::FnEqualFact(_) => 2,
1550 _ => unreachable!("其他情况不是builtin predicate"),
1551 }
1552 }
1553}
1554
1555impl AtomicFact {
1556 pub fn number_of_args(&self) -> usize {
1557 match self {
1558 AtomicFact::EqualFact(_) => 2,
1559 AtomicFact::LessFact(_) => 2,
1560 AtomicFact::GreaterFact(_) => 2,
1561 AtomicFact::LessEqualFact(_) => 2,
1562 AtomicFact::GreaterEqualFact(_) => 2,
1563 AtomicFact::IsSetFact(_) => 1,
1564 AtomicFact::IsNonemptySetFact(_) => 1,
1565 AtomicFact::IsFiniteSetFact(_) => 1,
1566 AtomicFact::InFact(_) => 2,
1567 AtomicFact::IsCartFact(_) => 1,
1568 AtomicFact::IsTupleFact(_) => 1,
1569 AtomicFact::SubsetFact(_) => 2,
1570 AtomicFact::SupersetFact(_) => 2,
1571 AtomicFact::NotEqualFact(_) => 2,
1572 AtomicFact::NotLessFact(_) => 2,
1573 AtomicFact::NotGreaterFact(_) => 2,
1574 AtomicFact::NotLessEqualFact(_) => 2,
1575 AtomicFact::NotGreaterEqualFact(_) => 2,
1576 AtomicFact::NotIsSetFact(_) => 1,
1577 AtomicFact::NotIsNonemptySetFact(_) => 1,
1578 AtomicFact::NotIsFiniteSetFact(_) => 1,
1579 AtomicFact::NotInFact(_) => 2,
1580 AtomicFact::NotIsCartFact(_) => 1,
1581 AtomicFact::NotIsTupleFact(_) => 1,
1582 AtomicFact::NotSubsetFact(_) => 2,
1583 AtomicFact::NotSupersetFact(_) => 2,
1584 AtomicFact::NormalAtomicFact(a) => a.body.len(),
1585 AtomicFact::NotNormalAtomicFact(a) => a.body.len(),
1586 AtomicFact::RestrictFact(_) => 2,
1587 AtomicFact::NotRestrictFact(_) => 2,
1588 AtomicFact::FnEqualInFact(_) => 3,
1589 AtomicFact::FnEqualFact(_) => 2,
1590 }
1591 }
1592
1593 pub fn line_file(&self) -> LineFile {
1594 match self {
1595 AtomicFact::EqualFact(a) => a.line_file.clone(),
1596 AtomicFact::LessFact(a) => a.line_file.clone(),
1597 AtomicFact::GreaterFact(a) => a.line_file.clone(),
1598 AtomicFact::LessEqualFact(a) => a.line_file.clone(),
1599 AtomicFact::GreaterEqualFact(a) => a.line_file.clone(),
1600 AtomicFact::IsSetFact(a) => a.line_file.clone(),
1601 AtomicFact::IsNonemptySetFact(a) => a.line_file.clone(),
1602 AtomicFact::IsFiniteSetFact(a) => a.line_file.clone(),
1603 AtomicFact::InFact(a) => a.line_file.clone(),
1604 AtomicFact::IsCartFact(a) => a.line_file.clone(),
1605 AtomicFact::IsTupleFact(a) => a.line_file.clone(),
1606 AtomicFact::SubsetFact(a) => a.line_file.clone(),
1607 AtomicFact::SupersetFact(a) => a.line_file.clone(),
1608 AtomicFact::NormalAtomicFact(a) => a.line_file.clone(),
1609 AtomicFact::NotNormalAtomicFact(a) => a.line_file.clone(),
1610 AtomicFact::NotEqualFact(a) => a.line_file.clone(),
1611 AtomicFact::NotLessFact(a) => a.line_file.clone(),
1612 AtomicFact::NotGreaterFact(a) => a.line_file.clone(),
1613 AtomicFact::NotLessEqualFact(a) => a.line_file.clone(),
1614 AtomicFact::NotGreaterEqualFact(a) => a.line_file.clone(),
1615 AtomicFact::NotIsSetFact(a) => a.line_file.clone(),
1616 AtomicFact::NotIsNonemptySetFact(a) => a.line_file.clone(),
1617 AtomicFact::NotIsFiniteSetFact(a) => a.line_file.clone(),
1618 AtomicFact::NotInFact(a) => a.line_file.clone(),
1619 AtomicFact::NotIsCartFact(a) => a.line_file.clone(),
1620 AtomicFact::NotIsTupleFact(a) => a.line_file.clone(),
1621 AtomicFact::NotSubsetFact(a) => a.line_file.clone(),
1622 AtomicFact::NotSupersetFact(a) => a.line_file.clone(),
1623 AtomicFact::RestrictFact(a) => a.line_file.clone(),
1624 AtomicFact::NotRestrictFact(a) => a.line_file.clone(),
1625 AtomicFact::FnEqualInFact(a) => a.line_file.clone(),
1626 AtomicFact::FnEqualFact(a) => a.line_file.clone(),
1627 }
1628 }
1629
1630 pub fn with_line_file(mut self, line_file: LineFile) -> Self {
1631 match &mut self {
1632 AtomicFact::EqualFact(a) => a.line_file = line_file,
1633 AtomicFact::LessFact(a) => a.line_file = line_file,
1634 AtomicFact::GreaterFact(a) => a.line_file = line_file,
1635 AtomicFact::LessEqualFact(a) => a.line_file = line_file,
1636 AtomicFact::GreaterEqualFact(a) => a.line_file = line_file,
1637 AtomicFact::IsSetFact(a) => a.line_file = line_file,
1638 AtomicFact::IsNonemptySetFact(a) => a.line_file = line_file,
1639 AtomicFact::IsFiniteSetFact(a) => a.line_file = line_file,
1640 AtomicFact::InFact(a) => a.line_file = line_file,
1641 AtomicFact::IsCartFact(a) => a.line_file = line_file,
1642 AtomicFact::IsTupleFact(a) => a.line_file = line_file,
1643 AtomicFact::SubsetFact(a) => a.line_file = line_file,
1644 AtomicFact::SupersetFact(a) => a.line_file = line_file,
1645 AtomicFact::NormalAtomicFact(a) => a.line_file = line_file,
1646 AtomicFact::NotNormalAtomicFact(a) => a.line_file = line_file,
1647 AtomicFact::NotEqualFact(a) => a.line_file = line_file,
1648 AtomicFact::NotLessFact(a) => a.line_file = line_file,
1649 AtomicFact::NotGreaterFact(a) => a.line_file = line_file,
1650 AtomicFact::NotLessEqualFact(a) => a.line_file = line_file,
1651 AtomicFact::NotGreaterEqualFact(a) => a.line_file = line_file,
1652 AtomicFact::NotIsSetFact(a) => a.line_file = line_file,
1653 AtomicFact::NotIsNonemptySetFact(a) => a.line_file = line_file,
1654 AtomicFact::NotIsFiniteSetFact(a) => a.line_file = line_file,
1655 AtomicFact::NotInFact(a) => a.line_file = line_file,
1656 AtomicFact::NotIsCartFact(a) => a.line_file = line_file,
1657 AtomicFact::NotIsTupleFact(a) => a.line_file = line_file,
1658 AtomicFact::NotSubsetFact(a) => a.line_file = line_file,
1659 AtomicFact::NotSupersetFact(a) => a.line_file = line_file,
1660 AtomicFact::RestrictFact(a) => a.line_file = line_file,
1661 AtomicFact::NotRestrictFact(a) => a.line_file = line_file,
1662 AtomicFact::FnEqualInFact(a) => a.line_file = line_file,
1663 AtomicFact::FnEqualFact(a) => a.line_file = line_file,
1664 }
1665 self
1666 }
1667}
1668
1669impl RestrictFact {
1670 pub fn new(obj: Obj, obj_can_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1671 RestrictFact {
1672 obj,
1673 obj_can_restrict_to_fn_set,
1674 line_file,
1675 }
1676 }
1677}
1678
1679impl NotRestrictFact {
1680 pub fn new(obj: Obj, obj_cannot_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1681 NotRestrictFact {
1682 obj,
1683 obj_cannot_restrict_to_fn_set,
1684 line_file,
1685 }
1686 }
1687}
1688
1689impl fmt::Display for RestrictFact {
1690 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1691 write!(
1692 f,
1693 "{} {}{} {}",
1694 self.obj, FACT_PREFIX, RESTRICT_FN_IN, self.obj_can_restrict_to_fn_set
1695 )
1696 }
1697}
1698
1699impl fmt::Display for NotRestrictFact {
1700 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1701 write!(
1702 f,
1703 "{} {} {}{} {}",
1704 NOT, self.obj, FACT_PREFIX, RESTRICT_FN_IN, self.obj_cannot_restrict_to_fn_set
1705 )
1706 }
1707}
1708
1709impl AtomicFact {
1710 pub fn get_args_from_fact(&self) -> Vec<Obj> {
1711 self.args()
1712 }
1713}
1714
1715impl AtomicFact {
1716 pub fn make_reversed(&self) -> AtomicFact {
1717 match self {
1718 AtomicFact::NormalAtomicFact(a) => AtomicFact::NotNormalAtomicFact(
1719 NotNormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1720 ),
1721 AtomicFact::NotNormalAtomicFact(a) => AtomicFact::NormalAtomicFact(
1722 NormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1723 ),
1724 AtomicFact::EqualFact(a) => {
1725 NotEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1726 }
1727 AtomicFact::LessFact(a) => {
1728 NotLessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1729 }
1730 AtomicFact::GreaterFact(a) => {
1731 NotGreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1732 }
1733 AtomicFact::LessEqualFact(a) => {
1734 NotLessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1735 }
1736 AtomicFact::GreaterEqualFact(a) => AtomicFact::NotGreaterEqualFact(
1737 NotGreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1738 ),
1739 AtomicFact::IsSetFact(a) => {
1740 NotIsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1741 }
1742 AtomicFact::IsNonemptySetFact(a) => AtomicFact::NotIsNonemptySetFact(
1743 NotIsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1744 ),
1745 AtomicFact::IsFiniteSetFact(a) => AtomicFact::NotIsFiniteSetFact(
1746 NotIsFiniteSetFact::new(a.set.clone(), a.line_file.clone()),
1747 ),
1748 AtomicFact::InFact(a) => {
1749 NotInFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1750 }
1751 AtomicFact::IsCartFact(a) => {
1752 NotIsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1753 }
1754 AtomicFact::IsTupleFact(a) => {
1755 NotIsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1756 }
1757 AtomicFact::SubsetFact(a) => {
1758 NotSubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1759 }
1760 AtomicFact::SupersetFact(a) => {
1761 NotSupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1762 }
1763 AtomicFact::RestrictFact(a) => NotRestrictFact::new(
1764 a.obj.clone(),
1765 a.obj_can_restrict_to_fn_set.clone(),
1766 a.line_file.clone(),
1767 )
1768 .into(),
1769 AtomicFact::NotEqualFact(a) => {
1770 EqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1771 }
1772 AtomicFact::NotLessFact(a) => {
1773 LessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1774 }
1775 AtomicFact::NotGreaterFact(a) => {
1776 GreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1777 }
1778 AtomicFact::NotLessEqualFact(a) => {
1779 LessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1780 }
1781 AtomicFact::NotGreaterEqualFact(a) => AtomicFact::GreaterEqualFact(
1782 GreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1783 ),
1784 AtomicFact::NotIsSetFact(a) => {
1785 IsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1786 }
1787 AtomicFact::NotIsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1788 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1789 ),
1790 AtomicFact::NotIsFiniteSetFact(a) => {
1791 IsFiniteSetFact::new(a.set.clone(), a.line_file.clone()).into()
1792 }
1793 AtomicFact::NotInFact(a) => {
1794 InFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1795 }
1796 AtomicFact::NotIsCartFact(a) => {
1797 IsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1798 }
1799 AtomicFact::NotIsTupleFact(a) => {
1800 IsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1801 }
1802 AtomicFact::NotSubsetFact(a) => {
1803 SubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1804 }
1805 AtomicFact::NotSupersetFact(a) => {
1806 SupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1807 }
1808 AtomicFact::NotRestrictFact(a) => RestrictFact::new(
1809 a.obj.clone(),
1810 a.obj_cannot_restrict_to_fn_set.clone(),
1811 a.line_file.clone(),
1812 )
1813 .into(),
1814 AtomicFact::FnEqualInFact(a) => FnEqualInFact::new(
1815 a.right.clone(),
1816 a.left.clone(),
1817 a.set.clone(),
1818 a.line_file.clone(),
1819 )
1820 .into(),
1821 AtomicFact::FnEqualFact(a) => {
1822 FnEqualFact::new(a.right.clone(), a.left.clone(), a.line_file.clone()).into()
1823 }
1824 }
1825 }
1826}
1827
1828impl AtomicFact {
1829 fn body_vec_after_calculate_each_calculable_arg(original_body: &Vec<Obj>) -> Vec<Obj> {
1830 let mut next_body = Vec::new();
1831 for obj in original_body {
1832 next_body.push(obj.replace_with_numeric_result_if_can_be_calculated().0);
1833 }
1834 next_body
1835 }
1836
1837 pub fn calculate_args(&self) -> (AtomicFact, bool) {
1838 let calculated_atomic_fact: AtomicFact = match self {
1839 AtomicFact::NormalAtomicFact(inner) => NormalAtomicFact::new(
1840 inner.predicate.clone(),
1841 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1842 inner.line_file.clone(),
1843 )
1844 .into(),
1845 AtomicFact::NotNormalAtomicFact(inner) => NotNormalAtomicFact::new(
1846 inner.predicate.clone(),
1847 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1848 inner.line_file.clone(),
1849 )
1850 .into(),
1851 AtomicFact::EqualFact(inner) => EqualFact::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::NotEqualFact(inner) => NotEqualFact::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::LessFact(inner) => LessFact::new(
1876 inner
1877 .left
1878 .replace_with_numeric_result_if_can_be_calculated()
1879 .0,
1880 inner
1881 .right
1882 .replace_with_numeric_result_if_can_be_calculated()
1883 .0,
1884 inner.line_file.clone(),
1885 )
1886 .into(),
1887 AtomicFact::NotLessFact(inner) => NotLessFact::new(
1888 inner
1889 .left
1890 .replace_with_numeric_result_if_can_be_calculated()
1891 .0,
1892 inner
1893 .right
1894 .replace_with_numeric_result_if_can_be_calculated()
1895 .0,
1896 inner.line_file.clone(),
1897 )
1898 .into(),
1899 AtomicFact::GreaterFact(inner) => GreaterFact::new(
1900 inner
1901 .left
1902 .replace_with_numeric_result_if_can_be_calculated()
1903 .0,
1904 inner
1905 .right
1906 .replace_with_numeric_result_if_can_be_calculated()
1907 .0,
1908 inner.line_file.clone(),
1909 )
1910 .into(),
1911 AtomicFact::NotGreaterFact(inner) => NotGreaterFact::new(
1912 inner
1913 .left
1914 .replace_with_numeric_result_if_can_be_calculated()
1915 .0,
1916 inner
1917 .right
1918 .replace_with_numeric_result_if_can_be_calculated()
1919 .0,
1920 inner.line_file.clone(),
1921 )
1922 .into(),
1923 AtomicFact::LessEqualFact(inner) => LessEqualFact::new(
1924 inner
1925 .left
1926 .replace_with_numeric_result_if_can_be_calculated()
1927 .0,
1928 inner
1929 .right
1930 .replace_with_numeric_result_if_can_be_calculated()
1931 .0,
1932 inner.line_file.clone(),
1933 )
1934 .into(),
1935 AtomicFact::NotLessEqualFact(inner) => NotLessEqualFact::new(
1936 inner
1937 .left
1938 .replace_with_numeric_result_if_can_be_calculated()
1939 .0,
1940 inner
1941 .right
1942 .replace_with_numeric_result_if_can_be_calculated()
1943 .0,
1944 inner.line_file.clone(),
1945 )
1946 .into(),
1947 AtomicFact::GreaterEqualFact(inner) => GreaterEqualFact::new(
1948 inner
1949 .left
1950 .replace_with_numeric_result_if_can_be_calculated()
1951 .0,
1952 inner
1953 .right
1954 .replace_with_numeric_result_if_can_be_calculated()
1955 .0,
1956 inner.line_file.clone(),
1957 )
1958 .into(),
1959 AtomicFact::NotGreaterEqualFact(inner) => NotGreaterEqualFact::new(
1960 inner
1961 .left
1962 .replace_with_numeric_result_if_can_be_calculated()
1963 .0,
1964 inner
1965 .right
1966 .replace_with_numeric_result_if_can_be_calculated()
1967 .0,
1968 inner.line_file.clone(),
1969 )
1970 .into(),
1971 AtomicFact::IsSetFact(inner) => IsSetFact::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::NotIsSetFact(inner) => NotIsSetFact::new(
1980 inner
1981 .set
1982 .replace_with_numeric_result_if_can_be_calculated()
1983 .0,
1984 inner.line_file.clone(),
1985 )
1986 .into(),
1987 AtomicFact::IsNonemptySetFact(inner) => IsNonemptySetFact::new(
1988 inner
1989 .set
1990 .replace_with_numeric_result_if_can_be_calculated()
1991 .0,
1992 inner.line_file.clone(),
1993 )
1994 .into(),
1995 AtomicFact::NotIsNonemptySetFact(inner) => NotIsNonemptySetFact::new(
1996 inner
1997 .set
1998 .replace_with_numeric_result_if_can_be_calculated()
1999 .0,
2000 inner.line_file.clone(),
2001 )
2002 .into(),
2003 AtomicFact::IsFiniteSetFact(inner) => IsFiniteSetFact::new(
2004 inner
2005 .set
2006 .replace_with_numeric_result_if_can_be_calculated()
2007 .0,
2008 inner.line_file.clone(),
2009 )
2010 .into(),
2011 AtomicFact::NotIsFiniteSetFact(inner) => NotIsFiniteSetFact::new(
2012 inner
2013 .set
2014 .replace_with_numeric_result_if_can_be_calculated()
2015 .0,
2016 inner.line_file.clone(),
2017 )
2018 .into(),
2019 AtomicFact::InFact(inner) => InFact::new(
2020 inner
2021 .element
2022 .replace_with_numeric_result_if_can_be_calculated()
2023 .0,
2024 inner
2025 .set
2026 .replace_with_numeric_result_if_can_be_calculated()
2027 .0,
2028 inner.line_file.clone(),
2029 )
2030 .into(),
2031 AtomicFact::NotInFact(inner) => NotInFact::new(
2032 inner
2033 .element
2034 .replace_with_numeric_result_if_can_be_calculated()
2035 .0,
2036 inner
2037 .set
2038 .replace_with_numeric_result_if_can_be_calculated()
2039 .0,
2040 inner.line_file.clone(),
2041 )
2042 .into(),
2043 AtomicFact::IsCartFact(inner) => IsCartFact::new(
2044 inner
2045 .set
2046 .replace_with_numeric_result_if_can_be_calculated()
2047 .0,
2048 inner.line_file.clone(),
2049 )
2050 .into(),
2051 AtomicFact::NotIsCartFact(inner) => NotIsCartFact::new(
2052 inner
2053 .set
2054 .replace_with_numeric_result_if_can_be_calculated()
2055 .0,
2056 inner.line_file.clone(),
2057 )
2058 .into(),
2059 AtomicFact::IsTupleFact(inner) => IsTupleFact::new(
2060 inner
2061 .set
2062 .replace_with_numeric_result_if_can_be_calculated()
2063 .0,
2064 inner.line_file.clone(),
2065 )
2066 .into(),
2067 AtomicFact::NotIsTupleFact(inner) => NotIsTupleFact::new(
2068 inner
2069 .set
2070 .replace_with_numeric_result_if_can_be_calculated()
2071 .0,
2072 inner.line_file.clone(),
2073 )
2074 .into(),
2075 AtomicFact::SubsetFact(inner) => SubsetFact::new(
2076 inner
2077 .left
2078 .replace_with_numeric_result_if_can_be_calculated()
2079 .0,
2080 inner
2081 .right
2082 .replace_with_numeric_result_if_can_be_calculated()
2083 .0,
2084 inner.line_file.clone(),
2085 )
2086 .into(),
2087 AtomicFact::NotSubsetFact(inner) => NotSubsetFact::new(
2088 inner
2089 .left
2090 .replace_with_numeric_result_if_can_be_calculated()
2091 .0,
2092 inner
2093 .right
2094 .replace_with_numeric_result_if_can_be_calculated()
2095 .0,
2096 inner.line_file.clone(),
2097 )
2098 .into(),
2099 AtomicFact::SupersetFact(inner) => SupersetFact::new(
2100 inner
2101 .left
2102 .replace_with_numeric_result_if_can_be_calculated()
2103 .0,
2104 inner
2105 .right
2106 .replace_with_numeric_result_if_can_be_calculated()
2107 .0,
2108 inner.line_file.clone(),
2109 )
2110 .into(),
2111 AtomicFact::NotSupersetFact(inner) => NotSupersetFact::new(
2112 inner
2113 .left
2114 .replace_with_numeric_result_if_can_be_calculated()
2115 .0,
2116 inner
2117 .right
2118 .replace_with_numeric_result_if_can_be_calculated()
2119 .0,
2120 inner.line_file.clone(),
2121 )
2122 .into(),
2123 AtomicFact::RestrictFact(inner) => RestrictFact::new(
2124 inner
2125 .obj
2126 .replace_with_numeric_result_if_can_be_calculated()
2127 .0,
2128 inner
2129 .obj_can_restrict_to_fn_set
2130 .replace_with_numeric_result_if_can_be_calculated()
2131 .0,
2132 inner.line_file.clone(),
2133 )
2134 .into(),
2135 AtomicFact::NotRestrictFact(inner) => NotRestrictFact::new(
2136 inner
2137 .obj
2138 .replace_with_numeric_result_if_can_be_calculated()
2139 .0,
2140 inner
2141 .obj_cannot_restrict_to_fn_set
2142 .replace_with_numeric_result_if_can_be_calculated()
2143 .0,
2144 inner.line_file.clone(),
2145 )
2146 .into(),
2147 AtomicFact::FnEqualInFact(inner) => FnEqualInFact::new(
2148 inner
2149 .left
2150 .replace_with_numeric_result_if_can_be_calculated()
2151 .0,
2152 inner
2153 .right
2154 .replace_with_numeric_result_if_can_be_calculated()
2155 .0,
2156 inner
2157 .set
2158 .replace_with_numeric_result_if_can_be_calculated()
2159 .0,
2160 inner.line_file.clone(),
2161 )
2162 .into(),
2163 AtomicFact::FnEqualFact(inner) => FnEqualFact::new(
2164 inner
2165 .left
2166 .replace_with_numeric_result_if_can_be_calculated()
2167 .0,
2168 inner
2169 .right
2170 .replace_with_numeric_result_if_can_be_calculated()
2171 .0,
2172 inner.line_file.clone(),
2173 )
2174 .into(),
2175 };
2176 let any_argument_replaced = calculated_atomic_fact.to_string() != self.to_string();
2177 (calculated_atomic_fact, any_argument_replaced)
2178 }
2179}
2180
2181impl From<NormalAtomicFact> for AtomicFact {
2182 fn from(f: NormalAtomicFact) -> Self {
2183 AtomicFact::NormalAtomicFact(f)
2184 }
2185}
2186
2187impl From<EqualFact> for AtomicFact {
2188 fn from(f: EqualFact) -> Self {
2189 AtomicFact::EqualFact(f)
2190 }
2191}
2192
2193impl From<LessFact> for AtomicFact {
2194 fn from(f: LessFact) -> Self {
2195 AtomicFact::LessFact(f)
2196 }
2197}
2198
2199impl From<GreaterFact> for AtomicFact {
2200 fn from(f: GreaterFact) -> Self {
2201 AtomicFact::GreaterFact(f)
2202 }
2203}
2204
2205impl From<LessEqualFact> for AtomicFact {
2206 fn from(f: LessEqualFact) -> Self {
2207 AtomicFact::LessEqualFact(f)
2208 }
2209}
2210
2211impl From<GreaterEqualFact> for AtomicFact {
2212 fn from(f: GreaterEqualFact) -> Self {
2213 AtomicFact::GreaterEqualFact(f)
2214 }
2215}
2216
2217impl From<IsSetFact> for AtomicFact {
2218 fn from(f: IsSetFact) -> Self {
2219 AtomicFact::IsSetFact(f)
2220 }
2221}
2222
2223impl From<IsNonemptySetFact> for AtomicFact {
2224 fn from(f: IsNonemptySetFact) -> Self {
2225 AtomicFact::IsNonemptySetFact(f)
2226 }
2227}
2228
2229impl From<IsFiniteSetFact> for AtomicFact {
2230 fn from(f: IsFiniteSetFact) -> Self {
2231 AtomicFact::IsFiniteSetFact(f)
2232 }
2233}
2234
2235impl From<InFact> for AtomicFact {
2236 fn from(f: InFact) -> Self {
2237 AtomicFact::InFact(f)
2238 }
2239}
2240
2241impl From<IsCartFact> for AtomicFact {
2242 fn from(f: IsCartFact) -> Self {
2243 AtomicFact::IsCartFact(f)
2244 }
2245}
2246
2247impl From<IsTupleFact> for AtomicFact {
2248 fn from(f: IsTupleFact) -> Self {
2249 AtomicFact::IsTupleFact(f)
2250 }
2251}
2252
2253impl From<SubsetFact> for AtomicFact {
2254 fn from(f: SubsetFact) -> Self {
2255 AtomicFact::SubsetFact(f)
2256 }
2257}
2258
2259impl From<SupersetFact> for AtomicFact {
2260 fn from(f: SupersetFact) -> Self {
2261 AtomicFact::SupersetFact(f)
2262 }
2263}
2264
2265impl From<RestrictFact> for AtomicFact {
2266 fn from(f: RestrictFact) -> Self {
2267 AtomicFact::RestrictFact(f)
2268 }
2269}
2270
2271impl From<NotRestrictFact> for AtomicFact {
2272 fn from(f: NotRestrictFact) -> Self {
2273 AtomicFact::NotRestrictFact(f)
2274 }
2275}
2276
2277impl From<NotNormalAtomicFact> for AtomicFact {
2278 fn from(f: NotNormalAtomicFact) -> Self {
2279 AtomicFact::NotNormalAtomicFact(f)
2280 }
2281}
2282
2283impl From<NotEqualFact> for AtomicFact {
2284 fn from(f: NotEqualFact) -> Self {
2285 AtomicFact::NotEqualFact(f)
2286 }
2287}
2288
2289impl From<NotLessFact> for AtomicFact {
2290 fn from(f: NotLessFact) -> Self {
2291 AtomicFact::NotLessFact(f)
2292 }
2293}
2294
2295impl From<NotGreaterFact> for AtomicFact {
2296 fn from(f: NotGreaterFact) -> Self {
2297 AtomicFact::NotGreaterFact(f)
2298 }
2299}
2300
2301impl From<NotLessEqualFact> for AtomicFact {
2302 fn from(f: NotLessEqualFact) -> Self {
2303 AtomicFact::NotLessEqualFact(f)
2304 }
2305}
2306
2307impl From<NotGreaterEqualFact> for AtomicFact {
2308 fn from(f: NotGreaterEqualFact) -> Self {
2309 AtomicFact::NotGreaterEqualFact(f)
2310 }
2311}
2312
2313impl From<NotIsSetFact> for AtomicFact {
2314 fn from(f: NotIsSetFact) -> Self {
2315 AtomicFact::NotIsSetFact(f)
2316 }
2317}
2318
2319impl From<NotIsNonemptySetFact> for AtomicFact {
2320 fn from(f: NotIsNonemptySetFact) -> Self {
2321 AtomicFact::NotIsNonemptySetFact(f)
2322 }
2323}
2324
2325impl From<NotIsFiniteSetFact> for AtomicFact {
2326 fn from(f: NotIsFiniteSetFact) -> Self {
2327 AtomicFact::NotIsFiniteSetFact(f)
2328 }
2329}
2330
2331impl From<NotInFact> for AtomicFact {
2332 fn from(f: NotInFact) -> Self {
2333 AtomicFact::NotInFact(f)
2334 }
2335}
2336
2337impl From<NotIsCartFact> for AtomicFact {
2338 fn from(f: NotIsCartFact) -> Self {
2339 AtomicFact::NotIsCartFact(f)
2340 }
2341}
2342
2343impl From<NotIsTupleFact> for AtomicFact {
2344 fn from(f: NotIsTupleFact) -> Self {
2345 AtomicFact::NotIsTupleFact(f)
2346 }
2347}
2348
2349impl From<NotSubsetFact> for AtomicFact {
2350 fn from(f: NotSubsetFact) -> Self {
2351 AtomicFact::NotSubsetFact(f)
2352 }
2353}
2354
2355impl From<NotSupersetFact> for AtomicFact {
2356 fn from(f: NotSupersetFact) -> Self {
2357 AtomicFact::NotSupersetFact(f)
2358 }
2359}
2360
2361impl From<FnEqualInFact> for AtomicFact {
2362 fn from(f: FnEqualInFact) -> Self {
2363 AtomicFact::FnEqualInFact(f)
2364 }
2365}
2366
2367impl From<FnEqualFact> for AtomicFact {
2368 fn from(f: FnEqualFact) -> Self {
2369 AtomicFact::FnEqualFact(f)
2370 }
2371}
2372
2373impl From<NormalAtomicFact> for Fact {
2374 fn from(f: NormalAtomicFact) -> Self {
2375 Fact::AtomicFact(f.into())
2376 }
2377}
2378
2379impl From<EqualFact> for Fact {
2380 fn from(f: EqualFact) -> Self {
2381 Fact::AtomicFact(f.into())
2382 }
2383}
2384
2385impl From<LessFact> for Fact {
2386 fn from(f: LessFact) -> Self {
2387 Fact::AtomicFact(f.into())
2388 }
2389}
2390
2391impl From<GreaterFact> for Fact {
2392 fn from(f: GreaterFact) -> Self {
2393 Fact::AtomicFact(f.into())
2394 }
2395}
2396
2397impl From<LessEqualFact> for Fact {
2398 fn from(f: LessEqualFact) -> Self {
2399 Fact::AtomicFact(f.into())
2400 }
2401}
2402
2403impl From<GreaterEqualFact> for Fact {
2404 fn from(f: GreaterEqualFact) -> Self {
2405 Fact::AtomicFact(f.into())
2406 }
2407}
2408
2409impl From<IsSetFact> for Fact {
2410 fn from(f: IsSetFact) -> Self {
2411 Fact::AtomicFact(f.into())
2412 }
2413}
2414
2415impl From<IsNonemptySetFact> for Fact {
2416 fn from(f: IsNonemptySetFact) -> Self {
2417 Fact::AtomicFact(f.into())
2418 }
2419}
2420
2421impl From<IsFiniteSetFact> for Fact {
2422 fn from(f: IsFiniteSetFact) -> Self {
2423 Fact::AtomicFact(f.into())
2424 }
2425}
2426
2427impl From<InFact> for Fact {
2428 fn from(f: InFact) -> Self {
2429 Fact::AtomicFact(f.into())
2430 }
2431}
2432
2433impl From<IsCartFact> for Fact {
2434 fn from(f: IsCartFact) -> Self {
2435 Fact::AtomicFact(f.into())
2436 }
2437}
2438
2439impl From<IsTupleFact> for Fact {
2440 fn from(f: IsTupleFact) -> Self {
2441 Fact::AtomicFact(f.into())
2442 }
2443}
2444
2445impl From<SubsetFact> for Fact {
2446 fn from(f: SubsetFact) -> Self {
2447 Fact::AtomicFact(f.into())
2448 }
2449}
2450
2451impl From<SupersetFact> for Fact {
2452 fn from(f: SupersetFact) -> Self {
2453 Fact::AtomicFact(f.into())
2454 }
2455}
2456
2457impl From<RestrictFact> for Fact {
2458 fn from(f: RestrictFact) -> Self {
2459 Fact::AtomicFact(f.into())
2460 }
2461}
2462
2463impl From<NotRestrictFact> for Fact {
2464 fn from(f: NotRestrictFact) -> Self {
2465 Fact::AtomicFact(f.into())
2466 }
2467}
2468
2469impl From<FnEqualInFact> for Fact {
2470 fn from(f: FnEqualInFact) -> Self {
2471 Fact::AtomicFact(f.into())
2472 }
2473}
2474
2475impl From<FnEqualFact> for Fact {
2476 fn from(f: FnEqualFact) -> Self {
2477 Fact::AtomicFact(f.into())
2478 }
2479}
2480
2481impl From<NotNormalAtomicFact> for Fact {
2482 fn from(f: NotNormalAtomicFact) -> Self {
2483 Fact::AtomicFact(f.into())
2484 }
2485}
2486
2487impl From<NotEqualFact> for Fact {
2488 fn from(f: NotEqualFact) -> Self {
2489 Fact::AtomicFact(f.into())
2490 }
2491}
2492
2493impl From<NotLessFact> for Fact {
2494 fn from(f: NotLessFact) -> Self {
2495 Fact::AtomicFact(f.into())
2496 }
2497}
2498
2499impl From<NotGreaterFact> for Fact {
2500 fn from(f: NotGreaterFact) -> Self {
2501 Fact::AtomicFact(f.into())
2502 }
2503}
2504
2505impl From<NotLessEqualFact> for Fact {
2506 fn from(f: NotLessEqualFact) -> Self {
2507 Fact::AtomicFact(f.into())
2508 }
2509}
2510
2511impl From<NotGreaterEqualFact> for Fact {
2512 fn from(f: NotGreaterEqualFact) -> Self {
2513 Fact::AtomicFact(f.into())
2514 }
2515}
2516
2517impl From<NotIsSetFact> for Fact {
2518 fn from(f: NotIsSetFact) -> Self {
2519 Fact::AtomicFact(f.into())
2520 }
2521}
2522
2523impl From<NotIsNonemptySetFact> for Fact {
2524 fn from(f: NotIsNonemptySetFact) -> Self {
2525 Fact::AtomicFact(f.into())
2526 }
2527}
2528
2529impl From<NotIsFiniteSetFact> for Fact {
2530 fn from(f: NotIsFiniteSetFact) -> Self {
2531 Fact::AtomicFact(f.into())
2532 }
2533}
2534
2535impl From<NotInFact> for Fact {
2536 fn from(f: NotInFact) -> Self {
2537 Fact::AtomicFact(f.into())
2538 }
2539}
2540
2541impl From<NotIsCartFact> for Fact {
2542 fn from(f: NotIsCartFact) -> Self {
2543 Fact::AtomicFact(f.into())
2544 }
2545}
2546
2547impl From<NotIsTupleFact> for Fact {
2548 fn from(f: NotIsTupleFact) -> Self {
2549 Fact::AtomicFact(f.into())
2550 }
2551}
2552
2553impl From<NotSubsetFact> for Fact {
2554 fn from(f: NotSubsetFact) -> Self {
2555 Fact::AtomicFact(f.into())
2556 }
2557}
2558
2559impl From<NotSupersetFact> for Fact {
2560 fn from(f: NotSupersetFact) -> Self {
2561 Fact::AtomicFact(f.into())
2562 }
2563}