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