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.to_string(),
980 AtomicFact::NotRestrictFact(_) => RESTRICT.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 => {
1329 if args.len() != 2 {
1330 let msg = format!("{} requires 2 arguments, but got {}", RESTRICT, args.len());
1331 return Err(NewAtomicFactRuntimeError(
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(RestrictFact::new(a0, a1, line_file).into())
1341 } else {
1342 Ok(NotRestrictFact::new(a0, a1, line_file).into())
1343 }
1344 }
1345 FN_EQ_IN => {
1346 if !is_true {
1347 let msg = format!("{} does not support `not`", FN_EQ_IN);
1348 return Err(NewAtomicFactRuntimeError(
1349 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1350 )
1351 .into());
1352 }
1353 if args.len() != 3 {
1354 let msg = format!(
1355 "{} requires 3 arguments (f, g, set), but got {}",
1356 FN_EQ_IN,
1357 args.len()
1358 );
1359 return Err(NewAtomicFactRuntimeError(
1360 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1361 )
1362 .into());
1363 }
1364 let mut args = args;
1365 let a0 = args.remove(0);
1366 let a1 = args.remove(0);
1367 let a2 = args.remove(0);
1368 Ok(FnEqualInFact::new(a0, a1, a2, line_file).into())
1369 }
1370 FN_EQ => {
1371 if !is_true {
1372 let msg = format!("{} does not support `not`", FN_EQ);
1373 return Err(NewAtomicFactRuntimeError(
1374 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1375 )
1376 .into());
1377 }
1378 if args.len() != 2 {
1379 let msg = format!(
1380 "{} requires 2 arguments (f, g), but got {}",
1381 FN_EQ,
1382 args.len()
1383 );
1384 return Err(NewAtomicFactRuntimeError(
1385 RuntimeErrorStruct::new_with_msg_and_line_file(msg, line_file.clone()),
1386 )
1387 .into());
1388 }
1389 let mut args = args;
1390 let a0 = args.remove(0);
1391 let a1 = args.remove(0);
1392 Ok(FnEqualFact::new(a0, a1, line_file).into())
1393 }
1394 _ => {
1395 if is_true {
1396 Ok(NormalAtomicFact::new(prop_name, args, line_file).into())
1397 } else {
1398 Ok(NotNormalAtomicFact::new(prop_name, args, line_file).into())
1399 }
1400 }
1401 }
1402 }
1403}
1404
1405impl AtomicFact {
1406 pub fn args(&self) -> Vec<Obj> {
1407 match self {
1408 AtomicFact::NormalAtomicFact(normal_atomic_fact) => normal_atomic_fact.body.clone(),
1409 AtomicFact::EqualFact(equal_fact) => {
1410 vec![equal_fact.left.clone(), equal_fact.right.clone()]
1411 }
1412 AtomicFact::LessFact(less_fact) => {
1413 vec![less_fact.left.clone(), less_fact.right.clone()]
1414 }
1415 AtomicFact::GreaterFact(greater_fact) => {
1416 vec![greater_fact.left.clone(), greater_fact.right.clone()]
1417 }
1418 AtomicFact::LessEqualFact(less_equal_fact) => {
1419 vec![less_equal_fact.left.clone(), less_equal_fact.right.clone()]
1420 }
1421 AtomicFact::GreaterEqualFact(greater_equal_fact) => vec![
1422 greater_equal_fact.left.clone(),
1423 greater_equal_fact.right.clone(),
1424 ],
1425 AtomicFact::IsSetFact(is_set_fact) => vec![is_set_fact.set.clone()],
1426 AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => {
1427 vec![is_nonempty_set_fact.set.clone()]
1428 }
1429 AtomicFact::IsFiniteSetFact(is_finite_set_fact) => vec![is_finite_set_fact.set.clone()],
1430 AtomicFact::InFact(in_fact) => vec![in_fact.element.clone(), in_fact.set.clone()],
1431 AtomicFact::IsCartFact(is_cart_fact) => vec![is_cart_fact.set.clone()],
1432 AtomicFact::IsTupleFact(is_tuple_fact) => vec![is_tuple_fact.set.clone()],
1433 AtomicFact::SubsetFact(subset_fact) => {
1434 vec![subset_fact.left.clone(), subset_fact.right.clone()]
1435 }
1436 AtomicFact::SupersetFact(superset_fact) => {
1437 vec![superset_fact.left.clone(), superset_fact.right.clone()]
1438 }
1439 AtomicFact::NotNormalAtomicFact(not_normal_atomic_fact) => {
1440 not_normal_atomic_fact.body.clone()
1441 }
1442 AtomicFact::NotEqualFact(not_equal_fact) => {
1443 vec![not_equal_fact.left.clone(), not_equal_fact.right.clone()]
1444 }
1445 AtomicFact::NotLessFact(not_less_fact) => {
1446 vec![not_less_fact.left.clone(), not_less_fact.right.clone()]
1447 }
1448 AtomicFact::NotGreaterFact(not_greater_fact) => vec![
1449 not_greater_fact.left.clone(),
1450 not_greater_fact.right.clone(),
1451 ],
1452 AtomicFact::NotLessEqualFact(not_less_equal_fact) => vec![
1453 not_less_equal_fact.left.clone(),
1454 not_less_equal_fact.right.clone(),
1455 ],
1456 AtomicFact::NotGreaterEqualFact(not_greater_equal_fact) => vec![
1457 not_greater_equal_fact.left.clone(),
1458 not_greater_equal_fact.right.clone(),
1459 ],
1460 AtomicFact::NotIsSetFact(not_is_set_fact) => vec![not_is_set_fact.set.clone()],
1461 AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => {
1462 vec![not_is_nonempty_set_fact.set.clone()]
1463 }
1464 AtomicFact::NotIsFiniteSetFact(not_is_finite_set_fact) => {
1465 vec![not_is_finite_set_fact.set.clone()]
1466 }
1467 AtomicFact::NotInFact(not_in_fact) => {
1468 vec![not_in_fact.element.clone(), not_in_fact.set.clone()]
1469 }
1470 AtomicFact::NotIsCartFact(not_is_cart_fact) => vec![not_is_cart_fact.set.clone()],
1471 AtomicFact::NotIsTupleFact(not_is_tuple_fact) => vec![not_is_tuple_fact.set.clone()],
1472 AtomicFact::NotSubsetFact(not_subset_fact) => {
1473 vec![not_subset_fact.left.clone(), not_subset_fact.right.clone()]
1474 }
1475 AtomicFact::NotSupersetFact(not_superset_fact) => vec![
1476 not_superset_fact.left.clone(),
1477 not_superset_fact.right.clone(),
1478 ],
1479 AtomicFact::RestrictFact(restrict_fact) => vec![
1480 restrict_fact.obj.clone(),
1481 restrict_fact.obj_can_restrict_to_fn_set.clone().into(),
1482 ],
1483 AtomicFact::NotRestrictFact(not_restrict_fact) => vec![
1484 not_restrict_fact.obj.clone(),
1485 not_restrict_fact.obj_cannot_restrict_to_fn_set.clone(),
1486 ],
1487 AtomicFact::FnEqualInFact(f) => {
1488 vec![f.left.clone(), f.right.clone(), f.set.clone()]
1489 }
1490 AtomicFact::FnEqualFact(f) => vec![f.left.clone(), f.right.clone()],
1491 }
1492 }
1493}
1494
1495impl AtomicFact {
1497 pub fn is_builtin_predicate_and_return_expected_args_len(&self) -> usize {
1498 match self {
1499 AtomicFact::EqualFact(_) => 2,
1500 AtomicFact::LessFact(_) => 2,
1501 AtomicFact::GreaterFact(_) => 2,
1502 AtomicFact::LessEqualFact(_) => 2,
1503 AtomicFact::GreaterEqualFact(_) => 2,
1504 AtomicFact::IsSetFact(_) => 1,
1505 AtomicFact::IsNonemptySetFact(_) => 1,
1506 AtomicFact::IsFiniteSetFact(_) => 1,
1507 AtomicFact::InFact(_) => 2,
1508 AtomicFact::IsCartFact(_) => 1,
1509 AtomicFact::IsTupleFact(_) => 1,
1510 AtomicFact::SubsetFact(_) => 2,
1511 AtomicFact::SupersetFact(_) => 2,
1512 AtomicFact::NotEqualFact(_) => 2,
1513 AtomicFact::NotLessFact(_) => 2,
1514 AtomicFact::NotGreaterFact(_) => 2,
1515 AtomicFact::NotLessEqualFact(_) => 2,
1516 AtomicFact::NotGreaterEqualFact(_) => 2,
1517 AtomicFact::NotIsSetFact(_) => 1,
1518 AtomicFact::NotIsNonemptySetFact(_) => 1,
1519 AtomicFact::NotIsFiniteSetFact(_) => 1,
1520 AtomicFact::NotInFact(_) => 2,
1521 AtomicFact::NotIsCartFact(_) => 1,
1522 AtomicFact::NotIsTupleFact(_) => 1,
1523 AtomicFact::NotSubsetFact(_) => 2,
1524 AtomicFact::NotSupersetFact(_) => 2,
1525 AtomicFact::RestrictFact(_) => 2,
1526 AtomicFact::NotRestrictFact(_) => 2,
1527 AtomicFact::FnEqualInFact(_) => 3,
1528 AtomicFact::FnEqualFact(_) => 2,
1529 _ => unreachable!("其他情况不是builtin predicate"),
1530 }
1531 }
1532}
1533
1534impl AtomicFact {
1535 pub fn number_of_args(&self) -> usize {
1536 match self {
1537 AtomicFact::EqualFact(_) => 2,
1538 AtomicFact::LessFact(_) => 2,
1539 AtomicFact::GreaterFact(_) => 2,
1540 AtomicFact::LessEqualFact(_) => 2,
1541 AtomicFact::GreaterEqualFact(_) => 2,
1542 AtomicFact::IsSetFact(_) => 1,
1543 AtomicFact::IsNonemptySetFact(_) => 1,
1544 AtomicFact::IsFiniteSetFact(_) => 1,
1545 AtomicFact::InFact(_) => 2,
1546 AtomicFact::IsCartFact(_) => 1,
1547 AtomicFact::IsTupleFact(_) => 1,
1548 AtomicFact::SubsetFact(_) => 2,
1549 AtomicFact::SupersetFact(_) => 2,
1550 AtomicFact::NotEqualFact(_) => 2,
1551 AtomicFact::NotLessFact(_) => 2,
1552 AtomicFact::NotGreaterFact(_) => 2,
1553 AtomicFact::NotLessEqualFact(_) => 2,
1554 AtomicFact::NotGreaterEqualFact(_) => 2,
1555 AtomicFact::NotIsSetFact(_) => 1,
1556 AtomicFact::NotIsNonemptySetFact(_) => 1,
1557 AtomicFact::NotIsFiniteSetFact(_) => 1,
1558 AtomicFact::NotInFact(_) => 2,
1559 AtomicFact::NotIsCartFact(_) => 1,
1560 AtomicFact::NotIsTupleFact(_) => 1,
1561 AtomicFact::NotSubsetFact(_) => 2,
1562 AtomicFact::NotSupersetFact(_) => 2,
1563 AtomicFact::NormalAtomicFact(a) => a.body.len(),
1564 AtomicFact::NotNormalAtomicFact(a) => a.body.len(),
1565 AtomicFact::RestrictFact(_) => 2,
1566 AtomicFact::NotRestrictFact(_) => 2,
1567 AtomicFact::FnEqualInFact(_) => 3,
1568 AtomicFact::FnEqualFact(_) => 2,
1569 }
1570 }
1571
1572 pub fn line_file(&self) -> LineFile {
1573 match self {
1574 AtomicFact::EqualFact(a) => a.line_file.clone(),
1575 AtomicFact::LessFact(a) => a.line_file.clone(),
1576 AtomicFact::GreaterFact(a) => a.line_file.clone(),
1577 AtomicFact::LessEqualFact(a) => a.line_file.clone(),
1578 AtomicFact::GreaterEqualFact(a) => a.line_file.clone(),
1579 AtomicFact::IsSetFact(a) => a.line_file.clone(),
1580 AtomicFact::IsNonemptySetFact(a) => a.line_file.clone(),
1581 AtomicFact::IsFiniteSetFact(a) => a.line_file.clone(),
1582 AtomicFact::InFact(a) => a.line_file.clone(),
1583 AtomicFact::IsCartFact(a) => a.line_file.clone(),
1584 AtomicFact::IsTupleFact(a) => a.line_file.clone(),
1585 AtomicFact::SubsetFact(a) => a.line_file.clone(),
1586 AtomicFact::SupersetFact(a) => a.line_file.clone(),
1587 AtomicFact::NormalAtomicFact(a) => a.line_file.clone(),
1588 AtomicFact::NotNormalAtomicFact(a) => a.line_file.clone(),
1589 AtomicFact::NotEqualFact(a) => a.line_file.clone(),
1590 AtomicFact::NotLessFact(a) => a.line_file.clone(),
1591 AtomicFact::NotGreaterFact(a) => a.line_file.clone(),
1592 AtomicFact::NotLessEqualFact(a) => a.line_file.clone(),
1593 AtomicFact::NotGreaterEqualFact(a) => a.line_file.clone(),
1594 AtomicFact::NotIsSetFact(a) => a.line_file.clone(),
1595 AtomicFact::NotIsNonemptySetFact(a) => a.line_file.clone(),
1596 AtomicFact::NotIsFiniteSetFact(a) => a.line_file.clone(),
1597 AtomicFact::NotInFact(a) => a.line_file.clone(),
1598 AtomicFact::NotIsCartFact(a) => a.line_file.clone(),
1599 AtomicFact::NotIsTupleFact(a) => a.line_file.clone(),
1600 AtomicFact::NotSubsetFact(a) => a.line_file.clone(),
1601 AtomicFact::NotSupersetFact(a) => a.line_file.clone(),
1602 AtomicFact::RestrictFact(a) => a.line_file.clone(),
1603 AtomicFact::NotRestrictFact(a) => a.line_file.clone(),
1604 AtomicFact::FnEqualInFact(a) => a.line_file.clone(),
1605 AtomicFact::FnEqualFact(a) => a.line_file.clone(),
1606 }
1607 }
1608}
1609
1610impl RestrictFact {
1611 pub fn new(obj: Obj, obj_can_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1612 RestrictFact {
1613 obj,
1614 obj_can_restrict_to_fn_set,
1615 line_file,
1616 }
1617 }
1618}
1619
1620impl NotRestrictFact {
1621 pub fn new(obj: Obj, obj_cannot_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1622 NotRestrictFact {
1623 obj,
1624 obj_cannot_restrict_to_fn_set,
1625 line_file,
1626 }
1627 }
1628}
1629
1630impl fmt::Display for RestrictFact {
1631 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1632 write!(
1633 f,
1634 "{} {}{} {}",
1635 self.obj, FACT_PREFIX, RESTRICT, self.obj_can_restrict_to_fn_set
1636 )
1637 }
1638}
1639
1640impl fmt::Display for NotRestrictFact {
1641 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1642 write!(
1643 f,
1644 "{} {} {}{} {}",
1645 NOT, self.obj, FACT_PREFIX, RESTRICT, self.obj_cannot_restrict_to_fn_set
1646 )
1647 }
1648}
1649
1650impl AtomicFact {
1651 pub fn get_args_from_fact(&self) -> Vec<Obj> {
1652 self.args()
1653 }
1654}
1655
1656impl AtomicFact {
1657 pub fn make_reversed(&self) -> AtomicFact {
1658 match self {
1659 AtomicFact::NormalAtomicFact(a) => AtomicFact::NotNormalAtomicFact(
1660 NotNormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1661 ),
1662 AtomicFact::NotNormalAtomicFact(a) => AtomicFact::NormalAtomicFact(
1663 NormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1664 ),
1665 AtomicFact::EqualFact(a) => {
1666 NotEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1667 }
1668 AtomicFact::LessFact(a) => {
1669 NotLessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1670 }
1671 AtomicFact::GreaterFact(a) => {
1672 NotGreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1673 }
1674 AtomicFact::LessEqualFact(a) => {
1675 NotLessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1676 }
1677 AtomicFact::GreaterEqualFact(a) => AtomicFact::NotGreaterEqualFact(
1678 NotGreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1679 ),
1680 AtomicFact::IsSetFact(a) => {
1681 NotIsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1682 }
1683 AtomicFact::IsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1684 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1685 ),
1686 AtomicFact::IsFiniteSetFact(a) => AtomicFact::NotIsFiniteSetFact(
1687 NotIsFiniteSetFact::new(a.set.clone(), a.line_file.clone()),
1688 ),
1689 AtomicFact::InFact(a) => {
1690 NotInFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1691 }
1692 AtomicFact::IsCartFact(a) => {
1693 NotIsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1694 }
1695 AtomicFact::IsTupleFact(a) => {
1696 NotIsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1697 }
1698 AtomicFact::SubsetFact(a) => {
1699 NotSubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1700 }
1701 AtomicFact::SupersetFact(a) => {
1702 NotSupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1703 }
1704 AtomicFact::RestrictFact(a) => NotRestrictFact::new(
1705 a.obj.clone(),
1706 a.obj_can_restrict_to_fn_set.clone(),
1707 a.line_file.clone(),
1708 )
1709 .into(),
1710 AtomicFact::NotEqualFact(a) => {
1711 EqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1712 }
1713 AtomicFact::NotLessFact(a) => {
1714 LessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1715 }
1716 AtomicFact::NotGreaterFact(a) => {
1717 GreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1718 }
1719 AtomicFact::NotLessEqualFact(a) => {
1720 LessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1721 }
1722 AtomicFact::NotGreaterEqualFact(a) => AtomicFact::GreaterEqualFact(
1723 GreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1724 ),
1725 AtomicFact::NotIsSetFact(a) => {
1726 IsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1727 }
1728 AtomicFact::NotIsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1729 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1730 ),
1731 AtomicFact::NotIsFiniteSetFact(a) => {
1732 IsFiniteSetFact::new(a.set.clone(), a.line_file.clone()).into()
1733 }
1734 AtomicFact::NotInFact(a) => {
1735 InFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1736 }
1737 AtomicFact::NotIsCartFact(a) => {
1738 IsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1739 }
1740 AtomicFact::NotIsTupleFact(a) => {
1741 IsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1742 }
1743 AtomicFact::NotSubsetFact(a) => {
1744 SubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1745 }
1746 AtomicFact::NotSupersetFact(a) => {
1747 SupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1748 }
1749 AtomicFact::NotRestrictFact(a) => RestrictFact::new(
1750 a.obj.clone(),
1751 a.obj_cannot_restrict_to_fn_set.clone(),
1752 a.line_file.clone(),
1753 )
1754 .into(),
1755 AtomicFact::FnEqualInFact(a) => FnEqualInFact::new(
1756 a.right.clone(),
1757 a.left.clone(),
1758 a.set.clone(),
1759 a.line_file.clone(),
1760 )
1761 .into(),
1762 AtomicFact::FnEqualFact(a) => {
1763 FnEqualFact::new(a.right.clone(), a.left.clone(), a.line_file.clone()).into()
1764 }
1765 }
1766 }
1767}
1768
1769impl AtomicFact {
1770 fn body_vec_after_calculate_each_calculable_arg(original_body: &Vec<Obj>) -> Vec<Obj> {
1771 let mut next_body = Vec::new();
1772 for obj in original_body {
1773 next_body.push(obj.replace_with_numeric_result_if_can_be_calculated().0);
1774 }
1775 next_body
1776 }
1777
1778 pub fn calculate_args(&self) -> (AtomicFact, bool) {
1779 let calculated_atomic_fact: AtomicFact = match self {
1780 AtomicFact::NormalAtomicFact(inner) => NormalAtomicFact::new(
1781 inner.predicate.clone(),
1782 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1783 inner.line_file.clone(),
1784 )
1785 .into(),
1786 AtomicFact::NotNormalAtomicFact(inner) => NotNormalAtomicFact::new(
1787 inner.predicate.clone(),
1788 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1789 inner.line_file.clone(),
1790 )
1791 .into(),
1792 AtomicFact::EqualFact(inner) => EqualFact::new(
1793 inner
1794 .left
1795 .replace_with_numeric_result_if_can_be_calculated()
1796 .0,
1797 inner
1798 .right
1799 .replace_with_numeric_result_if_can_be_calculated()
1800 .0,
1801 inner.line_file.clone(),
1802 )
1803 .into(),
1804 AtomicFact::NotEqualFact(inner) => NotEqualFact::new(
1805 inner
1806 .left
1807 .replace_with_numeric_result_if_can_be_calculated()
1808 .0,
1809 inner
1810 .right
1811 .replace_with_numeric_result_if_can_be_calculated()
1812 .0,
1813 inner.line_file.clone(),
1814 )
1815 .into(),
1816 AtomicFact::LessFact(inner) => LessFact::new(
1817 inner
1818 .left
1819 .replace_with_numeric_result_if_can_be_calculated()
1820 .0,
1821 inner
1822 .right
1823 .replace_with_numeric_result_if_can_be_calculated()
1824 .0,
1825 inner.line_file.clone(),
1826 )
1827 .into(),
1828 AtomicFact::NotLessFact(inner) => NotLessFact::new(
1829 inner
1830 .left
1831 .replace_with_numeric_result_if_can_be_calculated()
1832 .0,
1833 inner
1834 .right
1835 .replace_with_numeric_result_if_can_be_calculated()
1836 .0,
1837 inner.line_file.clone(),
1838 )
1839 .into(),
1840 AtomicFact::GreaterFact(inner) => GreaterFact::new(
1841 inner
1842 .left
1843 .replace_with_numeric_result_if_can_be_calculated()
1844 .0,
1845 inner
1846 .right
1847 .replace_with_numeric_result_if_can_be_calculated()
1848 .0,
1849 inner.line_file.clone(),
1850 )
1851 .into(),
1852 AtomicFact::NotGreaterFact(inner) => NotGreaterFact::new(
1853 inner
1854 .left
1855 .replace_with_numeric_result_if_can_be_calculated()
1856 .0,
1857 inner
1858 .right
1859 .replace_with_numeric_result_if_can_be_calculated()
1860 .0,
1861 inner.line_file.clone(),
1862 )
1863 .into(),
1864 AtomicFact::LessEqualFact(inner) => LessEqualFact::new(
1865 inner
1866 .left
1867 .replace_with_numeric_result_if_can_be_calculated()
1868 .0,
1869 inner
1870 .right
1871 .replace_with_numeric_result_if_can_be_calculated()
1872 .0,
1873 inner.line_file.clone(),
1874 )
1875 .into(),
1876 AtomicFact::NotLessEqualFact(inner) => NotLessEqualFact::new(
1877 inner
1878 .left
1879 .replace_with_numeric_result_if_can_be_calculated()
1880 .0,
1881 inner
1882 .right
1883 .replace_with_numeric_result_if_can_be_calculated()
1884 .0,
1885 inner.line_file.clone(),
1886 )
1887 .into(),
1888 AtomicFact::GreaterEqualFact(inner) => GreaterEqualFact::new(
1889 inner
1890 .left
1891 .replace_with_numeric_result_if_can_be_calculated()
1892 .0,
1893 inner
1894 .right
1895 .replace_with_numeric_result_if_can_be_calculated()
1896 .0,
1897 inner.line_file.clone(),
1898 )
1899 .into(),
1900 AtomicFact::NotGreaterEqualFact(inner) => NotGreaterEqualFact::new(
1901 inner
1902 .left
1903 .replace_with_numeric_result_if_can_be_calculated()
1904 .0,
1905 inner
1906 .right
1907 .replace_with_numeric_result_if_can_be_calculated()
1908 .0,
1909 inner.line_file.clone(),
1910 )
1911 .into(),
1912 AtomicFact::IsSetFact(inner) => IsSetFact::new(
1913 inner
1914 .set
1915 .replace_with_numeric_result_if_can_be_calculated()
1916 .0,
1917 inner.line_file.clone(),
1918 )
1919 .into(),
1920 AtomicFact::NotIsSetFact(inner) => NotIsSetFact::new(
1921 inner
1922 .set
1923 .replace_with_numeric_result_if_can_be_calculated()
1924 .0,
1925 inner.line_file.clone(),
1926 )
1927 .into(),
1928 AtomicFact::IsNonemptySetFact(inner) => IsNonemptySetFact::new(
1929 inner
1930 .set
1931 .replace_with_numeric_result_if_can_be_calculated()
1932 .0,
1933 inner.line_file.clone(),
1934 )
1935 .into(),
1936 AtomicFact::NotIsNonemptySetFact(inner) => NotIsNonemptySetFact::new(
1937 inner
1938 .set
1939 .replace_with_numeric_result_if_can_be_calculated()
1940 .0,
1941 inner.line_file.clone(),
1942 )
1943 .into(),
1944 AtomicFact::IsFiniteSetFact(inner) => IsFiniteSetFact::new(
1945 inner
1946 .set
1947 .replace_with_numeric_result_if_can_be_calculated()
1948 .0,
1949 inner.line_file.clone(),
1950 )
1951 .into(),
1952 AtomicFact::NotIsFiniteSetFact(inner) => NotIsFiniteSetFact::new(
1953 inner
1954 .set
1955 .replace_with_numeric_result_if_can_be_calculated()
1956 .0,
1957 inner.line_file.clone(),
1958 )
1959 .into(),
1960 AtomicFact::InFact(inner) => InFact::new(
1961 inner
1962 .element
1963 .replace_with_numeric_result_if_can_be_calculated()
1964 .0,
1965 inner
1966 .set
1967 .replace_with_numeric_result_if_can_be_calculated()
1968 .0,
1969 inner.line_file.clone(),
1970 )
1971 .into(),
1972 AtomicFact::NotInFact(inner) => NotInFact::new(
1973 inner
1974 .element
1975 .replace_with_numeric_result_if_can_be_calculated()
1976 .0,
1977 inner
1978 .set
1979 .replace_with_numeric_result_if_can_be_calculated()
1980 .0,
1981 inner.line_file.clone(),
1982 )
1983 .into(),
1984 AtomicFact::IsCartFact(inner) => IsCartFact::new(
1985 inner
1986 .set
1987 .replace_with_numeric_result_if_can_be_calculated()
1988 .0,
1989 inner.line_file.clone(),
1990 )
1991 .into(),
1992 AtomicFact::NotIsCartFact(inner) => NotIsCartFact::new(
1993 inner
1994 .set
1995 .replace_with_numeric_result_if_can_be_calculated()
1996 .0,
1997 inner.line_file.clone(),
1998 )
1999 .into(),
2000 AtomicFact::IsTupleFact(inner) => IsTupleFact::new(
2001 inner
2002 .set
2003 .replace_with_numeric_result_if_can_be_calculated()
2004 .0,
2005 inner.line_file.clone(),
2006 )
2007 .into(),
2008 AtomicFact::NotIsTupleFact(inner) => NotIsTupleFact::new(
2009 inner
2010 .set
2011 .replace_with_numeric_result_if_can_be_calculated()
2012 .0,
2013 inner.line_file.clone(),
2014 )
2015 .into(),
2016 AtomicFact::SubsetFact(inner) => SubsetFact::new(
2017 inner
2018 .left
2019 .replace_with_numeric_result_if_can_be_calculated()
2020 .0,
2021 inner
2022 .right
2023 .replace_with_numeric_result_if_can_be_calculated()
2024 .0,
2025 inner.line_file.clone(),
2026 )
2027 .into(),
2028 AtomicFact::NotSubsetFact(inner) => NotSubsetFact::new(
2029 inner
2030 .left
2031 .replace_with_numeric_result_if_can_be_calculated()
2032 .0,
2033 inner
2034 .right
2035 .replace_with_numeric_result_if_can_be_calculated()
2036 .0,
2037 inner.line_file.clone(),
2038 )
2039 .into(),
2040 AtomicFact::SupersetFact(inner) => SupersetFact::new(
2041 inner
2042 .left
2043 .replace_with_numeric_result_if_can_be_calculated()
2044 .0,
2045 inner
2046 .right
2047 .replace_with_numeric_result_if_can_be_calculated()
2048 .0,
2049 inner.line_file.clone(),
2050 )
2051 .into(),
2052 AtomicFact::NotSupersetFact(inner) => NotSupersetFact::new(
2053 inner
2054 .left
2055 .replace_with_numeric_result_if_can_be_calculated()
2056 .0,
2057 inner
2058 .right
2059 .replace_with_numeric_result_if_can_be_calculated()
2060 .0,
2061 inner.line_file.clone(),
2062 )
2063 .into(),
2064 AtomicFact::RestrictFact(inner) => RestrictFact::new(
2065 inner
2066 .obj
2067 .replace_with_numeric_result_if_can_be_calculated()
2068 .0,
2069 inner
2070 .obj_can_restrict_to_fn_set
2071 .replace_with_numeric_result_if_can_be_calculated()
2072 .0,
2073 inner.line_file.clone(),
2074 )
2075 .into(),
2076 AtomicFact::NotRestrictFact(inner) => NotRestrictFact::new(
2077 inner
2078 .obj
2079 .replace_with_numeric_result_if_can_be_calculated()
2080 .0,
2081 inner
2082 .obj_cannot_restrict_to_fn_set
2083 .replace_with_numeric_result_if_can_be_calculated()
2084 .0,
2085 inner.line_file.clone(),
2086 )
2087 .into(),
2088 AtomicFact::FnEqualInFact(inner) => FnEqualInFact::new(
2089 inner
2090 .left
2091 .replace_with_numeric_result_if_can_be_calculated()
2092 .0,
2093 inner
2094 .right
2095 .replace_with_numeric_result_if_can_be_calculated()
2096 .0,
2097 inner
2098 .set
2099 .replace_with_numeric_result_if_can_be_calculated()
2100 .0,
2101 inner.line_file.clone(),
2102 )
2103 .into(),
2104 AtomicFact::FnEqualFact(inner) => FnEqualFact::new(
2105 inner
2106 .left
2107 .replace_with_numeric_result_if_can_be_calculated()
2108 .0,
2109 inner
2110 .right
2111 .replace_with_numeric_result_if_can_be_calculated()
2112 .0,
2113 inner.line_file.clone(),
2114 )
2115 .into(),
2116 };
2117 let any_argument_replaced = calculated_atomic_fact.to_string() != self.to_string();
2118 (calculated_atomic_fact, any_argument_replaced)
2119 }
2120}
2121
2122impl From<NormalAtomicFact> for AtomicFact {
2123 fn from(f: NormalAtomicFact) -> Self {
2124 AtomicFact::NormalAtomicFact(f)
2125 }
2126}
2127
2128impl From<EqualFact> for AtomicFact {
2129 fn from(f: EqualFact) -> Self {
2130 AtomicFact::EqualFact(f)
2131 }
2132}
2133
2134impl From<LessFact> for AtomicFact {
2135 fn from(f: LessFact) -> Self {
2136 AtomicFact::LessFact(f)
2137 }
2138}
2139
2140impl From<GreaterFact> for AtomicFact {
2141 fn from(f: GreaterFact) -> Self {
2142 AtomicFact::GreaterFact(f)
2143 }
2144}
2145
2146impl From<LessEqualFact> for AtomicFact {
2147 fn from(f: LessEqualFact) -> Self {
2148 AtomicFact::LessEqualFact(f)
2149 }
2150}
2151
2152impl From<GreaterEqualFact> for AtomicFact {
2153 fn from(f: GreaterEqualFact) -> Self {
2154 AtomicFact::GreaterEqualFact(f)
2155 }
2156}
2157
2158impl From<IsSetFact> for AtomicFact {
2159 fn from(f: IsSetFact) -> Self {
2160 AtomicFact::IsSetFact(f)
2161 }
2162}
2163
2164impl From<IsNonemptySetFact> for AtomicFact {
2165 fn from(f: IsNonemptySetFact) -> Self {
2166 AtomicFact::IsNonemptySetFact(f)
2167 }
2168}
2169
2170impl From<IsFiniteSetFact> for AtomicFact {
2171 fn from(f: IsFiniteSetFact) -> Self {
2172 AtomicFact::IsFiniteSetFact(f)
2173 }
2174}
2175
2176impl From<InFact> for AtomicFact {
2177 fn from(f: InFact) -> Self {
2178 AtomicFact::InFact(f)
2179 }
2180}
2181
2182impl From<IsCartFact> for AtomicFact {
2183 fn from(f: IsCartFact) -> Self {
2184 AtomicFact::IsCartFact(f)
2185 }
2186}
2187
2188impl From<IsTupleFact> for AtomicFact {
2189 fn from(f: IsTupleFact) -> Self {
2190 AtomicFact::IsTupleFact(f)
2191 }
2192}
2193
2194impl From<SubsetFact> for AtomicFact {
2195 fn from(f: SubsetFact) -> Self {
2196 AtomicFact::SubsetFact(f)
2197 }
2198}
2199
2200impl From<SupersetFact> for AtomicFact {
2201 fn from(f: SupersetFact) -> Self {
2202 AtomicFact::SupersetFact(f)
2203 }
2204}
2205
2206impl From<RestrictFact> for AtomicFact {
2207 fn from(f: RestrictFact) -> Self {
2208 AtomicFact::RestrictFact(f)
2209 }
2210}
2211
2212impl From<NotRestrictFact> for AtomicFact {
2213 fn from(f: NotRestrictFact) -> Self {
2214 AtomicFact::NotRestrictFact(f)
2215 }
2216}
2217
2218impl From<NotNormalAtomicFact> for AtomicFact {
2219 fn from(f: NotNormalAtomicFact) -> Self {
2220 AtomicFact::NotNormalAtomicFact(f)
2221 }
2222}
2223
2224impl From<NotEqualFact> for AtomicFact {
2225 fn from(f: NotEqualFact) -> Self {
2226 AtomicFact::NotEqualFact(f)
2227 }
2228}
2229
2230impl From<NotLessFact> for AtomicFact {
2231 fn from(f: NotLessFact) -> Self {
2232 AtomicFact::NotLessFact(f)
2233 }
2234}
2235
2236impl From<NotGreaterFact> for AtomicFact {
2237 fn from(f: NotGreaterFact) -> Self {
2238 AtomicFact::NotGreaterFact(f)
2239 }
2240}
2241
2242impl From<NotLessEqualFact> for AtomicFact {
2243 fn from(f: NotLessEqualFact) -> Self {
2244 AtomicFact::NotLessEqualFact(f)
2245 }
2246}
2247
2248impl From<NotGreaterEqualFact> for AtomicFact {
2249 fn from(f: NotGreaterEqualFact) -> Self {
2250 AtomicFact::NotGreaterEqualFact(f)
2251 }
2252}
2253
2254impl From<NotIsSetFact> for AtomicFact {
2255 fn from(f: NotIsSetFact) -> Self {
2256 AtomicFact::NotIsSetFact(f)
2257 }
2258}
2259
2260impl From<NotIsNonemptySetFact> for AtomicFact {
2261 fn from(f: NotIsNonemptySetFact) -> Self {
2262 AtomicFact::NotIsNonemptySetFact(f)
2263 }
2264}
2265
2266impl From<NotIsFiniteSetFact> for AtomicFact {
2267 fn from(f: NotIsFiniteSetFact) -> Self {
2268 AtomicFact::NotIsFiniteSetFact(f)
2269 }
2270}
2271
2272impl From<NotInFact> for AtomicFact {
2273 fn from(f: NotInFact) -> Self {
2274 AtomicFact::NotInFact(f)
2275 }
2276}
2277
2278impl From<NotIsCartFact> for AtomicFact {
2279 fn from(f: NotIsCartFact) -> Self {
2280 AtomicFact::NotIsCartFact(f)
2281 }
2282}
2283
2284impl From<NotIsTupleFact> for AtomicFact {
2285 fn from(f: NotIsTupleFact) -> Self {
2286 AtomicFact::NotIsTupleFact(f)
2287 }
2288}
2289
2290impl From<NotSubsetFact> for AtomicFact {
2291 fn from(f: NotSubsetFact) -> Self {
2292 AtomicFact::NotSubsetFact(f)
2293 }
2294}
2295
2296impl From<NotSupersetFact> for AtomicFact {
2297 fn from(f: NotSupersetFact) -> Self {
2298 AtomicFact::NotSupersetFact(f)
2299 }
2300}
2301
2302impl From<FnEqualInFact> for AtomicFact {
2303 fn from(f: FnEqualInFact) -> Self {
2304 AtomicFact::FnEqualInFact(f)
2305 }
2306}
2307
2308impl From<FnEqualFact> for AtomicFact {
2309 fn from(f: FnEqualFact) -> Self {
2310 AtomicFact::FnEqualFact(f)
2311 }
2312}
2313
2314impl From<NormalAtomicFact> for Fact {
2315 fn from(f: NormalAtomicFact) -> Self {
2316 Fact::AtomicFact(f.into())
2317 }
2318}
2319
2320impl From<EqualFact> for Fact {
2321 fn from(f: EqualFact) -> Self {
2322 Fact::AtomicFact(f.into())
2323 }
2324}
2325
2326impl From<LessFact> for Fact {
2327 fn from(f: LessFact) -> Self {
2328 Fact::AtomicFact(f.into())
2329 }
2330}
2331
2332impl From<GreaterFact> for Fact {
2333 fn from(f: GreaterFact) -> Self {
2334 Fact::AtomicFact(f.into())
2335 }
2336}
2337
2338impl From<LessEqualFact> for Fact {
2339 fn from(f: LessEqualFact) -> Self {
2340 Fact::AtomicFact(f.into())
2341 }
2342}
2343
2344impl From<GreaterEqualFact> for Fact {
2345 fn from(f: GreaterEqualFact) -> Self {
2346 Fact::AtomicFact(f.into())
2347 }
2348}
2349
2350impl From<IsSetFact> for Fact {
2351 fn from(f: IsSetFact) -> Self {
2352 Fact::AtomicFact(f.into())
2353 }
2354}
2355
2356impl From<IsNonemptySetFact> for Fact {
2357 fn from(f: IsNonemptySetFact) -> Self {
2358 Fact::AtomicFact(f.into())
2359 }
2360}
2361
2362impl From<IsFiniteSetFact> for Fact {
2363 fn from(f: IsFiniteSetFact) -> Self {
2364 Fact::AtomicFact(f.into())
2365 }
2366}
2367
2368impl From<InFact> for Fact {
2369 fn from(f: InFact) -> Self {
2370 Fact::AtomicFact(f.into())
2371 }
2372}
2373
2374impl From<IsCartFact> for Fact {
2375 fn from(f: IsCartFact) -> Self {
2376 Fact::AtomicFact(f.into())
2377 }
2378}
2379
2380impl From<IsTupleFact> for Fact {
2381 fn from(f: IsTupleFact) -> Self {
2382 Fact::AtomicFact(f.into())
2383 }
2384}
2385
2386impl From<SubsetFact> for Fact {
2387 fn from(f: SubsetFact) -> Self {
2388 Fact::AtomicFact(f.into())
2389 }
2390}
2391
2392impl From<SupersetFact> for Fact {
2393 fn from(f: SupersetFact) -> Self {
2394 Fact::AtomicFact(f.into())
2395 }
2396}
2397
2398impl From<RestrictFact> for Fact {
2399 fn from(f: RestrictFact) -> Self {
2400 Fact::AtomicFact(f.into())
2401 }
2402}
2403
2404impl From<NotRestrictFact> for Fact {
2405 fn from(f: NotRestrictFact) -> Self {
2406 Fact::AtomicFact(f.into())
2407 }
2408}
2409
2410impl From<FnEqualInFact> for Fact {
2411 fn from(f: FnEqualInFact) -> Self {
2412 Fact::AtomicFact(f.into())
2413 }
2414}
2415
2416impl From<FnEqualFact> for Fact {
2417 fn from(f: FnEqualFact) -> Self {
2418 Fact::AtomicFact(f.into())
2419 }
2420}
2421
2422impl From<NotNormalAtomicFact> for Fact {
2423 fn from(f: NotNormalAtomicFact) -> Self {
2424 Fact::AtomicFact(f.into())
2425 }
2426}
2427
2428impl From<NotEqualFact> for Fact {
2429 fn from(f: NotEqualFact) -> Self {
2430 Fact::AtomicFact(f.into())
2431 }
2432}
2433
2434impl From<NotLessFact> for Fact {
2435 fn from(f: NotLessFact) -> Self {
2436 Fact::AtomicFact(f.into())
2437 }
2438}
2439
2440impl From<NotGreaterFact> for Fact {
2441 fn from(f: NotGreaterFact) -> Self {
2442 Fact::AtomicFact(f.into())
2443 }
2444}
2445
2446impl From<NotLessEqualFact> for Fact {
2447 fn from(f: NotLessEqualFact) -> Self {
2448 Fact::AtomicFact(f.into())
2449 }
2450}
2451
2452impl From<NotGreaterEqualFact> for Fact {
2453 fn from(f: NotGreaterEqualFact) -> Self {
2454 Fact::AtomicFact(f.into())
2455 }
2456}
2457
2458impl From<NotIsSetFact> for Fact {
2459 fn from(f: NotIsSetFact) -> Self {
2460 Fact::AtomicFact(f.into())
2461 }
2462}
2463
2464impl From<NotIsNonemptySetFact> for Fact {
2465 fn from(f: NotIsNonemptySetFact) -> Self {
2466 Fact::AtomicFact(f.into())
2467 }
2468}
2469
2470impl From<NotIsFiniteSetFact> for Fact {
2471 fn from(f: NotIsFiniteSetFact) -> Self {
2472 Fact::AtomicFact(f.into())
2473 }
2474}
2475
2476impl From<NotInFact> for Fact {
2477 fn from(f: NotInFact) -> Self {
2478 Fact::AtomicFact(f.into())
2479 }
2480}
2481
2482impl From<NotIsCartFact> for Fact {
2483 fn from(f: NotIsCartFact) -> Self {
2484 Fact::AtomicFact(f.into())
2485 }
2486}
2487
2488impl From<NotIsTupleFact> for Fact {
2489 fn from(f: NotIsTupleFact) -> Self {
2490 Fact::AtomicFact(f.into())
2491 }
2492}
2493
2494impl From<NotSubsetFact> for Fact {
2495 fn from(f: NotSubsetFact) -> Self {
2496 Fact::AtomicFact(f.into())
2497 }
2498}
2499
2500impl From<NotSupersetFact> for Fact {
2501 fn from(f: NotSupersetFact) -> Self {
2502 Fact::AtomicFact(f.into())
2503 }
2504}