anthem/syntax_tree/fol/
sigma_0.rs

1use {
2    crate::{
3        convenience::apply::Apply as _,
4        formatting::fol::sigma_0::default::Format,
5        parsing::fol::sigma_0::pest::{
6            AnnotatedFormulaParser, AtomParser, AtomicFormulaParser, BinaryConnectiveParser,
7            BinaryOperatorParser, ComparisonParser, DirectionParser, FormulaParser,
8            FunctionConstantParser, GeneralTermParser, GuardParser, IntegerTermParser,
9            PlaceholderDeclarationParser, PredicateParser, QuantificationParser, QuantifierParser,
10            RelationParser, RoleParser, SortParser, SpecificationParser, SymbolicTermParser,
11            TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser,
12            UserGuideParser, VariableParser,
13        },
14        simplifying::fol::sigma_0::intuitionistic::join_nested_quantifiers,
15        syntax_tree::{Node, impl_node},
16        verifying::problem,
17    },
18    clap::ValueEnum,
19    derive_more::derive::IntoIterator,
20    indexmap::{IndexMap, IndexSet},
21    std::hash::Hash,
22};
23
24#[derive(Clone, Debug, Eq, PartialEq, Hash)]
25pub enum UnaryOperator {
26    Negative,
27}
28
29impl_node!(UnaryOperator, Format, UnaryOperatorParser);
30
31#[derive(Clone, Debug, Eq, PartialEq, Hash)]
32pub enum BinaryOperator {
33    Add,
34    Subtract,
35    Multiply,
36}
37
38impl_node!(BinaryOperator, Format, BinaryOperatorParser);
39
40#[derive(Clone, Debug, Eq, PartialEq, Hash)]
41pub enum IntegerTerm {
42    Numeral(isize),
43    FunctionConstant(String),
44    Variable(String),
45    UnaryOperation {
46        op: UnaryOperator,
47        arg: Box<IntegerTerm>,
48    },
49    BinaryOperation {
50        op: BinaryOperator,
51        lhs: Box<IntegerTerm>,
52        rhs: Box<IntegerTerm>,
53    },
54}
55
56impl_node!(IntegerTerm, Format, IntegerTermParser);
57
58impl IntegerTerm {
59    pub fn variables(&self) -> IndexSet<Variable> {
60        match &self {
61            IntegerTerm::Numeral(_) | IntegerTerm::FunctionConstant(_) => IndexSet::new(),
62            IntegerTerm::Variable(v) => IndexSet::from([Variable {
63                name: v.to_string(),
64                sort: Sort::Integer,
65            }]),
66            IntegerTerm::UnaryOperation { arg: t, .. } => t.variables(),
67            IntegerTerm::BinaryOperation { lhs, rhs, .. } => {
68                let mut vars = lhs.variables();
69                vars.extend(rhs.variables());
70                vars
71            }
72        }
73    }
74
75    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
76        match &self {
77            IntegerTerm::FunctionConstant(c) => IndexSet::from([FunctionConstant {
78                name: c.clone(),
79                sort: Sort::Integer,
80            }]),
81            IntegerTerm::Numeral(_) | IntegerTerm::Variable(_) => IndexSet::new(),
82            IntegerTerm::UnaryOperation { arg: t, .. } => t.function_constants(),
83            IntegerTerm::BinaryOperation { lhs, rhs, .. } => {
84                let mut constants = lhs.function_constants();
85                constants.extend(rhs.function_constants());
86                constants
87            }
88        }
89    }
90
91    pub fn substitute(self, var: Variable, term: IntegerTerm) -> Self {
92        match self {
93            IntegerTerm::Variable(s) if var.name == s && var.sort == Sort::Integer => term,
94            IntegerTerm::Numeral(_)
95            | IntegerTerm::FunctionConstant(_)
96            | IntegerTerm::Variable(_) => self,
97            IntegerTerm::UnaryOperation { op, arg } => IntegerTerm::UnaryOperation {
98                op,
99                arg: arg.substitute(var, term).into(),
100            },
101            IntegerTerm::BinaryOperation { op, lhs, rhs } => IntegerTerm::BinaryOperation {
102                op,
103                lhs: lhs.substitute(var.clone(), term.clone()).into(),
104                rhs: rhs.substitute(var, term).into(),
105            },
106        }
107    }
108}
109
110#[derive(Clone, Debug, Eq, PartialEq, Hash)]
111pub enum SymbolicTerm {
112    Symbol(String),
113    FunctionConstant(String),
114    Variable(String),
115}
116
117impl_node!(SymbolicTerm, Format, SymbolicTermParser);
118
119impl SymbolicTerm {
120    pub fn variables(&self) -> IndexSet<Variable> {
121        match &self {
122            SymbolicTerm::Symbol(_) | SymbolicTerm::FunctionConstant(_) => IndexSet::new(),
123            SymbolicTerm::Variable(v) => IndexSet::from([Variable {
124                name: v.to_string(),
125                sort: Sort::Symbol,
126            }]),
127        }
128    }
129
130    pub fn symbols(&self) -> IndexSet<String> {
131        match &self {
132            SymbolicTerm::Symbol(s) => IndexSet::from([s.clone()]),
133            SymbolicTerm::FunctionConstant(_) | SymbolicTerm::Variable(_) => IndexSet::new(),
134        }
135    }
136
137    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
138        match &self {
139            SymbolicTerm::FunctionConstant(c) => IndexSet::from([FunctionConstant {
140                name: c.clone(),
141                sort: Sort::Symbol,
142            }]),
143            SymbolicTerm::Symbol(_) | SymbolicTerm::Variable(_) => IndexSet::new(),
144        }
145    }
146
147    pub fn substitute(self, var: Variable, term: SymbolicTerm) -> Self {
148        match self {
149            SymbolicTerm::Variable(s) if var.name == s && var.sort == Sort::Symbol => term,
150            _ => self,
151        }
152    }
153}
154
155#[derive(Clone, Debug, Eq, PartialEq, Hash)]
156pub enum GeneralTerm {
157    Infimum,
158    Supremum,
159    FunctionConstant(String),
160    Variable(String),
161    IntegerTerm(IntegerTerm),
162    SymbolicTerm(SymbolicTerm),
163}
164
165impl_node!(GeneralTerm, Format, GeneralTermParser);
166
167impl GeneralTerm {
168    pub fn variables(&self) -> IndexSet<Variable> {
169        match &self {
170            GeneralTerm::Infimum | GeneralTerm::Supremum | GeneralTerm::FunctionConstant(_) => {
171                IndexSet::new()
172            }
173            GeneralTerm::Variable(v) => IndexSet::from([Variable {
174                name: v.to_string(),
175                sort: Sort::General,
176            }]),
177            GeneralTerm::IntegerTerm(t) => t.variables(),
178            GeneralTerm::SymbolicTerm(t) => t.variables(),
179        }
180    }
181
182    pub fn symbols(&self) -> IndexSet<String> {
183        match &self {
184            GeneralTerm::SymbolicTerm(t) => t.symbols(),
185            _ => IndexSet::new(),
186        }
187    }
188
189    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
190        match &self {
191            GeneralTerm::FunctionConstant(c) => IndexSet::from([FunctionConstant {
192                name: c.clone(),
193                sort: Sort::General,
194            }]),
195            GeneralTerm::IntegerTerm(t) => t.function_constants(),
196            GeneralTerm::SymbolicTerm(t) => t.function_constants(),
197            GeneralTerm::Infimum | GeneralTerm::Supremum | GeneralTerm::Variable(_) => {
198                IndexSet::new()
199            }
200        }
201    }
202
203    pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
204        match self {
205            GeneralTerm::Variable(s) if var.name == s && var.sort == Sort::General => term,
206            GeneralTerm::IntegerTerm(t) if var.sort == Sort::Integer => match term {
207                GeneralTerm::IntegerTerm(term) => GeneralTerm::IntegerTerm(t.substitute(var, term)),
208                _ => panic!(
209                    "cannot substitute general term `{term}` for the integer variable `{var}`"
210                ),
211            },
212            GeneralTerm::SymbolicTerm(t) if var.sort == Sort::Symbol => match term {
213                GeneralTerm::SymbolicTerm(term) => {
214                    GeneralTerm::SymbolicTerm(t.substitute(var, term))
215                }
216                _ => panic!(
217                    "cannot substitute general term `{term}` for the symbolic variable `{var}`"
218                ),
219            },
220            t => t,
221        }
222    }
223
224    fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Self {
225        match self {
226            GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol(s)) => {
227                let predicate = Predicate {
228                    symbol: s.clone(),
229                    arity: 0,
230                };
231                // TODO: increment new name while conflicts exist
232                if possible_conflicts.contains(&predicate) {
233                    GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol(format!("{s}__s")))
234                } else {
235                    GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol(s))
236                }
237            }
238            x => x,
239        }
240    }
241
242    fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
243        match self {
244            GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol(s)) => {
245                if let Some(fc) = mapping.get(&s) {
246                    match fc.sort {
247                        Sort::General => GeneralTerm::FunctionConstant(s),
248                        Sort::Integer => GeneralTerm::IntegerTerm(IntegerTerm::FunctionConstant(s)),
249                        Sort::Symbol => {
250                            GeneralTerm::SymbolicTerm(SymbolicTerm::FunctionConstant(s))
251                        }
252                    }
253                } else {
254                    GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol(s))
255                }
256            }
257            x => x,
258        }
259    }
260}
261
262impl From<Variable> for GeneralTerm {
263    fn from(variable: Variable) -> Self {
264        match variable.sort {
265            Sort::General => GeneralTerm::Variable(variable.name),
266            Sort::Integer => GeneralTerm::IntegerTerm(IntegerTerm::Variable(variable.name)),
267            Sort::Symbol => GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(variable.name)),
268        }
269    }
270}
271
272#[derive(Clone, Debug, Eq, PartialEq, Hash)]
273pub struct Predicate {
274    pub symbol: String,
275    pub arity: usize,
276}
277
278impl_node!(Predicate, Format, PredicateParser);
279
280impl Predicate {
281    pub fn to_formula(self) -> Formula {
282        Formula::AtomicFormula(AtomicFormula::Atom(Atom {
283            predicate_symbol: self.symbol,
284            terms: (1..=self.arity)
285                .map(|i| GeneralTerm::Variable(format!("X{i}")))
286                .collect(),
287        }))
288    }
289}
290
291impl From<crate::syntax_tree::asp::mini_gringo::Predicate> for Predicate {
292    fn from(value: crate::syntax_tree::asp::mini_gringo::Predicate) -> Self {
293        Predicate {
294            symbol: value.symbol,
295            arity: value.arity,
296        }
297    }
298}
299
300#[derive(Clone, Debug, Eq, PartialEq, Hash)]
301pub struct Atom {
302    pub predicate_symbol: String,
303    pub terms: Vec<GeneralTerm>,
304}
305
306impl Atom {
307    pub fn predicate(&self) -> Predicate {
308        Predicate {
309            symbol: self.predicate_symbol.clone(),
310            arity: self.terms.len(),
311        }
312    }
313
314    fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Self {
315        Atom {
316            predicate_symbol: self.predicate_symbol,
317            terms: self
318                .terms
319                .into_iter()
320                .map(|t| t.rename_conflicting_symbols(possible_conflicts))
321                .collect(),
322        }
323    }
324
325    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
326        Atom {
327            predicate_symbol: self.predicate_symbol,
328            terms: self
329                .terms
330                .into_iter()
331                .map(|t| t.replace_placeholders(mapping))
332                .collect(),
333        }
334    }
335}
336
337impl_node!(Atom, Format, AtomParser);
338
339impl Atom {
340    pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
341        let predicate_symbol = self.predicate_symbol;
342
343        let mut terms = Vec::new();
344        for t in self.terms {
345            terms.push(t.substitute(var.clone(), term.clone()))
346        }
347
348        Atom {
349            predicate_symbol,
350            terms,
351        }
352    }
353}
354
355#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
356pub enum Relation {
357    Equal,
358    NotEqual,
359    Greater,
360    Less,
361    GreaterEqual,
362    LessEqual,
363}
364
365impl_node!(Relation, Format, RelationParser);
366
367impl From<crate::syntax_tree::asp::mini_gringo::Relation> for Relation {
368    fn from(value: crate::syntax_tree::asp::mini_gringo::Relation) -> Self {
369        match value {
370            crate::syntax_tree::asp::mini_gringo::Relation::Equal => Relation::Equal,
371            crate::syntax_tree::asp::mini_gringo::Relation::NotEqual => Relation::NotEqual,
372            crate::syntax_tree::asp::mini_gringo::Relation::Greater => Relation::Greater,
373            crate::syntax_tree::asp::mini_gringo::Relation::Less => Relation::Less,
374            crate::syntax_tree::asp::mini_gringo::Relation::GreaterEqual => Relation::GreaterEqual,
375            crate::syntax_tree::asp::mini_gringo::Relation::LessEqual => Relation::LessEqual,
376        }
377    }
378}
379
380#[derive(Clone, Debug, Eq, PartialEq, Hash)]
381pub struct Guard {
382    pub relation: Relation,
383    pub term: GeneralTerm,
384}
385
386impl_node!(Guard, Format, GuardParser);
387
388impl Guard {
389    pub fn variables(&self) -> IndexSet<Variable> {
390        self.term.variables()
391    }
392
393    pub fn symbols(&self) -> IndexSet<String> {
394        self.term.symbols()
395    }
396
397    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
398        self.term.function_constants()
399    }
400
401    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
402        Guard {
403            relation: self.relation,
404            term: self.term.replace_placeholders(mapping),
405        }
406    }
407}
408
409#[derive(Clone, Debug, Eq, PartialEq, Hash)]
410pub struct Comparison {
411    pub term: GeneralTerm,
412    pub guards: Vec<Guard>,
413}
414
415impl_node!(Comparison, Format, ComparisonParser);
416
417impl Comparison {
418    pub fn individuals(&self) -> impl Iterator<Item = (&GeneralTerm, &Relation, &GeneralTerm)> {
419        struct Individuals<'a> {
420            lhs: &'a GeneralTerm,
421            guards_iter: std::slice::Iter<'a, Guard>,
422        }
423
424        impl<'a> Iterator for Individuals<'a> {
425            type Item = (&'a GeneralTerm, &'a Relation, &'a GeneralTerm);
426
427            fn next(&mut self) -> Option<Self::Item> {
428                if let Some(Guard {
429                    relation,
430                    term: rhs,
431                }) = self.guards_iter.next()
432                {
433                    let result = Some((self.lhs, relation, rhs));
434                    self.lhs = rhs;
435                    result
436                } else {
437                    None
438                }
439            }
440        }
441
442        Individuals {
443            lhs: &self.term,
444            guards_iter: self.guards.iter(),
445        }
446    }
447
448    pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
449        let lhs = self.term.substitute(var.clone(), term.clone());
450
451        let mut guards = Vec::new();
452        for old_guard in self.guards {
453            let new_guard = Guard {
454                relation: old_guard.relation,
455                term: old_guard.term.substitute(var.clone(), term.clone()),
456            };
457            guards.push(new_guard);
458        }
459
460        Comparison { term: lhs, guards }
461    }
462
463    fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Self {
464        let term = self.term.rename_conflicting_symbols(possible_conflicts);
465
466        let mut guards = Vec::new();
467        for old_guard in self.guards {
468            let new_guard = Guard {
469                relation: old_guard.relation,
470                term: old_guard
471                    .term
472                    .rename_conflicting_symbols(possible_conflicts),
473            };
474            guards.push(new_guard);
475        }
476
477        Comparison { term, guards }
478    }
479
480    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
481        Comparison {
482            term: self.term.replace_placeholders(mapping),
483            guards: self
484                .guards
485                .into_iter()
486                .map(|g| g.replace_placeholders(mapping))
487                .collect(),
488        }
489    }
490}
491
492#[derive(Clone, Debug, Eq, PartialEq, Hash)]
493pub enum AtomicFormula {
494    Truth,
495    Falsity,
496    Atom(Atom),
497    Comparison(Comparison),
498}
499
500impl_node!(AtomicFormula, Format, AtomicFormulaParser);
501
502impl AtomicFormula {
503    pub fn variables(&self) -> IndexSet<Variable> {
504        match &self {
505            AtomicFormula::Falsity | AtomicFormula::Truth => IndexSet::new(),
506            AtomicFormula::Atom(a) => {
507                let mut vars = IndexSet::new();
508                for t in a.terms.iter() {
509                    vars.extend(t.variables());
510                }
511                vars
512            }
513            AtomicFormula::Comparison(c) => {
514                let mut vars = c.term.variables();
515                for guard in c.guards.iter() {
516                    vars.extend(guard.variables())
517                }
518                vars
519            }
520        }
521    }
522
523    pub fn predicates(&self) -> IndexSet<Predicate> {
524        match &self {
525            AtomicFormula::Falsity | AtomicFormula::Truth | AtomicFormula::Comparison(_) => {
526                IndexSet::new()
527            }
528            AtomicFormula::Atom(a) => IndexSet::from([a.predicate()]),
529        }
530    }
531
532    pub fn symbols(&self) -> IndexSet<String> {
533        match &self {
534            AtomicFormula::Falsity | AtomicFormula::Truth => IndexSet::new(),
535            AtomicFormula::Atom(a) => {
536                let mut symbols = IndexSet::new();
537                for t in a.terms.iter() {
538                    symbols.extend(t.symbols());
539                }
540                symbols
541            }
542            AtomicFormula::Comparison(c) => {
543                let mut symbols = c.term.symbols();
544                for guard in c.guards.iter() {
545                    symbols.extend(guard.symbols())
546                }
547                symbols
548            }
549        }
550    }
551
552    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
553        match &self {
554            AtomicFormula::Falsity | AtomicFormula::Truth => IndexSet::new(),
555            AtomicFormula::Atom(a) => {
556                let mut function_constants = IndexSet::new();
557                for t in a.terms.iter() {
558                    function_constants.extend(t.function_constants());
559                }
560                function_constants
561            }
562            AtomicFormula::Comparison(c) => {
563                let mut function_constants = c.term.function_constants();
564                for guard in c.guards.iter() {
565                    function_constants.extend(guard.function_constants())
566                }
567                function_constants
568            }
569        }
570    }
571
572    pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
573        match self {
574            AtomicFormula::Atom(a) => AtomicFormula::Atom(a.substitute(var, term)),
575            AtomicFormula::Comparison(c) => AtomicFormula::Comparison(c.substitute(var, term)),
576            f => f,
577        }
578    }
579
580    fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Self {
581        match self {
582            AtomicFormula::Atom(a) => {
583                AtomicFormula::Atom(a.rename_conflicting_symbols(possible_conflicts))
584            }
585            AtomicFormula::Comparison(c) => {
586                AtomicFormula::Comparison(c.rename_conflicting_symbols(possible_conflicts))
587            }
588            x => x,
589        }
590    }
591
592    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
593        match self {
594            AtomicFormula::Atom(a) => AtomicFormula::Atom(a.replace_placeholders(mapping)),
595            AtomicFormula::Comparison(c) => {
596                AtomicFormula::Comparison(c.replace_placeholders(mapping))
597            }
598            x => x,
599        }
600    }
601}
602
603#[derive(Clone, Debug, Eq, PartialEq, Hash)]
604pub enum UnaryConnective {
605    Negation,
606}
607
608impl_node!(UnaryConnective, Format, UnaryConnectiveParser);
609
610#[derive(Clone, Debug, Eq, PartialEq, Hash)]
611pub enum Quantifier {
612    Forall,
613    Exists,
614}
615
616impl_node!(Quantifier, Format, QuantifierParser);
617
618#[derive(Clone, Debug, Eq, PartialEq, Hash)]
619pub struct Quantification {
620    pub quantifier: Quantifier,
621    pub variables: Vec<Variable>,
622}
623
624impl_node!(Quantification, Format, QuantificationParser);
625
626#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
627pub enum Sort {
628    General,
629    Integer,
630    Symbol,
631}
632
633impl_node!(Sort, Format, SortParser);
634
635#[derive(Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
636pub struct FunctionConstant {
637    pub name: String,
638    pub sort: Sort,
639}
640
641impl_node!(FunctionConstant, Format, FunctionConstantParser);
642
643impl From<PlaceholderDeclaration> for FunctionConstant {
644    fn from(value: PlaceholderDeclaration) -> Self {
645        FunctionConstant {
646            name: value.name,
647            sort: value.sort,
648        }
649    }
650}
651
652#[derive(Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
653pub struct Variable {
654    pub name: String,
655    pub sort: Sort,
656}
657
658impl_node!(Variable, Format, VariableParser);
659
660impl Variable {
661    fn sequence(prefix: &Variable) -> impl Iterator<Item = Self> {
662        (1..).map(|i| Variable {
663            name: format!("{}{}", prefix.name, i),
664            sort: prefix.sort,
665        })
666    }
667}
668
669impl TryFrom<GeneralTerm> for Variable {
670    type Error = GeneralTerm;
671
672    fn try_from(term: GeneralTerm) -> std::result::Result<Self, Self::Error> {
673        match term {
674            GeneralTerm::Variable(v) => Ok(Variable {
675                name: v,
676                sort: Sort::General,
677            }),
678            GeneralTerm::IntegerTerm(IntegerTerm::Variable(v)) => Ok(Variable {
679                name: v,
680                sort: Sort::Integer,
681            }),
682            GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(v)) => Ok(Variable {
683                name: v,
684                sort: Sort::Symbol,
685            }),
686            x => Err(x),
687        }
688    }
689}
690
691#[derive(Clone, Debug, Eq, PartialEq, Hash)]
692pub enum BinaryConnective {
693    Conjunction,
694    Disjunction,
695    Implication,
696    ReverseImplication,
697    Equivalence,
698}
699
700impl_node!(BinaryConnective, Format, BinaryConnectiveParser);
701
702#[derive(Clone, Debug, Eq, PartialEq, Hash)]
703pub enum Formula {
704    AtomicFormula(AtomicFormula),
705    UnaryFormula {
706        connective: UnaryConnective,
707        formula: Box<Formula>,
708    },
709    BinaryFormula {
710        connective: BinaryConnective,
711        lhs: Box<Formula>,
712        rhs: Box<Formula>,
713    },
714    QuantifiedFormula {
715        quantification: Quantification,
716        formula: Box<Formula>,
717    },
718}
719
720impl_node!(Formula, Format, FormulaParser);
721
722impl Formula {
723    /// Recursively turn a list of formulas into a conjunction tree
724    pub fn conjoin(formulas: impl IntoIterator<Item = Formula>) -> Formula {
725        /*
726         * One could also implement this recursively:
727         *
728         * Case 1: List of formulas is empty
729         * -> Return #true
730         *
731         * Case 2: List of formulas contains a single formula
732         * -> Return that formula
733         *
734         * Case 3: List of formulas contains more than a single formula
735         * -> Return conjoin(formula[0..n-2]) and formula[n-1]
736         */
737
738        formulas
739            .into_iter()
740            .reduce(|acc, e| Formula::BinaryFormula {
741                connective: BinaryConnective::Conjunction,
742                lhs: acc.into(),
743                rhs: e.into(),
744            })
745            .unwrap_or(Formula::AtomicFormula(AtomicFormula::Truth))
746    }
747
748    /// Recursively turn a list of formulas into a tree of disjunctions
749    pub fn disjoin(formulas: impl IntoIterator<Item = Formula>) -> Formula {
750        /*
751         * One could also implement this recursively:
752         *
753         * Case 1: List of formulas is empty
754         * -> Return #false
755         *
756         * Case 2: List of formulas contains a single formula
757         * -> Return that formula
758         *
759         * Case 3: List of formulas contains more than a single formula
760         * -> Return conjoin(formula[0..n-2]) or formula[n-1]
761         */
762
763        formulas
764            .into_iter()
765            .reduce(|acc, e| Formula::BinaryFormula {
766                connective: BinaryConnective::Disjunction,
767                lhs: acc.into(),
768                rhs: e.into(),
769            })
770            .unwrap_or(Formula::AtomicFormula(AtomicFormula::Falsity))
771    }
772
773    pub fn variables(&self) -> IndexSet<Variable> {
774        match &self {
775            Formula::AtomicFormula(f) => f.variables(),
776            Formula::UnaryFormula { formula, .. } => formula.variables(),
777            Formula::BinaryFormula { lhs, rhs, .. } => {
778                let mut vars = lhs.variables();
779                vars.extend(rhs.variables());
780                vars
781            }
782            Formula::QuantifiedFormula { formula, .. } => formula.variables(),
783        }
784    }
785
786    pub fn free_variables(&self) -> IndexSet<Variable> {
787        match &self {
788            Formula::AtomicFormula(f) => f.variables(),
789            Formula::UnaryFormula { formula, .. } => formula.free_variables(),
790            Formula::BinaryFormula { lhs, rhs, .. } => {
791                let mut vars = lhs.free_variables();
792                vars.extend(rhs.free_variables());
793                vars
794            }
795            Formula::QuantifiedFormula {
796                quantification,
797                formula,
798            } => {
799                let mut vars = formula.free_variables();
800                for var in &quantification.variables {
801                    vars.shift_remove(var);
802                }
803                vars
804            }
805        }
806    }
807
808    pub fn predicates(&self) -> IndexSet<Predicate> {
809        match &self {
810            Formula::AtomicFormula(f) => f.predicates(),
811            Formula::UnaryFormula { formula, .. } => formula.predicates(),
812            Formula::BinaryFormula { lhs, rhs, .. } => {
813                let mut vars = lhs.predicates();
814                vars.extend(rhs.predicates());
815                vars
816            }
817            Formula::QuantifiedFormula { formula, .. } => formula.predicates(),
818        }
819    }
820
821    pub fn symbols(&self) -> IndexSet<String> {
822        match &self {
823            Formula::AtomicFormula(f) => f.symbols(),
824            Formula::UnaryFormula { formula, .. } => formula.symbols(),
825            Formula::BinaryFormula { lhs, rhs, .. } => {
826                let mut vars = lhs.symbols();
827                vars.extend(rhs.symbols());
828                vars
829            }
830            Formula::QuantifiedFormula { formula, .. } => formula.symbols(),
831        }
832    }
833
834    pub fn function_constants(&self) -> IndexSet<FunctionConstant> {
835        match &self {
836            Formula::AtomicFormula(f) => f.function_constants(),
837            Formula::UnaryFormula { formula, .. } => formula.function_constants(),
838            Formula::BinaryFormula { lhs, rhs, .. } => {
839                let mut vars = lhs.function_constants();
840                vars.extend(rhs.function_constants());
841                vars
842            }
843            Formula::QuantifiedFormula { formula, .. } => formula.function_constants(),
844        }
845    }
846
847    // Replace all free occurences of var with term within the formula
848    pub fn substitute(self, var: Variable, term: GeneralTerm) -> Self {
849        match self {
850            Formula::AtomicFormula(f) => Formula::AtomicFormula(f.substitute(var, term)),
851            Formula::UnaryFormula {
852                connective,
853                formula,
854            } => Formula::UnaryFormula {
855                connective,
856                formula: formula.substitute(var, term).into(),
857            },
858            Formula::BinaryFormula {
859                connective,
860                lhs,
861                rhs,
862            } => Formula::BinaryFormula {
863                connective,
864                lhs: lhs.substitute(var.clone(), term.clone()).into(),
865                rhs: rhs.substitute(var, term).into(),
866            },
867            Formula::QuantifiedFormula {
868                quantification,
869                formula,
870            } if !quantification.variables.contains(&var) => {
871                let mut formula = *formula;
872                let mut variables = vec![];
873
874                let term_variables = term.variables();
875                let formula_variables = formula.free_variables();
876
877                for variable in quantification.variables {
878                    if term_variables.contains(&variable) {
879                        let fresh_variable = Variable::sequence(&variable)
880                            .find(|candidate| {
881                                !term_variables.contains(candidate)
882                                    && !formula_variables.contains(candidate)
883                            })
884                            .unwrap();
885
886                        formula = formula.substitute(variable, fresh_variable.clone().into());
887                        variables.push(fresh_variable);
888                    } else {
889                        variables.push(variable);
890                    }
891                }
892
893                Formula::quantify(
894                    formula.substitute(var, term),
895                    quantification.quantifier,
896                    variables,
897                )
898            }
899            f @ Formula::QuantifiedFormula {
900                quantification: _,
901                formula: _,
902            } => f,
903        }
904    }
905
906    pub fn quantify(self, quantifier: Quantifier, variables: Vec<Variable>) -> Formula {
907        if variables.is_empty() {
908            self
909        } else {
910            Formula::QuantifiedFormula {
911                quantification: Quantification {
912                    quantifier,
913                    variables,
914                },
915                formula: Box::new(self),
916            }
917        }
918    }
919
920    pub fn universal_closure(self) -> Formula {
921        let variables = self.free_variables().into_iter().collect();
922        self.quantify(Quantifier::Forall, variables)
923    }
924
925    pub fn universal_closure_with_quantifier_joining(self) -> Formula {
926        join_nested_quantifiers(self.universal_closure())
927    }
928
929    pub fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Formula {
930        match self {
931            Formula::AtomicFormula(a) => {
932                Formula::AtomicFormula(a.rename_conflicting_symbols(possible_conflicts))
933            }
934            Formula::UnaryFormula {
935                connective,
936                formula,
937            } => Formula::UnaryFormula {
938                connective,
939                formula: formula
940                    .rename_conflicting_symbols(possible_conflicts)
941                    .into(),
942            },
943            Formula::BinaryFormula {
944                connective,
945                lhs,
946                rhs,
947            } => Formula::BinaryFormula {
948                connective,
949                lhs: lhs.rename_conflicting_symbols(possible_conflicts).into(),
950                rhs: rhs.rename_conflicting_symbols(possible_conflicts).into(),
951            },
952            Formula::QuantifiedFormula {
953                quantification,
954                formula,
955            } => Formula::QuantifiedFormula {
956                quantification,
957                formula: formula
958                    .rename_conflicting_symbols(possible_conflicts)
959                    .into(),
960            },
961        }
962    }
963
964    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
965        self.apply(&mut |formula| match formula {
966            Formula::AtomicFormula(a) => Formula::AtomicFormula(a.replace_placeholders(mapping)),
967            x => x,
968        })
969    }
970}
971
972#[derive(Clone, Debug, Eq, PartialEq, Hash, IntoIterator)]
973pub struct Theory {
974    #[into_iterator(owned, ref, ref_mut)]
975    pub formulas: Vec<Formula>,
976}
977
978impl_node!(Theory, Format, TheoryParser);
979
980impl Theory {
981    pub fn predicates(&self) -> IndexSet<Predicate> {
982        let mut preds = IndexSet::new();
983        for formula in self {
984            preds.extend(formula.predicates())
985        }
986        preds
987    }
988
989    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
990        self.into_iter()
991            .map(|f| f.replace_placeholders(mapping))
992            .collect()
993    }
994}
995
996impl FromIterator<Formula> for Theory {
997    fn from_iter<T: IntoIterator<Item = Formula>>(iter: T) -> Self {
998        Theory {
999            formulas: iter.into_iter().collect(),
1000        }
1001    }
1002}
1003
1004#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
1005pub enum Role {
1006    Assumption,
1007    Spec,
1008    Lemma,
1009    Definition,
1010    InductiveLemma,
1011}
1012
1013impl_node!(Role, Format, RoleParser);
1014
1015#[derive(Copy, Clone, Debug, Default, Eq, PartialEq, Hash, ValueEnum)]
1016pub enum Direction {
1017    #[default]
1018    Universal,
1019    Forward,
1020    Backward,
1021}
1022
1023impl_node!(Direction, Format, DirectionParser);
1024
1025#[derive(Clone, Debug, Eq, PartialEq, Hash)]
1026pub struct AnnotatedFormula {
1027    pub role: Role,
1028    pub direction: Direction,
1029    pub name: String,
1030    pub formula: Formula,
1031}
1032
1033impl_node!(AnnotatedFormula, Format, AnnotatedFormulaParser);
1034
1035impl AnnotatedFormula {
1036    pub fn into_problem_formula(self, role: problem::Role) -> problem::AnnotatedFormula {
1037        problem::AnnotatedFormula {
1038            // TODO: Revisit default naming scheme!
1039            name: self.name,
1040            role,
1041            formula: self.formula,
1042        }
1043    }
1044
1045    pub fn predicates(&self) -> IndexSet<Predicate> {
1046        self.formula.predicates()
1047    }
1048
1049    pub fn universal_closure(&self) -> Self {
1050        AnnotatedFormula {
1051            role: self.role,
1052            direction: self.direction,
1053            name: self.name.clone(),
1054            formula: self.formula.clone().universal_closure(),
1055        }
1056    }
1057
1058    pub fn universal_closure_with_quantifier_joining(&self) -> Self {
1059        AnnotatedFormula {
1060            role: self.role,
1061            direction: self.direction,
1062            name: self.name.clone(),
1063            formula: self
1064                .formula
1065                .clone()
1066                .universal_closure_with_quantifier_joining(),
1067        }
1068    }
1069
1070    pub fn replace_placeholders(mut self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
1071        self.formula = self.formula.replace_placeholders(mapping);
1072        self
1073    }
1074}
1075
1076#[derive(Clone, Debug, Eq, PartialEq, Hash, IntoIterator)]
1077pub struct Specification {
1078    #[into_iterator(owned, ref, ref_mut)]
1079    pub formulas: Vec<AnnotatedFormula>,
1080}
1081
1082impl_node!(Specification, Format, SpecificationParser);
1083
1084impl Specification {
1085    pub fn empty() -> Self {
1086        Specification { formulas: vec![] }
1087    }
1088
1089    pub fn predicates(&self) -> IndexSet<Predicate> {
1090        let mut predicates = IndexSet::new();
1091        for formula in &self.formulas {
1092            predicates.extend(formula.predicates())
1093        }
1094        predicates
1095    }
1096
1097    pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
1098        self.into_iter()
1099            .map(|f| f.replace_placeholders(mapping))
1100            .collect()
1101    }
1102}
1103
1104impl FromIterator<AnnotatedFormula> for Specification {
1105    fn from_iter<T: IntoIterator<Item = AnnotatedFormula>>(iter: T) -> Self {
1106        Specification {
1107            formulas: iter.into_iter().collect(),
1108        }
1109    }
1110}
1111
1112#[derive(Clone, Debug, Eq, PartialEq, Hash)]
1113pub struct PlaceholderDeclaration {
1114    pub name: String,
1115    pub sort: Sort,
1116}
1117
1118impl_node!(PlaceholderDeclaration, Format, PlaceholderDeclarationParser);
1119
1120#[derive(Clone, Debug, Eq, PartialEq, Hash)]
1121pub enum UserGuideEntry {
1122    InputPredicate(Predicate),
1123    OutputPredicate(Predicate),
1124    PlaceholderDeclaration(PlaceholderDeclaration),
1125    AnnotatedFormula(AnnotatedFormula),
1126}
1127
1128impl_node!(UserGuideEntry, Format, UserGuideEntryParser);
1129
1130#[derive(Clone, Debug, Eq, PartialEq, Hash, IntoIterator)]
1131pub struct UserGuide {
1132    #[into_iterator(owned, ref, ref_mut)]
1133    pub entries: Vec<UserGuideEntry>,
1134}
1135
1136impl_node!(UserGuide, Format, UserGuideParser);
1137
1138impl UserGuide {
1139    pub fn input_predicates(&self) -> IndexSet<Predicate> {
1140        let mut result = IndexSet::new();
1141        for entry in &self.entries {
1142            if let UserGuideEntry::InputPredicate(p) = entry {
1143                result.insert(p.clone());
1144            }
1145        }
1146        result
1147    }
1148
1149    pub fn output_predicates(&self) -> IndexSet<Predicate> {
1150        let mut result = IndexSet::new();
1151        for entry in &self.entries {
1152            if let UserGuideEntry::OutputPredicate(p) = entry {
1153                result.insert(p.clone());
1154            }
1155        }
1156        result
1157    }
1158
1159    pub fn public_predicates(&self) -> IndexSet<Predicate> {
1160        let mut result = self.input_predicates();
1161        result.extend(self.output_predicates());
1162        result
1163    }
1164
1165    pub fn placeholders(&self) -> IndexSet<FunctionConstant> {
1166        let mut result = IndexSet::new();
1167        for entry in &self.entries {
1168            if let UserGuideEntry::PlaceholderDeclaration(p) = entry {
1169                let fc = FunctionConstant::from(p.clone());
1170                result.insert(fc);
1171            }
1172        }
1173        result
1174    }
1175
1176    pub fn formulas(&self) -> Vec<AnnotatedFormula> {
1177        let mut result = Vec::new();
1178        for entry in &self.entries {
1179            if let UserGuideEntry::AnnotatedFormula(p) = entry {
1180                result.push(p.clone());
1181            }
1182        }
1183        result
1184    }
1185}
1186
1187impl FromIterator<UserGuideEntry> for UserGuide {
1188    fn from_iter<T: IntoIterator<Item = UserGuideEntry>>(iter: T) -> Self {
1189        UserGuide {
1190            entries: iter.into_iter().collect(),
1191        }
1192    }
1193}
1194
1195#[cfg(test)]
1196mod tests {
1197    use {super::Formula, indexmap::IndexSet};
1198
1199    #[test]
1200    fn test_formula_conjoin() {
1201        for (src, target) in [
1202            (vec![], "#true"),
1203            (vec!["X = Y"], "X = Y"),
1204            (vec!["X = Y", "p(a)", "q(X)"], "(X = Y and p(a)) and q(X)"),
1205        ] {
1206            assert_eq!(
1207                Formula::conjoin(src.iter().map(|x| x.parse().unwrap())),
1208                target.parse().unwrap(),
1209            )
1210        }
1211    }
1212
1213    #[test]
1214    fn test_formula_disjoin() {
1215        for (src, target) in [
1216            (vec![], "#false"),
1217            (vec!["X = Y"], "X = Y"),
1218            (vec!["X = Y", "p(a)", "q(X)"], "(X = Y or p(a)) or q(X)"),
1219        ] {
1220            assert_eq!(
1221                Formula::disjoin(src.iter().map(|x| x.parse().unwrap())),
1222                target.parse().unwrap(),
1223            )
1224        }
1225    }
1226
1227    #[test]
1228    fn test_formula_free_variables() {
1229        for (src, target) in [
1230            ("forall X (X = Y)", vec!["Y"]),
1231            ("forall X (X = Y) and Y = Z", vec!["Y", "Z"]),
1232            ("forall X exists Y (X = Y)", vec![]),
1233        ] {
1234            assert_eq!(
1235                src.parse::<Formula>().unwrap().free_variables(),
1236                target
1237                    .iter()
1238                    .map(|x| x.parse().unwrap())
1239                    .collect::<IndexSet<_>>(),
1240            )
1241        }
1242    }
1243
1244    #[test]
1245    fn test_formula_substitute() {
1246        for (src, var, term, target) in [
1247            ("p(X)", "X", "s", "p(s)"),
1248            ("p(X)", "X", "5", "p(5)"),
1249            ("prime(-X$i + 13)", "X$i", "3*Y$i", "prime(-(3*Y$i) + 13)"),
1250            ("prime(X$i, X)", "X$i", "Y$i", "prime(Y$i, X)"),
1251            ("exists X (X = Y)", "Y", "3", "exists X (X = 3)"),
1252            ("forall X p(X)", "X", "1", "forall X p(X)"),
1253            (
1254                "exists X (X = Y)",
1255                "Y",
1256                "X$i + 3",
1257                "exists X (X = (X$i + 3))",
1258            ),
1259            (
1260                "forall X (q(Y) or exists Y (p(1,Y) and X > Y))",
1261                "Y",
1262                "a",
1263                "forall X (q(a) or exists Y (p(1,Y) and X > Y))",
1264            ),
1265            (
1266                "forall X (q(Y$i) or exists Z (p(1,Z) and X > Y$i > Z))",
1267                "Y$i",
1268                "4",
1269                "forall X (q(4) or exists Z (p(1,Z) and X > 4 > Z))",
1270            ),
1271            (
1272                "exists J$i (J$i = N$i and Z = Z1)",
1273                "Z",
1274                "I",
1275                "exists J$i (J$i = N$i and I = Z1)",
1276            ),
1277            (
1278                "X = 5 and exists Y ( p(X, Y) )",
1279                "X",
1280                "Z",
1281                "Z = 5 and exists Y ( p(Z, Y) )",
1282            ),
1283            (
1284                "X = 5 and exists Y ( p(X, Y) )",
1285                "X",
1286                "Y",
1287                "Y = 5 and exists Y1 ( p(Y, Y1) )",
1288            ),
1289            (
1290                "X = 5 and exists Y ( p(X, Y, Y1) )",
1291                "X",
1292                "Y",
1293                "Y = 5 and exists Y2 ( p(Y, Y2, Y1) )",
1294            ),
1295        ] {
1296            assert_eq!(
1297                src.parse::<Formula>()
1298                    .unwrap()
1299                    .substitute(var.parse().unwrap(), term.parse().unwrap()),
1300                target.parse().unwrap()
1301            )
1302        }
1303    }
1304}
anthem/syntax_tree/fol/sigma_0.rs

anthem/syntax_tree/fol/
sigma_0.rs
