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: IdentifierOrIdentifierWithMod,
121 pub body: Vec<Obj>,
122 pub line_file: LineFile,
123}
124
125#[derive(Clone)]
126pub struct NotNormalAtomicFact {
127 pub predicate: IdentifierOrIdentifierWithMod,
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(
260 predicate: IdentifierOrIdentifierWithMod,
261 body: Vec<Obj>,
262 line_file: LineFile,
263 ) -> Self {
264 NormalAtomicFact {
265 predicate,
266 body,
267 line_file,
268 }
269 }
270}
271
272impl NotNormalAtomicFact {
273 pub fn new(
274 predicate: IdentifierOrIdentifierWithMod,
275 body: Vec<Obj>,
276 line_file: LineFile,
277 ) -> Self {
278 NotNormalAtomicFact {
279 predicate,
280 body,
281 line_file,
282 }
283 }
284}
285
286impl EqualFact {
287 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
288 EqualFact {
289 left,
290 right,
291 line_file,
292 }
293 }
294}
295
296impl NotEqualFact {
297 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
298 NotEqualFact {
299 left,
300 right,
301 line_file,
302 }
303 }
304}
305
306impl LessFact {
307 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
308 LessFact {
309 left,
310 right,
311 line_file,
312 }
313 }
314}
315
316impl NotLessFact {
317 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
318 NotLessFact {
319 left,
320 right,
321 line_file,
322 }
323 }
324}
325
326impl GreaterFact {
327 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
328 GreaterFact {
329 left,
330 right,
331 line_file,
332 }
333 }
334}
335
336impl NotGreaterFact {
337 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
338 NotGreaterFact {
339 left,
340 right,
341 line_file,
342 }
343 }
344}
345
346impl LessEqualFact {
347 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
348 LessEqualFact {
349 left,
350 right,
351 line_file,
352 }
353 }
354}
355
356impl NotLessEqualFact {
357 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
358 NotLessEqualFact {
359 left,
360 right,
361 line_file,
362 }
363 }
364}
365
366impl GreaterEqualFact {
367 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
368 GreaterEqualFact {
369 left,
370 right,
371 line_file,
372 }
373 }
374}
375
376impl NotGreaterEqualFact {
377 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
378 NotGreaterEqualFact {
379 left,
380 right,
381 line_file,
382 }
383 }
384}
385
386impl IsSetFact {
387 pub fn new(set: Obj, line_file: LineFile) -> Self {
388 IsSetFact { set, line_file }
389 }
390}
391
392impl NotIsSetFact {
393 pub fn new(set: Obj, line_file: LineFile) -> Self {
394 NotIsSetFact { set, line_file }
395 }
396}
397
398impl IsNonemptySetFact {
399 pub fn new(set: Obj, line_file: LineFile) -> Self {
400 IsNonemptySetFact { set, line_file }
401 }
402}
403
404impl NotIsNonemptySetFact {
405 pub fn new(set: Obj, line_file: LineFile) -> Self {
406 NotIsNonemptySetFact { set, line_file }
407 }
408}
409
410impl IsFiniteSetFact {
411 pub fn new(set: Obj, line_file: LineFile) -> Self {
412 IsFiniteSetFact { set, line_file }
413 }
414}
415
416impl NotIsFiniteSetFact {
417 pub fn new(set: Obj, line_file: LineFile) -> Self {
418 NotIsFiniteSetFact { set, line_file }
419 }
420}
421
422impl InFact {
423 pub fn new(element: Obj, set: Obj, line_file: LineFile) -> Self {
424 InFact {
425 element,
426 set,
427 line_file,
428 }
429 }
430}
431
432impl NotInFact {
433 pub fn new(element: Obj, set: Obj, line_file: LineFile) -> Self {
434 NotInFact {
435 element,
436 set,
437 line_file,
438 }
439 }
440}
441
442impl IsCartFact {
443 pub fn new(set: Obj, line_file: LineFile) -> Self {
444 IsCartFact { set, line_file }
445 }
446}
447
448impl NotIsCartFact {
449 pub fn new(set: Obj, line_file: LineFile) -> Self {
450 NotIsCartFact { set, line_file }
451 }
452}
453
454impl IsTupleFact {
455 pub fn new(tuple: Obj, line_file: LineFile) -> Self {
456 IsTupleFact {
457 set: tuple,
458 line_file,
459 }
460 }
461}
462
463impl NotIsTupleFact {
464 pub fn new(tuple: Obj, line_file: LineFile) -> Self {
465 NotIsTupleFact {
466 set: tuple,
467 line_file,
468 }
469 }
470}
471
472impl SupersetFact {
473 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
474 SupersetFact {
475 left,
476 right,
477 line_file,
478 }
479 }
480}
481
482impl NotSupersetFact {
483 pub fn new(left: Obj, right: Obj, line_file: LineFile) -> Self {
484 NotSupersetFact {
485 left,
486 right,
487 line_file,
488 }
489 }
490}
491
492impl fmt::Display for AtomicFact {
493 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
494 match self {
495 AtomicFact::NormalAtomicFact(x) => write!(f, "{}", x),
496 AtomicFact::EqualFact(x) => write!(f, "{}", x),
497 AtomicFact::LessFact(x) => write!(f, "{}", x),
498 AtomicFact::GreaterFact(x) => write!(f, "{}", x),
499 AtomicFact::LessEqualFact(x) => write!(f, "{}", x),
500 AtomicFact::GreaterEqualFact(x) => write!(f, "{}", x),
501 AtomicFact::IsSetFact(x) => write!(f, "{}", x),
502 AtomicFact::IsNonemptySetFact(x) => write!(f, "{}", x),
503 AtomicFact::IsFiniteSetFact(x) => write!(f, "{}", x),
504 AtomicFact::NotNormalAtomicFact(x) => write!(f, "{}", x),
505 AtomicFact::NotEqualFact(x) => write!(f, "{}", x),
506 AtomicFact::NotLessFact(x) => write!(f, "{}", x),
507 AtomicFact::NotGreaterFact(x) => write!(f, "{}", x),
508 AtomicFact::NotLessEqualFact(x) => write!(f, "{}", x),
509 AtomicFact::NotGreaterEqualFact(x) => write!(f, "{}", x),
510 AtomicFact::NotIsSetFact(x) => write!(f, "{}", x),
511 AtomicFact::NotIsNonemptySetFact(x) => write!(f, "{}", x),
512 AtomicFact::NotIsFiniteSetFact(x) => write!(f, "{}", x),
513 AtomicFact::InFact(x) => write!(f, "{}", x),
514 AtomicFact::NotInFact(x) => write!(f, "{}", x),
515 AtomicFact::IsCartFact(x) => write!(f, "{}", x),
516 AtomicFact::NotIsCartFact(x) => write!(f, "{}", x),
517 AtomicFact::IsTupleFact(x) => write!(f, "{}", x),
518 AtomicFact::NotIsTupleFact(x) => write!(f, "{}", x),
519 AtomicFact::SubsetFact(x) => write!(f, "{}", x),
520 AtomicFact::NotSubsetFact(x) => write!(f, "{}", x),
521 AtomicFact::SupersetFact(x) => write!(f, "{}", x),
522 AtomicFact::NotSupersetFact(x) => write!(f, "{}", x),
523 AtomicFact::RestrictFact(x) => write!(f, "{}", x),
524 AtomicFact::NotRestrictFact(x) => write!(f, "{}", x),
525 }
526 }
527}
528
529impl fmt::Display for SupersetFact {
530 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
531 write!(
532 f,
533 "{} {}{} {}",
534 self.left, FACT_PREFIX, SUPERSET, self.right
535 )
536 }
537}
538
539impl fmt::Display for NotSupersetFact {
540 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
541 write!(
542 f,
543 "{} {} {}{} {}",
544 NOT, self.left, FACT_PREFIX, SUPERSET, self.right
545 )
546 }
547}
548
549impl fmt::Display for SubsetFact {
550 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
551 write!(f, "{} {}{} {}", self.left, FACT_PREFIX, SUBSET, self.right)
552 }
553}
554
555impl fmt::Display for NotSubsetFact {
556 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
557 write!(
558 f,
559 "{} {} {}{} {}",
560 NOT, self.left, FACT_PREFIX, SUBSET, self.right
561 )
562 }
563}
564
565impl fmt::Display for InFact {
566 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
567 write!(f, "{} {}{} {}", self.element, FACT_PREFIX, IN, self.set)
568 }
569}
570
571impl fmt::Display for NotInFact {
572 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
573 write!(
574 f,
575 "{} {} {}{} {}",
576 NOT, self.element, FACT_PREFIX, IN, self.set
577 )
578 }
579}
580
581impl fmt::Display for IsCartFact {
582 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
583 write!(f, "{}{}{}", FACT_PREFIX, IS_CART, braced_string(&self.set))
584 }
585}
586
587impl fmt::Display for NotIsCartFact {
588 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
589 write!(
590 f,
591 "{} {}{}{}",
592 NOT,
593 FACT_PREFIX,
594 IS_CART,
595 braced_string(&self.set)
596 )
597 }
598}
599
600impl fmt::Display for IsTupleFact {
601 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
602 write!(f, "{}{}{}", FACT_PREFIX, IS_TUPLE, braced_string(&self.set))
603 }
604}
605
606impl fmt::Display for NotIsTupleFact {
607 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
608 write!(
609 f,
610 "{} {}{}{}",
611 NOT,
612 FACT_PREFIX,
613 IS_TUPLE,
614 braced_string(&self.set)
615 )
616 }
617}
618
619impl fmt::Display for NormalAtomicFact {
620 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
621 write!(
622 f,
623 "{}{}{}",
624 FACT_PREFIX,
625 self.predicate,
626 braced_vec_to_string(&self.body)
627 )
628 }
629}
630
631impl fmt::Display for NotNormalAtomicFact {
632 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
633 write!(
634 f,
635 "{} {}{}{}",
636 NOT,
637 FACT_PREFIX,
638 self.predicate,
639 braced_vec_to_string(&self.body)
640 )
641 }
642}
643
644impl fmt::Display for EqualFact {
645 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
646 write!(f, "{} {} {}", self.left, EQUAL, self.right)
647 }
648}
649
650impl fmt::Display for NotEqualFact {
651 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
652 write!(f, "{} {} {}", self.left, NOT_EQUAL, self.right)
653 }
654}
655
656impl fmt::Display for LessFact {
657 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
658 write!(f, "{} {} {}", self.left, LESS, self.right)
659 }
660}
661
662impl fmt::Display for NotLessFact {
663 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
664 write!(f, "{} {} {} {}", NOT, self.left, LESS, self.right)
665 }
666}
667
668impl fmt::Display for GreaterFact {
669 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
670 write!(f, "{} {} {}", self.left, GREATER, self.right)
671 }
672}
673
674impl fmt::Display for NotGreaterFact {
675 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
676 write!(f, "{} {} {} {}", NOT, self.left, GREATER, self.right)
677 }
678}
679
680impl fmt::Display for LessEqualFact {
681 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
682 write!(f, "{} {} {}", self.left, LESS_EQUAL, self.right)
683 }
684}
685
686impl fmt::Display for NotLessEqualFact {
687 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
688 write!(f, "{} {} {} {}", NOT, self.left, LESS_EQUAL, self.right)
689 }
690}
691
692impl fmt::Display for GreaterEqualFact {
693 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
694 write!(f, "{} {} {}", self.left, GREATER_EQUAL, self.right)
695 }
696}
697
698impl fmt::Display for NotGreaterEqualFact {
699 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
700 write!(f, "{} {} {} {}", NOT, self.left, GREATER_EQUAL, self.right)
701 }
702}
703
704impl fmt::Display for IsSetFact {
705 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
706 write!(f, "{}{}{}", FACT_PREFIX, IS_SET, braced_string(&self.set))
707 }
708}
709
710impl fmt::Display for NotIsSetFact {
711 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
712 write!(
713 f,
714 "{} {}{}{}",
715 NOT,
716 FACT_PREFIX,
717 IS_SET,
718 braced_string(&self.set)
719 )
720 }
721}
722
723impl fmt::Display for IsNonemptySetFact {
724 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
725 write!(
726 f,
727 "{}{}{}",
728 FACT_PREFIX,
729 IS_NONEMPTY_SET,
730 braced_string(&self.set)
731 )
732 }
733}
734
735impl fmt::Display for NotIsNonemptySetFact {
736 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
737 write!(
738 f,
739 "{} {}{}{}",
740 NOT,
741 FACT_PREFIX,
742 IS_NONEMPTY_SET,
743 braced_string(&self.set)
744 )
745 }
746}
747
748impl fmt::Display for IsFiniteSetFact {
749 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
750 write!(
751 f,
752 "{}{}{}",
753 FACT_PREFIX,
754 IS_FINITE_SET,
755 braced_string(&self.set)
756 )
757 }
758}
759
760impl fmt::Display for NotIsFiniteSetFact {
761 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
762 write!(
763 f,
764 "{} {}{}{}",
765 NOT,
766 FACT_PREFIX,
767 IS_FINITE_SET,
768 braced_string(&self.set)
769 )
770 }
771}
772
773impl AtomicFact {
774 pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
775 if from == to {
776 return self;
777 }
778 fn r(o: Obj, from: &str, to: &str) -> Obj {
779 Obj::replace_bound_identifier(o, from, to)
780 }
781 match self {
782 AtomicFact::NormalAtomicFact(x) => AtomicFact::NormalAtomicFact(NormalAtomicFact::new(
783 x.predicate,
784 x.body.into_iter().map(|o| r(o, from, to)).collect(),
785 x.line_file,
786 )),
787 AtomicFact::EqualFact(x) => {
788 AtomicFact::EqualFact(EqualFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file))
789 }
790 AtomicFact::LessFact(x) => {
791 AtomicFact::LessFact(LessFact::new(r(x.left, from, to), r(x.right, from, to), x.line_file))
792 }
793 AtomicFact::GreaterFact(x) => AtomicFact::GreaterFact(GreaterFact::new(
794 r(x.left, from, to),
795 r(x.right, from, to),
796 x.line_file,
797 )),
798 AtomicFact::LessEqualFact(x) => AtomicFact::LessEqualFact(LessEqualFact::new(
799 r(x.left, from, to),
800 r(x.right, from, to),
801 x.line_file,
802 )),
803 AtomicFact::GreaterEqualFact(x) => AtomicFact::GreaterEqualFact(GreaterEqualFact::new(
804 r(x.left, from, to),
805 r(x.right, from, to),
806 x.line_file,
807 )),
808 AtomicFact::IsSetFact(x) => {
809 AtomicFact::IsSetFact(IsSetFact::new(r(x.set, from, to), x.line_file))
810 }
811 AtomicFact::IsNonemptySetFact(x) => AtomicFact::IsNonemptySetFact(
812 IsNonemptySetFact::new(r(x.set, from, to), x.line_file),
813 ),
814 AtomicFact::IsFiniteSetFact(x) => AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(
815 r(x.set, from, to),
816 x.line_file,
817 )),
818 AtomicFact::InFact(x) => AtomicFact::InFact(InFact::new(
819 r(x.element, from, to),
820 r(x.set, from, to),
821 x.line_file,
822 )),
823 AtomicFact::IsCartFact(x) => {
824 AtomicFact::IsCartFact(IsCartFact::new(r(x.set, from, to), x.line_file))
825 }
826 AtomicFact::IsTupleFact(x) => {
827 AtomicFact::IsTupleFact(IsTupleFact::new(r(x.set, from, to), x.line_file))
828 }
829 AtomicFact::SubsetFact(x) => AtomicFact::SubsetFact(SubsetFact::new(
830 r(x.left, from, to),
831 r(x.right, from, to),
832 x.line_file,
833 )),
834 AtomicFact::SupersetFact(x) => AtomicFact::SupersetFact(SupersetFact::new(
835 r(x.left, from, to),
836 r(x.right, from, to),
837 x.line_file,
838 )),
839 AtomicFact::RestrictFact(x) => AtomicFact::RestrictFact(RestrictFact::new(
840 r(x.obj, from, to),
841 r(x.obj_can_restrict_to_fn_set, from, to),
842 x.line_file,
843 )),
844 AtomicFact::NotRestrictFact(x) => AtomicFact::NotRestrictFact(NotRestrictFact::new(
845 r(x.obj, from, to),
846 r(x.obj_cannot_restrict_to_fn_set, from, to),
847 x.line_file,
848 )),
849 AtomicFact::NotNormalAtomicFact(x) => {
850 AtomicFact::NotNormalAtomicFact(NotNormalAtomicFact::new(
851 x.predicate,
852 x.body.into_iter().map(|o| r(o, from, to)).collect(),
853 x.line_file,
854 ))
855 }
856 AtomicFact::NotEqualFact(x) => AtomicFact::NotEqualFact(NotEqualFact::new(
857 r(x.left, from, to),
858 r(x.right, from, to),
859 x.line_file,
860 )),
861 AtomicFact::NotLessFact(x) => AtomicFact::NotLessFact(NotLessFact::new(
862 r(x.left, from, to),
863 r(x.right, from, to),
864 x.line_file,
865 )),
866 AtomicFact::NotGreaterFact(x) => AtomicFact::NotGreaterFact(NotGreaterFact::new(
867 r(x.left, from, to),
868 r(x.right, from, to),
869 x.line_file,
870 )),
871 AtomicFact::NotLessEqualFact(x) => AtomicFact::NotLessEqualFact(NotLessEqualFact::new(
872 r(x.left, from, to),
873 r(x.right, from, to),
874 x.line_file,
875 )),
876 AtomicFact::NotGreaterEqualFact(x) => {
877 AtomicFact::NotGreaterEqualFact(NotGreaterEqualFact::new(
878 r(x.left, from, to),
879 r(x.right, from, to),
880 x.line_file,
881 ))
882 }
883 AtomicFact::NotIsSetFact(x) => {
884 AtomicFact::NotIsSetFact(NotIsSetFact::new(r(x.set, from, to), x.line_file))
885 }
886 AtomicFact::NotIsNonemptySetFact(x) => AtomicFact::NotIsNonemptySetFact(
887 NotIsNonemptySetFact::new(r(x.set, from, to), x.line_file),
888 ),
889 AtomicFact::NotIsFiniteSetFact(x) => AtomicFact::NotIsFiniteSetFact(
890 NotIsFiniteSetFact::new(r(x.set, from, to), x.line_file),
891 ),
892 AtomicFact::NotInFact(x) => AtomicFact::NotInFact(NotInFact::new(
893 r(x.element, from, to),
894 r(x.set, from, to),
895 x.line_file,
896 )),
897 AtomicFact::NotIsCartFact(x) => {
898 AtomicFact::NotIsCartFact(NotIsCartFact::new(r(x.set, from, to), x.line_file))
899 }
900 AtomicFact::NotIsTupleFact(x) => AtomicFact::NotIsTupleFact(NotIsTupleFact::new(
901 r(x.set, from, to),
902 x.line_file,
903 )),
904 AtomicFact::NotSubsetFact(x) => AtomicFact::NotSubsetFact(NotSubsetFact::new(
905 r(x.left, from, to),
906 r(x.right, from, to),
907 x.line_file,
908 )),
909 AtomicFact::NotSupersetFact(x) => AtomicFact::NotSupersetFact(NotSupersetFact::new(
910 r(x.left, from, to),
911 r(x.right, from, to),
912 x.line_file,
913 )),
914 }
915 }
916}
917
918impl AtomicFact {
919 fn predicate_string(&self) -> String {
920 match self {
921 AtomicFact::NormalAtomicFact(x) => x.predicate.to_string(),
922 AtomicFact::EqualFact(_) => EQUAL.to_string(),
923 AtomicFact::LessFact(_) => LESS.to_string(),
924 AtomicFact::GreaterFact(_) => GREATER.to_string(),
925 AtomicFact::LessEqualFact(_) => LESS_EQUAL.to_string(),
926 AtomicFact::GreaterEqualFact(_) => GREATER_EQUAL.to_string(),
927 AtomicFact::IsSetFact(_) => IS_SET.to_string(),
928 AtomicFact::IsNonemptySetFact(_) => IS_NONEMPTY_SET.to_string(),
929 AtomicFact::IsFiniteSetFact(_) => IS_FINITE_SET.to_string(),
930 AtomicFact::InFact(_) => IN.to_string(),
931 AtomicFact::IsCartFact(_) => IS_CART.to_string(),
932 AtomicFact::IsTupleFact(_) => IS_TUPLE.to_string(),
933 AtomicFact::SubsetFact(_) => SUBSET.to_string(),
934 AtomicFact::SupersetFact(_) => SUPERSET.to_string(),
935 AtomicFact::NotNormalAtomicFact(x) => x.predicate.to_string(),
936 AtomicFact::NotEqualFact(_) => EQUAL.to_string(),
937 AtomicFact::NotLessFact(_) => LESS.to_string(),
938 AtomicFact::NotGreaterFact(_) => GREATER.to_string(),
939 AtomicFact::NotLessEqualFact(_) => LESS_EQUAL.to_string(),
940 AtomicFact::NotGreaterEqualFact(_) => GREATER_EQUAL.to_string(),
941 AtomicFact::NotIsSetFact(_) => IS_SET.to_string(),
942 AtomicFact::NotIsNonemptySetFact(_) => IS_NONEMPTY_SET.to_string(),
943 AtomicFact::NotIsFiniteSetFact(_) => IS_FINITE_SET.to_string(),
944 AtomicFact::NotInFact(_) => IN.to_string(),
945 AtomicFact::NotIsCartFact(_) => IS_CART.to_string(),
946 AtomicFact::NotIsTupleFact(_) => IS_TUPLE.to_string(),
947 AtomicFact::NotSubsetFact(_) => SUBSET.to_string(),
948 AtomicFact::NotSupersetFact(_) => SUPERSET.to_string(),
949 AtomicFact::RestrictFact(_) => RESTRICT.to_string(),
950 AtomicFact::NotRestrictFact(_) => RESTRICT.to_string(),
951 }
952 }
953
954 pub fn is_true(&self) -> bool {
955 match self {
956 AtomicFact::NormalAtomicFact(_) => true,
957 AtomicFact::EqualFact(_) => true,
958 AtomicFact::LessFact(_) => true,
959 AtomicFact::GreaterFact(_) => true,
960 AtomicFact::LessEqualFact(_) => true,
961 AtomicFact::GreaterEqualFact(_) => true,
962 AtomicFact::IsSetFact(_) => true,
963 AtomicFact::IsNonemptySetFact(_) => true,
964 AtomicFact::IsFiniteSetFact(_) => true,
965 AtomicFact::InFact(_) => true,
966 AtomicFact::IsCartFact(_) => true,
967 AtomicFact::IsTupleFact(_) => true,
968 AtomicFact::SubsetFact(_) => true,
969 AtomicFact::SupersetFact(_) => true,
970 AtomicFact::RestrictFact(_) => true,
971 AtomicFact::NotNormalAtomicFact(_) => false,
972 AtomicFact::NotEqualFact(_) => false,
973 AtomicFact::NotLessFact(_) => false,
974 AtomicFact::NotGreaterFact(_) => false,
975 AtomicFact::NotLessEqualFact(_) => false,
976 AtomicFact::NotGreaterEqualFact(_) => false,
977 AtomicFact::NotIsSetFact(_) => false,
978 AtomicFact::NotIsNonemptySetFact(_) => false,
979 AtomicFact::NotIsFiniteSetFact(_) => false,
980 AtomicFact::NotInFact(_) => false,
981 AtomicFact::NotIsCartFact(_) => false,
982 AtomicFact::NotIsTupleFact(_) => false,
983 AtomicFact::NotSubsetFact(_) => false,
984 AtomicFact::NotSupersetFact(_) => false,
985 AtomicFact::NotRestrictFact(_) => false,
986 }
987 }
988
989 pub fn key(&self) -> String {
990 return self.predicate_string();
991 }
992
993 pub fn transposed_binary_order_equivalent(&self) -> Option<Self> {
994 match self {
995 AtomicFact::LessFact(f) => Some(AtomicFact::GreaterFact(GreaterFact::new(
996 f.right.clone(),
997 f.left.clone(),
998 f.line_file.clone(),
999 ))),
1000 AtomicFact::GreaterFact(f) => Some(AtomicFact::LessFact(LessFact::new(
1001 f.right.clone(),
1002 f.left.clone(),
1003 f.line_file.clone(),
1004 ))),
1005 AtomicFact::LessEqualFact(f) => Some(AtomicFact::GreaterEqualFact(
1006 GreaterEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
1007 )),
1008 AtomicFact::GreaterEqualFact(f) => Some(AtomicFact::LessEqualFact(LessEqualFact::new(
1009 f.right.clone(),
1010 f.left.clone(),
1011 f.line_file.clone(),
1012 ))),
1013 AtomicFact::NotLessFact(f) => Some(AtomicFact::NotGreaterFact(NotGreaterFact::new(
1014 f.right.clone(),
1015 f.left.clone(),
1016 f.line_file.clone(),
1017 ))),
1018 AtomicFact::NotGreaterFact(f) => Some(AtomicFact::NotLessFact(NotLessFact::new(
1019 f.right.clone(),
1020 f.left.clone(),
1021 f.line_file.clone(),
1022 ))),
1023 AtomicFact::NotLessEqualFact(f) => Some(AtomicFact::NotGreaterEqualFact(
1024 NotGreaterEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
1025 )),
1026 AtomicFact::NotGreaterEqualFact(f) => Some(AtomicFact::NotLessEqualFact(
1027 NotLessEqualFact::new(f.right.clone(), f.left.clone(), f.line_file.clone()),
1028 )),
1029 _ => None,
1030 }
1031 }
1032}
1033
1034impl AtomicFact {
1035 pub fn to_atomic_fact(
1036 prop_name: IdentifierOrIdentifierWithMod,
1037 is_true: bool,
1038 args: Vec<Obj>,
1039 line_file: LineFile,
1040 ) -> Result<AtomicFact, RuntimeErrorStruct> {
1041 let prop_name_as_string = prop_name.to_string();
1042 match prop_name_as_string.as_str() {
1043 EQUAL => {
1044 if args.len() != 2 {
1045 let msg = format!("{} requires 2 arguments, but got {}", EQUAL, args.len());
1046 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1047 }
1048 let mut args = args;
1049 let a0 = args.remove(0);
1050 let a1 = args.remove(0);
1051 if is_true {
1052 Ok(AtomicFact::EqualFact(EqualFact::new(a0, a1, line_file)))
1053 } else {
1054 Ok(AtomicFact::NotEqualFact(NotEqualFact::new(
1055 a0, a1, line_file,
1056 )))
1057 }
1058 }
1059 NOT_EQUAL => {
1060 if args.len() != 2 {
1061 let msg = format!("{} requires 2 arguments, but got {}", NOT_EQUAL, args.len());
1062 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1063 }
1064 let mut args = args;
1065 let a0 = args.remove(0);
1066 let a1 = args.remove(0);
1067 if is_true {
1068 Ok(AtomicFact::NotEqualFact(NotEqualFact::new(
1069 a0, a1, line_file,
1070 )))
1071 } else {
1072 Ok(AtomicFact::EqualFact(EqualFact::new(a0, a1, line_file)))
1073 }
1074 }
1075 LESS => {
1076 if args.len() != 2 {
1077 let msg = format!("{} requires 2 arguments, but got {}", LESS, args.len());
1078 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1079 }
1080 let mut args = args;
1081 let a0 = args.remove(0);
1082 let a1 = args.remove(0);
1083 if is_true {
1084 Ok(AtomicFact::LessFact(LessFact::new(a0, a1, line_file)))
1085 } else {
1086 Ok(AtomicFact::NotLessFact(NotLessFact::new(a0, a1, line_file)))
1087 }
1088 }
1089 GREATER => {
1090 if args.len() != 2 {
1091 let msg = format!("{} requires 2 arguments, but got {}", GREATER, args.len());
1092 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1093 }
1094 let mut args = args;
1095 let a0 = args.remove(0);
1096 let a1 = args.remove(0);
1097 if is_true {
1098 Ok(AtomicFact::GreaterFact(GreaterFact::new(a0, a1, line_file)))
1099 } else {
1100 Ok(AtomicFact::NotGreaterFact(NotGreaterFact::new(
1101 a0, a1, line_file,
1102 )))
1103 }
1104 }
1105 LESS_EQUAL => {
1106 if args.len() != 2 {
1107 let msg = format!(
1108 "{} requires 2 arguments, but got {}",
1109 LESS_EQUAL,
1110 args.len()
1111 );
1112 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1113 }
1114 let mut args = args;
1115 let a0 = args.remove(0);
1116 let a1 = args.remove(0);
1117 if is_true {
1118 Ok(AtomicFact::LessEqualFact(LessEqualFact::new(
1119 a0, a1, line_file,
1120 )))
1121 } else {
1122 Ok(AtomicFact::NotLessEqualFact(NotLessEqualFact::new(
1123 a0, a1, line_file,
1124 )))
1125 }
1126 }
1127 GREATER_EQUAL => {
1128 if args.len() != 2 {
1129 let msg = format!(
1130 "{} requires 2 arguments, but got {}",
1131 GREATER_EQUAL,
1132 args.len()
1133 );
1134 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1135 }
1136 let mut args = args;
1137 let a0 = args.remove(0);
1138 let a1 = args.remove(0);
1139 if is_true {
1140 Ok(AtomicFact::GreaterEqualFact(GreaterEqualFact::new(
1141 a0, a1, line_file,
1142 )))
1143 } else {
1144 Ok(AtomicFact::NotGreaterEqualFact(NotGreaterEqualFact::new(
1145 a0, a1, line_file,
1146 )))
1147 }
1148 }
1149 IS_SET => {
1150 if args.len() != 1 {
1151 let msg = format!("{} requires 1 argument, but got {}", IS_SET, args.len());
1152 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1153 }
1154 let mut args = args;
1155 let a0 = args.remove(0);
1156 if is_true {
1157 Ok(AtomicFact::IsSetFact(IsSetFact::new(a0, line_file)))
1158 } else {
1159 Ok(AtomicFact::NotIsSetFact(NotIsSetFact::new(a0, line_file)))
1160 }
1161 }
1162 IS_NONEMPTY_SET => {
1163 if args.len() != 1 {
1164 let msg = format!(
1165 "{} requires 1 argument, but got {}",
1166 IS_NONEMPTY_SET,
1167 args.len()
1168 );
1169 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1170 }
1171 let mut args = args;
1172 let a0 = args.remove(0);
1173 if is_true {
1174 Ok(AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(
1175 a0, line_file,
1176 )))
1177 } else {
1178 Ok(AtomicFact::NotIsNonemptySetFact(NotIsNonemptySetFact::new(
1179 a0, line_file,
1180 )))
1181 }
1182 }
1183 IS_FINITE_SET => {
1184 if args.len() != 1 {
1185 let msg = format!(
1186 "{} requires 1 argument, but got {}",
1187 IS_FINITE_SET,
1188 args.len()
1189 );
1190 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1191 }
1192 let mut args = args;
1193 let a0 = args.remove(0);
1194 if is_true {
1195 Ok(AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(
1196 a0, line_file,
1197 )))
1198 } else {
1199 Ok(AtomicFact::NotIsFiniteSetFact(NotIsFiniteSetFact::new(
1200 a0, line_file,
1201 )))
1202 }
1203 }
1204 IN => {
1205 if args.len() != 2 {
1206 let msg = format!("{} requires 2 arguments, but got {}", IN, args.len());
1207 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1208 }
1209 let mut args = args;
1210 let a0 = args.remove(0);
1211 let a1 = args.remove(0);
1212 if is_true {
1213 Ok(AtomicFact::InFact(InFact::new(a0, a1, line_file)))
1214 } else {
1215 Ok(AtomicFact::NotInFact(NotInFact::new(a0, a1, line_file)))
1216 }
1217 }
1218 IS_CART => {
1219 if args.len() != 1 {
1220 let msg = format!("{} requires 1 argument, but got {}", IS_CART, args.len());
1221 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1222 }
1223 let mut args = args;
1224 let a0 = args.remove(0);
1225 if is_true {
1226 Ok(AtomicFact::IsCartFact(IsCartFact::new(a0, line_file)))
1227 } else {
1228 Ok(AtomicFact::NotIsCartFact(NotIsCartFact::new(a0, line_file)))
1229 }
1230 }
1231 IS_TUPLE => {
1232 if args.len() != 1 {
1233 let msg = format!("{} requires 1 argument, but got {}", IS_TUPLE, args.len());
1234 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1235 }
1236 let mut args = args;
1237 let a0 = args.remove(0);
1238 if is_true {
1239 Ok(AtomicFact::IsTupleFact(IsTupleFact::new(a0, line_file)))
1240 } else {
1241 Ok(AtomicFact::NotIsTupleFact(NotIsTupleFact::new(
1242 a0, line_file,
1243 )))
1244 }
1245 }
1246 SUBSET => {
1247 if args.len() != 2 {
1248 let msg = format!("{} requires 2 arguments, but got {}", SUBSET, args.len());
1249 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1250 }
1251 let mut args = args;
1252 let a0 = args.remove(0);
1253 let a1 = args.remove(0);
1254 if is_true {
1255 Ok(AtomicFact::SubsetFact(SubsetFact::new(a0, a1, line_file)))
1256 } else {
1257 Ok(AtomicFact::NotSubsetFact(NotSubsetFact::new(
1258 a0, a1, line_file,
1259 )))
1260 }
1261 }
1262 SUPERSET => {
1263 if args.len() != 2 {
1264 let msg = format!("{} requires 2 arguments, but got {}", SUPERSET, args.len());
1265 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1266 }
1267 let mut args = args;
1268 let a0 = args.remove(0);
1269 let a1 = args.remove(0);
1270 if is_true {
1271 Ok(AtomicFact::SupersetFact(SupersetFact::new(
1272 a0, a1, line_file,
1273 )))
1274 } else {
1275 Ok(AtomicFact::NotSupersetFact(NotSupersetFact::new(
1276 a0, a1, line_file,
1277 )))
1278 }
1279 }
1280 RESTRICT => {
1281 if args.len() != 2 {
1282 let msg = format!("{} requires 2 arguments, but got {}", RESTRICT, args.len());
1283 return Err(RuntimeErrorStruct::new_with_msg_previous_error(msg, None));
1284 }
1285 let mut args = args;
1286 let a0 = args.remove(0);
1287 let a1 = args.remove(0);
1288 if is_true {
1289 Ok(AtomicFact::RestrictFact(RestrictFact::new(
1290 a0, a1, line_file,
1291 )))
1292 } else {
1293 Ok(AtomicFact::NotRestrictFact(NotRestrictFact::new(
1294 a0, a1, line_file,
1295 )))
1296 }
1297 }
1298 _ => {
1299 if is_true {
1300 Ok(AtomicFact::NormalAtomicFact(NormalAtomicFact::new(
1301 prop_name, args, line_file,
1302 )))
1303 } else {
1304 Ok(AtomicFact::NotNormalAtomicFact(NotNormalAtomicFact::new(
1305 prop_name, args, line_file,
1306 )))
1307 }
1308 }
1309 }
1310 }
1311}
1312
1313impl AtomicFact {
1314 pub fn args(&self) -> Vec<Obj> {
1315 match self {
1316 AtomicFact::NormalAtomicFact(normal_atomic_fact) => normal_atomic_fact.body.clone(),
1317 AtomicFact::EqualFact(equal_fact) => {
1318 vec![equal_fact.left.clone(), equal_fact.right.clone()]
1319 }
1320 AtomicFact::LessFact(less_fact) => {
1321 vec![less_fact.left.clone(), less_fact.right.clone()]
1322 }
1323 AtomicFact::GreaterFact(greater_fact) => {
1324 vec![greater_fact.left.clone(), greater_fact.right.clone()]
1325 }
1326 AtomicFact::LessEqualFact(less_equal_fact) => {
1327 vec![less_equal_fact.left.clone(), less_equal_fact.right.clone()]
1328 }
1329 AtomicFact::GreaterEqualFact(greater_equal_fact) => vec![
1330 greater_equal_fact.left.clone(),
1331 greater_equal_fact.right.clone(),
1332 ],
1333 AtomicFact::IsSetFact(is_set_fact) => vec![is_set_fact.set.clone()],
1334 AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => {
1335 vec![is_nonempty_set_fact.set.clone()]
1336 }
1337 AtomicFact::IsFiniteSetFact(is_finite_set_fact) => vec![is_finite_set_fact.set.clone()],
1338 AtomicFact::InFact(in_fact) => vec![in_fact.element.clone(), in_fact.set.clone()],
1339 AtomicFact::IsCartFact(is_cart_fact) => vec![is_cart_fact.set.clone()],
1340 AtomicFact::IsTupleFact(is_tuple_fact) => vec![is_tuple_fact.set.clone()],
1341 AtomicFact::SubsetFact(subset_fact) => {
1342 vec![subset_fact.left.clone(), subset_fact.right.clone()]
1343 }
1344 AtomicFact::SupersetFact(superset_fact) => {
1345 vec![superset_fact.left.clone(), superset_fact.right.clone()]
1346 }
1347 AtomicFact::NotNormalAtomicFact(not_normal_atomic_fact) => {
1348 not_normal_atomic_fact.body.clone()
1349 }
1350 AtomicFact::NotEqualFact(not_equal_fact) => {
1351 vec![not_equal_fact.left.clone(), not_equal_fact.right.clone()]
1352 }
1353 AtomicFact::NotLessFact(not_less_fact) => {
1354 vec![not_less_fact.left.clone(), not_less_fact.right.clone()]
1355 }
1356 AtomicFact::NotGreaterFact(not_greater_fact) => vec![
1357 not_greater_fact.left.clone(),
1358 not_greater_fact.right.clone(),
1359 ],
1360 AtomicFact::NotLessEqualFact(not_less_equal_fact) => vec![
1361 not_less_equal_fact.left.clone(),
1362 not_less_equal_fact.right.clone(),
1363 ],
1364 AtomicFact::NotGreaterEqualFact(not_greater_equal_fact) => vec![
1365 not_greater_equal_fact.left.clone(),
1366 not_greater_equal_fact.right.clone(),
1367 ],
1368 AtomicFact::NotIsSetFact(not_is_set_fact) => vec![not_is_set_fact.set.clone()],
1369 AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => {
1370 vec![not_is_nonempty_set_fact.set.clone()]
1371 }
1372 AtomicFact::NotIsFiniteSetFact(not_is_finite_set_fact) => {
1373 vec![not_is_finite_set_fact.set.clone()]
1374 }
1375 AtomicFact::NotInFact(not_in_fact) => {
1376 vec![not_in_fact.element.clone(), not_in_fact.set.clone()]
1377 }
1378 AtomicFact::NotIsCartFact(not_is_cart_fact) => vec![not_is_cart_fact.set.clone()],
1379 AtomicFact::NotIsTupleFact(not_is_tuple_fact) => vec![not_is_tuple_fact.set.clone()],
1380 AtomicFact::NotSubsetFact(not_subset_fact) => {
1381 vec![not_subset_fact.left.clone(), not_subset_fact.right.clone()]
1382 }
1383 AtomicFact::NotSupersetFact(not_superset_fact) => vec![
1384 not_superset_fact.left.clone(),
1385 not_superset_fact.right.clone(),
1386 ],
1387 AtomicFact::RestrictFact(restrict_fact) => vec![
1388 restrict_fact.obj.clone(),
1389 restrict_fact.obj_can_restrict_to_fn_set.clone().into(),
1390 ],
1391 AtomicFact::NotRestrictFact(not_restrict_fact) => vec![
1392 not_restrict_fact.obj.clone(),
1393 not_restrict_fact.obj_cannot_restrict_to_fn_set.clone(),
1394 ],
1395 }
1396 }
1397}
1398
1399impl AtomicFact {
1401 pub fn is_builtin_predicate_and_return_expected_args_len(&self) -> usize {
1402 match self {
1403 AtomicFact::EqualFact(_) => 2,
1404 AtomicFact::LessFact(_) => 2,
1405 AtomicFact::GreaterFact(_) => 2,
1406 AtomicFact::LessEqualFact(_) => 2,
1407 AtomicFact::GreaterEqualFact(_) => 2,
1408 AtomicFact::IsSetFact(_) => 1,
1409 AtomicFact::IsNonemptySetFact(_) => 1,
1410 AtomicFact::IsFiniteSetFact(_) => 1,
1411 AtomicFact::InFact(_) => 2,
1412 AtomicFact::IsCartFact(_) => 1,
1413 AtomicFact::IsTupleFact(_) => 1,
1414 AtomicFact::SubsetFact(_) => 2,
1415 AtomicFact::SupersetFact(_) => 2,
1416 AtomicFact::NotEqualFact(_) => 2,
1417 AtomicFact::NotLessFact(_) => 2,
1418 AtomicFact::NotGreaterFact(_) => 2,
1419 AtomicFact::NotLessEqualFact(_) => 2,
1420 AtomicFact::NotGreaterEqualFact(_) => 2,
1421 AtomicFact::NotIsSetFact(_) => 1,
1422 AtomicFact::NotIsNonemptySetFact(_) => 1,
1423 AtomicFact::NotIsFiniteSetFact(_) => 1,
1424 AtomicFact::NotInFact(_) => 2,
1425 AtomicFact::NotIsCartFact(_) => 1,
1426 AtomicFact::NotIsTupleFact(_) => 1,
1427 AtomicFact::NotSubsetFact(_) => 2,
1428 AtomicFact::NotSupersetFact(_) => 2,
1429 AtomicFact::RestrictFact(_) => 2,
1430 AtomicFact::NotRestrictFact(_) => 2,
1431 _ => unreachable!("其他情况不是builtin predicate"),
1432 }
1433 }
1434}
1435
1436impl AtomicFact {
1437 pub fn number_of_args(&self) -> usize {
1438 match self {
1439 AtomicFact::EqualFact(_) => 2,
1440 AtomicFact::LessFact(_) => 2,
1441 AtomicFact::GreaterFact(_) => 2,
1442 AtomicFact::LessEqualFact(_) => 2,
1443 AtomicFact::GreaterEqualFact(_) => 2,
1444 AtomicFact::IsSetFact(_) => 1,
1445 AtomicFact::IsNonemptySetFact(_) => 1,
1446 AtomicFact::IsFiniteSetFact(_) => 1,
1447 AtomicFact::InFact(_) => 2,
1448 AtomicFact::IsCartFact(_) => 1,
1449 AtomicFact::IsTupleFact(_) => 1,
1450 AtomicFact::SubsetFact(_) => 2,
1451 AtomicFact::SupersetFact(_) => 2,
1452 AtomicFact::NotEqualFact(_) => 2,
1453 AtomicFact::NotLessFact(_) => 2,
1454 AtomicFact::NotGreaterFact(_) => 2,
1455 AtomicFact::NotLessEqualFact(_) => 2,
1456 AtomicFact::NotGreaterEqualFact(_) => 2,
1457 AtomicFact::NotIsSetFact(_) => 1,
1458 AtomicFact::NotIsNonemptySetFact(_) => 1,
1459 AtomicFact::NotIsFiniteSetFact(_) => 1,
1460 AtomicFact::NotInFact(_) => 2,
1461 AtomicFact::NotIsCartFact(_) => 1,
1462 AtomicFact::NotIsTupleFact(_) => 1,
1463 AtomicFact::NotSubsetFact(_) => 2,
1464 AtomicFact::NotSupersetFact(_) => 2,
1465 AtomicFact::NormalAtomicFact(a) => a.body.len(),
1466 AtomicFact::NotNormalAtomicFact(a) => a.body.len(),
1467 AtomicFact::RestrictFact(_) => 2,
1468 AtomicFact::NotRestrictFact(_) => 2,
1469 }
1470 }
1471
1472 pub fn line_file(&self) -> LineFile {
1473 match self {
1474 AtomicFact::EqualFact(a) => a.line_file.clone(),
1475 AtomicFact::LessFact(a) => a.line_file.clone(),
1476 AtomicFact::GreaterFact(a) => a.line_file.clone(),
1477 AtomicFact::LessEqualFact(a) => a.line_file.clone(),
1478 AtomicFact::GreaterEqualFact(a) => a.line_file.clone(),
1479 AtomicFact::IsSetFact(a) => a.line_file.clone(),
1480 AtomicFact::IsNonemptySetFact(a) => a.line_file.clone(),
1481 AtomicFact::IsFiniteSetFact(a) => a.line_file.clone(),
1482 AtomicFact::InFact(a) => a.line_file.clone(),
1483 AtomicFact::IsCartFact(a) => a.line_file.clone(),
1484 AtomicFact::IsTupleFact(a) => a.line_file.clone(),
1485 AtomicFact::SubsetFact(a) => a.line_file.clone(),
1486 AtomicFact::SupersetFact(a) => a.line_file.clone(),
1487 AtomicFact::NormalAtomicFact(a) => a.line_file.clone(),
1488 AtomicFact::NotNormalAtomicFact(a) => a.line_file.clone(),
1489 AtomicFact::NotEqualFact(a) => a.line_file.clone(),
1490 AtomicFact::NotLessFact(a) => a.line_file.clone(),
1491 AtomicFact::NotGreaterFact(a) => a.line_file.clone(),
1492 AtomicFact::NotLessEqualFact(a) => a.line_file.clone(),
1493 AtomicFact::NotGreaterEqualFact(a) => a.line_file.clone(),
1494 AtomicFact::NotIsSetFact(a) => a.line_file.clone(),
1495 AtomicFact::NotIsNonemptySetFact(a) => a.line_file.clone(),
1496 AtomicFact::NotIsFiniteSetFact(a) => a.line_file.clone(),
1497 AtomicFact::NotInFact(a) => a.line_file.clone(),
1498 AtomicFact::NotIsCartFact(a) => a.line_file.clone(),
1499 AtomicFact::NotIsTupleFact(a) => a.line_file.clone(),
1500 AtomicFact::NotSubsetFact(a) => a.line_file.clone(),
1501 AtomicFact::NotSupersetFact(a) => a.line_file.clone(),
1502 AtomicFact::RestrictFact(a) => a.line_file.clone(),
1503 AtomicFact::NotRestrictFact(a) => a.line_file.clone(),
1504 }
1505 }
1506
1507 pub fn with_new_line_file(self, line_file: LineFile) -> Self {
1508 match self {
1509 AtomicFact::EqualFact(x) => {
1510 AtomicFact::EqualFact(EqualFact::new(x.left, x.right, line_file))
1511 }
1512 AtomicFact::LessFact(x) => {
1513 AtomicFact::LessFact(LessFact::new(x.left, x.right, line_file))
1514 }
1515 AtomicFact::GreaterFact(x) => {
1516 AtomicFact::GreaterFact(GreaterFact::new(x.left, x.right, line_file))
1517 }
1518 AtomicFact::LessEqualFact(x) => {
1519 AtomicFact::LessEqualFact(LessEqualFact::new(x.left, x.right, line_file))
1520 }
1521 AtomicFact::GreaterEqualFact(x) => {
1522 AtomicFact::GreaterEqualFact(GreaterEqualFact::new(x.left, x.right, line_file))
1523 }
1524 AtomicFact::IsSetFact(x) => AtomicFact::IsSetFact(IsSetFact::new(x.set, line_file)),
1525 AtomicFact::IsNonemptySetFact(x) => {
1526 AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(x.set, line_file))
1527 }
1528 AtomicFact::IsFiniteSetFact(x) => {
1529 AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(x.set, line_file))
1530 }
1531 AtomicFact::InFact(x) => AtomicFact::InFact(InFact::new(x.element, x.set, line_file)),
1532 AtomicFact::IsCartFact(x) => AtomicFact::IsCartFact(IsCartFact::new(x.set, line_file)),
1533 AtomicFact::IsTupleFact(x) => {
1534 AtomicFact::IsTupleFact(IsTupleFact::new(x.set, line_file))
1535 }
1536 AtomicFact::SubsetFact(x) => {
1537 AtomicFact::SubsetFact(SubsetFact::new(x.left, x.right, line_file))
1538 }
1539 AtomicFact::SupersetFact(x) => {
1540 AtomicFact::SupersetFact(SupersetFact::new(x.left, x.right, line_file))
1541 }
1542 AtomicFact::NormalAtomicFact(x) => {
1543 AtomicFact::NormalAtomicFact(NormalAtomicFact::new(x.predicate, x.body, line_file))
1544 }
1545 AtomicFact::NotNormalAtomicFact(x) => AtomicFact::NotNormalAtomicFact(
1546 NotNormalAtomicFact::new(x.predicate, x.body, line_file),
1547 ),
1548 AtomicFact::NotEqualFact(x) => {
1549 AtomicFact::NotEqualFact(NotEqualFact::new(x.left, x.right, line_file))
1550 }
1551 AtomicFact::NotLessFact(x) => {
1552 AtomicFact::NotLessFact(NotLessFact::new(x.left, x.right, line_file))
1553 }
1554 AtomicFact::NotGreaterFact(x) => {
1555 AtomicFact::NotGreaterFact(NotGreaterFact::new(x.left, x.right, line_file))
1556 }
1557 AtomicFact::NotLessEqualFact(x) => {
1558 AtomicFact::NotLessEqualFact(NotLessEqualFact::new(x.left, x.right, line_file))
1559 }
1560 AtomicFact::NotGreaterEqualFact(x) => AtomicFact::NotGreaterEqualFact(
1561 NotGreaterEqualFact::new(x.left, x.right, line_file),
1562 ),
1563 AtomicFact::NotIsSetFact(x) => {
1564 AtomicFact::NotIsSetFact(NotIsSetFact::new(x.set, line_file))
1565 }
1566 AtomicFact::NotIsNonemptySetFact(x) => {
1567 AtomicFact::NotIsNonemptySetFact(NotIsNonemptySetFact::new(x.set, line_file))
1568 }
1569 AtomicFact::NotIsFiniteSetFact(x) => {
1570 AtomicFact::NotIsFiniteSetFact(NotIsFiniteSetFact::new(x.set, line_file))
1571 }
1572 AtomicFact::NotInFact(x) => {
1573 AtomicFact::NotInFact(NotInFact::new(x.element, x.set, line_file))
1574 }
1575 AtomicFact::NotIsCartFact(x) => {
1576 AtomicFact::NotIsCartFact(NotIsCartFact::new(x.set, line_file))
1577 }
1578 AtomicFact::NotIsTupleFact(x) => {
1579 AtomicFact::NotIsTupleFact(NotIsTupleFact::new(x.set, line_file))
1580 }
1581 AtomicFact::NotSubsetFact(x) => {
1582 AtomicFact::NotSubsetFact(NotSubsetFact::new(x.left, x.right, line_file))
1583 }
1584 AtomicFact::NotSupersetFact(x) => {
1585 AtomicFact::NotSupersetFact(NotSupersetFact::new(x.left, x.right, line_file))
1586 }
1587 AtomicFact::RestrictFact(x) => AtomicFact::RestrictFact(RestrictFact::new(
1588 x.obj,
1589 x.obj_can_restrict_to_fn_set,
1590 line_file,
1591 )),
1592 AtomicFact::NotRestrictFact(x) => AtomicFact::NotRestrictFact(NotRestrictFact::new(
1593 x.obj,
1594 x.obj_cannot_restrict_to_fn_set,
1595 line_file,
1596 )),
1597 }
1598 }
1599}
1600
1601impl RestrictFact {
1602 pub fn new(obj: Obj, obj_can_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1603 RestrictFact {
1604 obj,
1605 obj_can_restrict_to_fn_set,
1606 line_file,
1607 }
1608 }
1609}
1610
1611impl NotRestrictFact {
1612 pub fn new(obj: Obj, obj_cannot_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1613 NotRestrictFact {
1614 obj,
1615 obj_cannot_restrict_to_fn_set,
1616 line_file,
1617 }
1618 }
1619}
1620
1621impl fmt::Display for RestrictFact {
1622 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1623 write!(
1624 f,
1625 "{} {}{} {}",
1626 self.obj, FACT_PREFIX, RESTRICT, self.obj_can_restrict_to_fn_set
1627 )
1628 }
1629}
1630
1631impl fmt::Display for NotRestrictFact {
1632 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1633 write!(
1634 f,
1635 "{} {} {}{} {}",
1636 NOT, self.obj, FACT_PREFIX, RESTRICT, self.obj_cannot_restrict_to_fn_set
1637 )
1638 }
1639}
1640
1641impl AtomicFact {
1642 pub fn get_args_from_fact(&self) -> Vec<Obj> {
1643 self.args()
1644 }
1645}
1646
1647impl AtomicFact {
1648 pub fn make_reversed(&self) -> AtomicFact {
1649 match self {
1650 AtomicFact::NormalAtomicFact(a) => AtomicFact::NotNormalAtomicFact(
1651 NotNormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1652 ),
1653 AtomicFact::NotNormalAtomicFact(a) => AtomicFact::NormalAtomicFact(
1654 NormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1655 ),
1656 AtomicFact::EqualFact(a) => AtomicFact::NotEqualFact(NotEqualFact::new(
1657 a.left.clone(),
1658 a.right.clone(),
1659 a.line_file.clone(),
1660 )),
1661 AtomicFact::LessFact(a) => AtomicFact::NotLessFact(NotLessFact::new(
1662 a.left.clone(),
1663 a.right.clone(),
1664 a.line_file.clone(),
1665 )),
1666 AtomicFact::GreaterFact(a) => AtomicFact::NotGreaterFact(NotGreaterFact::new(
1667 a.left.clone(),
1668 a.right.clone(),
1669 a.line_file.clone(),
1670 )),
1671 AtomicFact::LessEqualFact(a) => AtomicFact::NotLessEqualFact(NotLessEqualFact::new(
1672 a.left.clone(),
1673 a.right.clone(),
1674 a.line_file.clone(),
1675 )),
1676 AtomicFact::GreaterEqualFact(a) => AtomicFact::NotGreaterEqualFact(
1677 NotGreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1678 ),
1679 AtomicFact::IsSetFact(a) => {
1680 AtomicFact::NotIsSetFact(NotIsSetFact::new(a.set.clone(), a.line_file.clone()))
1681 }
1682 AtomicFact::IsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1683 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1684 ),
1685 AtomicFact::IsFiniteSetFact(a) => AtomicFact::NotIsFiniteSetFact(
1686 NotIsFiniteSetFact::new(a.set.clone(), a.line_file.clone()),
1687 ),
1688 AtomicFact::InFact(a) => AtomicFact::NotInFact(NotInFact::new(
1689 a.element.clone(),
1690 a.set.clone(),
1691 a.line_file.clone(),
1692 )),
1693 AtomicFact::IsCartFact(a) => {
1694 AtomicFact::NotIsCartFact(NotIsCartFact::new(a.set.clone(), a.line_file.clone()))
1695 }
1696 AtomicFact::IsTupleFact(a) => {
1697 AtomicFact::NotIsTupleFact(NotIsTupleFact::new(a.set.clone(), a.line_file.clone()))
1698 }
1699 AtomicFact::SubsetFact(a) => AtomicFact::NotSubsetFact(NotSubsetFact::new(
1700 a.left.clone(),
1701 a.right.clone(),
1702 a.line_file.clone(),
1703 )),
1704 AtomicFact::SupersetFact(a) => AtomicFact::NotSupersetFact(NotSupersetFact::new(
1705 a.left.clone(),
1706 a.right.clone(),
1707 a.line_file.clone(),
1708 )),
1709 AtomicFact::RestrictFact(a) => AtomicFact::NotRestrictFact(NotRestrictFact::new(
1710 a.obj.clone(),
1711 a.obj_can_restrict_to_fn_set.clone(),
1712 a.line_file.clone(),
1713 )),
1714 AtomicFact::NotEqualFact(a) => AtomicFact::EqualFact(EqualFact::new(
1715 a.left.clone(),
1716 a.right.clone(),
1717 a.line_file.clone(),
1718 )),
1719 AtomicFact::NotLessFact(a) => AtomicFact::LessFact(LessFact::new(
1720 a.left.clone(),
1721 a.right.clone(),
1722 a.line_file.clone(),
1723 )),
1724 AtomicFact::NotGreaterFact(a) => AtomicFact::GreaterFact(GreaterFact::new(
1725 a.left.clone(),
1726 a.right.clone(),
1727 a.line_file.clone(),
1728 )),
1729 AtomicFact::NotLessEqualFact(a) => AtomicFact::LessEqualFact(LessEqualFact::new(
1730 a.left.clone(),
1731 a.right.clone(),
1732 a.line_file.clone(),
1733 )),
1734 AtomicFact::NotGreaterEqualFact(a) => AtomicFact::GreaterEqualFact(
1735 GreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1736 ),
1737 AtomicFact::NotIsSetFact(a) => {
1738 AtomicFact::IsSetFact(IsSetFact::new(a.set.clone(), a.line_file.clone()))
1739 }
1740 AtomicFact::NotIsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1741 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1742 ),
1743 AtomicFact::NotIsFiniteSetFact(a) => AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(
1744 a.set.clone(),
1745 a.line_file.clone(),
1746 )),
1747 AtomicFact::NotInFact(a) => AtomicFact::InFact(InFact::new(
1748 a.element.clone(),
1749 a.set.clone(),
1750 a.line_file.clone(),
1751 )),
1752 AtomicFact::NotIsCartFact(a) => {
1753 AtomicFact::IsCartFact(IsCartFact::new(a.set.clone(), a.line_file.clone()))
1754 }
1755 AtomicFact::NotIsTupleFact(a) => {
1756 AtomicFact::IsTupleFact(IsTupleFact::new(a.set.clone(), a.line_file.clone()))
1757 }
1758 AtomicFact::NotSubsetFact(a) => AtomicFact::SubsetFact(SubsetFact::new(
1759 a.left.clone(),
1760 a.right.clone(),
1761 a.line_file.clone(),
1762 )),
1763 AtomicFact::NotSupersetFact(a) => AtomicFact::SupersetFact(SupersetFact::new(
1764 a.left.clone(),
1765 a.right.clone(),
1766 a.line_file.clone(),
1767 )),
1768 AtomicFact::NotRestrictFact(a) => AtomicFact::RestrictFact(RestrictFact::new(
1769 a.obj.clone(),
1770 a.obj_cannot_restrict_to_fn_set.clone(),
1771 a.line_file.clone(),
1772 )),
1773 }
1774 }
1775}
1776
1777impl AtomicFact {
1778 fn body_vec_after_calculate_each_calculable_arg(original_body: &Vec<Obj>) -> Vec<Obj> {
1779 let mut next_body = Vec::new();
1780 for obj in original_body {
1781 next_body.push(obj.replace_with_numeric_result_if_can_be_calculated().0);
1782 }
1783 next_body
1784 }
1785
1786 pub fn calculate_args(&self) -> (AtomicFact, bool) {
1787 let calculated_atomic_fact = match self {
1788 AtomicFact::NormalAtomicFact(inner) => {
1789 AtomicFact::NormalAtomicFact(NormalAtomicFact::new(
1790 inner.predicate.clone(),
1791 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1792 inner.line_file.clone(),
1793 ))
1794 }
1795 AtomicFact::NotNormalAtomicFact(inner) => {
1796 AtomicFact::NotNormalAtomicFact(NotNormalAtomicFact::new(
1797 inner.predicate.clone(),
1798 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1799 inner.line_file.clone(),
1800 ))
1801 }
1802 AtomicFact::EqualFact(inner) => AtomicFact::EqualFact(EqualFact::new(
1803 inner
1804 .left
1805 .replace_with_numeric_result_if_can_be_calculated()
1806 .0,
1807 inner
1808 .right
1809 .replace_with_numeric_result_if_can_be_calculated()
1810 .0,
1811 inner.line_file.clone(),
1812 )),
1813 AtomicFact::NotEqualFact(inner) => AtomicFact::NotEqualFact(NotEqualFact::new(
1814 inner
1815 .left
1816 .replace_with_numeric_result_if_can_be_calculated()
1817 .0,
1818 inner
1819 .right
1820 .replace_with_numeric_result_if_can_be_calculated()
1821 .0,
1822 inner.line_file.clone(),
1823 )),
1824 AtomicFact::LessFact(inner) => AtomicFact::LessFact(LessFact::new(
1825 inner
1826 .left
1827 .replace_with_numeric_result_if_can_be_calculated()
1828 .0,
1829 inner
1830 .right
1831 .replace_with_numeric_result_if_can_be_calculated()
1832 .0,
1833 inner.line_file.clone(),
1834 )),
1835 AtomicFact::NotLessFact(inner) => AtomicFact::NotLessFact(NotLessFact::new(
1836 inner
1837 .left
1838 .replace_with_numeric_result_if_can_be_calculated()
1839 .0,
1840 inner
1841 .right
1842 .replace_with_numeric_result_if_can_be_calculated()
1843 .0,
1844 inner.line_file.clone(),
1845 )),
1846 AtomicFact::GreaterFact(inner) => AtomicFact::GreaterFact(GreaterFact::new(
1847 inner
1848 .left
1849 .replace_with_numeric_result_if_can_be_calculated()
1850 .0,
1851 inner
1852 .right
1853 .replace_with_numeric_result_if_can_be_calculated()
1854 .0,
1855 inner.line_file.clone(),
1856 )),
1857 AtomicFact::NotGreaterFact(inner) => AtomicFact::NotGreaterFact(NotGreaterFact::new(
1858 inner
1859 .left
1860 .replace_with_numeric_result_if_can_be_calculated()
1861 .0,
1862 inner
1863 .right
1864 .replace_with_numeric_result_if_can_be_calculated()
1865 .0,
1866 inner.line_file.clone(),
1867 )),
1868 AtomicFact::LessEqualFact(inner) => AtomicFact::LessEqualFact(LessEqualFact::new(
1869 inner
1870 .left
1871 .replace_with_numeric_result_if_can_be_calculated()
1872 .0,
1873 inner
1874 .right
1875 .replace_with_numeric_result_if_can_be_calculated()
1876 .0,
1877 inner.line_file.clone(),
1878 )),
1879 AtomicFact::NotLessEqualFact(inner) => {
1880 AtomicFact::NotLessEqualFact(NotLessEqualFact::new(
1881 inner
1882 .left
1883 .replace_with_numeric_result_if_can_be_calculated()
1884 .0,
1885 inner
1886 .right
1887 .replace_with_numeric_result_if_can_be_calculated()
1888 .0,
1889 inner.line_file.clone(),
1890 ))
1891 }
1892 AtomicFact::GreaterEqualFact(inner) => {
1893 AtomicFact::GreaterEqualFact(GreaterEqualFact::new(
1894 inner
1895 .left
1896 .replace_with_numeric_result_if_can_be_calculated()
1897 .0,
1898 inner
1899 .right
1900 .replace_with_numeric_result_if_can_be_calculated()
1901 .0,
1902 inner.line_file.clone(),
1903 ))
1904 }
1905 AtomicFact::NotGreaterEqualFact(inner) => {
1906 AtomicFact::NotGreaterEqualFact(NotGreaterEqualFact::new(
1907 inner
1908 .left
1909 .replace_with_numeric_result_if_can_be_calculated()
1910 .0,
1911 inner
1912 .right
1913 .replace_with_numeric_result_if_can_be_calculated()
1914 .0,
1915 inner.line_file.clone(),
1916 ))
1917 }
1918 AtomicFact::IsSetFact(inner) => AtomicFact::IsSetFact(IsSetFact::new(
1919 inner
1920 .set
1921 .replace_with_numeric_result_if_can_be_calculated()
1922 .0,
1923 inner.line_file.clone(),
1924 )),
1925 AtomicFact::NotIsSetFact(inner) => AtomicFact::NotIsSetFact(NotIsSetFact::new(
1926 inner
1927 .set
1928 .replace_with_numeric_result_if_can_be_calculated()
1929 .0,
1930 inner.line_file.clone(),
1931 )),
1932 AtomicFact::IsNonemptySetFact(inner) => {
1933 AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(
1934 inner
1935 .set
1936 .replace_with_numeric_result_if_can_be_calculated()
1937 .0,
1938 inner.line_file.clone(),
1939 ))
1940 }
1941 AtomicFact::NotIsNonemptySetFact(inner) => {
1942 AtomicFact::NotIsNonemptySetFact(NotIsNonemptySetFact::new(
1943 inner
1944 .set
1945 .replace_with_numeric_result_if_can_be_calculated()
1946 .0,
1947 inner.line_file.clone(),
1948 ))
1949 }
1950 AtomicFact::IsFiniteSetFact(inner) => {
1951 AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(
1952 inner
1953 .set
1954 .replace_with_numeric_result_if_can_be_calculated()
1955 .0,
1956 inner.line_file.clone(),
1957 ))
1958 }
1959 AtomicFact::NotIsFiniteSetFact(inner) => {
1960 AtomicFact::NotIsFiniteSetFact(NotIsFiniteSetFact::new(
1961 inner
1962 .set
1963 .replace_with_numeric_result_if_can_be_calculated()
1964 .0,
1965 inner.line_file.clone(),
1966 ))
1967 }
1968 AtomicFact::InFact(inner) => AtomicFact::InFact(InFact::new(
1969 inner
1970 .element
1971 .replace_with_numeric_result_if_can_be_calculated()
1972 .0,
1973 inner
1974 .set
1975 .replace_with_numeric_result_if_can_be_calculated()
1976 .0,
1977 inner.line_file.clone(),
1978 )),
1979 AtomicFact::NotInFact(inner) => AtomicFact::NotInFact(NotInFact::new(
1980 inner
1981 .element
1982 .replace_with_numeric_result_if_can_be_calculated()
1983 .0,
1984 inner
1985 .set
1986 .replace_with_numeric_result_if_can_be_calculated()
1987 .0,
1988 inner.line_file.clone(),
1989 )),
1990 AtomicFact::IsCartFact(inner) => AtomicFact::IsCartFact(IsCartFact::new(
1991 inner
1992 .set
1993 .replace_with_numeric_result_if_can_be_calculated()
1994 .0,
1995 inner.line_file.clone(),
1996 )),
1997 AtomicFact::NotIsCartFact(inner) => AtomicFact::NotIsCartFact(NotIsCartFact::new(
1998 inner
1999 .set
2000 .replace_with_numeric_result_if_can_be_calculated()
2001 .0,
2002 inner.line_file.clone(),
2003 )),
2004 AtomicFact::IsTupleFact(inner) => AtomicFact::IsTupleFact(IsTupleFact::new(
2005 inner
2006 .set
2007 .replace_with_numeric_result_if_can_be_calculated()
2008 .0,
2009 inner.line_file.clone(),
2010 )),
2011 AtomicFact::NotIsTupleFact(inner) => AtomicFact::NotIsTupleFact(NotIsTupleFact::new(
2012 inner
2013 .set
2014 .replace_with_numeric_result_if_can_be_calculated()
2015 .0,
2016 inner.line_file.clone(),
2017 )),
2018 AtomicFact::SubsetFact(inner) => AtomicFact::SubsetFact(SubsetFact::new(
2019 inner
2020 .left
2021 .replace_with_numeric_result_if_can_be_calculated()
2022 .0,
2023 inner
2024 .right
2025 .replace_with_numeric_result_if_can_be_calculated()
2026 .0,
2027 inner.line_file.clone(),
2028 )),
2029 AtomicFact::NotSubsetFact(inner) => AtomicFact::NotSubsetFact(NotSubsetFact::new(
2030 inner
2031 .left
2032 .replace_with_numeric_result_if_can_be_calculated()
2033 .0,
2034 inner
2035 .right
2036 .replace_with_numeric_result_if_can_be_calculated()
2037 .0,
2038 inner.line_file.clone(),
2039 )),
2040 AtomicFact::SupersetFact(inner) => AtomicFact::SupersetFact(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 AtomicFact::NotSupersetFact(inner) => {
2052 AtomicFact::NotSupersetFact(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 }
2064 AtomicFact::RestrictFact(inner) => AtomicFact::RestrictFact(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 AtomicFact::NotRestrictFact(inner) => {
2076 AtomicFact::NotRestrictFact(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 }
2088 };
2089 let any_argument_replaced = calculated_atomic_fact.to_string() != self.to_string();
2090 (calculated_atomic_fact, any_argument_replaced)
2091 }
2092}