diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 4c5a847..b9cc8df 100644 --- a/src/output/tptp.rs +++ b/src/output/tptp.rs @@ -1,53 +1,31 @@ -pub(crate) struct VariableDeclarationDisplay<'a> +pub(crate) struct DomainDisplay { - variable_declaration: &'a foliage::VariableDeclaration, + domain: crate::translate::common::Domain, } -pub(crate) struct TermDisplay<'a> +pub(crate) fn display_domain(domain: crate::translate::common::Domain) -> DomainDisplay { - term: &'a foliage::Term, -} - -pub(crate) struct FormulaDisplay<'a> -{ - formula: &'a foliage::Formula, -} - -pub(crate) fn display_variable_declaration<'a>(variable_declaration: &'a foliage::VariableDeclaration) - -> VariableDeclarationDisplay<'a> -{ - VariableDeclarationDisplay + DomainDisplay { - variable_declaration, + domain, } } -pub(crate) fn display_term<'a>(term: &'a foliage::Term) -> TermDisplay<'a> -{ - TermDisplay - { - term, - } -} - -pub(crate) fn display_formula<'a>(formula: &'a foliage::Formula) - -> FormulaDisplay<'a> -{ - FormulaDisplay - { - formula, - } -} - -impl<'a> std::fmt::Debug for VariableDeclarationDisplay<'a> +impl std::fmt::Debug for DomainDisplay { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", &self.variable_declaration.name) + let domain_name = match self.domain + { + crate::translate::common::Domain::Integer => "$int", + crate::translate::common::Domain::Program => "object", + }; + + write!(format, "{}", domain_name) } } -impl<'a> std::fmt::Display for VariableDeclarationDisplay<'a> +impl std::fmt::Display for DomainDisplay { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -55,10 +33,107 @@ impl<'a> std::fmt::Display for VariableDeclarationDisplay<'a> } } -impl<'a> std::fmt::Debug for TermDisplay<'a> +pub(crate) struct VariableDeclarationDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID +{ + variable_declaration: &'a std::rc::Rc, + context: &'b C, +} + +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::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID +{ + VariableDeclarationDisplay + { + variable_declaration, + context, + } +} + +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::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID +{ + TermDisplay + { + term, + context, + } +} + +pub(crate) struct FormulaDisplay<'a, 'b, C> +{ + formula: &'a foliage::Formula, + context: &'b C, +} + +pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, context: &'b C) + -> FormulaDisplay<'a, 'b, C> +{ + FormulaDisplay + { + formula, + context, + } +} + +impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID { fn fmt(&self, format: &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::translate::common::Domain::Integer => "N", + crate::translate::common::Domain::Program => "X", + }; + + write!(format, "{}{}", prefix, id + 1) + } +} + +impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + +impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID +{ + fn fmt(&self, format: &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); + match &self.term { foliage::Term::Boolean(true) => write!(format, "$true"), @@ -119,7 +194,10 @@ impl<'a> std::fmt::Debug for TermDisplay<'a> } } -impl<'term> std::fmt::Display for TermDisplay<'term> +impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -127,10 +205,18 @@ impl<'term> std::fmt::Display for TermDisplay<'term> } } -impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> +impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID { fn fmt(&self, format: &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); + match &self.formula { foliage::Formula::Exists(exists) => @@ -141,7 +227,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for parameter in exists.parameters.iter() { - write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; + let parameter_domain = self.context.variable_declaration_domain(parameter) + .expect("unspecified variable domain"); + + write!(format, "{}{:?}: {}", separator, display_variable_declaration(parameter), + display_domain(parameter_domain))?; separator = ", " } @@ -156,7 +246,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for parameter in for_all.parameters.iter() { - write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; + let parameter_domain = self.context.variable_declaration_domain(parameter) + .expect("unspecified variable domain"); + + write!(format, "{}{:?}: {}", separator, display_variable_declaration(parameter), + display_domain(parameter_domain))?; separator = ", " } @@ -199,7 +293,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> write!(format, ")")?; }, foliage::Formula::Implies(foliage::Implies{antecedent, implication}) - => write!(format, "({:?} => {:?})", display_formula(antecedent), display_formula(implication))?, + => write!(format, "({:?} => {:?})", display_formula(antecedent), + display_formula(implication))?, foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right}) => write!(format, "({:?} <=> {:?})", display_formula(left), display_formula(right))?, foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right}) @@ -242,7 +337,10 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> } } -impl<'formula> std::fmt::Display for FormulaDisplay<'formula> +impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C> +where + C: crate::translate::common::VariableDeclarationDomain + + crate::translate::common::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/translate.rs b/src/translate.rs index 854878b..2375987 100644 --- a/src/translate.rs +++ b/src/translate.rs @@ -1,2 +1,2 @@ -mod common; +pub(crate) mod common; pub mod verify_properties; diff --git a/src/translate/common.rs b/src/translate/common.rs index 050fe8f..1619f1f 100644 --- a/src/translate/common.rs +++ b/src/translate/common.rs @@ -1,89 +1,46 @@ -pub(crate) trait FindOrCreateFunctionDeclaration +#[derive(Clone, Copy, Debug, PartialEq)] +pub(crate) enum Domain { - fn find_or_create(&mut self, name: &str, arity: usize) + Program, + Integer, +} + +pub(crate) trait AssignVariableDeclarationDomain +{ + fn assign_variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc, domain: 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; +} + +pub(crate) trait GetOrCreateFunctionDeclaration +{ + fn get_or_create_function_declaration(&self, name: &str, arity: usize) -> std::rc::Rc; } -pub(crate) trait FindOrCreatePredicateDeclaration +pub(crate) trait GetOrCreatePredicateDeclaration { - fn find_or_create(&mut self, name: &str, arity: usize) + fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) -> std::rc::Rc; } -pub(crate) trait FindOrCreateVariableDeclaration +pub(crate) trait GetOrCreateVariableDeclaration { - fn find_or_create(&mut self, name: &str) + fn get_or_create_variable_declaration(&self, name: &str) -> std::rc::Rc; } -impl FindOrCreateFunctionDeclaration for foliage::FunctionDeclarations -{ - fn find_or_create(&mut self, name: &str, arity: usize) - -> std::rc::Rc - { - match self.iter() - .find(|x| x.name == name && x.arity == arity) - { - Some(value) => std::rc::Rc::clone(value), - None => - { - let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new( - name.to_string(), arity)); - - self.insert(std::rc::Rc::clone(&declaration)); - - log::debug!("new function declaration: {}/{}", name, arity); - - declaration - }, - } - } -} - -impl FindOrCreatePredicateDeclaration for foliage::PredicateDeclarations -{ - fn find_or_create(&mut self, name: &str, arity: usize) - -> std::rc::Rc - { - match self.iter() - .find(|x| x.name == name && x.arity == arity) - { - Some(value) => std::rc::Rc::clone(value), - None => - { - let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new( - name.to_string(), arity)); - - self.insert(std::rc::Rc::clone(&declaration)); - - log::debug!("new predicate declaration: {}/{}", name, arity); - - declaration - }, - } - } -} - -impl FindOrCreateVariableDeclaration for foliage::VariableDeclarationStack -{ - fn find_or_create(&mut self, name: &str) - -> std::rc::Rc - { - // TODO: check correctness - if name == "_" - { - let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new( - "_".to_owned())); - - self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration)); - - return variable_declaration; - } - - self.find_or_create(name) - } -} - pub(crate) fn translate_binary_operator(binary_operator: clingo::ast::BinaryOperator) -> Result { @@ -137,11 +94,13 @@ pub(crate) fn choose_value_in_primitive(term: Box, foliage::Formula::equal(Box::new(variable), term) } -pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, - variable_declaration: &std::rc::Rc, - mut function_declarations: &mut foliage::FunctionDeclarations, - mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) +pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, + variable_declaration: &std::rc::Rc, context: &C) -> Result +where + C: crate::translate::common::GetOrCreateFunctionDeclaration + + crate::translate::common::GetOrCreateVariableDeclaration + + crate::translate::common::AssignVariableDeclarationDomain { match term.term_type() { @@ -176,7 +135,7 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, let constant_name = symbol.name() .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; - let constant_declaration = function_declarations.find_or_create(constant_name, 0); + let constant_declaration = context.get_or_create_function_declaration(constant_name, 0); let function = foliage::Term::function(&constant_declaration, vec![]); Ok(choose_value_in_primitive(Box::new(function), variable_declaration)) @@ -184,7 +143,10 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, }, clingo::ast::TermType::Variable(variable_name) => { - let other_variable_declaration = variable_declaration_stack.find_or_create(variable_name); + let other_variable_declaration = context.get_or_create_variable_declaration( + variable_name); + context.assign_variable_declaration_domain(&other_variable_declaration, + Domain::Program); let other_variable = foliage::Term::variable(&other_variable_declaration); Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration)) @@ -201,8 +163,14 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, | foliage::BinaryOperator::Multiply => { - let parameters = (0..2).map(|_| std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string()))) + let parameters = (0..2).map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + context.assign_variable_declaration_domain(&variable_declaration, + Domain::Integer); + variable_declaration + }) .collect::(); let parameters = std::rc::Rc::new(parameters); @@ -218,12 +186,10 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, Box::new(translated_binary_operation)); let choose_value_from_left_argument = choose_value_in_term( - binary_operation.left(), ¶meter_1, &mut function_declarations, - &mut variable_declaration_stack)?; + binary_operation.left(), ¶meter_1, context)?; let choose_value_from_right_argument = choose_value_in_term( - binary_operation.right(), ¶meter_2, &mut function_declarations, - &mut variable_declaration_stack)?; + binary_operation.right(), ¶meter_2, context)?; let and = foliage::Formula::And(vec![Box::new(equals), Box::new(choose_value_from_left_argument), @@ -235,8 +201,14 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, | foliage::BinaryOperator::Modulo => { - let parameters = (0..4).map(|_| std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string()))) + let parameters = (0..4).map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + context.assign_variable_declaration_domain(&variable_declaration, + Domain::Integer); + variable_declaration + }) .collect::(); let parameters = std::rc::Rc::new(parameters); @@ -256,10 +228,10 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, Box::new(foliage::Term::variable(parameter_j)), Box::new(j_times_q_plus_r)); let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i, - &mut function_declarations, &mut variable_declaration_stack)?; + context)?; let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j, - &mut function_declarations, &mut variable_declaration_stack)?; + context)?; let j_not_equal_to_0 = foliage::Formula::not_equal( Box::new(foliage::Term::variable(parameter_j)), @@ -295,7 +267,8 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, Ok(foliage::Formula::exists(parameters, Box::new(and))) }, - _ => Err(crate::Error::new_not_yet_implemented("todo")), + foliage::BinaryOperator::Exponentiate => + Err(crate::Error::new_unsupported_language_feature("exponentiation")), } }, clingo::ast::TermType::UnaryOperation(unary_operation) => @@ -308,6 +281,7 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, { let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new( "".to_string())); + context.assign_variable_declaration_domain(¶meter_z_prime, Domain::Integer); let negative_z_prime = foliage::Term::negative(Box::new( foliage::Term::variable(¶meter_z_prime))); @@ -316,8 +290,7 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, Box::new(negative_z_prime)); let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(), - ¶meter_z_prime, &mut function_declarations, - &mut variable_declaration_stack)?; + ¶meter_z_prime, context)?; let and = foliage::Formula::and(vec![Box::new(equals), Box::new(choose_z_prime_in_t_prime)]); @@ -331,8 +304,14 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, }, clingo::ast::TermType::Interval(interval) => { - let parameters = (0..3).map(|_| std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string()))) + let parameters = (0..3).map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + context.assign_variable_declaration_domain(&variable_declaration, + Domain::Integer); + variable_declaration + }) .collect::(); let parameters = std::rc::Rc::new(parameters); @@ -340,11 +319,9 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, let parameter_j = ¶meters[1]; let parameter_k = ¶meters[2]; - let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i, - &mut function_declarations, &mut variable_declaration_stack)?; + let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i, context)?; - let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, - &mut function_declarations, &mut variable_declaration_stack)?; + let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, context)?; let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal( Box::new(foliage::Term::variable(parameter_i)), diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 5a85bab..7dbee6c 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -3,6 +3,7 @@ mod translate_body; use head_type::*; use translate_body::*; +use crate::translate::common::AssignVariableDeclarationDomain as _; struct ScopedFormula { @@ -16,14 +17,24 @@ struct Definitions definitions: Vec, } +type VariableDeclarationDomains + = std::collections::BTreeMap, + crate::translate::common::Domain>; + +type VariableDeclarationIDs + = std::collections::BTreeMap::, usize>; + struct Context { - pub definitions: std::collections::BTreeMap::, Definitions>, - pub integrity_constraints: foliage::Formulas, + pub definitions: std::cell::RefCell, + Definitions>>, + pub integrity_constraints: std::cell::RefCell, - pub function_declarations: foliage::FunctionDeclarations, - pub predicate_declarations: foliage::PredicateDeclarations, - pub variable_declaration_stack: foliage::VariableDeclarationStack, + pub function_declarations: std::cell::RefCell, + pub predicate_declarations: std::cell::RefCell, + pub variable_declaration_stack: std::cell::RefCell, + pub variable_declaration_domains: std::cell::RefCell, + pub variable_declaration_ids: std::cell::RefCell, } impl Context @@ -32,11 +43,149 @@ impl Context { Self { - definitions: std::collections::BTreeMap::<_, _>::new(), - integrity_constraints: vec![], - function_declarations: foliage::FunctionDeclarations::new(), - predicate_declarations: foliage::PredicateDeclarations::new(), - variable_declaration_stack: foliage::VariableDeclarationStack::new(), + definitions: std::cell::RefCell::new(std::collections::BTreeMap::<_, _>::new()), + integrity_constraints: std::cell::RefCell::new(vec![]), + + function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()), + predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()), + variable_declaration_stack: std::cell::RefCell::new(foliage::VariableDeclarationStack::new()), + variable_declaration_domains: std::cell::RefCell::new(VariableDeclarationDomains::new()), + variable_declaration_ids: std::cell::RefCell::new(VariableDeclarationIDs::new()), + } + } +} + +impl crate::translate::common::GetOrCreateFunctionDeclaration for Context +{ + fn get_or_create_function_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc + { + let mut function_declarations = self.function_declarations.borrow_mut(); + + match function_declarations.iter() + .find(|x| x.name == name && x.arity == arity) + { + Some(value) => std::rc::Rc::clone(value), + None => + { + let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new( + name.to_string(), arity)); + + function_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new function declaration: {}/{}", name, arity); + + declaration + }, + } + } +} + +impl crate::translate::common::GetOrCreatePredicateDeclaration for Context +{ + fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc + { + let mut predicate_declarations = self.predicate_declarations.borrow_mut(); + + match predicate_declarations.iter() + .find(|x| x.name == name && x.arity == arity) + { + Some(value) => std::rc::Rc::clone(value), + None => + { + let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new( + name.to_string(), arity)); + + predicate_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new predicate declaration: {}/{}", name, arity); + + declaration + }, + } + } +} + +impl crate::translate::common::GetOrCreateVariableDeclaration for Context +{ + fn get_or_create_variable_declaration(&self, name: &str) + -> std::rc::Rc + { + let mut variable_declaration_stack = self.variable_declaration_stack.borrow_mut(); + + // TODO: check correctness + if name == "_" + { + let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new( + "_".to_owned())); + + variable_declaration_stack.free_variable_declarations.push( + std::rc::Rc::clone(&variable_declaration)); + + return variable_declaration; + } + + variable_declaration_stack.find_or_create(name) + } +} + +impl crate::translate::common::AssignVariableDeclarationDomain for Context +{ + fn assign_variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc, + domain: crate::translate::common::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::translate::common::VariableDeclarationDomain for Context +{ + fn variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc) + -> Option + { + let variable_declaration_domains = self.variable_declaration_domains.borrow(); + + variable_declaration_domains.get(variable_declaration) + .map(|x| *x) + } +} + +impl crate::translate::common::VariableDeclarationID for Context +{ + fn variable_declaration_id(&self, + variable_declaration: &std::rc::Rc) + -> usize + { + let mut variable_declaration_ids = self.variable_declaration_ids.borrow_mut(); + + match variable_declaration_ids.get(variable_declaration) + { + Some(id) => + { + //log::trace!("{:p} → {} (already known)", *variable_declaration, id); + *id + } + None => + { + let id = variable_declaration_ids.len(); + variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); + //log::trace!("{:p} → {} (new)", *variable_declaration, id); + id + }, } } } @@ -104,11 +253,8 @@ where } let context = statement_handler.context; - let mut definitions = context.definitions; - let integrity_constraints = context.integrity_constraints; - let predicate_declarations = context.predicate_declarations; - for (predicate_declaration, definitions) in definitions.iter() + for (predicate_declaration, definitions) in context.definitions.borrow().iter() { for definition in definitions.definitions.iter() { @@ -117,9 +263,9 @@ where } } - let mut completed_definition = |predicate_declaration| + let completed_definition = |predicate_declaration| { - match definitions.remove(predicate_declaration) + match context.definitions.borrow_mut().remove(predicate_declaration) { // This predicate symbol has at least one definition, so build the disjunction of those Some(definitions) => @@ -151,7 +297,14 @@ where None => { let head_atom_parameters = std::rc::Rc::new((0..predicate_declaration.arity) - .map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new("".to_string()))) + .map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + context.assign_variable_declaration_domain(&variable_declaration, + crate::translate::common::Domain::Program); + variable_declaration + }) .collect::>()); let head_arguments = head_atom_parameters.iter() @@ -174,6 +327,7 @@ where } }; + let predicate_declarations = context.predicate_declarations.borrow(); let completed_definitions = predicate_declarations.iter() .map(|x| (std::rc::Rc::clone(x), completed_definition(x))); @@ -181,37 +335,43 @@ where { println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name, predicate_declaration.arity, - crate::output::tptp::display_formula(&completed_definition)); + crate::output::tptp::display_formula(&completed_definition, &context)); } - for integrity_constraint in integrity_constraints + for integrity_constraint in context.integrity_constraints.borrow().iter() { println!("tff(integrity_constraint, axiom, {}).", - crate::output::tptp::display_formula(&integrity_constraint)); + crate::output::tptp::display_formula(&integrity_constraint, &context)); } Ok(()) } -fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate::Error> +fn read_rule(rule: &clingo::ast::Rule, context: &Context) + -> Result<(), crate::Error> { - use super::common::FindOrCreatePredicateDeclaration; - - let head_type = determine_head_type(rule.head(), - |name, arity| context.predicate_declarations.find_or_create(name, arity))?; + let head_type = determine_head_type(rule.head(), context)?; match &head_type { HeadType::SingleAtom(head_atom) | HeadType::ChoiceWithSingleAtom(head_atom) => { - if !context.definitions.contains_key(&head_atom.predicate_declaration) + if !context.definitions.borrow().contains_key(&head_atom.predicate_declaration) { let head_atom_parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity) - .map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new("".to_string()))) + .map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + context.assign_variable_declaration_domain(&variable_declaration, + crate::translate::common::Domain::Program); + variable_declaration + }) .collect()); - context.definitions.insert(std::rc::Rc::clone(&head_atom.predicate_declaration), + context.definitions.borrow_mut().insert( + std::rc::Rc::clone(&head_atom.predicate_declaration), Definitions { head_atom_parameters, @@ -219,14 +379,13 @@ fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crat }); } - let definitions = context.definitions.get_mut(&head_atom.predicate_declaration).unwrap(); + let mut definitions = context.definitions.borrow_mut(); + let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap(); - context.variable_declaration_stack.push(std::rc::Rc::clone( - &definitions.head_atom_parameters)); + let head_atom_parameters = std::rc::Rc::clone(&definitions.head_atom_parameters); + context.variable_declaration_stack.borrow_mut().push(head_atom_parameters); - let mut definition_arguments = translate_body(rule.body(), - &mut context.function_declarations, &mut context.predicate_declarations, - &mut context.variable_declaration_stack)?; + let mut definition_arguments = translate_body(rule.body(), context)?; assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len()); @@ -249,17 +408,17 @@ fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crat let head_atom_argument = head_atom_arguments_iterator.next().unwrap(); let translated_head_term = crate::translate::common::choose_value_in_term( - head_atom_argument, head_atom_parameter, &mut context.function_declarations, - &mut context.variable_declaration_stack)?; + head_atom_argument, head_atom_parameter, context)?; definition_arguments.push(Box::new(translated_head_term)); } - context.variable_declaration_stack.pop(); + context.variable_declaration_stack.borrow_mut().pop(); let mut free_variable_declarations = vec![]; - std::mem::swap(&mut context.variable_declaration_stack.free_variable_declarations, + std::mem::swap( + &mut context.variable_declaration_stack.borrow_mut().free_variable_declarations, &mut free_variable_declarations); let definition = match definition_arguments.len() @@ -281,13 +440,12 @@ fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crat }, HeadType::IntegrityConstraint => { - let mut arguments = translate_body(rule.body(), - &mut context.function_declarations, &mut context.predicate_declarations, - &mut context.variable_declaration_stack)?; + let mut arguments = translate_body(rule.body(), context)?; let mut free_variable_declarations = vec![]; - std::mem::swap(&mut context.variable_declaration_stack.free_variable_declarations, + std::mem::swap( + &mut context.variable_declaration_stack.borrow_mut().free_variable_declarations, &mut free_variable_declarations); let formula = match arguments.len() @@ -307,7 +465,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crat log::debug!("translated integrity constraint: {:?}", integrity_constraint); - context.integrity_constraints.push(integrity_constraint); + context.integrity_constraints.borrow_mut().push(integrity_constraint); }, HeadType::Trivial => log::info!("skipping trivial rule"), } diff --git a/src/translate/verify_properties/head_type.rs b/src/translate/verify_properties/head_type.rs index d08843d..c687f35 100644 --- a/src/translate/verify_properties/head_type.rs +++ b/src/translate/verify_properties/head_type.rs @@ -12,19 +12,18 @@ pub(crate) enum HeadType<'a> Trivial, } -pub(crate) fn determine_head_type<'a, F>(head_literal: &'a clingo::ast::HeadLiteral, - mut find_or_create_predicate_declaration: F) +pub(crate) fn determine_head_type<'a, C>(head_literal: &'a clingo::ast::HeadLiteral, context: &C) -> Result, crate::Error> where - F: FnMut(&str, usize) -> std::rc::Rc + C: crate::translate::common::GetOrCreatePredicateDeclaration { - let mut create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error> + let create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error> { let function_name = function.name() .map_err(|error| crate::Error::new_decode_identifier(error))?; - let predicate_declaration - = find_or_create_predicate_declaration(function_name, function.arguments().len()); + let predicate_declaration = context.get_or_create_predicate_declaration(function_name, + function.arguments().len()); Ok(HeadAtom { diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 0f9a2dd..db66fbd 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,11 +1,12 @@ -pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, - mut function_declarations: &mut foliage::FunctionDeclarations, - predicate_declarations: &mut foliage::PredicateDeclarations, - mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) +pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, + context: &C) -> Result +where + C: crate::translate::common::GetOrCreateVariableDeclaration + + crate::translate::common::GetOrCreateFunctionDeclaration + + crate::translate::common::GetOrCreatePredicateDeclaration + + crate::translate::common::AssignVariableDeclarationDomain { - use crate::translate::common::FindOrCreatePredicateDeclaration; - let function = match body_term.term_type() { clingo::ast::TermType::Function(value) => value, @@ -14,11 +15,17 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a let function_name = function.name().map_err(|error| crate::Error::new_decode_identifier(error))?; - let predicate_declaration = predicate_declarations.find_or_create(function_name, + let predicate_declaration = context.get_or_create_predicate_declaration(function_name, function.arguments().len()); - let parameters = function.arguments().iter().map(|_| std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string()))) + 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::translate::common::Domain::Program); + variable_declaration + }) .collect::(); let parameters = std::rc::Rc::new(parameters); @@ -47,7 +54,7 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a let mut parameters_iterator = parameters.iter(); let mut arguments = function.arguments().iter().map( |x| crate::translate::common::choose_value_in_term(x, ¶meters_iterator.next().unwrap(), - &mut function_declarations, &mut variable_declaration_stack) + context) .map(|x| Box::new(x))) .collect::, _>>()?; @@ -58,11 +65,14 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a Ok(foliage::Formula::exists(parameters, Box::new(and))) } -pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, - mut function_declarations: &mut foliage::FunctionDeclarations, - mut predicate_declarations: &mut foliage::PredicateDeclarations, - mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) +pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, + context: &C) -> Result +where + C: crate::translate::common::GetOrCreateVariableDeclaration + + crate::translate::common::GetOrCreateFunctionDeclaration + + crate::translate::common::GetOrCreatePredicateDeclaration + + crate::translate::common::AssignVariableDeclarationDomain { match body_literal.sign() { @@ -91,12 +101,17 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, Ok(foliage::Formula::Boolean(value)) }, clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), - &mut function_declarations, &mut predicate_declarations, - &mut variable_declaration_stack), + context), clingo::ast::LiteralType::Comparison(comparison) => { - let parameters = (0..2).map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new( - "".to_string()))) + 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::translate::common::Domain::Program); + variable_declaration + }) .collect::(); let parameters = std::rc::Rc::new(parameters); @@ -105,9 +120,9 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, let parameter_z2 = ¶meters_iterator.next().unwrap(); let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), - parameter_z1, &mut function_declarations, &mut variable_declaration_stack)?; + parameter_z1, context)?; let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), - parameter_z2, &mut function_declarations, &mut variable_declaration_stack)?; + parameter_z2, context)?; let variable_1 = foliage::Term::variable(parameter_z1); let variable_2 = foliage::Term::variable(parameter_z2); @@ -128,15 +143,17 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, } } -pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], - mut function_declaration: &mut foliage::FunctionDeclarations, - mut predicate_declaration: &mut foliage::PredicateDeclarations, - mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) +pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], + context: &C) -> Result +where + C: crate::translate::common::GetOrCreateVariableDeclaration + + crate::translate::common::GetOrCreateFunctionDeclaration + + crate::translate::common::GetOrCreatePredicateDeclaration + + crate::translate::common::AssignVariableDeclarationDomain { body_literals.iter() - .map(|body_literal| translate_body_literal(body_literal, &mut function_declaration, - &mut predicate_declaration, &mut variable_declaration_stack) + .map(|body_literal| translate_body_literal(body_literal, context) .map(|value| Box::new(value))) .collect::>() }