diff --git a/Cargo.toml b/Cargo.toml index 9be6a3f..f282b0e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ authors = ["Patrick Lühne "] edition = "2018" [dependencies] -foliage = {git = "https://github.com/pluehne/foliage", branch = "master"} +foliage = {git = "https://github.com/pluehne/foliage", branch = "parser"} log = "0.4" pretty_env_logger = "0.4" structopt = "0.3" diff --git a/src/traits.rs b/src/traits.rs index d31034f..9409c77 100644 --- a/src/traits.rs +++ b/src/traits.rs @@ -33,9 +33,3 @@ pub(crate) trait GetOrCreatePredicateDeclaration fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) -> std::rc::Rc; } - -pub(crate) trait GetOrCreateVariableDeclaration -{ - fn get_or_create_variable_declaration(&self, name: &str) - -> std::rc::Rc; -} diff --git a/src/translate/common/choose_value_in_term.rs b/src/translate/common/choose_value_in_term.rs index 0f55a3d..14aea4e 100644 --- a/src/translate/common/choose_value_in_term.rs +++ b/src/translate/common/choose_value_in_term.rs @@ -8,11 +8,11 @@ pub(crate) fn choose_value_in_primitive(term: Box, } pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, - variable_declaration: std::rc::Rc, context: &C) + variable_declaration: std::rc::Rc, context: &C, + variable_declaration_stack: &foliage::VariableDeclarationStackLayer) -> Result where C: crate::traits::GetOrCreateFunctionDeclaration - + crate::traits::GetOrCreateVariableDeclaration + crate::traits::AssignVariableDeclarationDomain { match term.term_type() @@ -58,8 +58,23 @@ where }, clingo::ast::TermType::Variable(variable_name) => { - let other_variable_declaration = context.get_or_create_variable_declaration( - variable_name); + 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| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("_".to_owned())); + + free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration)); + + variable_declaration + }), + _ => 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); @@ -100,10 +115,12 @@ where Box::new(translated_binary_operation)); let choose_value_from_left_argument = choose_value_in_term( - binary_operation.left(), std::rc::Rc::clone(¶meter_1), context)?; + binary_operation.left(), std::rc::Rc::clone(¶meter_1), context, + variable_declaration_stack)?; let choose_value_from_right_argument = choose_value_in_term( - binary_operation.right(), std::rc::Rc::clone(¶meter_2), context)?; + 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, choose_value_from_right_argument]); @@ -142,10 +159,10 @@ where Box::new(j_times_q_plus_r)); let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), - std::rc::Rc::clone(parameter_i), context)?; + std::rc::Rc::clone(parameter_i), context, variable_declaration_stack)?; let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), - std::rc::Rc::clone(parameter_j), context)?; + 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))), @@ -205,7 +222,8 @@ where 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)?; + std::rc::Rc::clone(¶meter_z_prime), context, + variable_declaration_stack)?; let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]); @@ -234,10 +252,10 @@ where let parameter_k = ¶meters[2]; let choose_i_in_t_1 = choose_value_in_term(interval.left(), - std::rc::Rc::clone(parameter_i), context)?; + std::rc::Rc::clone(parameter_i), context, variable_declaration_stack)?; let choose_j_in_t_2 = choose_value_in_term(interval.right(), - std::rc::Rc::clone(parameter_j), context)?; + 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))), diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 44675fc..61eadc2 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -333,11 +333,6 @@ where fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::Error> { - if !context.variable_declaration_stack.borrow().is_empty() - { - return Err(crate::Error::new_logic("variable declaration stack in unexpected state")); - } - let head_type = determine_head_type(rule.head(), context)?; match &head_type @@ -371,10 +366,14 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap(); let head_atom_parameters = std::rc::Rc::clone(&definitions.head_atom_parameters); - let variable_declaration_stack_guard = foliage::VariableDeclarationStack::push( - &context.variable_declaration_stack, head_atom_parameters); + let free_variable_declarations = std::cell::RefCell::new(vec![]); + let free_layer = + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); + let head_atom_parameters_layer = foliage::VariableDeclarationStackLayer::bound( + &free_layer, head_atom_parameters); - let mut definition_arguments = translate_body(rule.body(), context)?; + let mut definition_arguments = translate_body(rule.body(), context, + &head_atom_parameters_layer)?; assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len()); @@ -397,16 +396,19 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let head_atom_argument = head_atom_arguments_iterator.next().unwrap(); let translated_head_term = crate::translate::common::choose_value_in_term( - head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context)?; + head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context, + &head_atom_parameters_layer)?; definition_arguments.push(translated_head_term); } - drop(variable_declaration_stack_guard); - - let free_variable_declarations = std::mem::replace( - &mut context.variable_declaration_stack.borrow_mut().free_variable_declarations, - vec![]); + // TODO: refactor + let free_variable_declarations = match free_layer + { + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + => free_variable_declarations.into_inner(), + _ => unreachable!(), + }; let definition = match definition_arguments.len() { @@ -428,11 +430,19 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E }, HeadType::IntegrityConstraint => { - let mut arguments = translate_body(rule.body(), context)?; + let free_variable_declarations = std::cell::RefCell::new(vec![]); + let free_layer = + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); - let free_variable_declarations = std::mem::replace( - &mut context.variable_declaration_stack.borrow_mut().free_variable_declarations, - vec![]); + let mut arguments = translate_body(rule.body(), context, &free_layer)?; + + // TODO: refactor + let free_variable_declarations = match free_layer + { + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + => free_variable_declarations.into_inner(), + _ => unreachable!(), + }; let formula = match arguments.len() { diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index a0a9a80..6300221 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -22,7 +22,6 @@ pub(crate) struct Context 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 program_variable_declaration_ids: std::cell::RefCell, pub integer_variable_declaration_ids: std::cell::RefCell, @@ -44,8 +43,6 @@ impl Context 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()), program_variable_declaration_ids: @@ -121,29 +118,6 @@ impl crate::traits::GetOrCreatePredicateDeclaration for Context } } -impl crate::traits::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::traits::AssignVariableDeclarationDomain for Context { fn assign_variable_declaration_domain(&self, diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 860d4c7..dbb358a 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,9 +1,8 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, - context: &C) + context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer) -> Result where - C: crate::traits::GetOrCreateVariableDeclaration - + crate::traits::GetOrCreateFunctionDeclaration + C: crate::traits::GetOrCreateFunctionDeclaration + crate::traits::GetOrCreatePredicateDeclaration + crate::traits::AssignVariableDeclarationDomain { @@ -54,7 +53,8 @@ where let mut parameters_iterator = parameters.iter(); let mut arguments = function.arguments().iter().map( |x| crate::translate::common::choose_value_in_term(x, - std::rc::Rc::clone(¶meters_iterator.next().unwrap()), context)) + std::rc::Rc::clone(¶meters_iterator.next().unwrap()), context, + variable_declaration_stack)) .collect::, _>>()?; arguments.push(predicate_literal); @@ -65,11 +65,10 @@ where } pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, - context: &C) + context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer) -> Result where - C: crate::traits::GetOrCreateVariableDeclaration - + crate::traits::GetOrCreateFunctionDeclaration + C: crate::traits::GetOrCreateFunctionDeclaration + crate::traits::GetOrCreatePredicateDeclaration + crate::traits::AssignVariableDeclarationDomain { @@ -100,7 +99,7 @@ where Ok(foliage::Formula::Boolean(value)) }, clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), - context), + context, variable_declaration_stack), clingo::ast::LiteralType::Comparison(comparison) => { let parameters = (0..2).map(|_| @@ -119,9 +118,9 @@ where let parameter_z2 = ¶meters_iterator.next().unwrap(); let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), - std::rc::Rc::clone(parameter_z1), context)?; + std::rc::Rc::clone(parameter_z1), context, variable_declaration_stack)?; let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), - std::rc::Rc::clone(parameter_z2), context)?; + 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)); @@ -142,16 +141,16 @@ where } } -pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], - context: &C) +pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &C, + variable_declaration_stack: &foliage::VariableDeclarationStackLayer) -> Result where - C: crate::traits::GetOrCreateVariableDeclaration - + crate::traits::GetOrCreateFunctionDeclaration + C: crate::traits::GetOrCreateFunctionDeclaration + crate::traits::GetOrCreatePredicateDeclaration + crate::traits::AssignVariableDeclarationDomain { body_literals.iter() - .map(|body_literal| translate_body_literal(body_literal, context)) + .map(|body_literal| translate_body_literal(body_literal, context, + variable_declaration_stack)) .collect::>() }