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 }