diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..6a68381 --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,361 @@ +pub struct FoliageFlavor; + +pub struct FunctionDeclaration +{ + pub declaration: foliage::FunctionDeclaration, + pub domain: std::cell::RefCell, + pub is_input: std::cell::RefCell, +} + +impl FunctionDeclaration +{ + pub fn is_built_in(&self) -> bool + { + use foliage::flavor::FunctionDeclaration; + + self.declaration.name.starts_with("f__") && self.declaration.name.ends_with("__") + } +} + +impl std::cmp::PartialEq for FunctionDeclaration +{ + #[inline(always)] + fn eq(&self, other: &Self) -> bool + { + self.declaration.eq(&other.declaration) + } +} + +impl std::cmp::Eq for FunctionDeclaration +{ +} + +impl std::cmp::PartialOrd for FunctionDeclaration +{ + #[inline(always)] + fn partial_cmp(&self, other: &FunctionDeclaration) -> Option + { + self.declaration.partial_cmp(&other.declaration) + } +} + +impl std::cmp::Ord for FunctionDeclaration +{ + #[inline(always)] + fn cmp(&self, other: &FunctionDeclaration) -> std::cmp::Ordering + { + self.declaration.cmp(&other.declaration) + } +} + +impl std::hash::Hash for FunctionDeclaration +{ + #[inline(always)] + fn hash(&self, state: &mut H) + { + self.declaration.hash(state) + } +} + +impl foliage::flavor::FunctionDeclaration for FunctionDeclaration +{ + fn new(name: String, arity: usize) -> Self + { + Self + { + declaration: foliage::FunctionDeclaration::new(name, arity), + domain: std::cell::RefCell::new(crate::Domain::Program), + is_input: std::cell::RefCell::new(false), + } + } + + fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + self.declaration.display_name(formatter) + } + + fn arity(&self) -> usize + { + self.declaration.arity + } + + fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool + { + self.declaration.matches_signature(other_name, other_arity) + } +} + +pub struct PredicateDeclaration +{ + pub declaration: foliage::PredicateDeclaration, + pub is_input: std::cell::RefCell, + pub is_output: std::cell::RefCell, +} + +impl PredicateDeclaration +{ + pub fn tptp_statement_name(&self) -> String + { + format!("{}_{}", self.declaration.name, self.declaration.arity) + } + + pub fn is_built_in(&self) -> bool + { + self.declaration.name.starts_with("p__") && self.declaration.name.ends_with("__") + } +} + +impl std::cmp::PartialEq for PredicateDeclaration +{ + #[inline(always)] + fn eq(&self, other: &Self) -> bool + { + self.declaration.eq(&other.declaration) + } +} + +impl std::cmp::Eq for PredicateDeclaration +{ +} + +impl std::cmp::PartialOrd for PredicateDeclaration +{ + #[inline(always)] + fn partial_cmp(&self, other: &PredicateDeclaration) -> Option + { + self.declaration.partial_cmp(&other.declaration) + } +} + +impl std::cmp::Ord for PredicateDeclaration +{ + #[inline(always)] + fn cmp(&self, other: &PredicateDeclaration) -> std::cmp::Ordering + { + self.declaration.cmp(&other.declaration) + } +} + +impl std::hash::Hash for PredicateDeclaration +{ + #[inline(always)] + fn hash(&self, state: &mut H) + { + self.declaration.hash(state) + } +} + +impl foliage::flavor::PredicateDeclaration for PredicateDeclaration +{ + fn new(name: String, arity: usize) -> Self + { + Self + { + declaration: foliage::PredicateDeclaration::new(name, arity), + is_input: std::cell::RefCell::new(false), + is_output: std::cell::RefCell::new(false), + } + } + + fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + self.declaration.display_name(formatter) + } + + fn arity(&self) -> usize + { + self.declaration.arity + } + + fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool + { + self.declaration.matches_signature(other_name, other_arity) + } +} + +#[derive(Clone)] +pub struct GeneratedVariableName +{ + pub domain: crate::Domain, + pub id: Option, +} + +#[derive(Clone)] +pub enum VariableName +{ + UserDefined(String), + Generated(GeneratedVariableName), +} + +#[derive(Clone)] +pub struct VariableDeclaration +{ + pub name: std::cell::RefCell, +} + +impl VariableDeclaration +{ + pub fn new_generated(domain: crate::Domain) -> Self + { + let generated_variable_name = GeneratedVariableName + { + domain, + id: None, + }; + + Self + { + name: std::cell::RefCell::new(VariableName::Generated(generated_variable_name)), + } + } + + pub fn domain(&self) -> Result + { + match *self.name.borrow() + { + VariableName::UserDefined(ref name) => + { + let mut name_characters = name.chars(); + + loop + { + match name_characters.next() + { + Some('I') + | Some('J') + | Some('K') + | Some('L') + | Some('M') + | Some('N') => return Ok(crate::Domain::Integer), + Some('X') + | Some('Y') + | Some('Z') => return Ok(crate::Domain::Program), + Some('_') => continue, + _ => return Err( + crate::Error::new_variable_name_not_allowed(name.to_string())), + } + } + }, + VariableName::Generated(ref generated_variable_name) => + Ok(generated_variable_name.domain), + } + } +} + +impl std::cmp::PartialEq for VariableDeclaration +{ + #[inline(always)] + fn eq(&self, other: &Self) -> bool + { + let l = self as *const Self; + let r = other as *const Self; + + l.eq(&r) + } +} + +impl std::cmp::Eq for VariableDeclaration +{ +} + +impl std::cmp::PartialOrd for VariableDeclaration +{ + #[inline(always)] + fn partial_cmp(&self, other: &VariableDeclaration) -> Option + { + let l = self as *const VariableDeclaration; + let r = other as *const VariableDeclaration; + + l.partial_cmp(&r) + } +} + +impl std::cmp::Ord for VariableDeclaration +{ + #[inline(always)] + fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering + { + let l = self as *const VariableDeclaration; + let r = other as *const VariableDeclaration; + + l.cmp(&r) + } +} + +impl std::hash::Hash for VariableDeclaration +{ + #[inline(always)] + fn hash(&self, state: &mut H) + { + let p = self as *const VariableDeclaration; + + p.hash(state); + } +} + +impl foliage::flavor::VariableDeclaration for VariableDeclaration +{ + fn new(name: String) -> Self + { + Self + { + name: std::cell::RefCell::new(VariableName::UserDefined(name)), + } + } + + fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + match *self.name.borrow() + { + VariableName::UserDefined(ref name) => write!(formatter, "{}", name), + VariableName::Generated(ref generated_variable_name) => + { + let variable_name_prefix = match generated_variable_name.domain + { + crate::Domain::Program => "X", + crate::Domain::Integer => "N", + }; + + let variable_id = match generated_variable_name.id + { + Some(id) => id, + None => unreachable!("all variable IDs should be assigned at this point"), + }; + + write!(formatter, "{}{}", variable_name_prefix, variable_id + 1) + }, + } + } + + fn matches_name(&self, other_name: &str) -> bool + { + match *self.name.borrow() + { + VariableName::UserDefined(ref name) => name == other_name, + // Generated variable declarations never match user-defined variables by name + VariableName::Generated(_) => false, + } + } +} + +impl foliage::flavor::Flavor for FoliageFlavor +{ + type FunctionDeclaration = FunctionDeclaration; + type PredicateDeclaration = PredicateDeclaration; + type VariableDeclaration = VariableDeclaration; +} + +pub type BinaryOperation = foliage::BinaryOperation; +pub type Formula = foliage::Formula; +pub type Formulas = foliage::Formulas; +pub type FunctionDeclarations = foliage::FunctionDeclarations; +pub type OpenFormula = foliage::OpenFormula; +pub type Predicate = foliage::Predicate; +pub type PredicateDeclarations = foliage::PredicateDeclarations; +pub type QuantifiedFormula = foliage::QuantifiedFormula; +pub type Term = foliage::Term; +pub type UnaryOperation = foliage::UnaryOperation; +pub type Variable = foliage::Variable; +pub type VariableDeclarationStackLayer<'p> = + foliage::VariableDeclarationStackLayer<'p, FoliageFlavor>; +pub type VariableDeclarations = foliage::VariableDeclarations; diff --git a/src/error.rs b/src/error.rs index b5052a8..a0250ac 100644 --- a/src/error.rs +++ b/src/error.rs @@ -1,3 +1,5 @@ +use foliage::flavor::VariableDeclaration as _; + pub type Source = Box; pub enum Kind @@ -21,10 +23,10 @@ pub enum Kind UnknownProofDirection(String), UnknownDomainIdentifier(String), VariableNameNotAllowed(String), - FormulaNotClosed(std::rc::Rc), - NoCompletedDefinitionFound(std::rc::Rc), - CannotHidePredicate(std::rc::Rc), - PredicateShouldNotOccurInSpecification(std::rc::Rc), + FormulaNotClosed(std::rc::Rc), + NoCompletedDefinitionFound(std::rc::Rc), + CannotHidePredicate(std::rc::Rc), + PredicateShouldNotOccurInSpecification(std::rc::Rc), WriteTPTPProgram, RunVampire, // TODO: rename to something Vampire-specific @@ -146,28 +148,28 @@ impl Error Self::new(Kind::VariableNameNotAllowed(variable_name)) } - pub(crate) fn new_formula_not_closed(free_variables: std::rc::Rc) + pub(crate) fn new_formula_not_closed(free_variables: std::rc::Rc) -> Self { Self::new(Kind::FormulaNotClosed(free_variables)) } pub(crate) fn new_no_completed_definition_found( - predicate_declaration: std::rc::Rc) + predicate_declaration: std::rc::Rc) -> Self { Self::new(Kind::NoCompletedDefinitionFound(predicate_declaration)) } pub(crate) fn new_cannot_hide_predicate( - predicate_declaration: std::rc::Rc) + predicate_declaration: std::rc::Rc) -> Self { Self::new(Kind::CannotHidePredicate(predicate_declaration)) } pub(crate) fn new_predicate_should_not_occur_in_specification( - predicate_declaration: std::rc::Rc) + predicate_declaration: std::rc::Rc) -> Self { Self::new(Kind::PredicateShouldNotOccurInSpecification(predicate_declaration)) @@ -240,25 +242,29 @@ impl std::fmt::Debug for Error Kind::WriteTPTPProgram => write!(formatter, "error writing TPTP program"), Kind::FormulaNotClosed(free_variable_declarations) => { - let free_variable_names = free_variable_declarations - .iter() - .map(|variable_declaration| &variable_declaration.name); + write!(formatter, "formula may not contain free variables (free variables in this formula: ")?; - let free_variable_names_output = itertools::join(free_variable_names, ", "); + let mut separator = ""; - write!(formatter, "formula may not contain free variables (free variables in this formula: {})", - free_variable_names_output) + for free_variable_declaration in &**free_variable_declarations + { + write!(formatter, "{}", separator)?; + free_variable_declaration.display_name(formatter)?; + separator = ", "; + } + + write!(formatter, ")") }, Kind::NoCompletedDefinitionFound(ref predicate_declaration) => - write!(formatter, "no completed definition found for {}", predicate_declaration), + write!(formatter, "no completed definition found for {}", predicate_declaration.declaration), Kind::CannotHidePredicate(ref predicate_declaration) => write!(formatter, "cannot hide predicate {} (the completed definition transitively depends on itself)", - predicate_declaration), + predicate_declaration.declaration), Kind::PredicateShouldNotOccurInSpecification(ref predicate_declaration) => write!(formatter, "{} should not occur in specification because it’s a private predicate (consider declaring it an input or output predicate)", - predicate_declaration), + predicate_declaration.declaration), Kind::RunVampire => write!(formatter, "could not run Vampire"), Kind::ProveProgram(exit_code, ref stdout, ref stderr) => { diff --git a/src/input/specification.rs b/src/input/specification.rs index 3f4c4ce..ecd8ead 100644 --- a/src/input/specification.rs +++ b/src/input/specification.rs @@ -1,96 +1,8 @@ -// TODO: refactor -fn term_assign_variable_declaration_domains(term: &foliage::Term, declarations: &D) - -> Result<(), crate::Error> -where - D: crate::traits::AssignVariableDeclarationDomain, -{ - match term - { - foliage::Term::BinaryOperation(binary_operation) => - { - term_assign_variable_declaration_domains(&binary_operation.left, declarations)?; - term_assign_variable_declaration_domains(&binary_operation.right, declarations)?; - }, - foliage::Term::Function(function) => - for argument in &function.arguments - { - term_assign_variable_declaration_domains(&argument, declarations)?; - }, - foliage::Term::UnaryOperation(unary_operation) => - term_assign_variable_declaration_domains(&unary_operation.argument, declarations)?, - foliage::Term::Variable(variable) => - { - let domain = match variable.declaration.name.chars().next() - { - Some('X') - | Some('Y') - | Some('Z') => crate::Domain::Program, - Some('I') - | Some('J') - | Some('K') - | Some('L') - | Some('M') - | Some('N') => crate::Domain::Integer, - Some(_) => return Err( - crate::Error::new_variable_name_not_allowed(variable.declaration.name.clone())), - None => unreachable!(), - }; - - declarations.assign_variable_declaration_domain(&variable.declaration, domain); - }, - _ => (), - } - - Ok(()) -} - -fn formula_assign_variable_declaration_domains(formula: &foliage::Formula, declarations: &D) - -> Result<(), crate::Error> -where - D: crate::traits::AssignVariableDeclarationDomain, -{ - match formula - { - foliage::Formula::And(arguments) - | foliage::Formula::Or(arguments) - | foliage::Formula::IfAndOnlyIf(arguments) => - for argument in arguments - { - formula_assign_variable_declaration_domains(&argument, declarations)?; - }, - foliage::Formula::Compare(compare) => - { - term_assign_variable_declaration_domains(&compare.left, declarations)?; - term_assign_variable_declaration_domains(&compare.right, declarations)?; - }, - foliage::Formula::Exists(quantified_formula) - | foliage::Formula::ForAll(quantified_formula) => - formula_assign_variable_declaration_domains(&quantified_formula.argument, - declarations)?, - foliage::Formula::Implies(implies) => - { - formula_assign_variable_declaration_domains(&implies.antecedent, declarations)?; - formula_assign_variable_declaration_domains(&implies.implication, declarations)?; - } - foliage::Formula::Not(argument) => - formula_assign_variable_declaration_domains(&argument, declarations)?, - foliage::Formula::Predicate(predicate) => - for argument in &predicate.arguments - { - term_assign_variable_declaration_domains(&argument, declarations)?; - }, - _ => (), - } - - Ok(()) -} - fn open_formula<'i, D>(input: &'i str, declarations: &D) - -> Result<(foliage::OpenFormula, &'i str), crate::Error> + -> Result<(crate::OpenFormula, &'i str), crate::Error> where - D: foliage::FindOrCreateFunctionDeclaration - + foliage::FindOrCreatePredicateDeclaration - + crate::traits::AssignVariableDeclarationDomain, + D: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration { let terminator_position = match input.find('.') { @@ -106,9 +18,7 @@ where let open_formula = foliage::parse::formula(formula_input, declarations) .map_err(|error| crate::Error::new_parse_formula(error))?; - formula_assign_variable_declaration_domains(&open_formula.formula, declarations)?; - - let open_formula = foliage::OpenFormula + let open_formula = crate::OpenFormula { free_variable_declarations: open_formula.free_variable_declarations, formula: open_formula.formula, @@ -118,11 +28,10 @@ where } fn formula<'i, D>(mut input: &'i str, declarations: &D) - -> Result<(foliage::Formula, &'i str), crate::Error> + -> Result<(crate::Formula, &'i str), crate::Error> where - D: foliage::FindOrCreateFunctionDeclaration - + foliage::FindOrCreatePredicateDeclaration - + crate::traits::AssignVariableDeclarationDomain, + D: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration { let (open_formula, remaining_input) = open_formula(input, declarations)?; @@ -137,7 +46,7 @@ where } fn formula_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) - -> Result<(foliage::Formula, &'i str), crate::Error> + -> Result<(crate::Formula, &'i str), crate::Error> { input = foliage::parse::tokens::trim_start(input); @@ -257,15 +166,12 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) { input = remaining_input; - let mut input_predicate_declarations = - problem.input_predicate_declarations.borrow_mut(); - use foliage::FindOrCreatePredicateDeclaration as _; let predicate_declaration = problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity); - input_predicate_declarations.insert(predicate_declaration); + *predicate_declaration.is_input.borrow_mut() = true; } // Parse input constant specifiers else @@ -279,20 +185,13 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) input = remaining_input; - let mut input_constant_declarations = - problem.input_constant_declarations.borrow_mut(); - use foliage::FindOrCreateFunctionDeclaration as _; let constant_declaration = problem.find_or_create_function_declaration(constant_or_predicate_name, 0); - input_constant_declarations.insert(std::rc::Rc::clone(&constant_declaration)); - - let mut input_constant_declaration_domains = - problem.input_constant_declaration_domains.borrow_mut(); - - input_constant_declaration_domains.insert(constant_declaration, domain); + *constant_declaration.is_input.borrow_mut() = true; + *constant_declaration.domain.borrow_mut() = domain; } let mut input_characters = input.chars(); @@ -337,15 +236,12 @@ fn output_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) { input = remaining_input; - let mut output_predicate_declarations = - problem.output_predicate_declarations.borrow_mut(); - use foliage::FindOrCreatePredicateDeclaration as _; let predicate_declaration = problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity); - output_predicate_declarations.insert(predicate_declaration); + *predicate_declaration.is_output.borrow_mut() = true; } else { diff --git a/src/lib.rs b/src/lib.rs index 01cf22d..41c7448 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,16 +1,17 @@ #![feature(trait_alias)] #![feature(vec_remove_item)] +mod ast; pub mod commands; pub mod error; pub mod input; pub mod output; pub mod problem; pub mod simplify; -pub(crate) mod traits; pub mod translate; mod utils; +pub use crate::ast::*; pub use error::Error; pub use problem::Problem; pub(crate) use simplify::*; diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 70100e8..6bbf268 100644 --- a/src/output/tptp.rs +++ b/src/output/tptp.rs @@ -1,3 +1,6 @@ +use foliage::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, + VariableDeclaration as _}; + pub(crate) struct DomainDisplay { domain: crate::Domain, @@ -33,37 +36,22 @@ impl std::fmt::Display for DomainDisplay } } -pub(crate) struct FunctionDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain +pub(crate) struct FunctionDeclarationDisplay<'a>(&'a crate::FunctionDeclaration); + +pub(crate) fn display_function_declaration<'a>(function_declaration: &'a crate::FunctionDeclaration) + -> FunctionDeclarationDisplay<'a> { - function_declaration: &'a std::rc::Rc, - context: &'b C, + FunctionDeclarationDisplay(function_declaration) } -pub(crate) fn display_function_declaration<'a, 'b, C>( - function_declaration: &'a std::rc::Rc, context: &'b C) - -> FunctionDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain -{ - FunctionDeclarationDisplay - { - function_declaration, - context, - } -} - -impl<'a, 'b, C> std::fmt::Debug for FunctionDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain +impl<'a> std::fmt::Debug for FunctionDeclarationDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{}:", self.function_declaration.name)?; + self.0.display_name(formatter)?; + write!(formatter, ":")?; - let domain = self.context.input_constant_declaration_domain(self.function_declaration); - let domain_identifier = match domain + let domain_identifier = match *self.0.domain.borrow() { crate::Domain::Integer => "$int", crate::Domain::Program => "object", @@ -71,11 +59,11 @@ where let mut separator = ""; - if self.function_declaration.arity > 0 + if self.0.arity() > 0 { write!(formatter, " (")?; - for _ in 0..self.function_declaration.arity + for _ in 0..self.0.arity() { write!(formatter, "{}object", separator)?; separator = " * "; @@ -88,9 +76,7 @@ where } } -impl<'a, 'b, C> std::fmt::Display for FunctionDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain +impl<'a> std::fmt::Display for FunctionDeclarationDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -98,10 +84,10 @@ where } } -pub(crate) struct PredicateDeclarationDisplay<'a>(&'a std::rc::Rc); +pub(crate) struct PredicateDeclarationDisplay<'a>(&'a crate::PredicateDeclaration); pub(crate) fn display_predicate_declaration<'a>( - predicate_declaration: &'a std::rc::Rc) + predicate_declaration: &'a crate::PredicateDeclaration) -> PredicateDeclarationDisplay<'a> { PredicateDeclarationDisplay(predicate_declaration) @@ -111,15 +97,16 @@ impl<'a> std::fmt::Debug for PredicateDeclarationDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{}:", self.0.name)?; + self.0.display_name(formatter)?; + write!(formatter, ":")?; let mut separator = ""; - if self.0.arity > 0 + if self.0.arity() > 0 { write!(formatter, " (")?; - for _ in 0..self.0.arity + for _ in 0..self.0.arity() { write!(formatter, "{}object", separator)?; separator = " * "; @@ -140,94 +127,20 @@ impl<'a> std::fmt::Display for PredicateDeclarationDisplay<'a> } } -pub(crate) struct VariableDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID +pub(crate) struct TermDisplay<'a>(&'a crate::Term); + +pub(crate) fn display_term<'a>(term: &'a crate::Term) -> TermDisplay<'a> { - variable_declaration: &'a std::rc::Rc, - context: &'b C, + TermDisplay(term) } -pub(crate) fn display_variable_declaration<'a, 'b, C>( - variable_declaration: &'a std::rc::Rc, context: &'b C) - -> VariableDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - VariableDeclarationDisplay - { - variable_declaration, - context, - } -} - -impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID +impl<'a> std::fmt::Debug for TermDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - let id = self.context.variable_declaration_id(self.variable_declaration); - let domain = self.context.variable_declaration_domain(self.variable_declaration) - .expect("unspecified variable domain"); - - let prefix = match domain - { - crate::Domain::Integer => "N", - crate::Domain::Program => "X", - }; - - write!(formatter, "{}{}", prefix, id + 1) - } -} - -impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result - { - write!(formatter, "{:?}", &self) - } -} - -pub(crate) struct TermDisplay<'a, 'b, C> -{ - term: &'a foliage::Term, - context: &'b C, -} - -pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, context: &'b C) - -> TermDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - TermDisplay - { - term, - context, - } -} - -impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result - { - let display_variable_declaration = |variable_declaration| - display_variable_declaration(variable_declaration, self.context); - let display_term = |term| display_term(term, self.context); - use foliage::*; - match &self.term + match &self.0 { Term::Boolean(true) => write!(formatter, "$true"), Term::Boolean(false) => write!(formatter, "$false"), @@ -239,19 +152,19 @@ where false => write!(formatter, "{}", value), }, Term::String(_) => panic!("strings not supported in TPTP"), - Term::Variable(variable) => - write!(formatter, "{:?}", display_variable_declaration(&variable.declaration)), + Term::Variable(variable) => variable.declaration.display_name(formatter), Term::Function(function) => { - write!(formatter, "{}", function.declaration.name)?; + function.declaration.display_name(formatter)?; - assert!(function.declaration.arity == function.arguments.len(), + assert!(function.declaration.arity() == function.arguments.len(), "function has a different number of arguments than declared (expected {}, got {})", - function.declaration.arity, function.arguments.len()); + function.declaration.arity(), function.arguments.len()); if function.arguments.len() > 0 { - write!(formatter, "{}(", function.declaration.name)?; + function.declaration.display_name(formatter)?; + write!(formatter, "(")?; let mut separator = ""; @@ -290,10 +203,7 @@ where } } -impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID +impl<'a> std::fmt::Display for TermDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -301,47 +211,26 @@ where } } -pub(crate) struct FormulaDisplay<'a, 'b, C> +pub(crate) struct FormulaDisplay<'a>(&'a crate::Formula); + +pub(crate) fn display_formula<'a>(formula: &'a crate::Formula) -> FormulaDisplay<'a> { - formula: &'a foliage::Formula, - context: &'b C, + FormulaDisplay(formula) } -pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, context: &'b C) - -> FormulaDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - FormulaDisplay - { - formula, - context, - } -} - -impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain - + crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID +impl<'a> std::fmt::Debug for FormulaDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - let display_variable_declaration = |variable_declaration| - display_variable_declaration(variable_declaration, self.context); - let display_term = |term| display_term(term, self.context); - let display_formula = |formula| display_formula(formula, self.context); - let mut display_compare = |left, right, notation, integer_operator_name, auxiliary_predicate_name| -> std::fmt::Result { let mut notation = notation; let mut operation_identifier = integer_operator_name; - let is_left_term_arithmetic = crate::is_term_arithmetic(left, self.context) + let is_left_term_arithmetic = crate::is_term_arithmetic(left) .expect("could not determine whether term is arithmetic"); - let is_right_term_arithmetic = crate::is_term_arithmetic(right, self.context) + let is_right_term_arithmetic = crate::is_term_arithmetic(right) .expect("could not determine whether term is arithmetic"); match (!is_left_term_arithmetic || !is_right_term_arithmetic, auxiliary_predicate_name) @@ -387,47 +276,40 @@ where use foliage::*; - match &self.formula + match &self.0 { // TODO: handle cases with 0 parameters properly - Formula::Exists(exists) => + Formula::Exists(quantified_formula) + | Formula::ForAll(quantified_formula) => { - write!(formatter, "?[")?; + let operator_symbol = match &self.0 + { + Formula::Exists(_) => "?", + Formula::ForAll(_) => "!", + _ => unreachable!(), + }; + + write!(formatter, "{}[", operator_symbol)?; let mut separator = ""; - for parameter in exists.parameters.iter() + for parameter in quantified_formula.parameters.iter() { - let parameter_domain = self.context.variable_declaration_domain(parameter) - .expect("unspecified variable domain"); + let domain = match parameter.domain() + { + Ok(domain) => domain, + Err(_) => unreachable!( + "all variable domains should have been checked at this point"), + }; - write!(formatter, "{}{:?}: {}", separator, - display_variable_declaration(parameter), display_domain(parameter_domain))?; + write!(formatter, "{}", separator)?; + parameter.display_name(formatter)?; + write!(formatter, ": {}", display_domain(domain))?; separator = ", " } - write!(formatter, "]: ({:?})", display_formula(&exists.argument))?; - }, - // TODO: handle cases with 0 parameters properly - Formula::ForAll(for_all) => - { - write!(formatter, "![")?; - - let mut separator = ""; - - for parameter in for_all.parameters.iter() - { - let parameter_domain = self.context.variable_declaration_domain(parameter) - .expect("unspecified variable domain"); - - write!(formatter, "{}{:?}: {}", separator, - display_variable_declaration(parameter), display_domain(parameter_domain))?; - - separator = ", " - } - - write!(formatter, "]: ({:?})", display_formula(&for_all.argument))?; + write!(formatter, "]: ({:?})", display_formula(&quantified_formula.argument))?; }, Formula::Not(argument) => write!(formatter, "~{:?}", display_formula(argument))?, // TODO: handle cases with < 2 arguments properly @@ -524,7 +406,7 @@ where Formula::Boolean(false) => write!(formatter, "$false")?, Formula::Predicate(predicate) => { - write!(formatter, "{}", predicate.declaration.name)?; + predicate.declaration.display_name(formatter)?; if !predicate.arguments.is_empty() { @@ -536,9 +418,8 @@ where { write!(formatter, "{}", separator)?; - let is_argument_arithmetic = - crate::is_term_arithmetic(argument, self.context) - .expect("could not determine whether term is arithmetic"); + let is_argument_arithmetic = crate::is_term_arithmetic(argument) + .expect("could not determine whether term is arithmetic"); match is_argument_arithmetic { @@ -558,11 +439,7 @@ where } } -impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C> -where - C: crate::traits::InputConstantDeclarationDomain - + crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID +impl<'a> std::fmt::Display for FormulaDisplay<'a> { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/problem.rs b/src/problem.rs index 687de26..0ac3bda 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -6,6 +6,8 @@ pub use proof_direction::ProofDirection; pub(crate) use section_kind::SectionKind; pub(crate) use statement::{ProofStatus, Statement, StatementKind}; +use foliage::flavor::{FunctionDeclaration as _, PredicateDeclaration as _}; + #[derive(Copy, Clone, Eq, PartialEq)] pub enum ProofResult { @@ -15,36 +17,15 @@ pub enum ProofResult } type VariableDeclarationIDs - = std::collections::BTreeMap::, usize>; - -type InputConstantDeclarationDomains - = std::collections::BTreeMap, crate::Domain>; - -type VariableDeclarationDomains - = std::collections::BTreeMap, crate::Domain>; - -struct FormatContext<'a, 'b> -{ - pub program_variable_declaration_ids: std::cell::RefCell, - pub integer_variable_declaration_ids: std::cell::RefCell, - pub input_constant_declaration_domains: &'a InputConstantDeclarationDomains, - pub variable_declaration_domains: &'b VariableDeclarationDomains, -} + = std::collections::BTreeMap::, usize>; pub struct Problem { - function_declarations: std::cell::RefCell, - pub predicate_declarations: std::cell::RefCell, + function_declarations: std::cell::RefCell, + pub predicate_declarations: std::cell::RefCell, statements: std::cell::RefCell>>, - pub input_constant_declarations: std::cell::RefCell, - pub input_constant_declaration_domains: std::cell::RefCell, - pub input_predicate_declarations: std::cell::RefCell, - pub output_predicate_declarations: std::cell::RefCell, - // TODO: clean up as variable declarations are dropped - variable_declaration_domains: std::cell::RefCell, - shell: std::cell::RefCell, } @@ -54,27 +35,16 @@ impl Problem { Self { - function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()), - predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()), + function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()), + predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()), statements: std::cell::RefCell::new(std::collections::BTreeMap::new()), - input_constant_declarations: - std::cell::RefCell::new(foliage::FunctionDeclarations::new()), - input_constant_declaration_domains: - std::cell::RefCell::new(InputConstantDeclarationDomains::new()), - input_predicate_declarations: - std::cell::RefCell::new(foliage::PredicateDeclarations::new()), - output_predicate_declarations: - std::cell::RefCell::new(foliage::PredicateDeclarations::new()), - variable_declaration_domains: - std::cell::RefCell::new(VariableDeclarationDomains::new()), - shell: std::cell::RefCell::new(crate::output::Shell::from_stdout()), } } - pub(crate) fn add_statement(&self, section_kind: SectionKind, statement: Statement) + pub(crate) fn add_statement(&self, section_kind: SectionKind, mut statement: Statement) { let mut statements = self.statements.borrow_mut(); let section = statements.entry(section_kind).or_insert(vec![]); @@ -86,10 +56,8 @@ impl Problem -> Result<(), crate::Error> { let predicate_declarations = self.predicate_declarations.borrow(); - let input_predicate_declarations = self.input_predicate_declarations.borrow(); - let output_predicate_declarations = self.output_predicate_declarations.borrow(); - if output_predicate_declarations.is_empty() + if predicate_declarations.iter().find(|x| *x.is_output.borrow()).is_none() { return Ok(()); } @@ -97,12 +65,10 @@ impl Problem // Check that only input and output predicates are used in the specification for predicate_declaration in predicate_declarations.iter() { - if input_predicate_declarations.contains(predicate_declaration) - || output_predicate_declarations.contains(predicate_declaration) - // TODO: refactor + if *predicate_declaration.is_input.borrow() + || *predicate_declaration.is_output.borrow() // Auxiliary predicates may occur anywhere - || predicate_declaration.name.starts_with("p__") - && predicate_declaration.name.ends_with("__") + || predicate_declaration.is_built_in() { continue; } @@ -133,19 +99,15 @@ impl Problem pub(crate) fn restrict_to_output_predicates(&mut self) -> Result<(), crate::Error> { let predicate_declarations = self.predicate_declarations.borrow(); - let input_predicate_declarations = self.input_predicate_declarations.borrow(); - let output_predicate_declarations = self.output_predicate_declarations.borrow(); // If no output statements were provided, show all predicates by default - if output_predicate_declarations.is_empty() + if predicate_declarations.iter().find(|x| *x.is_output.borrow()).is_none() { return Ok(()); } - let hidden_predicate_declarations = - predicate_declarations.iter().filter(|x| !output_predicate_declarations.contains(*x) - && !input_predicate_declarations.contains(*x) - && !(x.name.starts_with("p__") && x.name.ends_with("__"))); + let hidden_predicate_declarations = predicate_declarations.iter() + .filter(|x| !*x.is_output.borrow() && !*x.is_input.borrow() && !x.is_built_in()); let mut statements = self.statements.borrow_mut(); @@ -181,7 +143,7 @@ impl Problem for statement in statements.iter_mut() { crate::utils::replace_predicate_in_formula_with_completed_definition( - &mut statement.formula, &completed_definition, self)?; + &mut statement.formula, &completed_definition)?; } } } @@ -357,17 +319,7 @@ impl Problem self.shell.borrow_mut().print(&format!("{}: ", statement.kind), &termcolor::ColorSpec::new())?; - let format_context = FormatContext - { - program_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - integer_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(), - variable_declaration_domains: &self.variable_declaration_domains.borrow(), - }; - - print!("{}", foliage::format::display_formula(&statement.formula, &format_context)); + print!("{}", statement.formula); Ok(()) }; @@ -405,11 +357,7 @@ impl Problem None => break, } - let mut tptp_problem_to_prove_next_statement = "".to_string(); - - self.write_tptp_problem_to_prove_next_statement( - &mut tptp_problem_to_prove_next_statement) - .map_err(|error| crate::Error::new_write_tptp_program(error))?; + let tptp_problem_to_prove_next_statement = format!("{}", self.display_tptp()); log::trace!("TPTP program:\n{}", &tptp_problem_to_prove_next_statement); @@ -463,21 +411,20 @@ impl Problem Ok(ProofResult::Proven) } - fn write_tptp_problem_to_prove_next_statement(&self, formatter: &mut String) -> std::fmt::Result + fn display_tptp(&self) -> ProblemTPTPDisplay { - use std::fmt::Write as _; + ProblemTPTPDisplay(self) + } +} - let format_context = FormatContext - { - program_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - integer_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(), - variable_declaration_domains: &self.variable_declaration_domains.borrow(), - }; +struct ProblemTPTPDisplay<'p>(&'p Problem); - let write_title = |formatter: &mut String, title, section_separator| -> std::fmt::Result +impl<'p> std::fmt::Display for ProblemTPTPDisplay<'p> +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + let write_title = |formatter: &mut dyn std::fmt::Write, title, section_separator| + -> std::fmt::Result { write!(formatter, "{}{}", section_separator, "%".repeat(72))?; write!(formatter, "\n% {}", title)?; @@ -499,42 +446,40 @@ impl Problem = include_str!("output/tptp/preamble_axioms.tptp").trim_end(); writeln!(formatter, "{}", tptp_preamble_anthem_types)?; - if !self.predicate_declarations.borrow().is_empty() - || !self.function_declarations.borrow().is_empty() + if !self.0.predicate_declarations.borrow().is_empty() + || !self.0.function_declarations.borrow().is_empty() { write_title(formatter, "types", section_separator)?; - if !self.predicate_declarations.borrow().is_empty() + if !self.0.predicate_declarations.borrow().is_empty() { writeln!(formatter, "% predicate types")?; } - for predicate_declaration in self.predicate_declarations.borrow().iter() - .filter(|x| !(x.name.starts_with("p__") || x.name.ends_with("__"))) + for predicate_declaration in self.0.predicate_declarations.borrow().iter() + .filter(|x| !x.is_built_in()) { writeln!(formatter, "tff(type, type, {}).", crate::output::tptp::display_predicate_declaration(predicate_declaration))?; } - if !self.function_declarations.borrow().is_empty() + if !self.0.function_declarations.borrow().is_empty() { writeln!(formatter, "% function types")?; } - for function_declaration in self.function_declarations.borrow().iter() - .filter(|x| !(x.name.starts_with("f__") || x.name.ends_with("__"))) + for function_declaration in self.0.function_declarations.borrow().iter() + .filter(|x| !x.is_built_in()) { writeln!(formatter, "tff(type, type, {}).", - crate::output::tptp::display_function_declaration(function_declaration, - &format_context))?; + crate::output::tptp::display_function_declaration(function_declaration))?; } } - let function_declarations = self.function_declarations.borrow(); - let symbolic_constants = function_declarations.iter().filter( - |x| !self.input_constant_declaration_domains.borrow().contains_key(*x)); + let function_declarations = self.0.function_declarations.borrow(); + let symbolic_constants = function_declarations.iter().filter(|x| !*x.is_input.borrow()); - let mut last_symbolic_constant: Option> = None; + let mut last_symbolic_constant: Option> = None; // TODO: put in axioms section for (i, symbolic_constant) in symbolic_constants.enumerate() @@ -545,7 +490,7 @@ impl Problem writeln!(formatter, "% axioms for order of symbolic constants")?; } - if symbolic_constant.arity > 0 + if symbolic_constant.arity() > 0 { // TODO: refactor unimplemented!("n-ary function declarations aren’t supported"); @@ -553,14 +498,17 @@ impl Problem if let Some(last_symbolic_constant) = last_symbolic_constant { - writeln!(formatter, "tff(symbolic_constant_order, axiom, p__less__({}, {})).", - last_symbolic_constant.name, symbolic_constant.name)?; + write!(formatter, "tff(symbolic_constant_order, axiom, p__less__(")?; + last_symbolic_constant.display_name(formatter)?; + write!(formatter, ", ")?; + symbolic_constant.display_name(formatter)?; + writeln!(formatter, ")).")?; } last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant)); } - for (section_kind, statements) in self.statements.borrow().iter() + for (section_kind, statements) in self.0.statements.borrow().iter() { if statements.is_empty() { @@ -615,7 +563,7 @@ impl Problem // TODO: add proper statement type writeln!(formatter, "tff({}, {}, {}).", name, statement_type, - crate::output::tptp::display_formula(&statement.formula, &format_context))?; + crate::output::tptp::display_formula(&statement.formula))?; } } @@ -623,23 +571,19 @@ impl Problem } } -impl foliage::FindOrCreateFunctionDeclaration for Problem +impl foliage::FindOrCreateFunctionDeclaration for Problem { fn find_or_create_function_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc + -> std::rc::Rc { let mut function_declarations = self.function_declarations.borrow_mut(); - match function_declarations.iter().find(|x| x.name == name && x.arity == arity) + match function_declarations.iter().find(|x| x.matches_signature(name, arity)) { Some(declaration) => std::rc::Rc::clone(&declaration), None => { - let declaration = foliage::FunctionDeclaration - { - name: name.to_string(), - arity, - }; + let declaration = crate::FunctionDeclaration::new(name.to_string(), arity); let declaration = std::rc::Rc::new(declaration); function_declarations.insert(std::rc::Rc::clone(&declaration)); @@ -652,23 +596,19 @@ impl foliage::FindOrCreateFunctionDeclaration for Problem } } -impl foliage::FindOrCreatePredicateDeclaration for Problem +impl foliage::FindOrCreatePredicateDeclaration for Problem { fn find_or_create_predicate_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc + -> std::rc::Rc { let mut predicate_declarations = self.predicate_declarations.borrow_mut(); - match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity) + match predicate_declarations.iter().find(|x| x.matches_signature(name, arity)) { Some(declaration) => std::rc::Rc::clone(&declaration), None => { - let declaration = foliage::PredicateDeclaration - { - name: name.to_string(), - arity, - }; + let declaration = crate::PredicateDeclaration::new(name.to_string(), arity); let declaration = std::rc::Rc::new(declaration); predicate_declarations.insert(std::rc::Rc::clone(&declaration)); @@ -681,143 +621,6 @@ impl foliage::FindOrCreatePredicateDeclaration for Problem } } -impl crate::traits::AssignVariableDeclarationDomain for Problem -{ - fn assign_variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc, domain: crate::Domain) - { - let mut variable_declaration_domains = self.variable_declaration_domains.borrow_mut(); - - match variable_declaration_domains.get(variable_declaration) - { - Some(current_domain) => assert_eq!(*current_domain, domain, - "inconsistent variable declaration domain"), - None => - { - variable_declaration_domains - .insert(std::rc::Rc::clone(variable_declaration).into(), domain); - }, - } - } -} - -impl crate::traits::VariableDeclarationDomain for Problem -{ - fn variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc) - -> Option - { - self.variable_declaration_domains.borrow().iter().find_map( - |(x, domain)| - match x == variable_declaration - { - true => Some(*domain), - false => None, - }) - } -} - -impl<'a, 'b> FormatContext<'a, 'b> -{ - fn variable_declaration_id(&self, - variable_declaration: &std::rc::Rc) - -> usize - { - let mut variable_declaration_ids = match self.variable_declaration_domains - .get(variable_declaration) - { - Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(), - Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(), - None => unreachable!("all variables should be declared at this point"), - }; - - match variable_declaration_ids.get(variable_declaration) - { - Some(id) => *id, - None => - { - let id = variable_declaration_ids.len(); - variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); - id - }, - } - } -} - -impl<'a, 'b> crate::traits::InputConstantDeclarationDomain for FormatContext<'a, 'b> -{ - fn input_constant_declaration_domain(&self, - declaration: &std::rc::Rc) -> crate::Domain - { - // Assume the program domain if not specified otherwise - self.input_constant_declaration_domains.get(declaration).map(|x| *x) - .unwrap_or(crate::Domain::Program) - } -} - -impl<'a, 'b> crate::traits::VariableDeclarationDomain for FormatContext<'a, 'b> -{ - fn variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc) - -> Option - { - self.variable_declaration_domains.get(variable_declaration) - .map(|x| *x) - } -} - -impl<'a, 'b> crate::traits::VariableDeclarationID for FormatContext<'a, 'b> -{ - fn variable_declaration_id(&self, - variable_declaration: &std::rc::Rc) - -> usize - { - use crate::traits::VariableDeclarationDomain; - - let mut variable_declaration_ids = match self.variable_declaration_domain( - variable_declaration) - { - Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(), - Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(), - None => panic!("all variables should be declared at this point"), - }; - - match variable_declaration_ids.get(variable_declaration) - { - Some(id) => - { - *id - } - None => - { - let id = variable_declaration_ids.len(); - variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); - id - }, - } - } -} - -impl<'a, 'b> foliage::format::Format for FormatContext<'a, 'b> -{ - fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter, - variable_declaration: &std::rc::Rc) - -> std::fmt::Result - { - let id = self.variable_declaration_id(variable_declaration); - let domain = self.variable_declaration_domains.get(variable_declaration) - .expect("unspecified variable domain"); - - let prefix = match domain - { - crate::Domain::Integer => "N", - crate::Domain::Program => "X", - }; - - write!(formatter, "{}{}", prefix, id + 1) - } -} - fn run_vampire(input: &str, arguments: Option) -> Result<(ProofResult, Option), crate::Error> where diff --git a/src/problem/statement.rs b/src/problem/statement.rs index 3b5b8fa..14d72e6 100644 --- a/src/problem/statement.rs +++ b/src/problem/statement.rs @@ -5,7 +5,7 @@ pub(crate) enum StatementKind { Axiom, Assumption, - CompletedDefinition(std::rc::Rc), + CompletedDefinition(std::rc::Rc), IntegrityConstraint, Lemma(ProofDirection), Assertion, @@ -20,7 +20,7 @@ impl std::fmt::Debug for StatementKind Self::Axiom => write!(formatter, "axiom"), Self::Assumption => write!(formatter, "assumption"), Self::CompletedDefinition(ref predicate_declaration) => - write!(formatter, "completed definition of {}", predicate_declaration), + write!(formatter, "completed definition of {}", predicate_declaration.declaration), Self::IntegrityConstraint => write!(formatter, "integrity constraint"), Self::Lemma(_) => write!(formatter, "lemma"), Self::Assertion => write!(formatter, "assertion"), @@ -52,13 +52,13 @@ pub(crate) struct Statement { pub kind: StatementKind, pub name: Option, - pub formula: foliage::Formula, + pub formula: crate::Formula, pub proof_status: ProofStatus, } impl Statement { - pub fn new(kind: StatementKind, formula: foliage::Formula) -> Self + pub fn new(kind: StatementKind, formula: crate::Formula) -> Self { Self { diff --git a/src/simplify.rs b/src/simplify.rs index 86d4925..b14f189 100644 --- a/src/simplify.rs +++ b/src/simplify.rs @@ -18,9 +18,9 @@ impl SimplificationResult } } -fn remove_unnecessary_exists_parameters(formula: &mut foliage::Formula) -> SimplificationResult +fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) -> SimplificationResult { - use foliage::Formula; + use crate::Formula; match formula { @@ -123,10 +123,10 @@ fn remove_unnecessary_exists_parameters(formula: &mut foliage::Formula) -> Simpl } } -fn simplify_quantified_formulas_without_parameters(formula: &mut foliage::Formula) +fn simplify_quantified_formulas_without_parameters(formula: &mut crate::Formula) -> SimplificationResult { - use foliage::Formula; + use crate::Formula; match formula { @@ -153,7 +153,7 @@ fn simplify_quantified_formulas_without_parameters(formula: &mut foliage::Formul if quantified_formula.parameters.is_empty() { // TODO: remove workaround - let mut argument = foliage::Formula::false_(); + let mut argument = crate::Formula::false_(); std::mem::swap(&mut argument, &mut quantified_formula.argument); *formula = argument; @@ -171,22 +171,22 @@ fn simplify_quantified_formulas_without_parameters(formula: &mut foliage::Formul } } -fn simplify_trivial_n_ary_formulas(formula: &mut foliage::Formula) -> SimplificationResult +fn simplify_trivial_n_ary_formulas(formula: &mut crate::Formula) -> SimplificationResult { - use foliage::Formula; + use crate::Formula; match formula { Formula::And(arguments) | Formula::IfAndOnlyIf(arguments) if arguments.is_empty() => { - *formula = foliage::Formula::true_(); + *formula = crate::Formula::true_(); return SimplificationResult::Simplified; }, | Formula::Or(arguments) if arguments.is_empty() => { - *formula = foliage::Formula::false_(); + *formula = crate::Formula::false_(); return SimplificationResult::Simplified; }, @@ -225,7 +225,7 @@ fn simplify_trivial_n_ary_formulas(formula: &mut foliage::Formula) -> Simplifica } } -pub(crate) fn simplify(formula: &mut foliage::Formula) +pub(crate) fn simplify(formula: &mut crate::Formula) { loop { diff --git a/src/traits.rs b/src/traits.rs deleted file mode 100644 index b2eee25..0000000 --- a/src/traits.rs +++ /dev/null @@ -1,23 +0,0 @@ -pub(crate) trait InputConstantDeclarationDomain -{ - fn input_constant_declaration_domain(&self, - declaration: &std::rc::Rc) -> crate::Domain; -} - -pub(crate) trait AssignVariableDeclarationDomain -{ - fn assign_variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc, domain: crate::Domain); -} - -pub(crate) trait VariableDeclarationDomain -{ - fn variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc) -> Option; -} - -pub(crate) trait VariableDeclarationID -{ - fn variable_declaration_id(&self, - variable_declaration: &std::rc::Rc) -> usize; -} diff --git a/src/translate/common/choose_value_in_term.rs b/src/translate/common/choose_value_in_term.rs index 7057cdb..a29c801 100644 --- a/src/translate/common/choose_value_in_term.rs +++ b/src/translate/common/choose_value_in_term.rs @@ -1,19 +1,18 @@ -pub(crate) fn choose_value_in_primitive(term: Box, - variable_declaration: std::rc::Rc) - -> foliage::Formula +pub(crate) fn choose_value_in_primitive(term: Box, + variable_declaration: std::rc::Rc) + -> crate::Formula { - let variable = foliage::Term::variable(variable_declaration); + let variable = crate::Term::variable(variable_declaration); - foliage::Formula::equal(Box::new(variable), term) + crate::Formula::equal(Box::new(variable), term) } pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, - variable_declaration: std::rc::Rc, context: &C, - variable_declaration_stack: &foliage::VariableDeclarationStackLayer) - -> Result + variable_declaration: std::rc::Rc, context: &C, + variable_declaration_stack: &crate::VariableDeclarationStackLayer) + -> Result where - C: foliage::FindOrCreateFunctionDeclaration - + crate::traits::AssignVariableDeclarationDomain + C: foliage::FindOrCreateFunctionDeclaration, { match term.term_type() { @@ -21,15 +20,15 @@ where .map_err(|error| crate::Error::new_logic("clingo error").with(error))? { clingo::SymbolType::Number => Ok(choose_value_in_primitive( - Box::new(foliage::Term::integer(symbol.number() + Box::new(crate::Term::integer(symbol.number() .map_err(|error| crate::Error::new_logic("clingo error").with(error))?)), variable_declaration)), clingo::SymbolType::Infimum => Ok(choose_value_in_primitive( - Box::new(foliage::Term::infimum()), variable_declaration)), + Box::new(crate::Term::infimum()), variable_declaration)), clingo::SymbolType::Supremum => Ok(choose_value_in_primitive( - Box::new(foliage::Term::supremum()), variable_declaration)), + Box::new(crate::Term::supremum()), variable_declaration)), clingo::SymbolType::String => Ok(choose_value_in_primitive( - Box::new(foliage::Term::string(symbol.string() + Box::new(crate::Term::string(symbol.string() .map_err(|error| crate::Error::new_logic("clingo error").with(error))? .to_string())), variable_declaration)), @@ -51,7 +50,7 @@ where let constant_declaration = context.find_or_create_function_declaration(constant_name, 0); - let function = foliage::Term::function(constant_declaration, vec![]); + let function = crate::Term::function(constant_declaration, vec![]); Ok(choose_value_in_primitive(Box::new(function), variable_declaration)) } @@ -60,14 +59,14 @@ where { let other_variable_declaration = match variable_name { - // TODO: check // Every occurrence of anonymous variables is treated as if it introduced a fresh // variable declaration "_" => variable_declaration_stack.free_variable_declarations_do_mut( |free_variable_declarations| { + // TODO: check domain type let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("_".to_owned())); + crate::VariableDeclaration::new_generated(crate::Domain::Program)); free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration)); @@ -75,9 +74,7 @@ where }), _ => variable_declaration_stack.find_or_create(variable_name), }; - context.assign_variable_declaration_domain(&other_variable_declaration, - crate::Domain::Program); - let other_variable = foliage::Term::variable(other_variable_declaration); + let other_variable = crate::Term::variable(other_variable_declaration); Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration)) }, @@ -92,26 +89,21 @@ where | foliage::BinaryOperator::Multiply => { - let parameters = (0..2).map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Integer); - variable_declaration - }) - .collect::(); + let parameters = (0..2).map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Integer))) + .collect::(); let parameters = std::rc::Rc::new(parameters); let parameter_1 = ¶meters[0]; let parameter_2 = ¶meters[1]; - let translated_binary_operation = foliage::Term::binary_operation(operator, - Box::new(foliage::Term::variable(std::rc::Rc::clone(¶meter_1))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(¶meter_2)))); + let translated_binary_operation = crate::Term::binary_operation(operator, + Box::new(crate::Term::variable(std::rc::Rc::clone(¶meter_1))), + Box::new(crate::Term::variable(std::rc::Rc::clone(¶meter_2)))); - let equals = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), + let equals = crate::Formula::equal( + Box::new(crate::Term::variable(variable_declaration)), Box::new(translated_binary_operation)); let choose_value_from_left_argument = choose_value_in_term( @@ -122,24 +114,19 @@ where binary_operation.right(), std::rc::Rc::clone(¶meter_2), context, variable_declaration_stack)?; - let and = foliage::Formula::And(vec![equals, choose_value_from_left_argument, + let and = crate::Formula::And(vec![equals, choose_value_from_left_argument, choose_value_from_right_argument]); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) }, foliage::BinaryOperator::Divide | foliage::BinaryOperator::Modulo => { - let parameters = (0..4).map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Integer); - variable_declaration - }) - .collect::(); + let parameters = (0..4).map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Integer))) + .collect::(); let parameters = std::rc::Rc::new(parameters); let parameter_i = ¶meters[0]; @@ -147,15 +134,15 @@ where let parameter_q = ¶meters[2]; let parameter_r = ¶meters[3]; - let j_times_q = foliage::Term::multiply( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q)))); + let j_times_q = crate::Term::multiply( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j))), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q)))); - let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r)))); + let j_times_q_plus_r = crate::Term::add(Box::new(j_times_q), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r)))); - let i_equals_j_times_q_plus_r = foliage::Formula::equal( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))), + let i_equals_j_times_q_plus_r = crate::Formula::equal( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_i))), Box::new(j_times_q_plus_r)); let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), @@ -164,26 +151,26 @@ where let choose_j_in_t2 = choose_value_in_term(binary_operation.right(), std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?; - let j_not_equal_to_0 = foliage::Formula::not_equal( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))), - Box::new(foliage::Term::integer(0))); + let j_not_equal_to_0 = crate::Formula::not_equal( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j))), + Box::new(crate::Term::integer(0))); - let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))), - Box::new(foliage::Term::integer(0))); + let r_greater_or_equal_to_0 = crate::Formula::greater_or_equal( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))), + Box::new(crate::Term::integer(0))); - let r_less_than_q = foliage::Formula::less( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q)))); + let r_less_than_q = crate::Formula::less( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q)))); - let z_equal_to_q = foliage::Formula::equal( + let z_equal_to_q = crate::Formula::equal( Box::new( - foliage::Term::variable(std::rc::Rc::clone(&variable_declaration))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q)))); + crate::Term::variable(std::rc::Rc::clone(&variable_declaration))), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q)))); - let z_equal_to_r = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r)))); + let z_equal_to_r = crate::Formula::equal( + Box::new(crate::Term::variable(variable_declaration)), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r)))); let last_argument = match operator { @@ -192,11 +179,11 @@ where _ => return Err(crate::Error::new_logic("unreachable code")), }; - let and = foliage::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1, + let and = crate::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1, choose_j_in_t2, j_not_equal_to_0, r_greater_or_equal_to_0, r_less_than_q, last_argument]); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) }, foliage::BinaryOperator::Exponentiate => Err(crate::Error::new_unsupported_language_feature("exponentiation")), @@ -210,41 +197,34 @@ where return Err(crate::Error::new_unsupported_language_feature("absolute value")), clingo::ast::UnaryOperator::Minus => { - let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new( - "".to_string())); - context.assign_variable_declaration_domain(¶meter_z_prime, - crate::Domain::Integer); + let parameter_z_prime = std::rc::Rc::new( + crate::VariableDeclaration::new_generated(crate::Domain::Integer)); - let negative_z_prime = foliage::Term::negative(Box::new( - foliage::Term::variable(std::rc::Rc::clone(¶meter_z_prime)))); - let equals = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), + let negative_z_prime = crate::Term::negative(Box::new( + crate::Term::variable(std::rc::Rc::clone(¶meter_z_prime)))); + let equals = crate::Formula::equal( + Box::new(crate::Term::variable(variable_declaration)), Box::new(negative_z_prime)); let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(), std::rc::Rc::clone(¶meter_z_prime), context, variable_declaration_stack)?; - let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]); + let and = crate::Formula::and(vec![equals, choose_z_prime_in_t_prime]); let parameters = std::rc::Rc::new(vec![parameter_z_prime]); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) }, _ => Err(crate::Error::new_not_yet_implemented("todo")), } }, clingo::ast::TermType::Interval(interval) => { - let parameters = (0..3).map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Integer); - variable_declaration - }) - .collect::(); + let parameters = (0..3).map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Integer))) + .collect::(); let parameters = std::rc::Rc::new(parameters); let parameter_i = ¶meters[0]; @@ -257,22 +237,22 @@ where let choose_j_in_t_2 = choose_value_in_term(interval.right(), std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?; - let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k)))); + let i_less_than_or_equal_to_k = crate::Formula::less_or_equal( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_i))), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k)))); - let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal( - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j)))); + let k_less_than_or_equal_to_j = crate::Formula::less_or_equal( + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k))), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j)))); - let z_equals_k = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k)))); + let z_equals_k = crate::Formula::equal( + Box::new(crate::Term::variable(variable_declaration)), + Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k)))); - let and = foliage::Formula::and(vec![choose_i_in_t_1, choose_j_in_t_2, + let and = crate::Formula::and(vec![choose_i_in_t_1, choose_j_in_t_2, i_less_than_or_equal_to_k, k_less_than_or_equal_to_j, z_equals_k]); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) }, clingo::ast::TermType::Function(_) => Err(crate::Error::new_unsupported_language_feature("symbolic functions")), diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index ee690c9..e6423a2 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -3,16 +3,17 @@ mod translate_body; use head_type::*; use translate_body::*; -use crate::traits::AssignVariableDeclarationDomain as _; + +use foliage::flavor::{PredicateDeclaration as _}; struct PredicateDefinitions { - pub parameters: std::rc::Rc, - pub definitions: Vec, + pub parameters: std::rc::Rc, + pub definitions: Vec, } type Definitions = - std::collections::BTreeMap::, PredicateDefinitions>; + std::collections::BTreeMap::, PredicateDefinitions>; pub(crate) struct Translator<'p> { @@ -76,8 +77,7 @@ impl<'p> Translator<'p> log::info!("read input program “{}”", program_path.as_ref().display()); - let completed_definition = |predicate_declaration, definitions: &mut Definitions, - problem: &crate::Problem| + let completed_definition = |predicate_declaration, definitions: &mut Definitions| { match definitions.remove(predicate_declaration) { @@ -87,19 +87,19 @@ impl<'p> Translator<'p> let or_arguments = predicate_definitions.definitions.into_iter() .map(|x| crate::existential_closure(x)) .collect::>(); - let or = foliage::Formula::or(or_arguments); + let or = crate::Formula::or(or_arguments); let head_arguments = predicate_definitions.parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .map(|x| crate::Term::variable(std::rc::Rc::clone(x))) .collect::>(); - let head_predicate = foliage::Formula::predicate( + let head_predicate = crate::Formula::predicate( std::rc::Rc::clone(predicate_declaration), head_arguments); let completed_definition = - foliage::Formula::if_and_only_if(vec![head_predicate, or]); + crate::Formula::if_and_only_if(vec![head_predicate, or]); - let open_formula = foliage::OpenFormula + let open_formula = crate::OpenFormula { free_variable_declarations: predicate_definitions.parameters, formula: completed_definition, @@ -110,27 +110,21 @@ impl<'p> Translator<'p> // This predicate has no definitions, so universally falsify it None => { - let parameters = std::rc::Rc::new((0..predicate_declaration.arity) - .map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - problem.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) + let parameters = std::rc::Rc::new((0..predicate_declaration.arity()).map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Program))) .collect::>()); let head_arguments = parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .map(|x| crate::Term::variable(std::rc::Rc::clone(x))) .collect(); - let head_predicate = foliage::Formula::predicate( + let head_predicate = crate::Formula::predicate( std::rc::Rc::clone(predicate_declaration), head_arguments); - let not = foliage::Formula::not(Box::new(head_predicate)); + let not = crate::Formula::not(Box::new(head_predicate)); - let open_formula = foliage::OpenFormula + let open_formula = crate::OpenFormula { free_variable_declarations: parameters, formula: not, @@ -144,9 +138,7 @@ impl<'p> Translator<'p> for predicate_declaration in self.problem.predicate_declarations.borrow().iter() { // Don’t perform completion for input predicates and built-in predicates - if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration) - || predicate_declaration.name.starts_with("p__") - && predicate_declaration.name.ends_with("__") + if *predicate_declaration.is_input.borrow() || predicate_declaration.is_built_in() { continue; } @@ -154,12 +146,18 @@ impl<'p> Translator<'p> let statement_kind = crate::problem::StatementKind::CompletedDefinition( std::rc::Rc::clone(&predicate_declaration)); - let completed_definition = completed_definition(predicate_declaration, - &mut self.definitions, self.problem); + let mut completed_definition = completed_definition(predicate_declaration, + &mut self.definitions); + + crate::autoname_variables(&mut completed_definition); + + //crate::simplify(&mut completed_definition); + + let statement_name = + format!("completed_definition_{}", predicate_declaration.tptp_statement_name()); let statement = crate::problem::Statement::new(statement_kind, completed_definition) - .with_name(format!("completed_definition_{}_{}", predicate_declaration.name, - predicate_declaration.arity)); + .with_name(statement_name); self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions, statement); @@ -180,15 +178,10 @@ impl<'p> Translator<'p> { if !self.definitions.contains_key(&head_atom.predicate_declaration) { - let parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity) - .map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - self.problem.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) + let parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity()) + .map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Program))) .collect()); self.definitions.insert( @@ -207,9 +200,9 @@ impl<'p> Translator<'p> let parameters = std::rc::Rc::clone(&predicate_definitions.parameters); let free_variable_declarations = std::cell::RefCell::new(vec![]); let free_layer = - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); + crate::VariableDeclarationStackLayer::Free(free_variable_declarations); let parameters_layer = - foliage::VariableDeclarationStackLayer::bound(&free_layer, parameters); + crate::VariableDeclarationStackLayer::bound(&free_layer, parameters); let mut definition_arguments = translate_body(rule.body(), self.problem, ¶meters_layer)?; @@ -220,10 +213,10 @@ impl<'p> Translator<'p> if let HeadType::ChoiceWithSingleAtom(_) = head_type { let head_arguments = predicate_definitions.parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .map(|x| crate::Term::variable(std::rc::Rc::clone(x))) .collect::>(); - let head_predicate = foliage::Formula::predicate( + let head_predicate = crate::Formula::predicate( std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments); definition_arguments.push(head_predicate); @@ -245,7 +238,7 @@ impl<'p> Translator<'p> // TODO: refactor let free_variable_declarations = match free_layer { - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + crate::VariableDeclarationStackLayer::Free(free_variable_declarations) => free_variable_declarations.into_inner(), _ => unreachable!(), }; @@ -253,11 +246,11 @@ impl<'p> Translator<'p> let definition = match definition_arguments.len() { 1 => definition_arguments.pop().unwrap(), - 0 => foliage::Formula::true_(), - _ => foliage::Formula::and(definition_arguments), + 0 => crate::Formula::true_(), + _ => crate::Formula::and(definition_arguments), }; - let definition = foliage::OpenFormula + let definition = crate::OpenFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula: definition, @@ -269,26 +262,26 @@ impl<'p> Translator<'p> { let free_variable_declarations = std::cell::RefCell::new(vec![]); let free_layer = - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); + crate::VariableDeclarationStackLayer::Free(free_variable_declarations); let mut arguments = translate_body(rule.body(), self.problem, &free_layer)?; // TODO: refactor let free_variable_declarations = match free_layer { - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + crate::VariableDeclarationStackLayer::Free(free_variable_declarations) => free_variable_declarations.into_inner(), _ => unreachable!(), }; let formula = match arguments.len() { - 1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())), - 0 => foliage::Formula::false_(), - _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), + 1 => crate::Formula::not(Box::new(arguments.pop().unwrap())), + 0 => crate::Formula::false_(), + _ => crate::Formula::not(Box::new(crate::Formula::and(arguments))), }; - let open_formula = foliage::OpenFormula + let open_formula = crate::OpenFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula, @@ -296,6 +289,8 @@ impl<'p> Translator<'p> let integrity_constraint = crate::universal_closure(open_formula); + //crate::simplify(&mut integrity_constraint); + let statement = crate::problem::Statement::new( crate::problem::StatementKind::IntegrityConstraint, integrity_constraint) .with_name("integrity_constraint".to_string()); diff --git a/src/translate/verify_properties/head_type.rs b/src/translate/verify_properties/head_type.rs index 01d6c0e..2913131 100644 --- a/src/translate/verify_properties/head_type.rs +++ b/src/translate/verify_properties/head_type.rs @@ -1,6 +1,6 @@ pub(crate) struct HeadAtom<'a> { - pub predicate_declaration: std::rc::Rc, + pub predicate_declaration: std::rc::Rc, pub arguments: &'a [clingo::ast::Term<'a>], } @@ -15,7 +15,7 @@ pub(crate) enum HeadType<'a> pub(crate) fn determine_head_type<'a, C>(head_literal: &'a clingo::ast::HeadLiteral, context: &C) -> Result, crate::Error> where - C: foliage::FindOrCreatePredicateDeclaration + C: foliage::FindOrCreatePredicateDeclaration { let create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error> { diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index db60d46..03fe584 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,11 +1,10 @@ // TODO: rename context pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, - context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer) - -> Result + context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer) + -> Result where - C: foliage::FindOrCreateFunctionDeclaration - + foliage::FindOrCreatePredicateDeclaration - + crate::traits::AssignVariableDeclarationDomain + C: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration, { let function = match body_term.term_type() { @@ -18,22 +17,16 @@ where let predicate_declaration = context.find_or_create_predicate_declaration(function_name, function.arguments().len()); - let parameters = function.arguments().iter().map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) - .collect::(); + let parameters = function.arguments().iter().map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(crate::Domain::Program))) + .collect::(); let parameters = std::rc::Rc::new(parameters); let predicate_arguments = parameters.iter().map( - |parameter| foliage::Term::variable(std::rc::Rc::clone(parameter))) + |parameter| crate::Term::variable(std::rc::Rc::clone(parameter))) .collect::>(); - let predicate = foliage::Formula::predicate(predicate_declaration, predicate_arguments); + let predicate = crate::Formula::predicate(predicate_declaration, predicate_arguments); let predicate_literal = match sign { @@ -41,7 +34,7 @@ where | clingo::ast::Sign::DoubleNegation => predicate, clingo::ast::Sign::Negation - => foliage::Formula::not(Box::new(predicate)), + => crate::Formula::not(Box::new(predicate)), }; if function.arguments().is_empty() @@ -60,18 +53,17 @@ where arguments.push(predicate_literal); - let and = foliage::Formula::and(arguments); + let and = crate::Formula::and(arguments); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) } pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, - context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer) - -> Result + context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer) + -> Result where - C: foliage::FindOrCreateFunctionDeclaration - + foliage::FindOrCreatePredicateDeclaration - + crate::traits::AssignVariableDeclarationDomain + C: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration, { match body_literal.sign() { @@ -97,21 +89,16 @@ where _ => return Err(crate::Error::new_logic("unexpected negated Boolean value")), } - Ok(foliage::Formula::Boolean(value)) + Ok(crate::Formula::Boolean(value)) }, clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), context, variable_declaration_stack), clingo::ast::LiteralType::Comparison(comparison) => { - let parameters = (0..2).map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) - .collect::(); + let parameters = (0..2).map( + |_| std::rc::Rc::new(crate::VariableDeclaration::new_generated( + crate::Domain::Program))) + .collect::(); let parameters = std::rc::Rc::new(parameters); let mut parameters_iterator = parameters.iter(); @@ -123,19 +110,19 @@ where let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), std::rc::Rc::clone(parameter_z2), context, variable_declaration_stack)?; - let variable_1 = foliage::Term::variable(std::rc::Rc::clone(parameter_z1)); - let variable_2 = foliage::Term::variable(std::rc::Rc::clone(parameter_z2)); + let variable_1 = crate::Term::variable(std::rc::Rc::clone(parameter_z1)); + let variable_2 = crate::Term::variable(std::rc::Rc::clone(parameter_z2)); let operator = crate::translate::common::translate_comparison_operator( comparison.comparison_type()); - let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1), + let compare_z1_and_z2 = crate::Formula::compare(operator, Box::new(variable_1), Box::new(variable_2)); let and = - foliage::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]); + crate::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]); - Ok(foliage::Formula::exists(parameters, Box::new(and))) + Ok(crate::Formula::exists(parameters, Box::new(and))) }, _ => Err(crate::Error::new_unsupported_language_feature( "body literals other than Booleans, terms, or comparisons")), @@ -143,15 +130,14 @@ where } pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &C, - variable_declaration_stack: &foliage::VariableDeclarationStackLayer) - -> Result + variable_declaration_stack: &crate::VariableDeclarationStackLayer) + -> Result where - C: foliage::FindOrCreateFunctionDeclaration - + foliage::FindOrCreatePredicateDeclaration - + crate::traits::AssignVariableDeclarationDomain + C: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration, { body_literals.iter() .map(|body_literal| translate_body_literal(body_literal, context, variable_declaration_stack)) - .collect::>() + .collect::>() } diff --git a/src/utils.rs b/src/utils.rs index 6ec4375..dff0305 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -1,9 +1,11 @@ mod arithmetic_terms; +mod autoname_variables; mod closures; mod copy_formula; mod output_predicates; mod variables_in_terms; +pub(crate) use autoname_variables::*; pub(crate) use arithmetic_terms::*; pub(crate) use closures::*; pub(crate) use copy_formula::*; diff --git a/src/utils/arithmetic_terms.rs b/src/utils/arithmetic_terms.rs index 6795892..b2c578e 100644 --- a/src/utils/arithmetic_terms.rs +++ b/src/utils/arithmetic_terms.rs @@ -1,16 +1,15 @@ -pub(crate) fn is_term_arithmetic(term: &foliage::Term, context: &C) -> Result -where - C: crate::traits::InputConstantDeclarationDomain - + crate::traits::VariableDeclarationDomain +pub(crate) fn is_term_arithmetic(term: &crate::Term) -> Result { + use crate::Term; + match term { - foliage::Term::Boolean(_) - | foliage::Term::SpecialInteger(_) - | foliage::Term::String(_) + Term::Boolean(_) + | Term::SpecialInteger(_) + | Term::String(_) => Ok(false), - foliage::Term::Integer(_) => Ok(true), - foliage::Term::Function(ref function) => + Term::Integer(_) => Ok(true), + Term::Function(ref function) => { if !function.arguments.is_empty() { @@ -18,20 +17,17 @@ where crate::Error::new_unsupported_language_feature("functions with arguments")); } - let domain = context.input_constant_declaration_domain(&function.declaration); - - Ok(domain == crate::Domain::Integer) + Ok(*function.declaration.domain.borrow() == crate::Domain::Integer) }, - foliage::Term::Variable(foliage::Variable{ref declaration}) => - match context.variable_declaration_domain(declaration) + Term::Variable(crate::Variable{ref declaration}) => + match declaration.domain()? { - Some(crate::Domain::Program) => Ok(false), - Some(crate::Domain::Integer) => Ok(true), - None => Err(crate::Error::new_logic("unspecified variable declaration domain")), + crate::Domain::Program => Ok(false), + crate::Domain::Integer => Ok(true), }, - foliage::Term::BinaryOperation(foliage::BinaryOperation{ref left, ref right, ..}) - => Ok(is_term_arithmetic(left, context)? && is_term_arithmetic(right, context)?), - foliage::Term::UnaryOperation(foliage::UnaryOperation{ref argument, ..}) - => is_term_arithmetic(argument, context), + Term::BinaryOperation(crate::BinaryOperation{ref left, ref right, ..}) + => Ok(is_term_arithmetic(left)? && is_term_arithmetic(right)?), + Term::UnaryOperation(crate::UnaryOperation{ref argument, ..}) + => is_term_arithmetic(argument), } } diff --git a/src/utils/autoname_variables.rs b/src/utils/autoname_variables.rs new file mode 100644 index 0000000..e3ce754 --- /dev/null +++ b/src/utils/autoname_variables.rs @@ -0,0 +1,223 @@ +struct IDs +{ + program_variable_id: usize, + integer_variable_id: usize, +} + +impl IDs +{ + pub fn new() -> Self + { + Self + { + program_variable_id: 0, + integer_variable_id: 0, + } + } +} + +fn reset_variable_name(variable_declaration: &crate::VariableDeclaration) +{ + let domain = match variable_declaration.domain() + { + Ok(domain) => domain, + Err(_) => unreachable!("all variable domains should be assigned at this point"), + }; + + let ref mut variable_name = *variable_declaration.name.borrow_mut(); + + match variable_name + { + crate::VariableName::Generated(ref mut generated_variable_name) => + generated_variable_name.id = None, + crate::VariableName::UserDefined(_) => + *variable_name = crate::VariableName::Generated( + crate::GeneratedVariableName + { + domain, + id: None, + }), + } +} + +fn reset_variable_names_in_term(term: &mut crate::Term) +{ + use foliage::Term; + + match term + { + Term::BinaryOperation(ref mut binary_operation) => + { + reset_variable_names_in_term(&mut *binary_operation.left); + reset_variable_names_in_term(&mut *binary_operation.right); + }, + Term::Boolean(_) + | Term::Integer(_) + | Term::SpecialInteger(_) + | Term::String(_) => (), + Term::Function(ref mut function) => + for mut argument in &mut function.arguments + { + reset_variable_names_in_term(&mut argument); + }, + Term::UnaryOperation(ref mut unary_operation) => + reset_variable_names_in_term(&mut *unary_operation.argument), + Term::Variable(ref mut variable) => reset_variable_name(&variable.declaration), + } +} + +fn reset_variable_names_in_formula(formula: &mut crate::Formula) +{ + use foliage::Formula; + + match formula + { + Formula::And(ref mut arguments) + | Formula::IfAndOnlyIf(ref mut arguments) + | Formula::Or(ref mut arguments) => + for argument in arguments + { + reset_variable_names_in_formula(argument); + }, + Formula::Boolean(_) => (), + Formula::Compare(ref mut compare) => + { + reset_variable_names_in_term(&mut *compare.left); + reset_variable_names_in_term(&mut *compare.right); + }, + Formula::Exists(ref mut quantified_formula) + | Formula::ForAll(ref mut quantified_formula) => + { + for ref parameter in &*quantified_formula.parameters + { + reset_variable_name(¶meter); + } + + reset_variable_names_in_formula(&mut *quantified_formula.argument); + }, + Formula::Implies(ref mut implies) => + { + reset_variable_names_in_formula(&mut *implies.antecedent); + reset_variable_names_in_formula(&mut *implies.implication); + }, + Formula::Not(ref mut argument) => reset_variable_names_in_formula(argument), + Formula::Predicate(ref mut predicate) => + for mut argument in &mut predicate.arguments + { + reset_variable_names_in_term(&mut argument); + }, + } +} + +fn set_variable_name(variable_declaration: &crate::VariableDeclaration, ids: &mut IDs) +{ + match *variable_declaration.name.borrow_mut() + { + crate::VariableName::Generated(ref mut generated_variable_name) => + { + if generated_variable_name.id.is_some() + { + return; + } + + match generated_variable_name.domain + { + crate::Domain::Program => + { + generated_variable_name.id = Some(ids.program_variable_id); + ids.program_variable_id += 1; + }, + crate::Domain::Integer => + { + generated_variable_name.id = Some(ids.integer_variable_id); + ids.integer_variable_id += 1; + }, + } + }, + crate::VariableName::UserDefined(_) => (), + } +} + +fn set_variable_names_in_term(term: &mut crate::Term, ids: &mut IDs) +{ + use foliage::Term; + + match term + { + Term::BinaryOperation(ref mut binary_operation) => + { + set_variable_names_in_term(&mut *binary_operation.left, ids); + set_variable_names_in_term(&mut *binary_operation.right, ids); + }, + Term::Boolean(_) + | Term::Integer(_) + | Term::SpecialInteger(_) + | Term::String(_) => (), + Term::Function(ref mut function) => + for mut argument in &mut function.arguments + { + set_variable_names_in_term(&mut argument, ids); + }, + Term::UnaryOperation(ref mut unary_operation) => + set_variable_names_in_term(&mut *unary_operation.argument, ids), + Term::Variable(ref mut variable) => set_variable_name(&variable.declaration, ids), + } +} + +fn set_variable_names_in_formula(formula: &mut crate::Formula, ids: &mut IDs) +{ + use foliage::Formula; + + match formula + { + Formula::And(ref mut arguments) + | Formula::IfAndOnlyIf(ref mut arguments) + | Formula::Or(ref mut arguments) => + for argument in arguments + { + set_variable_names_in_formula(argument, ids); + }, + Formula::Boolean(_) => (), + Formula::Compare(ref mut compare) => + { + set_variable_names_in_term(&mut *compare.left, ids); + set_variable_names_in_term(&mut *compare.right, ids); + }, + Formula::Exists(ref mut quantified_formula) + | Formula::ForAll(ref mut quantified_formula) => + { + for ref parameter in &*quantified_formula.parameters + { + set_variable_name(¶meter, ids); + } + + set_variable_names_in_formula(&mut *quantified_formula.argument, ids); + }, + Formula::Implies(ref mut implies) => + match implies.direction + { + foliage::ImplicationDirection::LeftToRight => + { + set_variable_names_in_formula(&mut *implies.antecedent, ids); + set_variable_names_in_formula(&mut *implies.implication, ids); + }, + foliage::ImplicationDirection::RightToLeft => + { + set_variable_names_in_formula(&mut *implies.implication, ids); + set_variable_names_in_formula(&mut *implies.antecedent, ids); + }, + }, + Formula::Not(ref mut argument) => set_variable_names_in_formula(argument, ids), + Formula::Predicate(ref mut predicate) => + for mut argument in &mut predicate.arguments + { + set_variable_names_in_term(&mut argument, ids); + }, + } +} + +pub(crate) fn autoname_variables(formula: &mut crate::Formula) +{ + reset_variable_names_in_formula(formula); + set_variable_names_in_formula(formula, &mut IDs::new()); +} diff --git a/src/utils/closures.rs b/src/utils/closures.rs index ce8b5b4..566e779 100644 --- a/src/utils/closures.rs +++ b/src/utils/closures.rs @@ -1,19 +1,19 @@ -pub(crate) fn existential_closure(open_formula: foliage::OpenFormula) -> foliage::Formula +pub(crate) fn existential_closure(open_formula: crate::OpenFormula) -> crate::Formula { match open_formula.free_variable_declarations.is_empty() { true => open_formula.formula, - false => foliage::Formula::exists(open_formula.free_variable_declarations, + false => crate::Formula::exists(open_formula.free_variable_declarations, Box::new(open_formula.formula)), } } -pub(crate) fn universal_closure(open_formula: foliage::OpenFormula) -> foliage::Formula +pub(crate) fn universal_closure(open_formula: crate::OpenFormula) -> crate::Formula { match open_formula.free_variable_declarations.is_empty() { true => open_formula.formula, - false => foliage::Formula::for_all(open_formula.free_variable_declarations, + false => crate::Formula::for_all(open_formula.free_variable_declarations, Box::new(open_formula.formula)), } } diff --git a/src/utils/copy_formula.rs b/src/utils/copy_formula.rs index 96c26fd..a24f7f2 100644 --- a/src/utils/copy_formula.rs +++ b/src/utils/copy_formula.rs @@ -1,10 +1,10 @@ -fn replace_variables_in_term(term: &mut foliage::Term, - old_variable_declarations: &foliage::VariableDeclarations, - new_variable_declarations: &foliage::VariableDeclarations) +fn replace_variables_in_term(term: &mut crate::Term, + old_variable_declarations: &crate::VariableDeclarations, + new_variable_declarations: &crate::VariableDeclarations) { assert_eq!(old_variable_declarations.len(), new_variable_declarations.len()); - use foliage::Term; + use crate::Term; match term { @@ -45,11 +45,11 @@ fn replace_variables_in_term(term: &mut foliage::Term, } } -fn replace_variables_in_formula(formula: &mut foliage::Formula, - old_variable_declarations: &foliage::VariableDeclarations, - new_variable_declarations: &foliage::VariableDeclarations) +fn replace_variables_in_formula(formula: &mut crate::Formula, + old_variable_declarations: &crate::VariableDeclarations, + new_variable_declarations: &crate::VariableDeclarations) { - use foliage::Formula; + use crate::Formula; match formula { @@ -92,10 +92,10 @@ fn replace_variables_in_formula(formula: &mut foliage::Formula, } } -fn replace_variable_in_term_with_term(term: &mut foliage::Term, - variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term) +fn replace_variable_in_term_with_term(term: &mut crate::Term, + variable_declaration: &crate::VariableDeclaration, replacement_term: &crate::Term) { - use foliage::Term; + use crate::Term; match term { @@ -127,10 +127,10 @@ fn replace_variable_in_term_with_term(term: &mut foliage::Term, } } -pub(crate) fn replace_variable_in_formula_with_term(formula: &mut foliage::Formula, - variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term) +pub(crate) fn replace_variable_in_formula_with_term(formula: &mut crate::Formula, + variable_declaration: &crate::VariableDeclaration, replacement_term: &crate::Term) { - use foliage::Formula; + use crate::Formula; match formula { @@ -172,9 +172,9 @@ pub(crate) fn replace_variable_in_formula_with_term(formula: &mut foliage::Formu } } -pub(crate) fn copy_term(term: &foliage::Term) -> foliage::Term +pub(crate) fn copy_term(term: &crate::Term) -> crate::Term { - use foliage::Term; + use crate::Term; match term { @@ -194,67 +194,49 @@ pub(crate) fn copy_term(term: &foliage::Term) -> foliage::Term } } -fn copy_quantified_formula(quantified_expression: &foliage::QuantifiedFormula, declarations: &D) - -> foliage::QuantifiedFormula -where - D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +fn copy_quantified_formula(quantified_expression: &crate::QuantifiedFormula) + -> crate::QuantifiedFormula { let copy_parameters = quantified_expression.parameters.iter() - .map( - |parameter| - { - let copy_parameter = std::rc::Rc::new( - foliage::VariableDeclaration::new(parameter.name.clone())); - - if let Some(domain) = declarations.variable_declaration_domain(parameter) - { - declarations.assign_variable_declaration_domain(©_parameter, domain); - } - - copy_parameter - }) + // TODO: check correctness of clone implementation + .map(|x| x.clone()) .collect(); let copy_parameters = std::rc::Rc::new(copy_parameters); - let mut copy_argument = copy_formula(&quantified_expression.argument, declarations); + let mut copy_argument = copy_formula(&quantified_expression.argument); replace_variables_in_formula(&mut copy_argument, &quantified_expression.parameters, ©_parameters); - foliage::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument)) + crate::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument)) } -pub(crate) fn copy_formula(formula: &foliage::Formula, declarations: &D) -> foliage::Formula -where - D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +pub(crate) fn copy_formula(formula: &crate::Formula) -> crate::Formula { - use foliage::Formula; + use crate::Formula; match formula { Formula::And(arguments) => - Formula::and(arguments.iter().map( - |argument| copy_formula(argument, declarations)).collect()), + Formula::and(arguments.iter().map(|argument| copy_formula(argument)).collect()), Formula::Boolean(value) => Formula::boolean(*value), Formula::Compare(compare) => Formula::compare(compare.operator, Box::new(copy_term(&compare.left)), Box::new(copy_term(&compare.right))), Formula::Exists(quantified_formula) => - Formula::Exists(copy_quantified_formula(quantified_formula, declarations)), + Formula::Exists(copy_quantified_formula(quantified_formula)), Formula::ForAll(quantified_formula) => - Formula::ForAll(copy_quantified_formula(quantified_formula, declarations)), + Formula::ForAll(copy_quantified_formula(quantified_formula)), Formula::IfAndOnlyIf(arguments) => Formula::if_and_only_if( - arguments.iter().map(|argument| copy_formula(argument, declarations)).collect()), + arguments.iter().map(|argument| copy_formula(argument)).collect()), Formula::Implies(implies) => - Formula::implies(implies.direction, - Box::new(copy_formula(&implies.antecedent, declarations)), - Box::new(copy_formula(&implies.implication, declarations))), - Formula::Not(argument) => Formula::not(Box::new(copy_formula(&argument, declarations))), + Formula::implies(implies.direction, Box::new(copy_formula(&implies.antecedent)), + Box::new(copy_formula(&implies.implication))), + Formula::Not(argument) => Formula::not(Box::new(copy_formula(&argument))), Formula::Or(arguments) => - Formula::or(arguments.iter().map( - |argument| copy_formula(argument, declarations)).collect()), + Formula::or(arguments.iter().map(|argument| copy_formula(argument)).collect()), Formula::Predicate(predicate) => Formula::predicate(std::rc::Rc::clone(&predicate.declaration), predicate.arguments.iter().map(|argument| copy_term(argument)).collect()), diff --git a/src/utils/output_predicates.rs b/src/utils/output_predicates.rs index 7609458..b8f6cd7 100644 --- a/src/utils/output_predicates.rs +++ b/src/utils/output_predicates.rs @@ -1,8 +1,8 @@ -pub(crate) fn formula_contains_predicate(formula: &foliage::Formula, - predicate_declaration: &foliage::PredicateDeclaration) +pub(crate) fn formula_contains_predicate(formula: &crate::Formula, + predicate_declaration: &crate::PredicateDeclaration) -> bool { - use foliage::Formula; + use crate::Formula; match formula { @@ -24,13 +24,10 @@ pub(crate) fn formula_contains_predicate(formula: &foliage::Formula, } } -fn replace_predicate_in_formula(formula: &mut foliage::Formula, - predicate_to_replace: &foliage::Predicate, replacement_formula: &foliage::Formula, - declarations: &D) -where - D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +fn replace_predicate_in_formula(formula: &mut crate::Formula, + predicate_to_replace: &crate::Predicate, replacement_formula: &crate::Formula) { - use foliage::{Formula, Term}; + use crate::{Formula, Term}; match formula { @@ -40,29 +37,27 @@ where for mut argument in arguments { replace_predicate_in_formula(&mut argument, predicate_to_replace, - replacement_formula, declarations); + replacement_formula); }, Formula::Boolean(_) | Formula::Compare(_) => (), Formula::Exists(quantified_expression) | Formula::ForAll(quantified_expression) => replace_predicate_in_formula(&mut quantified_expression.argument, predicate_to_replace, - replacement_formula, declarations), + replacement_formula), Formula::Implies(implies) => { replace_predicate_in_formula(&mut implies.antecedent, predicate_to_replace, - replacement_formula, declarations); + replacement_formula); replace_predicate_in_formula(&mut implies.implication, predicate_to_replace, - replacement_formula, declarations); + replacement_formula); }, Formula::Not(argument) => - replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula, - declarations), + replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula), Formula::Predicate(predicate) => if predicate.declaration == predicate_to_replace.declaration { - let mut replacement_formula = - crate::utils::copy_formula(replacement_formula, declarations); + let mut replacement_formula = crate::utils::copy_formula(replacement_formula); for (index, argument) in predicate.arguments.iter().enumerate() { @@ -81,49 +76,49 @@ where } } -pub(crate) fn replace_predicate_in_formula_with_completed_definition( - formula: &mut foliage::Formula, completed_definition: &foliage::Formula, declarations: &D) +pub(crate) fn replace_predicate_in_formula_with_completed_definition( + formula: &mut crate::Formula, completed_definition: &crate::Formula) -> Result<(), crate::Error> -where - D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, { - let false_ = foliage::Formula::false_(); + use crate::Formula; + + let false_ = crate::Formula::false_(); // TODO: refactor let (completed_definition_predicate, completed_definition) = match completed_definition { - foliage::Formula::ForAll(quantified_expression) => match *quantified_expression.argument + Formula::ForAll(quantified_expression) => match *quantified_expression.argument { - foliage::Formula::IfAndOnlyIf(ref arguments) => + Formula::IfAndOnlyIf(ref arguments) => { assert_eq!(arguments.len(), 2, "invalid completed definition"); match arguments[0] { - foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]), + Formula::Predicate(ref predicate) => (predicate, &arguments[1]), _ => panic!("invalid completed definition"), } }, - foliage::Formula::Not(ref argument) => match **argument + Formula::Not(ref argument) => match **argument { - foliage::Formula::Predicate(ref predicate) => (predicate, &false_), + Formula::Predicate(ref predicate) => (predicate, &false_), _ => panic!("invalid completed definition"), }, _ => panic!("invalid completed definition"), }, - foliage::Formula::IfAndOnlyIf(ref arguments) => + Formula::IfAndOnlyIf(ref arguments) => { assert_eq!(arguments.len(), 2, "invalid completed definition"); match arguments[0] { - foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]), + Formula::Predicate(ref predicate) => (predicate, &arguments[1]), _ => panic!("invalid completed definition"), } }, - foliage::Formula::Not(ref argument) => match **argument + Formula::Not(ref argument) => match **argument { - foliage::Formula::Predicate(ref predicate) => (predicate, &false_), + Formula::Predicate(ref predicate) => (predicate, &false_), _ => panic!("invalid completed definition"), }, _ => panic!("invalid completed definition"), @@ -139,8 +134,7 @@ where std::rc::Rc::clone(&completed_definition_predicate.declaration))); } - replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition, - declarations); + replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition); Ok(()) } diff --git a/src/utils/variables_in_terms.rs b/src/utils/variables_in_terms.rs index 73de49b..a93e4f1 100644 --- a/src/utils/variables_in_terms.rs +++ b/src/utils/variables_in_terms.rs @@ -1,8 +1,8 @@ -pub(crate) fn term_contains_variable(term: &foliage::Term, - variable_declaration: &foliage::VariableDeclaration) +pub(crate) fn term_contains_variable(term: &crate::Term, + variable_declaration: &crate::VariableDeclaration) -> bool { - use foliage::Term; + use crate::Term; match term {