From 81ddfd450aac3e301f2660258de9d032d637594c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 22 May 2020 02:25:00 +0200 Subject: [PATCH] Use custom foliage flavor With this patch, properties specific to variable, function, and predicate declarations are directly stored within those objects rather than external maps that need to be queried via traits. This greatly simplifies many parts of the logic. This is made possible by implementing a custom foliage flavor, which makes it possible to swap the built-in declaration types for extended versions of those types that fulfill certain requirements. --- src/ast.rs | 361 ++++++++++++++++++ src/error.rs | 40 +- src/input/specification.rs | 128 +------ src/lib.rs | 3 +- src/output/tptp.rs | 257 ++++--------- src/problem.rs | 311 +++------------ src/problem/statement.rs | 8 +- src/simplify.rs | 20 +- src/traits.rs | 23 -- src/translate/common/choose_value_in_term.rs | 178 ++++----- src/translate/verify_properties.rs | 103 +++-- src/translate/verify_properties/head_type.rs | 4 +- .../verify_properties/translate_body.rs | 76 ++-- src/utils.rs | 2 + src/utils/arithmetic_terms.rs | 38 +- src/utils/autoname_variables.rs | 223 +++++++++++ src/utils/closures.rs | 8 +- src/utils/copy_formula.rs | 82 ++-- src/utils/output_predicates.rs | 60 ++- src/utils/variables_in_terms.rs | 6 +- 20 files changed, 1005 insertions(+), 926 deletions(-) create mode 100644 src/ast.rs delete mode 100644 src/traits.rs create mode 100644 src/utils/autoname_variables.rs 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 {