diff --git a/src/lib.rs b/src/lib.rs index c772c5c..256bbb3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -3,5 +3,7 @@ pub mod error; pub mod output; pub mod translate; +mod utils; pub use error::Error; +pub(crate) use utils::*; diff --git a/src/output/human_readable.rs b/src/output/human_readable.rs index 16b7f2b..eb761ea 100644 --- a/src/output/human_readable.rs +++ b/src/output/human_readable.rs @@ -137,8 +137,8 @@ where let prefix = match domain { - crate::translate::common::Domain::Integer => "N", - crate::translate::common::Domain::Program => "X", + crate::Domain::Integer => "N", + crate::Domain::Program => "X", }; write!(format, "{}{}", prefix, id + 1) diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 9555bf1..3324cce 100644 --- a/src/output/tptp.rs +++ b/src/output/tptp.rs @@ -1,9 +1,9 @@ pub(crate) struct DomainDisplay { - domain: crate::translate::common::Domain, + domain: crate::Domain, } -pub(crate) fn display_domain(domain: crate::translate::common::Domain) -> DomainDisplay +pub(crate) fn display_domain(domain: crate::Domain) -> DomainDisplay { DomainDisplay { @@ -17,8 +17,8 @@ impl std::fmt::Debug for DomainDisplay { let domain_name = match self.domain { - crate::translate::common::Domain::Integer => "$int", - crate::translate::common::Domain::Program => "object", + crate::Domain::Integer => "$int", + crate::Domain::Program => "object", }; write!(format, "{}", domain_name) @@ -107,8 +107,8 @@ where let prefix = match domain { - crate::translate::common::Domain::Integer => "N", - crate::translate::common::Domain::Program => "X", + crate::Domain::Integer => "N", + crate::Domain::Program => "X", }; write!(format, "{}{}", prefix, id + 1) diff --git a/src/translate/common.rs b/src/translate/common.rs index 1619f1f..fbdaea2 100644 --- a/src/translate/common.rs +++ b/src/translate/common.rs @@ -1,20 +1,17 @@ -#[derive(Clone, Copy, Debug, PartialEq)] -pub(crate) enum Domain -{ - Program, - Integer, -} +mod choose_value_in_term; + +pub(crate) use choose_value_in_term::*; pub(crate) trait AssignVariableDeclarationDomain { fn assign_variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc, domain: Domain); + variable_declaration: &std::rc::Rc, domain: crate::Domain); } pub(crate) trait VariableDeclarationDomain { fn variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc) -> Option; + variable_declaration: &std::rc::Rc) -> Option; } pub(crate) trait VariableDeclarationID @@ -84,268 +81,3 @@ pub(crate) fn translate_comparison_operator(comparison_operator: clingo::ast::Co => foliage::ComparisonOperator::Equal, } } - -pub(crate) fn choose_value_in_primitive(term: Box, - variable_declaration: &std::rc::Rc) - -> foliage::Formula -{ - let variable = foliage::Term::variable(variable_declaration); - - foliage::Formula::equal(Box::new(variable), term) -} - -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() - { - clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type() - .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() - .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)), - clingo::SymbolType::Supremum => Ok(choose_value_in_primitive( - Box::new(foliage::Term::supremum()), variable_declaration)), - clingo::SymbolType::String => Ok(choose_value_in_primitive( - Box::new(foliage::Term::string(symbol.string() - .map_err(|error| crate::Error::new_logic("clingo error").with(error))? - .to_string())), - variable_declaration)), - clingo::SymbolType::Function => - { - let arguments = symbol.arguments() - .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; - - // Functions with arguments are represented as clingo::ast::Function by the parser. - // At this point, we only have to handle (0-ary) constants - if !arguments.is_empty() - { - return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol")); - } - - let constant_name = symbol.name() - .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; - - 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)) - } - }, - clingo::ast::TermType::Variable(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)) - }, - clingo::ast::TermType::BinaryOperation(binary_operation) => - { - let operator = crate::translate::common::translate_binary_operator( - binary_operation.binary_operator())?; - - match operator - { - foliage::BinaryOperator::Add - | foliage::BinaryOperator::Subtract - | 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, - Domain::Integer); - variable_declaration - }) - .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(¶meter_1)), - Box::new(foliage::Term::variable(¶meter_2))); - - let equals = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(translated_binary_operation)); - - let choose_value_from_left_argument = choose_value_in_term( - binary_operation.left(), ¶meter_1, context)?; - - let choose_value_from_right_argument = choose_value_in_term( - binary_operation.right(), ¶meter_2, context)?; - - let and = foliage::Formula::And(vec![Box::new(equals), - Box::new(choose_value_from_left_argument), - Box::new(choose_value_from_right_argument)]); - - Ok(foliage::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, - Domain::Integer); - variable_declaration - }) - .collect::(); - let parameters = std::rc::Rc::new(parameters); - - let parameter_i = ¶meters[0]; - let parameter_j = ¶meters[1]; - let parameter_q = ¶meters[2]; - let parameter_r = ¶meters[3]; - - let j_times_q = foliage::Term::multiply( - Box::new(foliage::Term::variable(parameter_j)), - Box::new(foliage::Term::variable(parameter_q))); - - let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q), - Box::new(foliage::Term::variable(parameter_r))); - - let i_equals_j_times_q_plus_r = foliage::Formula::equal( - 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, - context)?; - - let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j, - context)?; - - let j_not_equal_to_0 = foliage::Formula::not_equal( - Box::new(foliage::Term::variable(parameter_j)), - Box::new(foliage::Term::integer(0))); - - let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal( - Box::new(foliage::Term::variable(parameter_r)), - Box::new(foliage::Term::integer(0))); - - let r_less_than_q = foliage::Formula::less( - Box::new(foliage::Term::variable(parameter_r)), - Box::new(foliage::Term::variable(parameter_q))); - - let z_equal_to_q = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(parameter_q))); - - let z_equal_to_r = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(parameter_r))); - - let last_argument = match operator - { - foliage::BinaryOperator::Divide => z_equal_to_q, - foliage::BinaryOperator::Modulo => z_equal_to_r, - _ => return Err(crate::Error::new_logic("unreachable code")), - }; - - let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r), - Box::new(choose_i_in_t1), Box::new(choose_i_in_t2), - Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0), - Box::new(r_less_than_q), Box::new(last_argument)]); - - Ok(foliage::Formula::exists(parameters, Box::new(and))) - }, - foliage::BinaryOperator::Exponentiate => - Err(crate::Error::new_unsupported_language_feature("exponentiation")), - } - }, - clingo::ast::TermType::UnaryOperation(unary_operation) => - { - match unary_operation.unary_operator() - { - clingo::ast::UnaryOperator::Absolute => - 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, Domain::Integer); - - let negative_z_prime = foliage::Term::negative(Box::new( - foliage::Term::variable(¶meter_z_prime))); - let equals = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(negative_z_prime)); - - let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(), - ¶meter_z_prime, context)?; - - let and = foliage::Formula::and(vec![Box::new(equals), - Box::new(choose_z_prime_in_t_prime)]); - - let parameters = std::rc::Rc::new(vec![parameter_z_prime]); - - Ok(foliage::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, - Domain::Integer); - variable_declaration - }) - .collect::(); - let parameters = std::rc::Rc::new(parameters); - - let parameter_i = ¶meters[0]; - let parameter_j = ¶meters[1]; - let parameter_k = ¶meters[2]; - - 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, context)?; - - let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal( - Box::new(foliage::Term::variable(parameter_i)), - Box::new(foliage::Term::variable(parameter_k))); - - let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal( - Box::new(foliage::Term::variable(parameter_k)), - Box::new(foliage::Term::variable(parameter_j))); - - let z_equals_k = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(parameter_k))); - - let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1), - Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k), - Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]); - - Ok(foliage::Formula::exists(parameters, Box::new(and))) - }, - clingo::ast::TermType::Function(_) => - Err(crate::Error::new_unsupported_language_feature("symbolic functions")), - clingo::ast::TermType::Pool(_) => - Err(crate::Error::new_unsupported_language_feature("pools")), - clingo::ast::TermType::ExternalFunction(_) => - Err(crate::Error::new_unsupported_language_feature("external functions")), - } -} diff --git a/src/translate/common/choose_value_in_term.rs b/src/translate/common/choose_value_in_term.rs new file mode 100644 index 0000000..8c7a0f2 --- /dev/null +++ b/src/translate/common/choose_value_in_term.rs @@ -0,0 +1,265 @@ +pub(crate) fn choose_value_in_primitive(term: Box, + variable_declaration: &std::rc::Rc) + -> foliage::Formula +{ + let variable = foliage::Term::variable(variable_declaration); + + foliage::Formula::equal(Box::new(variable), term) +} + +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() + { + clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type() + .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() + .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)), + clingo::SymbolType::Supremum => Ok(choose_value_in_primitive( + Box::new(foliage::Term::supremum()), variable_declaration)), + clingo::SymbolType::String => Ok(choose_value_in_primitive( + Box::new(foliage::Term::string(symbol.string() + .map_err(|error| crate::Error::new_logic("clingo error").with(error))? + .to_string())), + variable_declaration)), + clingo::SymbolType::Function => + { + let arguments = symbol.arguments() + .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; + + // Functions with arguments are represented as clingo::ast::Function by the parser. + // At this point, we only have to handle (0-ary) constants + if !arguments.is_empty() + { + return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol")); + } + + let constant_name = symbol.name() + .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; + + 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)) + } + }, + clingo::ast::TermType::Variable(variable_name) => + { + let other_variable_declaration = context.get_or_create_variable_declaration( + variable_name); + context.assign_variable_declaration_domain(&other_variable_declaration, + crate::Domain::Program); + let other_variable = foliage::Term::variable(&other_variable_declaration); + + Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration)) + }, + clingo::ast::TermType::BinaryOperation(binary_operation) => + { + let operator = crate::translate::common::translate_binary_operator( + binary_operation.binary_operator())?; + + match operator + { + foliage::BinaryOperator::Add + | foliage::BinaryOperator::Subtract + | 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 = 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(¶meter_1)), + Box::new(foliage::Term::variable(¶meter_2))); + + let equals = foliage::Formula::equal( + Box::new(foliage::Term::variable(variable_declaration)), + Box::new(translated_binary_operation)); + + let choose_value_from_left_argument = choose_value_in_term( + binary_operation.left(), ¶meter_1, context)?; + + let choose_value_from_right_argument = choose_value_in_term( + binary_operation.right(), ¶meter_2, context)?; + + let and = foliage::Formula::And(vec![Box::new(equals), + Box::new(choose_value_from_left_argument), + Box::new(choose_value_from_right_argument)]); + + Ok(foliage::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 = std::rc::Rc::new(parameters); + + let parameter_i = ¶meters[0]; + let parameter_j = ¶meters[1]; + let parameter_q = ¶meters[2]; + let parameter_r = ¶meters[3]; + + let j_times_q = foliage::Term::multiply( + Box::new(foliage::Term::variable(parameter_j)), + Box::new(foliage::Term::variable(parameter_q))); + + let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q), + Box::new(foliage::Term::variable(parameter_r))); + + let i_equals_j_times_q_plus_r = foliage::Formula::equal( + 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, + context)?; + + let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j, + context)?; + + let j_not_equal_to_0 = foliage::Formula::not_equal( + Box::new(foliage::Term::variable(parameter_j)), + Box::new(foliage::Term::integer(0))); + + let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal( + Box::new(foliage::Term::variable(parameter_r)), + Box::new(foliage::Term::integer(0))); + + let r_less_than_q = foliage::Formula::less( + Box::new(foliage::Term::variable(parameter_r)), + Box::new(foliage::Term::variable(parameter_q))); + + let z_equal_to_q = foliage::Formula::equal( + Box::new(foliage::Term::variable(variable_declaration)), + Box::new(foliage::Term::variable(parameter_q))); + + let z_equal_to_r = foliage::Formula::equal( + Box::new(foliage::Term::variable(variable_declaration)), + Box::new(foliage::Term::variable(parameter_r))); + + let last_argument = match operator + { + foliage::BinaryOperator::Divide => z_equal_to_q, + foliage::BinaryOperator::Modulo => z_equal_to_r, + _ => return Err(crate::Error::new_logic("unreachable code")), + }; + + let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r), + Box::new(choose_i_in_t1), Box::new(choose_i_in_t2), + Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0), + Box::new(r_less_than_q), Box::new(last_argument)]); + + Ok(foliage::Formula::exists(parameters, Box::new(and))) + }, + foliage::BinaryOperator::Exponentiate => + Err(crate::Error::new_unsupported_language_feature("exponentiation")), + } + }, + clingo::ast::TermType::UnaryOperation(unary_operation) => + { + match unary_operation.unary_operator() + { + clingo::ast::UnaryOperator::Absolute => + 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 negative_z_prime = foliage::Term::negative(Box::new( + foliage::Term::variable(¶meter_z_prime))); + let equals = foliage::Formula::equal( + Box::new(foliage::Term::variable(variable_declaration)), + Box::new(negative_z_prime)); + + let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(), + ¶meter_z_prime, context)?; + + let and = foliage::Formula::and(vec![Box::new(equals), + Box::new(choose_z_prime_in_t_prime)]); + + let parameters = std::rc::Rc::new(vec![parameter_z_prime]); + + Ok(foliage::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 = std::rc::Rc::new(parameters); + + let parameter_i = ¶meters[0]; + let parameter_j = ¶meters[1]; + let parameter_k = ¶meters[2]; + + 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, context)?; + + let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal( + Box::new(foliage::Term::variable(parameter_i)), + Box::new(foliage::Term::variable(parameter_k))); + + let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal( + Box::new(foliage::Term::variable(parameter_k)), + Box::new(foliage::Term::variable(parameter_j))); + + let z_equals_k = foliage::Formula::equal( + Box::new(foliage::Term::variable(variable_declaration)), + Box::new(foliage::Term::variable(parameter_k))); + + let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1), + Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k), + Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]); + + Ok(foliage::Formula::exists(parameters, Box::new(and))) + }, + clingo::ast::TermType::Function(_) => + Err(crate::Error::new_unsupported_language_feature("symbolic functions")), + clingo::ast::TermType::Pool(_) => + Err(crate::Error::new_unsupported_language_feature("pools")), + clingo::ast::TermType::ExternalFunction(_) => + Err(crate::Error::new_unsupported_language_feature("external functions")), + } +} diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 978b571..e908a64 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -1,193 +1,12 @@ +mod context; mod head_type; mod translate_body; +use context::*; use head_type::*; use translate_body::*; use crate::translate::common::AssignVariableDeclarationDomain as _; -struct ScopedFormula -{ - free_variable_declarations: std::rc::Rc, - formula: Box, -} - -struct Definitions -{ - head_atom_parameters: std::rc::Rc, - definitions: Vec, -} - -type VariableDeclarationDomains - = std::collections::BTreeMap, - crate::translate::common::Domain>; - -type VariableDeclarationIDs - = std::collections::BTreeMap::, usize>; - -struct Context -{ - pub definitions: std::cell::RefCell, - Definitions>>, - pub integrity_constraints: std::cell::RefCell, - - 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 -{ - fn new() -> Self - { - Self - { - 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) => - { - *id - } - None => - { - let id = variable_declaration_ids.len(); - variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); - id - }, - } - } -} - struct StatementHandler { context: Context, @@ -284,7 +103,7 @@ where let completed_definition = foliage::Formula::if_and_only_if( Box::new(head_predicate), Box::new(or)); - let scoped_formula = ScopedFormula + let scoped_formula = crate::ScopedFormula { free_variable_declarations: definitions.head_atom_parameters, formula: Box::new(completed_definition), @@ -301,7 +120,7 @@ where let variable_declaration = std::rc::Rc::new( foliage::VariableDeclaration::new("".to_string())); context.assign_variable_declaration_domain(&variable_declaration, - crate::translate::common::Domain::Program); + crate::Domain::Program); variable_declaration }) .collect::>()); @@ -315,7 +134,7 @@ where let not = foliage::Formula::not(Box::new(head_predicate)); - let scoped_formula = ScopedFormula + let scoped_formula = crate::ScopedFormula { free_variable_declarations: head_atom_parameters, formula: Box::new(not), @@ -414,7 +233,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let variable_declaration = std::rc::Rc::new( foliage::VariableDeclaration::new("".to_string())); context.assign_variable_declaration_domain(&variable_declaration, - crate::translate::common::Domain::Program); + crate::Domain::Program); variable_declaration }) .collect()); @@ -475,7 +294,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E _ => Box::new(foliage::Formula::and(definition_arguments)), }; - let definition = ScopedFormula + let definition = crate::ScopedFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula: definition, @@ -501,7 +320,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), }; - let scoped_formula = ScopedFormula + let scoped_formula = crate::ScopedFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula: Box::new(formula), @@ -521,7 +340,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E Ok(()) } -fn existential_closure(scoped_formula: ScopedFormula) -> Box +fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box { match scoped_formula.free_variable_declarations.is_empty() { @@ -531,7 +350,7 @@ fn existential_closure(scoped_formula: ScopedFormula) -> Box } } -fn universal_closure(scoped_formula: ScopedFormula) -> Box +fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box { match scoped_formula.free_variable_declarations.is_empty() { diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index db66fbd..1ebadd9 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -23,7 +23,7 @@ where let variable_declaration = std::rc::Rc::new( foliage::VariableDeclaration::new("".to_string())); context.assign_variable_declaration_domain(&variable_declaration, - crate::translate::common::Domain::Program); + crate::Domain::Program); variable_declaration }) .collect::(); @@ -109,7 +109,7 @@ where let variable_declaration = std::rc::Rc::new( foliage::VariableDeclaration::new("".to_string())); context.assign_variable_declaration_domain(&variable_declaration, - crate::translate::common::Domain::Program); + crate::Domain::Program); variable_declaration }) .collect::();