From f01cbb69f1bc18af1184a8115fd9f0300c7a13ef Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachhansen@unomaha.edu>
Date: Tue, 21 Nov 2023 13:55:58 -0600
Subject: [PATCH 1/5] Adding predicates helper functions to ASP AST

---
 src/syntax_tree/asp.rs | 64 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/src/syntax_tree/asp.rs b/src/syntax_tree/asp.rs
index 882857c3..5400a849 100644
--- a/src/syntax_tree/asp.rs
+++ b/src/syntax_tree/asp.rs
@@ -77,6 +77,12 @@ impl Term {
     }
 }
 
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub struct Predicate {
+    pub symbol: String,
+    pub arity: usize,
+}
+
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Atom {
     pub predicate: String,
@@ -116,6 +122,10 @@ impl Literal {
     pub fn variables(&self) -> HashSet<Variable> {
         self.atom.variables()
     }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        HashSet::from([self.atom.predicate()])
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -162,6 +172,13 @@ impl AtomicFormula {
             AtomicFormula::Comparison(c) => c.variables(),
         }
     }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        match &self {
+            AtomicFormula::Literal(l) => l.predicates(),
+            AtomicFormula::Comparison(c) => HashSet::new(),
+        }
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -182,6 +199,13 @@ impl Head {
         }
     }
 
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        match self {
+            Head::Basic(a) | Head::Choice(a) => HashSet::from([a.predicate()]),
+            Head::Falsity => HashSet::new(),
+        }
+    }
+
     pub fn terms(&self) -> Option<&[Term]> {
         match self {
             Head::Basic(a) => Some(&a.terms),
@@ -213,6 +237,26 @@ pub struct Body {
 
 impl_node!(Body, Format, BodyParser);
 
+impl Body {
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = HashSet::<Predicate>::new();
+        for form in self.formulas.iter() {
+            preds.extend(form.predicates());
+        }
+        preds
+    }
+}
+
+impl Body {
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = HashSet::<Predicate>::new();
+        for form in self.formulas.iter() {
+            preds.extend(form.predicates());
+        }
+        preds
+    }
+}
+
 impl Body {
     pub fn variables(&self) -> HashSet<Variable> {
         let mut vars = HashSet::new();
@@ -237,6 +281,18 @@ impl Rule {
         vars.extend(self.body.variables());
         vars
     }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = self.body.predicates();
+        preds.extend(self.head.predicates());
+        preds
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = self.body.predicates();
+        preds.extend(self.head.predicates());
+        preds
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -254,4 +310,12 @@ impl Program {
         }
         vars
     }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = HashSet::new();
+        for rule in self.rules.iter() {
+            preds.extend(rule.predicates())
+        }
+        preds
+    }
 }

From 3e075aeff856126af41111958dca5294fbfbd1e2 Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Tue, 28 Nov 2023 10:53:12 -0600
Subject: [PATCH 2/5] Adding Predicate node to ASP AST

---
 src/formatting/asp/default.rs |  59 ++++--
 src/parsing/asp/pest.rs       | 172 +++++++++++-------
 src/syntax_tree/asp.rs        |  34 +---
 temp.rs                       | 326 ++++++++++++++++++++++++++++++++++
 4 files changed, 490 insertions(+), 101 deletions(-)
 create mode 100644 temp.rs

diff --git a/src/formatting/asp/default.rs b/src/formatting/asp/default.rs
index b5bb0208..f9c39bf3 100644
--- a/src/formatting/asp/default.rs
+++ b/src/formatting/asp/default.rs
@@ -108,7 +108,7 @@ impl Display for Format<'_, Term> {
 
 impl Display for Format<'_, Atom> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let predicate = &self.0.predicate;
+        let predicate = &self.0.predicate.symbol;
         let terms = &self.0.terms;
 
         write!(f, "{predicate}")?;
@@ -228,7 +228,7 @@ mod tests {
         formatting::asp::default::Format,
         syntax_tree::asp::{
             Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal, PrecomputedTerm,
-            Program, Relation, Rule, Sign, Term, UnaryOperator, Variable,
+            Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable,
         },
     };
 
@@ -342,7 +342,10 @@ mod tests {
     fn format_atom() {
         assert_eq!(
             Format(&Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 0,
+                },
                 terms: vec![],
             })
             .to_string(),
@@ -351,7 +354,10 @@ mod tests {
 
         assert_eq!(
             Format(&Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 1,
+                },
                 terms: vec![Term::PrecomputedTerm(PrecomputedTerm::Numeral(1))],
             })
             .to_string(),
@@ -360,7 +366,10 @@ mod tests {
 
         assert_eq!(
             Format(&Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 2,
+                },
                 terms: vec![
                     Term::PrecomputedTerm(PrecomputedTerm::Numeral(1)),
                     Term::PrecomputedTerm(PrecomputedTerm::Numeral(2))
@@ -384,7 +393,10 @@ mod tests {
             Format(&Literal {
                 sign: Sign::Negation,
                 atom: Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }
             })
@@ -422,7 +434,10 @@ mod tests {
             Format(&AtomicFormula::Literal(Literal {
                 sign: Sign::DoubleNegation,
                 atom: Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }
             }))
@@ -445,7 +460,10 @@ mod tests {
     fn format_head() {
         assert_eq!(
             Format(&Head::Basic(Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 0,
+                },
                 terms: vec![]
             }))
             .to_string(),
@@ -454,7 +472,10 @@ mod tests {
 
         assert_eq!(
             Format(&Head::Choice(Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 0,
+                },
                 terms: vec![]
             }))
             .to_string(),
@@ -474,7 +495,10 @@ mod tests {
                     AtomicFormula::Literal(Literal {
                         sign: Sign::NoSign,
                         atom: Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 1,
+                            },
                             terms: vec![Term::Variable(Variable("X".into()))]
                         }
                     }),
@@ -502,21 +526,30 @@ mod tests {
                 rules: vec![
                     Rule {
                         head: Head::Basic(Atom {
-                            predicate: "a".into(),
+                            predicate: Predicate {
+                                symbol: "a".into(),
+                                arity: 0,
+                            },
                             terms: vec![]
                         }),
                         body: Body { formulas: vec![] }
                     },
                     Rule {
                         head: Head::Basic(Atom {
-                            predicate: "b".into(),
+                            predicate: Predicate {
+                                symbol: "b".into(),
+                                arity: 0,
+                            },
                             terms: vec![]
                         }),
                         body: Body {
                             formulas: vec![AtomicFormula::Literal(Literal {
                                 sign: Sign::Negation,
                                 atom: Atom {
-                                    predicate: "a".into(),
+                                    predicate: Predicate {
+                                        symbol: "a".into(),
+                                        arity: 0,
+                                    },
                                     terms: vec![]
                                 }
                             })]
diff --git a/src/parsing/asp/pest.rs b/src/parsing/asp/pest.rs
index 85614444..b81484ad 100644
--- a/src/parsing/asp/pest.rs
+++ b/src/parsing/asp/pest.rs
@@ -2,7 +2,7 @@ use crate::{
     parsing::PestParser,
     syntax_tree::asp::{
         Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal, PrecomputedTerm,
-        Program, Relation, Rule, Sign, Term, UnaryOperator, Variable,
+        Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable,
     },
 };
 
@@ -153,13 +153,19 @@ impl PestParser for AtomParser {
 
         let mut pairs = pair.into_inner();
 
-        let predicate = pairs
+        let p = pairs
             .next()
             .unwrap_or_else(|| Self::report_missing_pair())
             .as_str()
             .into();
+
         let terms: Vec<_> = pairs.map(TermParser::translate_pair).collect();
 
+        let predicate = Predicate {
+            symbol: p,
+            arity: terms.len(),
+        };
+
         Atom { predicate, terms }
     }
 }
@@ -421,7 +427,8 @@ mod tests {
             parsing::TestedParser,
             syntax_tree::asp::{
                 Atom, AtomicFormula, BinaryOperator, Body, Comparison, Head, Literal,
-                PrecomputedTerm, Program, Relation, Rule, Sign, Term, UnaryOperator, Variable,
+                PrecomputedTerm, Predicate, Program, Relation, Rule, Sign, Term, UnaryOperator,
+                Variable,
             },
         },
     };
@@ -742,28 +749,40 @@ mod tests {
                 (
                     "p",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 ),
                 (
                     "p()",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 ),
                 (
                     "p(1)",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 1,
+                        },
                         terms: vec![Term::PrecomputedTerm(PrecomputedTerm::Numeral(1))],
                     },
                 ),
                 (
                     "p(1, 2)",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 2,
+                        },
                         terms: vec![
                             Term::PrecomputedTerm(PrecomputedTerm::Numeral(1)),
                             Term::PrecomputedTerm(PrecomputedTerm::Numeral(2)),
@@ -793,7 +812,10 @@ mod tests {
                 Literal {
                     sign: Sign::NoSign,
                     atom: Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 },
@@ -803,7 +825,10 @@ mod tests {
                 Literal {
                     sign: Sign::Negation,
                     atom: Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 },
@@ -813,7 +838,10 @@ mod tests {
                 Literal {
                     sign: Sign::DoubleNegation,
                     atom: Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 },
@@ -823,7 +851,10 @@ mod tests {
                 Literal {
                     sign: Sign::NoSign,
                     atom: Atom {
-                        predicate: "notp".into(),
+                        predicate: Predicate {
+                            symbol: "notp".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 },
@@ -873,7 +904,10 @@ mod tests {
                 AtomicFormula::Literal(Literal {
                     sign: Sign::Negation,
                     atom: Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 }),
@@ -887,14 +921,20 @@ mod tests {
             (
                 "p",
                 Head::Basic(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![],
                 }),
             ),
             (
                 "{p}",
                 Head::Choice(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![],
                 }),
             ),
@@ -912,7 +952,10 @@ mod tests {
                     formulas: vec![AtomicFormula::Literal(Literal {
                         sign: Sign::NoSign,
                         atom: Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 0,
+                            },
                             terms: vec![],
                         },
                     })],
@@ -925,7 +968,10 @@ mod tests {
                         AtomicFormula::Literal(Literal {
                             sign: Sign::NoSign,
                             atom: Atom {
-                                predicate: "p".into(),
+                                predicate: Predicate {
+                                    symbol: "p".into(),
+                                    arity: 0,
+                                },
                                 terms: vec![],
                             },
                         }),
@@ -955,14 +1001,20 @@ mod tests {
                     "a :- b.",
                     Rule {
                         head: Head::Basic(Atom {
-                            predicate: "a".into(),
+                            predicate: Predicate {
+                                symbol: "a".into(),
+                                arity: 0,
+                            },
                             terms: vec![],
                         }),
                         body: Body {
                             formulas: vec![AtomicFormula::Literal(Literal {
                                 sign: Sign::NoSign,
                                 atom: Atom {
-                                    predicate: "b".into(),
+                                    predicate: Predicate {
+                                        symbol: "b".into(),
+                                        arity: 0,
+                                    },
                                     terms: vec![],
                                 },
                             })],
@@ -973,7 +1025,10 @@ mod tests {
                     "a :-.",
                     Rule {
                         head: Head::Basic(Atom {
-                            predicate: "a".into(),
+                            predicate: Predicate {
+                                symbol: "a".into(),
+                                arity: 0,
+                            },
                             terms: vec![],
                         }),
                         body: Body { formulas: vec![] },
@@ -983,7 +1038,10 @@ mod tests {
                     "a.",
                     Rule {
                         head: Head::Basic(Atom {
-                            predicate: "a".into(),
+                            predicate: Predicate {
+                                symbol: "a".into(),
+                                arity: 0,
+                            },
                             terms: vec![],
                         }),
                         body: Body { formulas: vec![] },
@@ -995,49 +1053,43 @@ mod tests {
 
     #[test]
     fn parse_program() {
-        ProgramParser.should_parse_into([
-            ("", Program { rules: vec![] }),
-            (
-                "a. b :- a.",
-                Program {
-                    rules: vec![
-                        Rule {
-                            head: Head::Basic(Atom {
-                                predicate: "a".into(),
-                                terms: vec![],
-                            }),
-                            body: Body { formulas: vec![] },
-                        },
-                        Rule {
-                            head: Head::Basic(Atom {
-                                predicate: "b".into(),
-                                terms: vec![],
-                            }),
-                            body: Body {
-                                formulas: vec![AtomicFormula::Literal(Literal {
-                                    sign: Sign::NoSign,
-                                    atom: Atom {
-                                        predicate: "a".into(),
-                                        terms: vec![],
-                                    },
-                                })],
-                            },
-                        },
-                    ],
-                },
-            ),
-            (
-                "a.\n",
-                Program {
-                    rules: vec![Rule {
+        ProgramParser.should_parse_into([(
+            "a. b :- a.",
+            Program {
+                rules: vec![
+                    Rule {
                         head: Head::Basic(Atom {
-                            predicate: "a".into(),
+                            predicate: Predicate {
+                                symbol: "a".into(),
+                                arity: 0,
+                            },
                             terms: vec![],
                         }),
                         body: Body { formulas: vec![] },
-                    }],
-                },
-            ),
-        ]);
+                    },
+                    Rule {
+                        head: Head::Basic(Atom {
+                            predicate: Predicate {
+                                symbol: "b".into(),
+                                arity: 0,
+                            },
+                            terms: vec![],
+                        }),
+                        body: Body {
+                            formulas: vec![AtomicFormula::Literal(Literal {
+                                sign: Sign::NoSign,
+                                atom: Atom {
+                                    predicate: Predicate {
+                                        symbol: "a".into(),
+                                        arity: 0,
+                                    },
+                                    terms: vec![],
+                                },
+                            })],
+                        },
+                    },
+                ],
+            },
+        )]);
     }
 }
diff --git a/src/syntax_tree/asp.rs b/src/syntax_tree/asp.rs
index 5400a849..4b057c0c 100644
--- a/src/syntax_tree/asp.rs
+++ b/src/syntax_tree/asp.rs
@@ -85,7 +85,7 @@ pub struct Predicate {
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Atom {
-    pub predicate: String,
+    pub predicate: Predicate,
     pub terms: Vec<Term>,
 }
 
@@ -99,6 +99,10 @@ impl Atom {
         }
         vars
     }
+
+    pub fn predicate(&self) -> Predicate {
+        self.predicate.clone()
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -176,7 +180,7 @@ impl AtomicFormula {
     pub fn predicates(&self) -> HashSet<Predicate> {
         match &self {
             AtomicFormula::Literal(l) => l.predicates(),
-            AtomicFormula::Comparison(c) => HashSet::new(),
+            AtomicFormula::Comparison(_) => HashSet::new(),
         }
     }
 }
@@ -191,14 +195,6 @@ pub enum Head {
 impl_node!(Head, Format, HeadParser);
 
 impl Head {
-    pub fn predicate(&self) -> Option<&str> {
-        match self {
-            Head::Basic(a) => Some(&a.predicate),
-            Head::Choice(a) => Some(&a.predicate),
-            Head::Falsity => None,
-        }
-    }
-
     pub fn predicates(&self) -> HashSet<Predicate> {
         match self {
             Head::Basic(a) | Head::Choice(a) => HashSet::from([a.predicate()]),
@@ -245,19 +241,7 @@ impl Body {
         }
         preds
     }
-}
 
-impl Body {
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        let mut preds = HashSet::<Predicate>::new();
-        for form in self.formulas.iter() {
-            preds.extend(form.predicates());
-        }
-        preds
-    }
-}
-
-impl Body {
     pub fn variables(&self) -> HashSet<Variable> {
         let mut vars = HashSet::new();
         for formula in self.formulas.iter() {
@@ -287,12 +271,6 @@ impl Rule {
         preds.extend(self.head.predicates());
         preds
     }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        let mut preds = self.body.predicates();
-        preds.extend(self.head.predicates());
-        preds
-    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
diff --git a/temp.rs b/temp.rs
new file mode 100644
index 00000000..1c020b0d
--- /dev/null
+++ b/temp.rs
@@ -0,0 +1,326 @@
+use std::hash::Hash;
+
+use {
+    crate::{
+        formatting::asp::default::Format,
+        parsing::asp::pest::{
+            AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser,
+            HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser,
+            RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser,
+        },
+        syntax_tree::{impl_node, Node},
+    },
+    std::collections::HashSet,
+};
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum PrecomputedTerm {
+    Infimum,
+    Numeral(isize),
+    Symbol(String),
+    Supremum,
+}
+
+impl_node!(PrecomputedTerm, Format, PrecomputedTermParser);
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub struct Variable(pub String);
+
+impl_node!(Variable, Format, VariableParser);
+
+#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+pub enum UnaryOperator {
+    Negative,
+}
+
+impl_node!(UnaryOperator, Format, UnaryOperatorParser);
+
+#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+pub enum BinaryOperator {
+    Add,
+    Subtract,
+    Multiply,
+    Divide,
+    Modulo,
+    Interval,
+}
+
+impl_node!(BinaryOperator, Format, BinaryOperatorParser);
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum Term {
+    PrecomputedTerm(PrecomputedTerm),
+    Variable(Variable),
+    UnaryOperation {
+        op: UnaryOperator,
+        arg: Box<Term>,
+    },
+    BinaryOperation {
+        op: BinaryOperator,
+        lhs: Box<Term>,
+        rhs: Box<Term>,
+    },
+}
+
+impl_node!(Term, Format, TermParser);
+
+impl Term {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            Term::PrecomputedTerm(_) => HashSet::new(),
+            Term::Variable(v) => HashSet::from([v.clone()]),
+            Term::UnaryOperation { arg, .. } => arg.variables(),
+            Term::BinaryOperation { lhs, rhs, .. } => {
+                let mut vars = lhs.variables();
+                vars.extend(rhs.variables());
+                vars
+            }
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub struct Predicate {
+    pub symbol: String,
+    pub arity: usize,
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Atom {
+    pub predicate: Predicate,
+    pub terms: Vec<Term>,
+}
+
+impl_node!(Atom, Format, AtomParser);
+
+impl Atom {
+    pub fn predicate(&self) -> Predicate {
+        self.predicate.clone()
+    }
+
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for term in self.terms.iter() {
+            vars.extend(term.variables())
+        }
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum Sign {
+    NoSign,
+    Negation,
+    DoubleNegation,
+}
+
+impl_node!(Sign, Format, SignParser);
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Literal {
+    pub sign: Sign,
+    pub atom: Atom,
+}
+
+impl_node!(Literal, Format, LiteralParser);
+
+impl Literal {
+    pub fn variables(&self) -> HashSet<Variable> {
+        self.atom.variables()
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        HashSet::from([self.atom.predicate()])
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum Relation {
+    Equal,
+    NotEqual,
+    Less,
+    LessEqual,
+    Greater,
+    GreaterEqual,
+}
+
+impl_node!(Relation, Format, RelationParser);
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Comparison {
+    pub relation: Relation,
+    pub lhs: Term,
+    pub rhs: Term,
+}
+
+impl_node!(Comparison, Format, ComparisonParser);
+
+impl Comparison {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = self.lhs.variables();
+        vars.extend(self.rhs.variables());
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum AtomicFormula {
+    Literal(Literal),
+    Comparison(Comparison),
+}
+
+impl_node!(AtomicFormula, Format, AtomicFormulaParser);
+
+impl AtomicFormula {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            AtomicFormula::Literal(l) => l.variables(),
+            AtomicFormula::Comparison(c) => c.variables(),
+        }
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        match &self {
+            AtomicFormula::Literal(l) => l.predicates(),
+            AtomicFormula::Comparison(_) => HashSet::new(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum Head {
+    Basic(Atom),
+    Choice(Atom),
+    Falsity,
+}
+
+impl_node!(Head, Format, HeadParser);
+
+impl Head {
+    pub fn predicate(&self) -> Option<&Predicate> {
+        match self {
+            Head::Basic(a) => Some(&a.predicate),
+            Head::Choice(a) => Some(&a.predicate),
+            Head::Falsity => None,
+        }
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        match self {
+            Head::Basic(a) | Head::Choice(a) => HashSet::from([a.predicate()]),
+            Head::Falsity => HashSet::new(),
+        }
+    }
+
+    pub fn terms(&self) -> Option<&[Term]> {
+        match self {
+            Head::Basic(a) => Some(&a.terms),
+            Head::Choice(a) => Some(&a.terms),
+            Head::Falsity => None,
+        }
+    }
+
+    pub fn arity(&self) -> usize {
+        match self {
+            Head::Basic(a) => a.terms.len(),
+            Head::Choice(a) => a.terms.len(),
+            Head::Falsity => 0,
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Body {
+    pub formulas: Vec<AtomicFormula>,
+}
+
+impl_node!(Body, Format, BodyParser);
+
+impl Body {
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = HashSet::<Predicate>::new();
+        for form in self.formulas.iter() {
+            preds.extend(form.predicates());
+        }
+        preds
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Rule {
+    pub head: Head,
+    pub body: Body,
+}
+
+impl_node!(Rule, Format, RuleParser);
+
+impl Rule {
+    // TODO: Drop?
+    pub fn is_constraint(&self) -> bool {
+        match &self.head {
+            Head::Basic(_) | Head::Choice(_) => false,
+            Head::Falsity => true,
+        }
+    }
+
+    pub fn head_symbol(&self) -> Option<Predicate> {
+        match &self.head {
+            Head::Basic(a) => Some(a.predicate().clone()),
+            Head::Choice(a) => Some(a.predicate().clone()),
+            Head::Falsity => None,
+        }
+    }
+
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = self.head_variables();
+        vars.extend(self.body_variables());
+        vars
+    }
+
+    pub fn head_variables(&self) -> HashSet<Variable> {
+        match &self.head {
+            Head::Basic(a) | Head::Choice(a) => a.variables(),
+            Head::Falsity => HashSet::new(),
+        }
+    }
+
+    pub fn body_variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for formula in self.body.formulas.iter() {
+            vars.extend(formula.variables())
+        }
+        vars
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = self.body.predicates();
+        preds.extend(self.head.predicates());
+        preds
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Program {
+    pub rules: Vec<Rule>,
+}
+
+impl_node!(Program, Format, ProgramParser);
+
+impl Program {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for rule in self.rules.iter() {
+            vars.extend(rule.variables())
+        }
+        vars
+    }
+
+    pub fn predicates(&self) -> HashSet<Predicate> {
+        let mut preds = HashSet::new();
+        for rule in self.rules.iter() {
+            preds.extend(rule.predicates())
+        }
+        preds
+    }
+}
+

From acd258f558f1df04f1b47ca14b25ffa717a04b96 Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Tue, 28 Nov 2023 11:22:03 -0600
Subject: [PATCH 3/5] Adding Predicate node to fol AST

---
 src/formatting/fol/default.rs | 161 +++++++++++++++++++++++++++-------
 src/formatting/fol/tptp.rs    |  43 ++++++---
 src/parsing/fol/grammar.pest  |   3 +
 src/parsing/fol/pest.rs       | 141 ++++++++++++++++++++++++-----
 src/syntax_tree/fol.rs        |  15 +++-
 5 files changed, 291 insertions(+), 72 deletions(-)

diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs
index a97b8f02..ad79291d 100644
--- a/src/formatting/fol/default.rs
+++ b/src/formatting/fol/default.rs
@@ -4,8 +4,8 @@ use {
         syntax_tree::{
             fol::{
                 Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator,
-                Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier,
-                Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable,
+                Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification,
+                Quantifier, Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable,
             },
             Node,
         },
@@ -101,12 +101,21 @@ impl Display for Format<'_, GeneralTerm> {
     }
 }
 
+impl Display for Format<'_, Predicate> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        let symbol = &self.0.symbol;
+        let arity = &self.0.arity;
+        write!(f, "{symbol}/{arity}")?;
+        Ok(())
+    }
+}
+
 impl Display for Format<'_, Atom> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let predicate = &self.0.predicate;
+        let symbol = &self.0.predicate.symbol;
         let terms = &self.0.terms;
 
-        write!(f, "{predicate}")?;
+        write!(f, "{symbol}")?;
 
         if !terms.is_empty() {
             let mut iter = terms.iter().map(Format);
@@ -324,8 +333,8 @@ mod tests {
         formatting::fol::default::Format,
         syntax_tree::fol::{
             Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, Comparison,
-            Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, Relation, Sort,
-            UnaryConnective, Variable,
+            Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, Quantifier,
+            Relation, Sort, UnaryConnective, Variable,
         },
     };
 
@@ -445,7 +454,10 @@ mod tests {
     fn format_atomic_formula() {
         assert_eq!(
             Format(&AtomicFormula::Atom(Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 2,
+                },
                 terms: vec![
                     GeneralTerm::Symbol("a".into()),
                     GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm(
@@ -476,7 +488,10 @@ mod tests {
     fn format_formula() {
         assert_eq!(
             Format(&Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 0,
+                },
                 terms: vec![]
             })))
             .to_string(),
@@ -487,7 +502,10 @@ mod tests {
             Format(&Formula::UnaryFormula {
                 connective: UnaryConnective::Negation,
                 formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into()
@@ -506,7 +524,10 @@ mod tests {
                     }]
                 },
                 formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 1,
+                    },
                     terms: vec![GeneralTerm::GeneralVariable("X".into())]
                 }))
                 .into()
@@ -521,19 +542,28 @@ mod tests {
                 lhs: Formula::BinaryFormula {
                     connective: BinaryConnective::ReverseImplication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
                 }
                 .into(),
                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "r".into(),
+                    predicate: Predicate {
+                        symbol: "r".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
@@ -546,19 +576,28 @@ mod tests {
             Format(&Formula::BinaryFormula {
                 connective: BinaryConnective::ReverseImplication,
                 lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
                 rhs: Formula::BinaryFormula {
                     connective: BinaryConnective::ReverseImplication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "r".into(),
+                        predicate: Predicate {
+                            symbol: "r".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
@@ -575,19 +614,28 @@ mod tests {
                 lhs: Formula::BinaryFormula {
                     connective: BinaryConnective::Implication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
                 }
                 .into(),
                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "r".into(),
+                    predicate: Predicate {
+                        symbol: "r".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
@@ -600,19 +648,28 @@ mod tests {
             Format(&Formula::BinaryFormula {
                 connective: BinaryConnective::Implication,
                 lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
                 rhs: Formula::BinaryFormula {
                     connective: BinaryConnective::Implication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "r".into(),
+                        predicate: Predicate {
+                            symbol: "r".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
@@ -629,19 +686,28 @@ mod tests {
                 lhs: Formula::BinaryFormula {
                     connective: BinaryConnective::Implication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
                 }
                 .into(),
                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "r".into(),
+                    predicate: Predicate {
+                        symbol: "r".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
@@ -654,19 +720,28 @@ mod tests {
             Format(&Formula::BinaryFormula {
                 connective: BinaryConnective::Implication,
                 lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
                 rhs: Formula::BinaryFormula {
                     connective: BinaryConnective::ReverseImplication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "r".into(),
+                        predicate: Predicate {
+                            symbol: "r".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
@@ -683,19 +758,28 @@ mod tests {
                 lhs: Formula::BinaryFormula {
                     connective: BinaryConnective::ReverseImplication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
                 }
                 .into(),
                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "r".into(),
+                    predicate: Predicate {
+                        symbol: "r".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
@@ -708,19 +792,28 @@ mod tests {
             Format(&Formula::BinaryFormula {
                 connective: BinaryConnective::ReverseImplication,
                 lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "p".into(),
+                    predicate: Predicate {
+                        symbol: "p".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
                 rhs: Formula::BinaryFormula {
                     connective: BinaryConnective::Implication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "r".into(),
+                        predicate: Predicate {
+                            symbol: "r".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
diff --git a/src/formatting/fol/tptp.rs b/src/formatting/fol/tptp.rs
index d22427f6..366e8b19 100644
--- a/src/formatting/fol/tptp.rs
+++ b/src/formatting/fol/tptp.rs
@@ -84,10 +84,10 @@ impl Display for Format<'_, GeneralTerm> {
 
 impl Display for Format<'_, Atom> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let predicate = &self.0.predicate;
+        let symbol = &self.0.predicate.symbol;
         let terms = &self.0.terms;
 
-        write!(f, "{predicate}")?;
+        write!(f, "{symbol}")?;
 
         if !terms.is_empty() {
             let mut iter = terms.iter().map(Format);
@@ -268,8 +268,8 @@ mod tests {
         formatting::fol::tptp::Format,
         syntax_tree::fol::{
             Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, Comparison,
-            Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, Relation, Sort,
-            UnaryOperator, Variable,
+            Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, Quantifier,
+            Relation, Sort, UnaryOperator, Variable,
         },
     };
 
@@ -373,7 +373,10 @@ mod tests {
     fn format_atom() {
         assert_eq!(
             Format(&Atom {
-                predicate: "prime".into(),
+                predicate: Predicate {
+                    symbol: "prime".into(),
+                    arity: 2,
+                },
                 terms: vec![
                     GeneralTerm::IntegerTerm(IntegerTerm::BinaryOperation {
                         op: BinaryOperator::Add,
@@ -530,7 +533,10 @@ mod tests {
     fn format_formula() {
         assert_eq!(
             Format(&Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                predicate: "p".into(),
+                predicate: Predicate {
+                    symbol: "p".into(),
+                    arity: 0,
+                },
                 terms: vec![]
             })))
             .to_string(),
@@ -542,19 +548,28 @@ mod tests {
                 lhs: Formula::BinaryFormula {
                     connective: BinaryConnective::Implication,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![]
                     }))
                     .into()
                 }
                 .into(),
                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                    predicate: "r".into(),
+                    predicate: Predicate {
+                        symbol: "r".into(),
+                        arity: 0,
+                    },
                     terms: vec![]
                 }))
                 .into(),
@@ -580,12 +595,18 @@ mod tests {
                 formula: Formula::BinaryFormula {
                     connective: BinaryConnective::Conjunction,
                     lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     }))
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     }))
                     .into(),
diff --git a/src/parsing/fol/grammar.pest b/src/parsing/fol/grammar.pest
index 0c2d9bc2..ab072416 100644
--- a/src/parsing/fol/grammar.pest
+++ b/src/parsing/fol/grammar.pest
@@ -54,6 +54,9 @@ general_term = { integer_term | symbolic_constant | general_variable }
 
 variable = { integer_variable | general_variable }
 
+predicate = { predicate_symbol ~ "/" ~ arity }
+    arity = { ASCII_DIGIT+ }
+
 atom = { predicate_symbol ~ term_tuple? }
     predicate_symbol  = _{ symbolic_constant }
     term_tuple = _{ "(" ~ (general_term ~ ("," ~ general_term)*)? ~ ")" }
diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs
index 57d8c501..c10d6862 100644
--- a/src/parsing/fol/pest.rs
+++ b/src/parsing/fol/pest.rs
@@ -2,8 +2,8 @@ use crate::{
     parsing::PestParser,
     syntax_tree::fol::{
         Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator, Comparison,
-        Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier, Relation, Sort,
-        Theory, UnaryConnective, UnaryOperator, Variable,
+        Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification, Quantifier, Relation,
+        Sort, Theory, UnaryConnective, UnaryOperator, Variable,
     },
 };
 
@@ -176,17 +176,53 @@ impl PestParser for AtomParser {
 
         let mut pairs = pair.into_inner();
 
-        let predicate = pairs
+        let p = pairs
             .next()
             .unwrap_or_else(|| Self::report_missing_pair())
             .as_str()
             .into();
         let terms: Vec<_> = pairs.map(GeneralTermParser::translate_pair).collect();
 
+        let predicate = Predicate {
+            symbol: p,
+            arity: terms.len(),
+        };
+
         Atom { predicate, terms }
     }
 }
 
+pub struct PredicateParser;
+
+impl PestParser for PredicateParser {
+    type Node = Predicate;
+
+    type InternalParser = internal::Parser;
+    type Rule = internal::Rule;
+    const RULE: Self::Rule = internal::Rule::predicate;
+
+    fn translate_pair(pair: pest::iterators::Pair<'_, Self::Rule>) -> Self::Node {
+        if pair.as_rule() != internal::Rule::predicate {
+            Self::report_unexpected_pair(pair)
+        }
+
+        let mut pairs = pair.into_inner();
+        let symbol = pairs
+            .next()
+            .unwrap_or_else(|| Self::report_missing_pair())
+            .as_str()
+            .into();
+        let arity_string: &str = pairs
+            .next()
+            .unwrap_or_else(|| Self::report_missing_pair())
+            .as_str()
+            .into();
+        let arity: usize = arity_string.parse().unwrap();
+
+        Predicate { symbol, arity }
+    }
+}
+
 pub struct RelationParser;
 
 impl PestParser for RelationParser {
@@ -487,8 +523,8 @@ mod tests {
             parsing::TestedParser,
             syntax_tree::fol::{
                 Atom, AtomicFormula, BasicIntegerTerm, BinaryConnective, BinaryOperator,
-                Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Quantifier,
-                Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable,
+                Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Predicate, Quantification,
+                Quantifier, Relation, Sort, Theory, UnaryConnective, UnaryOperator, Variable,
             },
         },
     };
@@ -753,7 +789,10 @@ mod tests {
                 (
                     "p",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 ),
@@ -761,21 +800,30 @@ mod tests {
                     // Parsing "g" caused issues ealier because "g" is also a sort declaration.
                     "g",
                     Atom {
-                        predicate: "g".into(),
+                        predicate: Predicate {
+                            symbol: "g".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 ),
                 (
                     "p()",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     },
                 ),
                 (
                     "p(1)",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 1,
+                        },
                         terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm(
                             BasicIntegerTerm::Numeral(1),
                         ))],
@@ -784,7 +832,10 @@ mod tests {
                 (
                     "p(1, 2)",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 2,
+                        },
                         terms: vec![
                             GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm(
                                 BasicIntegerTerm::Numeral(1),
@@ -798,7 +849,10 @@ mod tests {
                 (
                     "p(X, a)",
                     Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 2,
+                        },
                         terms: vec![
                             GeneralTerm::GeneralVariable("X".into()),
                             GeneralTerm::Symbol("a".into()),
@@ -914,7 +968,10 @@ mod tests {
                 (
                     "p(N$i, 3*2)",
                     AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 2,
+                        },
                         terms: vec![
                             GeneralTerm::IntegerTerm(IntegerTerm::BasicIntegerTerm(
                                 BasicIntegerTerm::IntegerVariable("N".into()),
@@ -1054,7 +1111,10 @@ mod tests {
                 Formula::UnaryFormula {
                     connective: UnaryConnective::Negation,
                     formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "p".into(),
+                        predicate: Predicate {
+                            symbol: "p".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     }))
                     .into(),
@@ -1073,14 +1133,20 @@ mod tests {
                             }],
                         },
                         formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 1,
+                            },
                             terms: vec![GeneralTerm::GeneralVariable("A".into())],
                         }))
                         .into(),
                     }
                     .into(),
                     rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "q".into(),
+                        predicate: Predicate {
+                            symbol: "q".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     }))
                     .into(),
@@ -1099,7 +1165,10 @@ mod tests {
                             }],
                         },
                         formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 1,
+                            },
                             terms: vec![GeneralTerm::GeneralVariable("A".into())],
                         }))
                         .into(),
@@ -1121,7 +1190,10 @@ mod tests {
                             }],
                         },
                         formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 1,
+                            },
                             terms: vec![GeneralTerm::GeneralVariable("A".into())],
                         }))
                         .into(),
@@ -1161,7 +1233,10 @@ mod tests {
                             formula: Formula::UnaryFormula {
                                 connective: UnaryConnective::Negation,
                                 formula: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                                    predicate: "ra".to_string(),
+                                    predicate: Predicate {
+                                        symbol: "ra".into(),
+                                        arity: 2,
+                                    },
                                     terms: vec![
                                         GeneralTerm::GeneralVariable("V1".into()),
                                         GeneralTerm::GeneralVariable("V2".into()),
@@ -1173,7 +1248,10 @@ mod tests {
                         }
                         .into(),
                         rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                            predicate: "ra".to_string(),
+                            predicate: Predicate {
+                                symbol: "ra".into(),
+                                arity: 2,
+                            },
                             terms: vec![
                                 GeneralTerm::GeneralVariable("V1".into()),
                                 GeneralTerm::GeneralVariable("V2".into()),
@@ -1203,7 +1281,10 @@ mod tests {
                     formula: Formula::BinaryFormula {
                         connective: BinaryConnective::Equivalence,
                         lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                            predicate: "p".into(),
+                            predicate: Predicate {
+                                symbol: "p".into(),
+                                arity: 2,
+                            },
                             terms: vec![
                                 GeneralTerm::GeneralVariable("G".into()),
                                 GeneralTerm::IntegerTerm(IntegerTerm::BinaryOperation {
@@ -1223,19 +1304,28 @@ mod tests {
                         rhs: Formula::BinaryFormula {
                             connective: BinaryConnective::Disjunction,
                             lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                                predicate: "q".into(),
+                                predicate: Predicate {
+                                    symbol: "q".into(),
+                                    arity: 0,
+                                },
                                 terms: vec![],
                             }))
                             .into(),
                             rhs: Formula::BinaryFormula {
                                 connective: BinaryConnective::Conjunction,
                                 lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                                    predicate: "r".into(),
+                                    predicate: Predicate {
+                                        symbol: "r".into(),
+                                        arity: 0,
+                                    },
                                     terms: vec![],
                                 }))
                                 .into(),
                                 rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                                    predicate: "t".into(),
+                                    predicate: Predicate {
+                                        symbol: "t".into(),
+                                        arity: 0,
+                                    },
                                     terms: vec![],
                                 }))
                                 .into(),
@@ -1258,7 +1348,10 @@ mod tests {
                 "a.\n",
                 Theory {
                     formulas: vec![Formula::AtomicFormula(AtomicFormula::Atom(Atom {
-                        predicate: "a".into(),
+                        predicate: Predicate {
+                            symbol: "a".into(),
+                            arity: 0,
+                        },
                         terms: vec![],
                     }))],
                 },
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index dc805d41..765d16ab 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -4,8 +4,9 @@ use {
         parsing::fol::pest::{
             AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser,
             BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser,
-            IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser,
-            TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, VariableParser,
+            IntegerTermParser, PredicateParser, QuantificationParser, QuantifierParser,
+            RelationParser, TheoryParser, UnaryConnectiveParser, UnaryOperatorParser,
+            VariableParser,
         },
         syntax_tree::{impl_node, Node},
     },
@@ -102,9 +103,17 @@ impl GeneralTerm {
     }
 }
 
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+pub struct Predicate {
+    pub symbol: String,
+    pub arity: usize,
+}
+
+impl_node!(Predicate, Format, PredicateParser);
+
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Atom {
-    pub predicate: String,
+    pub predicate: Predicate,
     pub terms: Vec<GeneralTerm>,
 }
 

From 03598e9aa38dd0a42983b6c3bbc1dd67bac0772a Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Tue, 28 Nov 2023 11:23:58 -0600
Subject: [PATCH 4/5] Removing temp file

---
 temp.rs | 326 --------------------------------------------------------
 1 file changed, 326 deletions(-)
 delete mode 100644 temp.rs

diff --git a/temp.rs b/temp.rs
deleted file mode 100644
index 1c020b0d..00000000
--- a/temp.rs
+++ /dev/null
@@ -1,326 +0,0 @@
-use std::hash::Hash;
-
-use {
-    crate::{
-        formatting::asp::default::Format,
-        parsing::asp::pest::{
-            AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser,
-            HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser,
-            RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser,
-        },
-        syntax_tree::{impl_node, Node},
-    },
-    std::collections::HashSet,
-};
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum PrecomputedTerm {
-    Infimum,
-    Numeral(isize),
-    Symbol(String),
-    Supremum,
-}
-
-impl_node!(PrecomputedTerm, Format, PrecomputedTermParser);
-
-#[derive(Clone, Debug, Eq, PartialEq, Hash)]
-pub struct Variable(pub String);
-
-impl_node!(Variable, Format, VariableParser);
-
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
-pub enum UnaryOperator {
-    Negative,
-}
-
-impl_node!(UnaryOperator, Format, UnaryOperatorParser);
-
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
-pub enum BinaryOperator {
-    Add,
-    Subtract,
-    Multiply,
-    Divide,
-    Modulo,
-    Interval,
-}
-
-impl_node!(BinaryOperator, Format, BinaryOperatorParser);
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum Term {
-    PrecomputedTerm(PrecomputedTerm),
-    Variable(Variable),
-    UnaryOperation {
-        op: UnaryOperator,
-        arg: Box<Term>,
-    },
-    BinaryOperation {
-        op: BinaryOperator,
-        lhs: Box<Term>,
-        rhs: Box<Term>,
-    },
-}
-
-impl_node!(Term, Format, TermParser);
-
-impl Term {
-    pub fn variables(&self) -> HashSet<Variable> {
-        match &self {
-            Term::PrecomputedTerm(_) => HashSet::new(),
-            Term::Variable(v) => HashSet::from([v.clone()]),
-            Term::UnaryOperation { arg, .. } => arg.variables(),
-            Term::BinaryOperation { lhs, rhs, .. } => {
-                let mut vars = lhs.variables();
-                vars.extend(rhs.variables());
-                vars
-            }
-        }
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq, Hash)]
-pub struct Predicate {
-    pub symbol: String,
-    pub arity: usize,
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Atom {
-    pub predicate: Predicate,
-    pub terms: Vec<Term>,
-}
-
-impl_node!(Atom, Format, AtomParser);
-
-impl Atom {
-    pub fn predicate(&self) -> Predicate {
-        self.predicate.clone()
-    }
-
-    pub fn variables(&self) -> HashSet<Variable> {
-        let mut vars = HashSet::new();
-        for term in self.terms.iter() {
-            vars.extend(term.variables())
-        }
-        vars
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum Sign {
-    NoSign,
-    Negation,
-    DoubleNegation,
-}
-
-impl_node!(Sign, Format, SignParser);
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Literal {
-    pub sign: Sign,
-    pub atom: Atom,
-}
-
-impl_node!(Literal, Format, LiteralParser);
-
-impl Literal {
-    pub fn variables(&self) -> HashSet<Variable> {
-        self.atom.variables()
-    }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        HashSet::from([self.atom.predicate()])
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum Relation {
-    Equal,
-    NotEqual,
-    Less,
-    LessEqual,
-    Greater,
-    GreaterEqual,
-}
-
-impl_node!(Relation, Format, RelationParser);
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Comparison {
-    pub relation: Relation,
-    pub lhs: Term,
-    pub rhs: Term,
-}
-
-impl_node!(Comparison, Format, ComparisonParser);
-
-impl Comparison {
-    pub fn variables(&self) -> HashSet<Variable> {
-        let mut vars = self.lhs.variables();
-        vars.extend(self.rhs.variables());
-        vars
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum AtomicFormula {
-    Literal(Literal),
-    Comparison(Comparison),
-}
-
-impl_node!(AtomicFormula, Format, AtomicFormulaParser);
-
-impl AtomicFormula {
-    pub fn variables(&self) -> HashSet<Variable> {
-        match &self {
-            AtomicFormula::Literal(l) => l.variables(),
-            AtomicFormula::Comparison(c) => c.variables(),
-        }
-    }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        match &self {
-            AtomicFormula::Literal(l) => l.predicates(),
-            AtomicFormula::Comparison(_) => HashSet::new(),
-        }
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub enum Head {
-    Basic(Atom),
-    Choice(Atom),
-    Falsity,
-}
-
-impl_node!(Head, Format, HeadParser);
-
-impl Head {
-    pub fn predicate(&self) -> Option<&Predicate> {
-        match self {
-            Head::Basic(a) => Some(&a.predicate),
-            Head::Choice(a) => Some(&a.predicate),
-            Head::Falsity => None,
-        }
-    }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        match self {
-            Head::Basic(a) | Head::Choice(a) => HashSet::from([a.predicate()]),
-            Head::Falsity => HashSet::new(),
-        }
-    }
-
-    pub fn terms(&self) -> Option<&[Term]> {
-        match self {
-            Head::Basic(a) => Some(&a.terms),
-            Head::Choice(a) => Some(&a.terms),
-            Head::Falsity => None,
-        }
-    }
-
-    pub fn arity(&self) -> usize {
-        match self {
-            Head::Basic(a) => a.terms.len(),
-            Head::Choice(a) => a.terms.len(),
-            Head::Falsity => 0,
-        }
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Body {
-    pub formulas: Vec<AtomicFormula>,
-}
-
-impl_node!(Body, Format, BodyParser);
-
-impl Body {
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        let mut preds = HashSet::<Predicate>::new();
-        for form in self.formulas.iter() {
-            preds.extend(form.predicates());
-        }
-        preds
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Rule {
-    pub head: Head,
-    pub body: Body,
-}
-
-impl_node!(Rule, Format, RuleParser);
-
-impl Rule {
-    // TODO: Drop?
-    pub fn is_constraint(&self) -> bool {
-        match &self.head {
-            Head::Basic(_) | Head::Choice(_) => false,
-            Head::Falsity => true,
-        }
-    }
-
-    pub fn head_symbol(&self) -> Option<Predicate> {
-        match &self.head {
-            Head::Basic(a) => Some(a.predicate().clone()),
-            Head::Choice(a) => Some(a.predicate().clone()),
-            Head::Falsity => None,
-        }
-    }
-
-    pub fn variables(&self) -> HashSet<Variable> {
-        let mut vars = self.head_variables();
-        vars.extend(self.body_variables());
-        vars
-    }
-
-    pub fn head_variables(&self) -> HashSet<Variable> {
-        match &self.head {
-            Head::Basic(a) | Head::Choice(a) => a.variables(),
-            Head::Falsity => HashSet::new(),
-        }
-    }
-
-    pub fn body_variables(&self) -> HashSet<Variable> {
-        let mut vars = HashSet::new();
-        for formula in self.body.formulas.iter() {
-            vars.extend(formula.variables())
-        }
-        vars
-    }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        let mut preds = self.body.predicates();
-        preds.extend(self.head.predicates());
-        preds
-    }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Program {
-    pub rules: Vec<Rule>,
-}
-
-impl_node!(Program, Format, ProgramParser);
-
-impl Program {
-    pub fn variables(&self) -> HashSet<Variable> {
-        let mut vars = HashSet::new();
-        for rule in self.rules.iter() {
-            vars.extend(rule.variables())
-        }
-        vars
-    }
-
-    pub fn predicates(&self) -> HashSet<Predicate> {
-        let mut preds = HashSet::new();
-        for rule in self.rules.iter() {
-            preds.extend(rule.predicates())
-        }
-        preds
-    }
-}
-

From a248b2641f11ce2e289b5af9718f0c77c2ab46ad Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Tue, 28 Nov 2023 11:40:04 -0600
Subject: [PATCH 5/5] Fixing clippy

---
 src/parsing/fol/pest.rs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/parsing/fol/pest.rs b/src/parsing/fol/pest.rs
index c10d6862..08fbb0eb 100644
--- a/src/parsing/fol/pest.rs
+++ b/src/parsing/fol/pest.rs
@@ -215,8 +215,7 @@ impl PestParser for PredicateParser {
         let arity_string: &str = pairs
             .next()
             .unwrap_or_else(|| Self::report_missing_pair())
-            .as_str()
-            .into();
+            .as_str();
         let arity: usize = arity_string.parse().unwrap();
 
         Predicate { symbol, arity }