diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs index 1bc4710..4f79464 100644 --- a/src/commands/verify_program.rs +++ b/src/commands/verify_program.rs @@ -1,5 +1,5 @@ -pub fn run

(program_path: P, specification_path: P, proof_direction: - crate::problem::ProofDirection) +pub fn run

(program_path: P, specification_path: P, + proof_direction: crate::problem::ProofDirection, no_simplify: bool) where P: AsRef, { @@ -60,6 +60,19 @@ where } } + if !no_simplify + { + match problem.simplify() + { + Ok(_) => (), + Err(error) => + { + log::error!("could not simplify translated program: {}", error); + std::process::exit(1) + } + } + } + match problem.prove(proof_direction) { Ok(()) => (), diff --git a/src/main.rs b/src/main.rs index ed5c583..3ed04d8 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,6 +19,10 @@ enum Command /// Proof direction (forward, backward, both) #[structopt(long, default_value = "forward")] proof_direction: anthem::problem::ProofDirection, + + /// Do not simplify translated program + #[structopt(long)] + no_simplify: bool, } } @@ -35,8 +39,9 @@ fn main() program_path, specification_path, proof_direction, + no_simplify, } => anthem::commands::verify_program::run(&program_path, &specification_path, - proof_direction), + proof_direction, no_simplify), } } diff --git a/src/problem.rs b/src/problem.rs index d2c2c9d..c49572a 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -44,7 +44,7 @@ impl Problem } } - pub(crate) fn add_statement(&self, section_kind: SectionKind, mut statement: Statement) + pub(crate) fn add_statement(&self, section_kind: SectionKind, statement: Statement) { let mut statements = self.statements.borrow_mut(); let section = statements.entry(section_kind).or_insert(vec![]); @@ -151,6 +151,28 @@ impl Problem Ok(()) } + pub fn simplify(&mut self) -> Result<(), crate::Error> + { + let mut statements = self.statements.borrow_mut(); + + for (_, statements) in statements.iter_mut() + { + for statement in statements.iter_mut() + { + match statement.kind + { + // Only simplify generated formulas + | StatementKind::CompletedDefinition(_) + | StatementKind::IntegrityConstraint => + crate::simplify(&mut statement.formula)?, + _ => (), + } + } + } + + Ok(()) + } + fn print_step_title(&self, step_title: &str, color: &termcolor::ColorSpec) -> Result<(), crate::Error> { @@ -319,13 +341,8 @@ impl Problem self.shell.borrow_mut().print(&format!("{}: ", statement.kind), &termcolor::ColorSpec::new())?; - match statement.kind - { - StatementKind::CompletedDefinition(_) - | StatementKind::IntegrityConstraint => - crate::autoname_variables(&mut statement.formula), - _ => (), - } + // TODO: only perform autonaming when necessary + crate::autoname_variables(&mut statement.formula); print!("{}", statement.formula); diff --git a/src/simplify.rs b/src/simplify.rs index b14f189..200b28c 100644 --- a/src/simplify.rs +++ b/src/simplify.rs @@ -18,9 +18,10 @@ impl SimplificationResult } } -fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) -> SimplificationResult +fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) + -> Result { - use crate::Formula; + use crate::{Formula, Term}; match formula { @@ -33,18 +34,18 @@ fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) -> Simplif for argument in arguments { simplification_result = simplification_result.or( - remove_unnecessary_exists_parameters(argument)); + remove_unnecessary_exists_parameters(argument)?); } - simplification_result + Ok(simplification_result) }, Formula::Boolean(_) | Formula::Compare(_) - | Formula::Predicate(_) => SimplificationResult::NotSimplified, + | Formula::Predicate(_) => Ok(SimplificationResult::NotSimplified), Formula::Exists(ref mut quantified_formula) => { let mut simplification_result = - remove_unnecessary_exists_parameters(&mut quantified_formula.argument); + remove_unnecessary_exists_parameters(&mut quantified_formula.argument)?; let arguments = match *quantified_formula.argument { @@ -69,31 +70,55 @@ fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) -> Simplif _ => return None, }; - if let foliage::Term::Variable(ref variable) = **left + let assigned_term = match (&**left, &**right) { - if variable.declaration == *parameter - && !crate::term_contains_variable(right, parameter) + (Term::Variable(ref variable), right) + if variable.declaration == *parameter => + right, + (left, Term::Variable(ref variable)) + if variable.declaration == *parameter => + left, + _ => return None, + }; + + let parameter_domain = match parameter.domain() + { + Ok(domain) => domain, + Err(_) => + unreachable!("all variable domains should be assigned at this point"), + }; + + let is_parameter_integer = + parameter_domain == crate::Domain::Integer; + + let is_assigned_term_arithmetic = + match crate::is_term_arithmetic(assigned_term) { - // TODO: avoid copy - return Some((argument_index, crate::copy_term(right))); - } + Ok(is_term_arithmetic) => is_term_arithmetic, + Err(error) => return Some(Err(error)), + }; + + let is_assignment_narrowing = is_parameter_integer + && !is_assigned_term_arithmetic; + + if crate::term_contains_variable(assigned_term, parameter) + || is_assignment_narrowing + { + return None; } - if let foliage::Term::Variable(ref variable) = **right - { - if variable.declaration == *parameter - && !crate::term_contains_variable(left, parameter) - { - // TODO: avoid copy - return Some((argument_index, crate::copy_term(left))); - } - } - - None + // TODO: avoid copy + Some(Ok((argument_index, crate::copy_term(assigned_term)))) }); - if let Some((assignment_index, assigned_term)) = assignment + if let Some(assignment) = assignment { + let (assignment_index, assigned_term) = match assignment + { + Err(error) => return Some(Err(error)), + Ok(assignment) => assignment, + }; + arguments.remove(assignment_index); for argument in arguments.iter_mut() @@ -107,11 +132,11 @@ fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula) -> Simplif return None; } - Some(std::rc::Rc::clone(parameter)) + Some(Ok(std::rc::Rc::clone(parameter))) }) - .collect()); + .collect::>()?); - simplification_result + Ok(simplification_result) } Formula::ForAll(ref mut quantified_formula) => remove_unnecessary_exists_parameters(&mut quantified_formula.argument), @@ -225,22 +250,20 @@ fn simplify_trivial_n_ary_formulas(formula: &mut crate::Formula) -> Simplificati } } -pub(crate) fn simplify(formula: &mut crate::Formula) +pub(crate) fn simplify(formula: &mut crate::Formula) -> Result<(), crate::Error> { loop { - if remove_unnecessary_exists_parameters(formula) == SimplificationResult::Simplified + if remove_unnecessary_exists_parameters(formula)? == SimplificationResult::Simplified || simplify_quantified_formulas_without_parameters(formula) == SimplificationResult::Simplified || simplify_trivial_n_ary_formulas(formula) == SimplificationResult::Simplified { - log::debug!("cool, simplified!"); - continue; } - log::debug!("nope, that’s it"); - break; } + + Ok(()) } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 925bd12..bd9458c 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -146,11 +146,9 @@ impl<'p> Translator<'p> let statement_kind = crate::problem::StatementKind::CompletedDefinition( std::rc::Rc::clone(&predicate_declaration)); - let mut completed_definition = completed_definition(predicate_declaration, + let completed_definition = completed_definition(predicate_declaration, &mut self.definitions); - //crate::simplify(&mut completed_definition); - let statement_name = format!("completed_definition_{}", predicate_declaration.tptp_statement_name()); @@ -287,8 +285,6 @@ impl<'p> Translator<'p> let integrity_constraint = crate::universal_closure(open_formula); - //crate::simplify(&mut integrity_constraint); - let statement = crate::problem::Statement::new( crate::problem::StatementKind::IntegrityConstraint, integrity_constraint) .with_name("integrity_constraint".to_string());