Merge branch 'master' into zach/timing2

Cargo.toml

@@ -25,7 +25,7 @@ pest = "2"
 pest_derive = "2"
 petgraph = "0.6"
 regex = "1"
-thiserror = "1"
+thiserror = "2"
 threadpool = "1"
 walkdir = "2"
 

res/examples/external_equivalence/orphan/.gitignore

@@ -0,0 +1 @@
+out

res/examples/external_equivalence/orphan/README.md

@@ -0,0 +1,16 @@
+# `orphan`
+
+## Usage
+
+Note that the programs are not externally equivalent under user guide `orphan.a.ug`,
+but `orphan.b.ug` adds missing assumptions under which the programs are indeed externally equivalent.
+```
+anthem verify --equivalence external orphan.1.lp orphan.2.lp orphan.b.ug
+```
+
+## Origin
+This example was taken from
+
+> Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, Nathan Temple.
+> External Behavior of a Logic Program and Verification of Refactoring. TPLP 23(4): 933-947 (2023).
+> https://doi.org/10.1017/S1471068423000200

res/examples/external_equivalence/orphan/orphan.1.lp

@@ -0,0 +1,3 @@
+parent_living(X) :- father(Y,X), living(Y).
+parent_living(X) :- mother(Y,X), living(Y).
+orphan(X) :- living(X), not parent_living(X).

res/examples/external_equivalence/orphan/orphan.2.lp

@@ -0,0 +1 @@
+orphan(X) :- living(X), father(Y,X), mother(Z,X), not living(Y), not living(Z).

res/examples/external_equivalence/orphan/orphan.a.ug

@@ -0,0 +1,4 @@
+input: living/1.
+input: father/2.
+input: mother/2.
+output: orphan/1.

res/examples/external_equivalence/orphan/orphan.b.ug

@@ -0,0 +1,7 @@
+input: living/1.
+input: father/2.
+input: mother/2.
+output: orphan/1.
+
+assumption: forall X exists Y forall Z (father(Z,X) <-> Y=Z).
+assumption: forall X exists Y forall Z (mother(Z,X) <-> Y=Z).

src/formatting/fol/default.rs

@@ -438,11 +438,81 @@ mod tests {
         formatting::fol::default::Format,
         syntax_tree::fol::{
             AnnotatedFormula, Atom, AtomicFormula, BinaryConnective, BinaryOperator, Comparison,
-            Direction, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier,
-            Relation, Role, Sort, Specification, SymbolicTerm, UnaryConnective, Variable,
+            Direction, Formula, GeneralTerm, Guard, IntegerTerm, PlaceholderDeclaration, Predicate,
+            Quantification, Quantifier, Relation, Role, Sort, Specification, SymbolicTerm, Theory,
+            UnaryConnective, UnaryOperator, UserGuide, UserGuideEntry, Variable,
         },
     };
 
+    #[test]
+    fn format_unary_operator() {
+        assert_eq!(Format(&UnaryOperator::Negative).to_string(), "-");
+    }
+
+    #[test]
+    fn format_binary_operator() {
+        for (left, right) in [
+            (BinaryOperator::Add, "+"),
+            (BinaryOperator::Subtract, "-"),
+            (BinaryOperator::Multiply, "*"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_relation() {
+        for (left, right) in [
+            (Relation::Less, "<"),
+            (Relation::Greater, ">"),
+            (Relation::LessEqual, "<="),
+            (Relation::GreaterEqual, ">="),
+            (Relation::Equal, "="),
+            (Relation::NotEqual, "!="),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_unary_connective() {
+        assert_eq!(Format(&UnaryConnective::Negation).to_string(), "not");
+    }
+
+    #[test]
+    fn format_binary_connective() {
+        for (left, right) in [
+            (BinaryConnective::Conjunction, "and"),
+            (BinaryConnective::Disjunction, "or"),
+            (BinaryConnective::Implication, "->"),
+            (BinaryConnective::ReverseImplication, "<-"),
+            (BinaryConnective::Equivalence, "<->"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_quantifier() {
+        for (left, right) in [
+            (Quantifier::Forall, "forall"),
+            (Quantifier::Exists, "exists"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_sort() {
+        for (left, right) in [
+            (Sort::General, "g"),
+            (Sort::Integer, "i"),
+            (Sort::Symbol, "s"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
     #[test]
     fn format_integer_term() {
         assert_eq!(Format(&IntegerTerm::Numeral(-1)).to_string(), "-1");
@@ -832,6 +902,89 @@ mod tests {
         );
     }
 
+    #[test]
+    fn format_theory() {
+        assert_eq!(
+            Format(&Theory {
+                formulas: vec![
+                    Formula::AtomicFormula(AtomicFormula::Truth).into(),
+                    Formula::BinaryFormula {
+                        connective: BinaryConnective::Equivalence,
+                        lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                            predicate_symbol: "p".to_string(),
+                            terms: vec![]
+                        }))
+                        .into(),
+                        rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                            predicate_symbol: "q".to_string(),
+                            terms: vec![]
+                        }))
+                        .into()
+                    }
+                ],
+            })
+            .to_string(),
+            "#true.\np <-> q.\n"
+        );
+    }
+
+    #[test]
+    fn format_role() {
+        for (left, right) in [
+            (Role::Assumption, "assumption"),
+            (Role::Spec, "spec"),
+            (Role::Lemma, "lemma"),
+            (Role::Definition, "definition"),
+            (Role::InductiveLemma, "inductive-lemma"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_direction() {
+        for (left, right) in [
+            (Direction::Universal, "universal"),
+            (Direction::Forward, "forward"),
+            (Direction::Backward, "backward"),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_annotated_formula() {
+        for (left, right) in [
+            (
+                AnnotatedFormula {
+                    role: Role::Lemma,
+                    direction: Direction::Universal,
+                    name: "lemma_p".to_string(),
+                    formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                        predicate_symbol: "p".to_string(),
+                        terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Numeral(1))],
+                    })),
+                },
+                "lemma[lemma_p]: p(1)",
+            ),
+            (
+                AnnotatedFormula {
+                    role: Role::Assumption,
+                    direction: Direction::Forward,
+                    name: String::default(),
+                    formula: Formula::BinaryFormula {
+                        connective: BinaryConnective::Disjunction,
+                        lhs: Formula::AtomicFormula(AtomicFormula::Truth).into(),
+                        rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(),
+                    },
+                },
+                "assumption(forward): #true or #false",
+            ),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
     #[test]
     fn format_specification() {
         let left = Format(&Specification {
@@ -901,4 +1054,81 @@ mod tests {
         let right = "spec(forward)[about_p_0]: not p(0).\nassumption: p(5).\ninductive-lemma(backward)[il1]: forall X (p(X) <-> q(X) or t).\n".to_string();
         assert_eq!(left, right, "\n{left}!=\n{right}");
     }
+
+    #[test]
+    fn format_placeholder_declaration() {
+        assert_eq!(
+            Format(&PlaceholderDeclaration {
+                name: "n".to_string(),
+                sort: Sort::Integer,
+            })
+            .to_string(),
+            "n -> i"
+        );
+    }
+
+    #[test]
+    fn format_user_guide_entry() {
+        for (left, right) in [
+            (
+                UserGuideEntry::InputPredicate(Predicate {
+                    symbol: "p".to_string(),
+                    arity: 0,
+                }),
+                "input: p/0",
+            ),
+            (
+                UserGuideEntry::OutputPredicate(Predicate {
+                    symbol: "q".to_string(),
+                    arity: 1,
+                }),
+                "output: q/1",
+            ),
+            (
+                UserGuideEntry::PlaceholderDeclaration(PlaceholderDeclaration {
+                    name: "a".to_string(),
+                    sort: Sort::Symbol,
+                }),
+                "input: a -> s",
+            ),
+            (
+                UserGuideEntry::AnnotatedFormula(AnnotatedFormula {
+                    role: Role::Lemma,
+                    direction: Direction::Backward,
+                    name: String::default(),
+                    formula: Formula::UnaryFormula {
+                        connective: UnaryConnective::Negation,
+                        formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
+                            predicate_symbol: "p".to_string(),
+                            terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Numeral(1))],
+                        }))
+                        .into(),
+                    },
+                }),
+                "lemma(backward): not p(1)",
+            ),
+        ] {
+            assert_eq!(Format(&left).to_string(), right);
+        }
+    }
+
+    #[test]
+    fn format_user_guide() {
+        assert_eq!(
+            Format(&UserGuide {
+                entries: vec![
+                    UserGuideEntry::PlaceholderDeclaration(PlaceholderDeclaration {
+                        name: "n".to_string(),
+                        sort: Sort::Integer,
+                    }),
+                    UserGuideEntry::OutputPredicate(Predicate {
+                        symbol: "q".to_string(),
+                        arity: 2,
+                    }),
+                ],
+            })
+            .to_string(),
+            "input: n -> i.\noutput: q/2.\n",
+        );
+    }
 }

src/parsing/fol/grammar.pest

@@ -104,7 +104,7 @@ formula_eoi = _{ formula ~ EOI }
     infix   = _{ binary_connective }
     primary = _{ "(" ~ formula ~ ")" | atomic_formula }
 
-theory = { (formula ~ ".")* }
+theory = { &ANY? ~ (formula ~ ".")* }
 theory_eoi = _{ theory ~ EOI }
 
 role = { assumption | spec | lemma | definition | inductive_lemma }
@@ -124,7 +124,7 @@ direction_eoi = _{ direction ~ EOI }
 annotated_formula = { role ~ ("(" ~ direction ~ ")")? ~ ("[" ~ symbolic_constant ~ "]")? ~ ":" ~ formula }
 annotated_formula_eoi = _{ annotated_formula ~ EOI }
 
-specification = { (annotated_formula ~ ".")* }
+specification = { &ANY? ~ (annotated_formula ~ ".")* }
 specification_eoi = _{ specification ~ EOI }
 
 user_guide_entry = { input_predicate | output_predicate | placeholder_declaration | annotated_formula }
@@ -133,5 +133,5 @@ user_guide_entry_eoi = _{ user_guide_entry ~ EOI }
     output_predicate        = { "output" ~ ":" ~ predicate}
     placeholder_declaration = { "input" ~ ":" ~ symbolic_constant ~ ("->" ~ sort)? }
 
-user_guide = { (user_guide_entry ~ ".")* }
+user_guide = { &ANY? ~ (user_guide_entry ~ ".")* }
 user_guide_eoi = _{ user_guide ~ EOI }