From becd8d4c199e9e665e4eb00f13e13387c66e414e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 17 Apr 2020 00:09:44 +0200 Subject: [PATCH] Upgrade to foliage 0.2 development version --- Cargo.toml | 2 +- src/main.rs | 1 + src/output/human_readable.rs | 413 +----------------- src/output/tptp.rs | 39 +- src/translate/common/choose_value_in_term.rs | 94 ++-- src/translate/verify_properties.rs | 45 +- src/translate/verify_properties/context.rs | 11 + .../verify_properties/translate_body.rs | 26 +- src/utils.rs | 16 +- 9 files changed, 152 insertions(+), 495 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 39aac3b..9be6a3f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ authors = ["Patrick Lühne "] edition = "2018" [dependencies] -foliage = "0.1" +foliage = {git = "https://github.com/pluehne/foliage", branch = "master"} log = "0.4" pretty_env_logger = "0.4" structopt = "0.3" diff --git a/src/main.rs b/src/main.rs index 01f820b..3ef44a9 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,6 +5,7 @@ use structopt::StructOpt as _; enum Command { #[structopt(about = "Verifies a logic program against a specification")] + #[structopt(aliases = &["verify-specification", "verify-spec", "vspec"])] VerifyProgram { /// ASP input program (one or multiple files) diff --git a/src/output/human_readable.rs b/src/output/human_readable.rs index aff4b8d..48ad178 100644 --- a/src/output/human_readable.rs +++ b/src/output/human_readable.rs @@ -1,403 +1,18 @@ -trait Precedence +pub(crate) fn display_variable_declaration(context: &C, formatter: &mut std::fmt::Formatter, + variable_declaration: &std::rc::Rc) + -> std::fmt::Result +where C: + crate::traits::VariableDeclarationDomain + crate::traits::VariableDeclarationID { - fn precedence(&self) -> i32; -} + let id = context.variable_declaration_id(variable_declaration); + let domain = context.variable_declaration_domain(variable_declaration) + .expect("unspecified variable domain"); -impl Precedence for foliage::Term -{ - fn precedence(&self) -> i32 + let prefix = match domain { - match &self - { - Self::Boolean(_) - | Self::Function(_) - | Self::SpecialInteger(_) - | Self::Integer(_) - | Self::String(_) - | Self::Variable(_) - => 0, - Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, ..}) - => 1, - Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, ..}) - => 2, - Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, ..}) - | Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, ..}) - | Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, ..}) - => 3, - Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, ..}) - | Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, ..}) - => 4, - Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, ..}) - => 5, - } - } -} - -impl Precedence for foliage::Formula -{ - fn precedence(&self) -> i32 - { - match &self - { - Self::Predicate(_) - | Self::Boolean(_) - | Self::Compare(_) - => 0, - Self::Exists(_) - | Self::ForAll(_) - => 1, - Self::Not(_) - => 2, - Self::And(_) - => 3, - Self::Or(_) - => 4, - Self::Implies(_) - => 5, - Self::IfAndOnlyIf(_) - => 6, - } - } -} - -pub(crate) struct VariableDeclarationDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::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::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 -{ - 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::Domain::Integer => "N", - crate::Domain::Program => "X", - }; - - write!(format, "{}{}", 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, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - write!(format, "{:?}", &self) - } -} - -pub(crate) struct TermDisplay<'a, 'b, C> -{ - parent_precedence: Option, - term: &'a foliage::Term, - context: &'b C, -} - -pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, parent_precedence: Option, - context: &'b C) - -> TermDisplay<'a, 'b, C> -{ - TermDisplay - { - parent_precedence, - 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, 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, precedence| display_term(term, precedence, self.context); - - let precedence = self.term.precedence(); - let requires_parentheses = match self.parent_precedence - { - Some(parent_precedence) => precedence > parent_precedence, - None => false, - }; - let precedence = Some(precedence); - - if requires_parentheses - { - write!(format, "(")?; - } - - match &self.term - { - foliage::Term::Boolean(true) => write!(format, "true"), - foliage::Term::Boolean(false) => write!(format, "false"), - foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum) => write!(format, "#inf"), - foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum) => write!(format, "#sup"), - foliage::Term::Integer(value) => write!(format, "{}", value), - foliage::Term::String(value) => write!(format, "\"{}\"", value), - foliage::Term::Variable(variable) => write!(format, "{:?}", - display_variable_declaration(&variable.declaration)), - foliage::Term::Function(function) => - { - write!(format, "{}", function.declaration.name)?; - - assert!(function.declaration.arity == function.arguments.len(), - "function has a different number of arguments than declared (expected {}, got {})", - function.declaration.arity, function.arguments.len()); - - if function.arguments.len() > 0 - { - write!(format, "{}(", function.declaration.name)?; - - let mut separator = ""; - - for argument in &function.arguments - { - write!(format, "{}{:?}", separator, display_term(&argument, None))?; - - separator = ", "; - } - - write!(format, ")")?; - } - - Ok(()) - }, - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, left, right}) - => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, left, right}) - => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, left, right}) - => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, left, right}) - => write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, left, right}) - => write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, left, right}) - => write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)), - foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, argument}) - => write!(format, "-{:?}", display_term(argument, precedence)), - foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, argument}) - => write!(format, "|{:?}|", display_term(argument, precedence)), - }?; - - if requires_parentheses - { - write!(format, ")")?; - } - - Ok(()) - } -} - -impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - write!(format, "{:?}", self) - } -} - -pub(crate) struct FormulaDisplay<'a, 'b, C> -{ - parent_precedence: Option, - formula: &'a foliage::Formula, - context: &'b C, -} - -pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, - parent_precedence: Option, context: &'b C) - -> FormulaDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - FormulaDisplay - { - parent_precedence, - formula, - context, - } -} - -impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::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, precedence| display_term(term, precedence, self.context); - let display_formula = |formula, precedence| display_formula(formula, precedence, self.context); - - let precedence = self.formula.precedence(); - let requires_parentheses = match self.parent_precedence - { - Some(parent_precedence) => precedence > parent_precedence, - None => false, - }; - let precedence = Some(precedence); - - if requires_parentheses - { - write!(format, "(")?; - } - - match &self.formula - { - foliage::Formula::Exists(exists) => - { - assert!(!exists.parameters.is_empty()); - - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in exists.parameters.iter() - { - write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; - - separator = ", " - } - - write!(format, " {:?}", display_formula(&exists.argument, precedence))?; - }, - foliage::Formula::ForAll(for_all) => - { - assert!(!for_all.parameters.is_empty()); - - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in for_all.parameters.iter() - { - write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; - - separator = ", " - } - - write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; - }, - foliage::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?, - foliage::Formula::And(arguments) => - { - let mut separator = ""; - - assert!(!arguments.is_empty()); - - for argument in arguments - { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; - - separator = " and " - } - }, - foliage::Formula::Or(arguments) => - { - let mut separator = ""; - - assert!(!arguments.is_empty()); - - for argument in arguments - { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; - - separator = " or " - } - }, - foliage::Formula::Implies(foliage::Implies{antecedent, implication}) - => write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?, - foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right}) - => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right}) - => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right}) - => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right}) - => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right}) - => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right}) - => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right}) - => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?, - foliage::Formula::Boolean(true) => write!(format, "#true")?, - foliage::Formula::Boolean(false) => write!(format, "#false")?, - foliage::Formula::Predicate(predicate) => - { - write!(format, "{}", predicate.declaration.name)?; - - if !predicate.arguments.is_empty() - { - write!(format, "(")?; - - let mut separator = ""; - - for argument in &predicate.arguments - { - write!(format, "{}{:?}", separator, display_term(argument, None))?; - - separator = ", " - } - - write!(format, ")")?; - } - }, - } - - if requires_parentheses - { - write!(format, ")")?; - } - - Ok(()) - } -} - -impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C> -where - C: crate::traits::VariableDeclarationDomain - + crate::traits::VariableDeclarationID -{ - fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result - { - write!(format, "{:?}", self) - } + crate::Domain::Integer => "N", + crate::Domain::Program => "X", + }; + + write!(formatter, "{}{}", prefix, id + 1) } diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 5364572..9b8d4d1 100644 --- a/src/output/tptp.rs +++ b/src/output/tptp.rs @@ -456,12 +456,43 @@ where write!(format, ")")?; }, - foliage::Formula::Implies(foliage::Implies{antecedent, implication}) + foliage::Formula::Implies(foliage::Implies{antecedent, 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::IfAndOnlyIf(arguments) => match arguments.len() + { + 0 => write!(format, "$true")?, + _ => + { + let mut separator = ""; + let parentheses_required = arguments.len() > 2; + + let mut argument_iterator = arguments.iter().peekable(); + + while let Some(argument) = argument_iterator.next() + { + if let Some(next_argument) = argument_iterator.peek() + { + write!(format, "{}", separator)?; + + if parentheses_required + { + write!(format, "(")?; + } + + write!(format, "{:?} <=> {:?}", display_formula(argument), + display_formula(next_argument))?; + + if parentheses_required + { + write!(format, ")")?; + } + + separator = " & "; + } + } + }, + }, foliage::Formula::Compare( foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right}) => display_compare(left, right, crate::OperatorNotation::Prefix, "$less", diff --git a/src/translate/common/choose_value_in_term.rs b/src/translate/common/choose_value_in_term.rs index 3eeab70..0f55a3d 100644 --- a/src/translate/common/choose_value_in_term.rs +++ b/src/translate/common/choose_value_in_term.rs @@ -1,5 +1,5 @@ pub(crate) fn choose_value_in_primitive(term: Box, - variable_declaration: &std::rc::Rc) + variable_declaration: std::rc::Rc) -> foliage::Formula { let variable = foliage::Term::variable(variable_declaration); @@ -8,7 +8,7 @@ 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) -> Result where C: crate::traits::GetOrCreateFunctionDeclaration @@ -42,14 +42,16 @@ where // 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")); + 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![]); + 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)) } @@ -60,7 +62,7 @@ where 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 = foliage::Term::variable(other_variable_declaration); Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration)) }, @@ -90,22 +92,21 @@ where 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))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(¶meter_1))), + Box::new(foliage::Term::variable(std::rc::Rc::clone(¶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)?; + binary_operation.left(), std::rc::Rc::clone(¶meter_1), context)?; let choose_value_from_right_argument = choose_value_in_term( - binary_operation.right(), ¶meter_2, context)?; + binary_operation.right(), std::rc::Rc::clone(¶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)]); + let and = foliage::Formula::And(vec![equals, choose_value_from_left_argument, + choose_value_from_right_argument]); Ok(foliage::Formula::exists(parameters, Box::new(and))) }, @@ -130,40 +131,42 @@ where 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))); + 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_plus_r = foliage::Term::add(Box::new(j_times_q), - Box::new(foliage::Term::variable(parameter_r))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(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)); + Box::new(foliage::Term::variable(std::rc::Rc::clone(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_t1 = choose_value_in_term(binary_operation.left(), + std::rc::Rc::clone(parameter_i), context)?; - let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j, - context)?; + let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), + std::rc::Rc::clone(parameter_j), context)?; let j_not_equal_to_0 = foliage::Formula::not_equal( - Box::new(foliage::Term::variable(parameter_j)), + Box::new(foliage::Term::variable(std::rc::Rc::clone(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::variable(std::rc::Rc::clone(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))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))), + Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q)))); let z_equal_to_q = foliage::Formula::equal( - Box::new(foliage::Term::variable(variable_declaration)), - Box::new(foliage::Term::variable(parameter_q))); + Box::new( + foliage::Term::variable(std::rc::Rc::clone(&variable_declaration))), + Box::new(foliage::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(parameter_r))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r)))); let last_argument = match operator { @@ -172,10 +175,9 @@ where _ => 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)]); + let and = foliage::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1, + choose_i_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))) }, @@ -197,16 +199,15 @@ where crate::Domain::Integer); let negative_z_prime = foliage::Term::negative(Box::new( - foliage::Term::variable(¶meter_z_prime))); + foliage::Term::variable(std::rc::Rc::clone(¶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)?; + std::rc::Rc::clone(¶meter_z_prime), context)?; - let and = foliage::Formula::and(vec![Box::new(equals), - Box::new(choose_z_prime_in_t_prime)]); + let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]); let parameters = std::rc::Rc::new(vec![parameter_z_prime]); @@ -232,25 +233,26 @@ where 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_i_in_t_1 = choose_value_in_term(interval.left(), + std::rc::Rc::clone(parameter_i), context)?; - let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, context)?; + let choose_j_in_t_2 = choose_value_in_term(interval.right(), + std::rc::Rc::clone(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))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))), + Box::new(foliage::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(parameter_k)), - Box::new(foliage::Term::variable(parameter_j))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))), + Box::new(foliage::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(parameter_k))); + Box::new(foliage::Term::variable(std::rc::Rc::clone(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)]); + let and = foliage::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))) }, diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index e1249f8..d5cdcda 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -105,7 +105,7 @@ where for definition in definitions.definitions.iter() { log::debug!("definition({}/{}): {}.", predicate_declaration.name, predicate_declaration.arity, - crate::output::human_readable::display_formula(&definition.formula, None, &context)); + foliage::format::display_formula(&definition.formula, &context)); } } @@ -122,14 +122,14 @@ where let or = foliage::Formula::or(or_arguments); let head_arguments = definitions.head_atom_parameters.iter() - .map(|x| Box::new(foliage::Term::variable(x))) + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) .collect::>(); - let head_predicate = foliage::Formula::predicate(&predicate_declaration, - head_arguments); + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(predicate_declaration), head_arguments); - let completed_definition = foliage::Formula::if_and_only_if( - Box::new(head_predicate), Box::new(or)); + let completed_definition = + foliage::Formula::if_and_only_if(vec![head_predicate, or]); let scoped_formula = crate::ScopedFormula { @@ -154,11 +154,11 @@ where .collect::>()); let head_arguments = head_atom_parameters.iter() - .map(|x| Box::new(foliage::Term::variable(x))) + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) .collect(); - let head_predicate = foliage::Formula::predicate(&predicate_declaration, - head_arguments); + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(predicate_declaration), head_arguments); let not = foliage::Formula::not(Box::new(head_predicate)); @@ -197,7 +197,7 @@ where match output_format { crate::output::Format::HumanReadable => print!("{}", - crate::output::human_readable::display_formula(formula, None, &context)), + foliage::format::display_formula(formula, &context)), crate::output::Format::TPTP => print!("{}", crate::output::tptp::display_formula(formula, &context)), } @@ -380,13 +380,13 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E if let HeadType::ChoiceWithSingleAtom(_) = head_type { let head_arguments = definitions.head_atom_parameters.iter() - .map(|x| Box::new(foliage::Term::variable(x))) + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) .collect::>(); - let head_predicate = foliage::Formula::predicate(&head_atom.predicate_declaration, - head_arguments); + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments); - definition_arguments.push(Box::new(head_predicate)); + definition_arguments.push(head_predicate); } let mut head_atom_arguments_iterator = head_atom.arguments.iter(); @@ -396,9 +396,9 @@ 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, head_atom_parameter, context)?; + head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context)?; - definition_arguments.push(Box::new(translated_head_term)); + definition_arguments.push(translated_head_term); } context.variable_declaration_stack.borrow_mut().pop()?; @@ -410,18 +410,18 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let definition = match definition_arguments.len() { 1 => definition_arguments.pop().unwrap(), - 0 => Box::new(foliage::Formula::true_()), - _ => Box::new(foliage::Formula::and(definition_arguments)), + 0 => foliage::Formula::true_(), + _ => foliage::Formula::and(definition_arguments), }; let definition = crate::ScopedFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), - formula: definition, + formula: Box::new(definition), }; log::debug!("translated rule with single atom in head: {}", - crate::output::human_readable::display_formula(&definition.formula, None, context)); + foliage::format::display_formula(&definition.formula, context)); definitions.definitions.push(definition); }, @@ -435,7 +435,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let formula = match arguments.len() { - 1 => foliage::Formula::not(arguments.pop().unwrap()), + 1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())), 0 => foliage::Formula::false_(), _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), }; @@ -449,8 +449,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let integrity_constraint = crate::universal_closure(scoped_formula); log::debug!("translated integrity constraint: {}", - crate::output::human_readable::display_formula(&integrity_constraint, None, - context)); + foliage::format::display_formula(&integrity_constraint, context)); context.integrity_constraints.borrow_mut().push(integrity_constraint); }, diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index dc39153..1e20050 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -208,3 +208,14 @@ impl crate::traits::VariableDeclarationID for Context } } } + +impl foliage::format::Format for Context +{ + fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter, + variable_declaration: &std::rc::Rc) + -> std::fmt::Result + { + crate::output::human_readable::display_variable_declaration(self, formatter, + variable_declaration) + } +} diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index ff6a221..860d4c7 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -30,10 +30,10 @@ where let parameters = std::rc::Rc::new(parameters); let predicate_arguments = parameters.iter().map( - |parameter| Box::new(foliage::Term::variable(parameter))) + |parameter| foliage::Term::variable(std::rc::Rc::clone(parameter))) .collect::>(); - let predicate = foliage::Formula::predicate(&predicate_declaration, predicate_arguments); + let predicate = foliage::Formula::predicate(predicate_declaration, predicate_arguments); let predicate_literal = match sign { @@ -53,12 +53,11 @@ where 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(), - context) - .map(|x| Box::new(x))) + |x| crate::translate::common::choose_value_in_term(x, + std::rc::Rc::clone(¶meters_iterator.next().unwrap()), context)) .collect::, _>>()?; - arguments.push(Box::new(predicate_literal)); + arguments.push(predicate_literal); let and = foliage::Formula::and(arguments); @@ -120,12 +119,12 @@ where let parameter_z2 = ¶meters_iterator.next().unwrap(); let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), - parameter_z1, context)?; + std::rc::Rc::clone(parameter_z1), context)?; let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), - parameter_z2, context)?; + std::rc::Rc::clone(parameter_z2), context)?; - let variable_1 = foliage::Term::variable(parameter_z1); - let variable_2 = foliage::Term::variable(parameter_z2); + 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 operator = crate::translate::common::translate_comparison_operator( comparison.comparison_type()); @@ -133,8 +132,8 @@ where let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1), Box::new(variable_2)); - let and = foliage::Formula::and(vec![Box::new(choose_z1_in_t1), - Box::new(choose_z2_in_t2), Box::new(compare_z1_and_z2)]); + let and = + foliage::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]); Ok(foliage::Formula::exists(parameters, Box::new(and))) }, @@ -153,7 +152,6 @@ where + crate::traits::AssignVariableDeclarationDomain { body_literals.iter() - .map(|body_literal| translate_body_literal(body_literal, context) - .map(|value| Box::new(value))) + .map(|body_literal| translate_body_literal(body_literal, context)) .collect::>() } diff --git a/src/utils.rs b/src/utils.rs index dc1d90b..2439369 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -44,23 +44,23 @@ pub(crate) struct ScopedFormula pub formula: Box, } -pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box +pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula { match scoped_formula.free_variable_declarations.is_empty() { - true => scoped_formula.formula, - false => Box::new(foliage::Formula::exists(scoped_formula.free_variable_declarations, - scoped_formula.formula)), + true => *scoped_formula.formula, + false => foliage::Formula::exists(scoped_formula.free_variable_declarations, + scoped_formula.formula), } } -pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box +pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula { match scoped_formula.free_variable_declarations.is_empty() { - true => scoped_formula.formula, - false => Box::new(foliage::Formula::for_all(scoped_formula.free_variable_declarations, - scoped_formula.formula)), + true => *scoped_formula.formula, + false => foliage::Formula::for_all(scoped_formula.free_variable_declarations, + scoped_formula.formula), } }