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