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
1522impl RestrictFact {
1523 pub fn new(obj: Obj, obj_can_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1524 RestrictFact {
1525 obj,
1526 obj_can_restrict_to_fn_set,
1527 line_file,
1528 }
1529 }
1530}
1531
1532impl NotRestrictFact {
1533 pub fn new(obj: Obj, obj_cannot_restrict_to_fn_set: Obj, line_file: LineFile) -> Self {
1534 NotRestrictFact {
1535 obj,
1536 obj_cannot_restrict_to_fn_set,
1537 line_file,
1538 }
1539 }
1540}
1541
1542impl fmt::Display for RestrictFact {
1543 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1544 write!(
1545 f,
1546 "{} {}{} {}",
1547 self.obj, FACT_PREFIX, RESTRICT, self.obj_can_restrict_to_fn_set
1548 )
1549 }
1550}
1551
1552impl fmt::Display for NotRestrictFact {
1553 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1554 write!(
1555 f,
1556 "{} {} {}{} {}",
1557 NOT, self.obj, FACT_PREFIX, RESTRICT, self.obj_cannot_restrict_to_fn_set
1558 )
1559 }
1560}
1561
1562impl AtomicFact {
1563 pub fn get_args_from_fact(&self) -> Vec<Obj> {
1564 self.args()
1565 }
1566}
1567
1568impl AtomicFact {
1569 pub fn make_reversed(&self) -> AtomicFact {
1570 match self {
1571 AtomicFact::NormalAtomicFact(a) => AtomicFact::NotNormalAtomicFact(
1572 NotNormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1573 ),
1574 AtomicFact::NotNormalAtomicFact(a) => AtomicFact::NormalAtomicFact(
1575 NormalAtomicFact::new(a.predicate.clone(), a.body.clone(), a.line_file.clone()),
1576 ),
1577 AtomicFact::EqualFact(a) => {
1578 NotEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1579 }
1580 AtomicFact::LessFact(a) => {
1581 NotLessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1582 }
1583 AtomicFact::GreaterFact(a) => {
1584 NotGreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1585 }
1586 AtomicFact::LessEqualFact(a) => {
1587 NotLessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1588 }
1589 AtomicFact::GreaterEqualFact(a) => AtomicFact::NotGreaterEqualFact(
1590 NotGreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1591 ),
1592 AtomicFact::IsSetFact(a) => {
1593 NotIsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1594 }
1595 AtomicFact::IsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1596 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1597 ),
1598 AtomicFact::IsFiniteSetFact(a) => AtomicFact::NotIsFiniteSetFact(
1599 NotIsFiniteSetFact::new(a.set.clone(), a.line_file.clone()),
1600 ),
1601 AtomicFact::InFact(a) => {
1602 NotInFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1603 }
1604 AtomicFact::IsCartFact(a) => {
1605 NotIsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1606 }
1607 AtomicFact::IsTupleFact(a) => {
1608 NotIsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1609 }
1610 AtomicFact::SubsetFact(a) => {
1611 NotSubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1612 }
1613 AtomicFact::SupersetFact(a) => {
1614 NotSupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1615 }
1616 AtomicFact::RestrictFact(a) => NotRestrictFact::new(
1617 a.obj.clone(),
1618 a.obj_can_restrict_to_fn_set.clone(),
1619 a.line_file.clone(),
1620 )
1621 .into(),
1622 AtomicFact::NotEqualFact(a) => {
1623 EqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1624 }
1625 AtomicFact::NotLessFact(a) => {
1626 LessFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1627 }
1628 AtomicFact::NotGreaterFact(a) => {
1629 GreaterFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1630 }
1631 AtomicFact::NotLessEqualFact(a) => {
1632 LessEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1633 }
1634 AtomicFact::NotGreaterEqualFact(a) => AtomicFact::GreaterEqualFact(
1635 GreaterEqualFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()),
1636 ),
1637 AtomicFact::NotIsSetFact(a) => {
1638 IsSetFact::new(a.set.clone(), a.line_file.clone()).into()
1639 }
1640 AtomicFact::NotIsNonemptySetFact(a) => AtomicFact::IsNonemptySetFact(
1641 IsNonemptySetFact::new(a.set.clone(), a.line_file.clone()),
1642 ),
1643 AtomicFact::NotIsFiniteSetFact(a) => {
1644 IsFiniteSetFact::new(a.set.clone(), a.line_file.clone()).into()
1645 }
1646 AtomicFact::NotInFact(a) => {
1647 InFact::new(a.element.clone(), a.set.clone(), a.line_file.clone()).into()
1648 }
1649 AtomicFact::NotIsCartFact(a) => {
1650 IsCartFact::new(a.set.clone(), a.line_file.clone()).into()
1651 }
1652 AtomicFact::NotIsTupleFact(a) => {
1653 IsTupleFact::new(a.set.clone(), a.line_file.clone()).into()
1654 }
1655 AtomicFact::NotSubsetFact(a) => {
1656 SubsetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1657 }
1658 AtomicFact::NotSupersetFact(a) => {
1659 SupersetFact::new(a.left.clone(), a.right.clone(), a.line_file.clone()).into()
1660 }
1661 AtomicFact::NotRestrictFact(a) => RestrictFact::new(
1662 a.obj.clone(),
1663 a.obj_cannot_restrict_to_fn_set.clone(),
1664 a.line_file.clone(),
1665 )
1666 .into(),
1667 }
1668 }
1669}
1670
1671impl AtomicFact {
1672 fn body_vec_after_calculate_each_calculable_arg(original_body: &Vec<Obj>) -> Vec<Obj> {
1673 let mut next_body = Vec::new();
1674 for obj in original_body {
1675 next_body.push(obj.replace_with_numeric_result_if_can_be_calculated().0);
1676 }
1677 next_body
1678 }
1679
1680 pub fn calculate_args(&self) -> (AtomicFact, bool) {
1681 let calculated_atomic_fact: AtomicFact = match self {
1682 AtomicFact::NormalAtomicFact(inner) => NormalAtomicFact::new(
1683 inner.predicate.clone(),
1684 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1685 inner.line_file.clone(),
1686 )
1687 .into(),
1688 AtomicFact::NotNormalAtomicFact(inner) => NotNormalAtomicFact::new(
1689 inner.predicate.clone(),
1690 Self::body_vec_after_calculate_each_calculable_arg(&inner.body),
1691 inner.line_file.clone(),
1692 )
1693 .into(),
1694 AtomicFact::EqualFact(inner) => EqualFact::new(
1695 inner
1696 .left
1697 .replace_with_numeric_result_if_can_be_calculated()
1698 .0,
1699 inner
1700 .right
1701 .replace_with_numeric_result_if_can_be_calculated()
1702 .0,
1703 inner.line_file.clone(),
1704 )
1705 .into(),
1706 AtomicFact::NotEqualFact(inner) => NotEqualFact::new(
1707 inner
1708 .left
1709 .replace_with_numeric_result_if_can_be_calculated()
1710 .0,
1711 inner
1712 .right
1713 .replace_with_numeric_result_if_can_be_calculated()
1714 .0,
1715 inner.line_file.clone(),
1716 )
1717 .into(),
1718 AtomicFact::LessFact(inner) => LessFact::new(
1719 inner
1720 .left
1721 .replace_with_numeric_result_if_can_be_calculated()
1722 .0,
1723 inner
1724 .right
1725 .replace_with_numeric_result_if_can_be_calculated()
1726 .0,
1727 inner.line_file.clone(),
1728 )
1729 .into(),
1730 AtomicFact::NotLessFact(inner) => NotLessFact::new(
1731 inner
1732 .left
1733 .replace_with_numeric_result_if_can_be_calculated()
1734 .0,
1735 inner
1736 .right
1737 .replace_with_numeric_result_if_can_be_calculated()
1738 .0,
1739 inner.line_file.clone(),
1740 )
1741 .into(),
1742 AtomicFact::GreaterFact(inner) => GreaterFact::new(
1743 inner
1744 .left
1745 .replace_with_numeric_result_if_can_be_calculated()
1746 .0,
1747 inner
1748 .right
1749 .replace_with_numeric_result_if_can_be_calculated()
1750 .0,
1751 inner.line_file.clone(),
1752 )
1753 .into(),
1754 AtomicFact::NotGreaterFact(inner) => NotGreaterFact::new(
1755 inner
1756 .left
1757 .replace_with_numeric_result_if_can_be_calculated()
1758 .0,
1759 inner
1760 .right
1761 .replace_with_numeric_result_if_can_be_calculated()
1762 .0,
1763 inner.line_file.clone(),
1764 )
1765 .into(),
1766 AtomicFact::LessEqualFact(inner) => LessEqualFact::new(
1767 inner
1768 .left
1769 .replace_with_numeric_result_if_can_be_calculated()
1770 .0,
1771 inner
1772 .right
1773 .replace_with_numeric_result_if_can_be_calculated()
1774 .0,
1775 inner.line_file.clone(),
1776 )
1777 .into(),
1778 AtomicFact::NotLessEqualFact(inner) => NotLessEqualFact::new(
1779 inner
1780 .left
1781 .replace_with_numeric_result_if_can_be_calculated()
1782 .0,
1783 inner
1784 .right
1785 .replace_with_numeric_result_if_can_be_calculated()
1786 .0,
1787 inner.line_file.clone(),
1788 )
1789 .into(),
1790 AtomicFact::GreaterEqualFact(inner) => GreaterEqualFact::new(
1791 inner
1792 .left
1793 .replace_with_numeric_result_if_can_be_calculated()
1794 .0,
1795 inner
1796 .right
1797 .replace_with_numeric_result_if_can_be_calculated()
1798 .0,
1799 inner.line_file.clone(),
1800 )
1801 .into(),
1802 AtomicFact::NotGreaterEqualFact(inner) => NotGreaterEqualFact::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 .into(),
1814 AtomicFact::IsSetFact(inner) => IsSetFact::new(
1815 inner
1816 .set
1817 .replace_with_numeric_result_if_can_be_calculated()
1818 .0,
1819 inner.line_file.clone(),
1820 )
1821 .into(),
1822 AtomicFact::NotIsSetFact(inner) => NotIsSetFact::new(
1823 inner
1824 .set
1825 .replace_with_numeric_result_if_can_be_calculated()
1826 .0,
1827 inner.line_file.clone(),
1828 )
1829 .into(),
1830 AtomicFact::IsNonemptySetFact(inner) => IsNonemptySetFact::new(
1831 inner
1832 .set
1833 .replace_with_numeric_result_if_can_be_calculated()
1834 .0,
1835 inner.line_file.clone(),
1836 )
1837 .into(),
1838 AtomicFact::NotIsNonemptySetFact(inner) => NotIsNonemptySetFact::new(
1839 inner
1840 .set
1841 .replace_with_numeric_result_if_can_be_calculated()
1842 .0,
1843 inner.line_file.clone(),
1844 )
1845 .into(),
1846 AtomicFact::IsFiniteSetFact(inner) => IsFiniteSetFact::new(
1847 inner
1848 .set
1849 .replace_with_numeric_result_if_can_be_calculated()
1850 .0,
1851 inner.line_file.clone(),
1852 )
1853 .into(),
1854 AtomicFact::NotIsFiniteSetFact(inner) => NotIsFiniteSetFact::new(
1855 inner
1856 .set
1857 .replace_with_numeric_result_if_can_be_calculated()
1858 .0,
1859 inner.line_file.clone(),
1860 )
1861 .into(),
1862 AtomicFact::InFact(inner) => InFact::new(
1863 inner
1864 .element
1865 .replace_with_numeric_result_if_can_be_calculated()
1866 .0,
1867 inner
1868 .set
1869 .replace_with_numeric_result_if_can_be_calculated()
1870 .0,
1871 inner.line_file.clone(),
1872 )
1873 .into(),
1874 AtomicFact::NotInFact(inner) => NotInFact::new(
1875 inner
1876 .element
1877 .replace_with_numeric_result_if_can_be_calculated()
1878 .0,
1879 inner
1880 .set
1881 .replace_with_numeric_result_if_can_be_calculated()
1882 .0,
1883 inner.line_file.clone(),
1884 )
1885 .into(),
1886 AtomicFact::IsCartFact(inner) => IsCartFact::new(
1887 inner
1888 .set
1889 .replace_with_numeric_result_if_can_be_calculated()
1890 .0,
1891 inner.line_file.clone(),
1892 )
1893 .into(),
1894 AtomicFact::NotIsCartFact(inner) => NotIsCartFact::new(
1895 inner
1896 .set
1897 .replace_with_numeric_result_if_can_be_calculated()
1898 .0,
1899 inner.line_file.clone(),
1900 )
1901 .into(),
1902 AtomicFact::IsTupleFact(inner) => IsTupleFact::new(
1903 inner
1904 .set
1905 .replace_with_numeric_result_if_can_be_calculated()
1906 .0,
1907 inner.line_file.clone(),
1908 )
1909 .into(),
1910 AtomicFact::NotIsTupleFact(inner) => NotIsTupleFact::new(
1911 inner
1912 .set
1913 .replace_with_numeric_result_if_can_be_calculated()
1914 .0,
1915 inner.line_file.clone(),
1916 )
1917 .into(),
1918 AtomicFact::SubsetFact(inner) => SubsetFact::new(
1919 inner
1920 .left
1921 .replace_with_numeric_result_if_can_be_calculated()
1922 .0,
1923 inner
1924 .right
1925 .replace_with_numeric_result_if_can_be_calculated()
1926 .0,
1927 inner.line_file.clone(),
1928 )
1929 .into(),
1930 AtomicFact::NotSubsetFact(inner) => NotSubsetFact::new(
1931 inner
1932 .left
1933 .replace_with_numeric_result_if_can_be_calculated()
1934 .0,
1935 inner
1936 .right
1937 .replace_with_numeric_result_if_can_be_calculated()
1938 .0,
1939 inner.line_file.clone(),
1940 )
1941 .into(),
1942 AtomicFact::SupersetFact(inner) => SupersetFact::new(
1943 inner
1944 .left
1945 .replace_with_numeric_result_if_can_be_calculated()
1946 .0,
1947 inner
1948 .right
1949 .replace_with_numeric_result_if_can_be_calculated()
1950 .0,
1951 inner.line_file.clone(),
1952 )
1953 .into(),
1954 AtomicFact::NotSupersetFact(inner) => NotSupersetFact::new(
1955 inner
1956 .left
1957 .replace_with_numeric_result_if_can_be_calculated()
1958 .0,
1959 inner
1960 .right
1961 .replace_with_numeric_result_if_can_be_calculated()
1962 .0,
1963 inner.line_file.clone(),
1964 )
1965 .into(),
1966 AtomicFact::RestrictFact(inner) => RestrictFact::new(
1967 inner
1968 .obj
1969 .replace_with_numeric_result_if_can_be_calculated()
1970 .0,
1971 inner
1972 .obj_can_restrict_to_fn_set
1973 .replace_with_numeric_result_if_can_be_calculated()
1974 .0,
1975 inner.line_file.clone(),
1976 )
1977 .into(),
1978 AtomicFact::NotRestrictFact(inner) => NotRestrictFact::new(
1979 inner
1980 .obj
1981 .replace_with_numeric_result_if_can_be_calculated()
1982 .0,
1983 inner
1984 .obj_cannot_restrict_to_fn_set
1985 .replace_with_numeric_result_if_can_be_calculated()
1986 .0,
1987 inner.line_file.clone(),
1988 )
1989 .into(),
1990 };
1991 let any_argument_replaced = calculated_atomic_fact.to_string() != self.to_string();
1992 (calculated_atomic_fact, any_argument_replaced)
1993 }
1994}
1995
1996impl From<NormalAtomicFact> for AtomicFact {
1997 fn from(f: NormalAtomicFact) -> Self {
1998 AtomicFact::NormalAtomicFact(f)
1999 }
2000}
2001
2002impl From<EqualFact> for AtomicFact {
2003 fn from(f: EqualFact) -> Self {
2004 AtomicFact::EqualFact(f)
2005 }
2006}
2007
2008impl From<LessFact> for AtomicFact {
2009 fn from(f: LessFact) -> Self {
2010 AtomicFact::LessFact(f)
2011 }
2012}
2013
2014impl From<GreaterFact> for AtomicFact {
2015 fn from(f: GreaterFact) -> Self {
2016 AtomicFact::GreaterFact(f)
2017 }
2018}
2019
2020impl From<LessEqualFact> for AtomicFact {
2021 fn from(f: LessEqualFact) -> Self {
2022 AtomicFact::LessEqualFact(f)
2023 }
2024}
2025
2026impl From<GreaterEqualFact> for AtomicFact {
2027 fn from(f: GreaterEqualFact) -> Self {
2028 AtomicFact::GreaterEqualFact(f)
2029 }
2030}
2031
2032impl From<IsSetFact> for AtomicFact {
2033 fn from(f: IsSetFact) -> Self {
2034 AtomicFact::IsSetFact(f)
2035 }
2036}
2037
2038impl From<IsNonemptySetFact> for AtomicFact {
2039 fn from(f: IsNonemptySetFact) -> Self {
2040 AtomicFact::IsNonemptySetFact(f)
2041 }
2042}
2043
2044impl From<IsFiniteSetFact> for AtomicFact {
2045 fn from(f: IsFiniteSetFact) -> Self {
2046 AtomicFact::IsFiniteSetFact(f)
2047 }
2048}
2049
2050impl From<InFact> for AtomicFact {
2051 fn from(f: InFact) -> Self {
2052 AtomicFact::InFact(f)
2053 }
2054}
2055
2056impl From<IsCartFact> for AtomicFact {
2057 fn from(f: IsCartFact) -> Self {
2058 AtomicFact::IsCartFact(f)
2059 }
2060}
2061
2062impl From<IsTupleFact> for AtomicFact {
2063 fn from(f: IsTupleFact) -> Self {
2064 AtomicFact::IsTupleFact(f)
2065 }
2066}
2067
2068impl From<SubsetFact> for AtomicFact {
2069 fn from(f: SubsetFact) -> Self {
2070 AtomicFact::SubsetFact(f)
2071 }
2072}
2073
2074impl From<SupersetFact> for AtomicFact {
2075 fn from(f: SupersetFact) -> Self {
2076 AtomicFact::SupersetFact(f)
2077 }
2078}
2079
2080impl From<RestrictFact> for AtomicFact {
2081 fn from(f: RestrictFact) -> Self {
2082 AtomicFact::RestrictFact(f)
2083 }
2084}
2085
2086impl From<NotRestrictFact> for AtomicFact {
2087 fn from(f: NotRestrictFact) -> Self {
2088 AtomicFact::NotRestrictFact(f)
2089 }
2090}
2091
2092impl From<NotNormalAtomicFact> for AtomicFact {
2093 fn from(f: NotNormalAtomicFact) -> Self {
2094 AtomicFact::NotNormalAtomicFact(f)
2095 }
2096}
2097
2098impl From<NotEqualFact> for AtomicFact {
2099 fn from(f: NotEqualFact) -> Self {
2100 AtomicFact::NotEqualFact(f)
2101 }
2102}
2103
2104impl From<NotLessFact> for AtomicFact {
2105 fn from(f: NotLessFact) -> Self {
2106 AtomicFact::NotLessFact(f)
2107 }
2108}
2109
2110impl From<NotGreaterFact> for AtomicFact {
2111 fn from(f: NotGreaterFact) -> Self {
2112 AtomicFact::NotGreaterFact(f)
2113 }
2114}
2115
2116impl From<NotLessEqualFact> for AtomicFact {
2117 fn from(f: NotLessEqualFact) -> Self {
2118 AtomicFact::NotLessEqualFact(f)
2119 }
2120}
2121
2122impl From<NotGreaterEqualFact> for AtomicFact {
2123 fn from(f: NotGreaterEqualFact) -> Self {
2124 AtomicFact::NotGreaterEqualFact(f)
2125 }
2126}
2127
2128impl From<NotIsSetFact> for AtomicFact {
2129 fn from(f: NotIsSetFact) -> Self {
2130 AtomicFact::NotIsSetFact(f)
2131 }
2132}
2133
2134impl From<NotIsNonemptySetFact> for AtomicFact {
2135 fn from(f: NotIsNonemptySetFact) -> Self {
2136 AtomicFact::NotIsNonemptySetFact(f)
2137 }
2138}
2139
2140impl From<NotIsFiniteSetFact> for AtomicFact {
2141 fn from(f: NotIsFiniteSetFact) -> Self {
2142 AtomicFact::NotIsFiniteSetFact(f)
2143 }
2144}
2145
2146impl From<NotInFact> for AtomicFact {
2147 fn from(f: NotInFact) -> Self {
2148 AtomicFact::NotInFact(f)
2149 }
2150}
2151
2152impl From<NotIsCartFact> for AtomicFact {
2153 fn from(f: NotIsCartFact) -> Self {
2154 AtomicFact::NotIsCartFact(f)
2155 }
2156}
2157
2158impl From<NotIsTupleFact> for AtomicFact {
2159 fn from(f: NotIsTupleFact) -> Self {
2160 AtomicFact::NotIsTupleFact(f)
2161 }
2162}
2163
2164impl From<NotSubsetFact> for AtomicFact {
2165 fn from(f: NotSubsetFact) -> Self {
2166 AtomicFact::NotSubsetFact(f)
2167 }
2168}
2169
2170impl From<NotSupersetFact> for AtomicFact {
2171 fn from(f: NotSupersetFact) -> Self {
2172 AtomicFact::NotSupersetFact(f)
2173 }
2174}
2175
2176impl From<NormalAtomicFact> for Fact {
2177 fn from(f: NormalAtomicFact) -> Self {
2178 Fact::AtomicFact(f.into())
2179 }
2180}
2181
2182impl From<EqualFact> for Fact {
2183 fn from(f: EqualFact) -> Self {
2184 Fact::AtomicFact(f.into())
2185 }
2186}
2187
2188impl From<LessFact> for Fact {
2189 fn from(f: LessFact) -> Self {
2190 Fact::AtomicFact(f.into())
2191 }
2192}
2193
2194impl From<GreaterFact> for Fact {
2195 fn from(f: GreaterFact) -> Self {
2196 Fact::AtomicFact(f.into())
2197 }
2198}
2199
2200impl From<LessEqualFact> for Fact {
2201 fn from(f: LessEqualFact) -> Self {
2202 Fact::AtomicFact(f.into())
2203 }
2204}
2205
2206impl From<GreaterEqualFact> for Fact {
2207 fn from(f: GreaterEqualFact) -> Self {
2208 Fact::AtomicFact(f.into())
2209 }
2210}
2211
2212impl From<IsSetFact> for Fact {
2213 fn from(f: IsSetFact) -> Self {
2214 Fact::AtomicFact(f.into())
2215 }
2216}
2217
2218impl From<IsNonemptySetFact> for Fact {
2219 fn from(f: IsNonemptySetFact) -> Self {
2220 Fact::AtomicFact(f.into())
2221 }
2222}
2223
2224impl From<IsFiniteSetFact> for Fact {
2225 fn from(f: IsFiniteSetFact) -> Self {
2226 Fact::AtomicFact(f.into())
2227 }
2228}
2229
2230impl From<InFact> for Fact {
2231 fn from(f: InFact) -> Self {
2232 Fact::AtomicFact(f.into())
2233 }
2234}
2235
2236impl From<IsCartFact> for Fact {
2237 fn from(f: IsCartFact) -> Self {
2238 Fact::AtomicFact(f.into())
2239 }
2240}
2241
2242impl From<IsTupleFact> for Fact {
2243 fn from(f: IsTupleFact) -> Self {
2244 Fact::AtomicFact(f.into())
2245 }
2246}
2247
2248impl From<SubsetFact> for Fact {
2249 fn from(f: SubsetFact) -> Self {
2250 Fact::AtomicFact(f.into())
2251 }
2252}
2253
2254impl From<SupersetFact> for Fact {
2255 fn from(f: SupersetFact) -> Self {
2256 Fact::AtomicFact(f.into())
2257 }
2258}
2259
2260impl From<RestrictFact> for Fact {
2261 fn from(f: RestrictFact) -> Self {
2262 Fact::AtomicFact(f.into())
2263 }
2264}
2265
2266impl From<NotRestrictFact> for Fact {
2267 fn from(f: NotRestrictFact) -> Self {
2268 Fact::AtomicFact(f.into())
2269 }
2270}
2271
2272impl From<NotNormalAtomicFact> for Fact {
2273 fn from(f: NotNormalAtomicFact) -> Self {
2274 Fact::AtomicFact(f.into())
2275 }
2276}
2277
2278impl From<NotEqualFact> for Fact {
2279 fn from(f: NotEqualFact) -> Self {
2280 Fact::AtomicFact(f.into())
2281 }
2282}
2283
2284impl From<NotLessFact> for Fact {
2285 fn from(f: NotLessFact) -> Self {
2286 Fact::AtomicFact(f.into())
2287 }
2288}
2289
2290impl From<NotGreaterFact> for Fact {
2291 fn from(f: NotGreaterFact) -> Self {
2292 Fact::AtomicFact(f.into())
2293 }
2294}
2295
2296impl From<NotLessEqualFact> for Fact {
2297 fn from(f: NotLessEqualFact) -> Self {
2298 Fact::AtomicFact(f.into())
2299 }
2300}
2301
2302impl From<NotGreaterEqualFact> for Fact {
2303 fn from(f: NotGreaterEqualFact) -> Self {
2304 Fact::AtomicFact(f.into())
2305 }
2306}
2307
2308impl From<NotIsSetFact> for Fact {
2309 fn from(f: NotIsSetFact) -> Self {
2310 Fact::AtomicFact(f.into())
2311 }
2312}
2313
2314impl From<NotIsNonemptySetFact> for Fact {
2315 fn from(f: NotIsNonemptySetFact) -> Self {
2316 Fact::AtomicFact(f.into())
2317 }
2318}
2319
2320impl From<NotIsFiniteSetFact> for Fact {
2321 fn from(f: NotIsFiniteSetFact) -> Self {
2322 Fact::AtomicFact(f.into())
2323 }
2324}
2325
2326impl From<NotInFact> for Fact {
2327 fn from(f: NotInFact) -> Self {
2328 Fact::AtomicFact(f.into())
2329 }
2330}
2331
2332impl From<NotIsCartFact> for Fact {
2333 fn from(f: NotIsCartFact) -> Self {
2334 Fact::AtomicFact(f.into())
2335 }
2336}
2337
2338impl From<NotIsTupleFact> for Fact {
2339 fn from(f: NotIsTupleFact) -> Self {
2340 Fact::AtomicFact(f.into())
2341 }
2342}
2343
2344impl From<NotSubsetFact> for Fact {
2345 fn from(f: NotSubsetFact) -> Self {
2346 Fact::AtomicFact(f.into())
2347 }
2348}
2349
2350impl From<NotSupersetFact> for Fact {
2351 fn from(f: NotSupersetFact) -> Self {
2352 Fact::AtomicFact(f.into())
2353 }
2354}