diff --git a/examples/exact-cover.spec b/examples/exact-cover.spec index 1ce31bc..9bbf4b4 100644 --- a/examples/exact-cover.spec +++ b/examples/exact-cover.spec @@ -1,6 +1,4 @@ -# Auxiliary predicate to determine whether a variable is integer. is_int/1 is declared as an input -# predicate so that anthem doesn’t generate its completed definition -input: is_int/1. +# Auxiliary predicate to determine whether a variable is integer axiom: forall X (is_int(X) <-> exists N X = N). # Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands @@ -11,6 +9,10 @@ assume: n >= 0. # s/2 is the input predicate defining the sets for which the program searches for exact covers input: s/2. +# Only the in/1 predicate is an actual output, s/2 is an input and covered/1 and is_int/1 are +# auxiliary +output: in/1. + # Perform the proofs under the assumption that the second parameter of s/2 (the number of the set) # is always an integer assume: forall X, Y (s(X, Y) -> is_int(Y)). diff --git a/examples/example-0.spec b/examples/example-0.spec index 4260fe6..a4da9b4 100644 --- a/examples/example-0.spec +++ b/examples/example-0.spec @@ -1 +1,3 @@ +input: p/2. + assert: exists X, Y p(X, Y) <-> exists X q(X). diff --git a/examples/example-1.spec b/examples/example-1.spec index 6c813c5..6c9f890 100644 --- a/examples/example-1.spec +++ b/examples/example-1.spec @@ -1,3 +1,5 @@ +input: p/1. + assert: forall N ( diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs index 76d994d..aa2a775 100644 --- a/src/commands/verify_program.rs +++ b/src/commands/verify_program.rs @@ -44,6 +44,16 @@ where } } + match problem.restrict_to_output_predicates() + { + Ok(_) => (), + Err(error) => + { + log::error!("could not restrict problem to output predicates: {}", error); + std::process::exit(1) + } + } + match problem.prove(proof_direction) { Ok(()) => (), diff --git a/src/error.rs b/src/error.rs index 0068f56..ea3e06f 100644 --- a/src/error.rs +++ b/src/error.rs @@ -22,6 +22,9 @@ pub enum Kind UnknownDomainIdentifier(String), VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), + NoCompletedDefinitionFound(std::rc::Rc), + CannotHidePredicate(std::rc::Rc, + std::rc::Rc), WriteTPTPProgram, RunVampire, // TODO: rename to something Vampire-specific @@ -148,6 +151,21 @@ impl Error Self::new(Kind::FormulaNotClosed(free_variables)) } + pub(crate) fn new_no_completed_definition_found( + predicate_declaration: std::rc::Rc) + -> Self + { + Self::new(Kind::NoCompletedDefinitionFound(predicate_declaration)) + } + + pub(crate) fn new_cannot_hide_predicate( + predicate_declaration_1: std::rc::Rc, + predicate_declaration_2: std::rc::Rc) + -> Self + { + Self::new(Kind::CannotHidePredicate(predicate_declaration_1, predicate_declaration_2)) + } + pub(crate) fn new_write_tptp_program>(source: S) -> Self { Self::new(Kind::WriteTPTPProgram).with(source) @@ -219,6 +237,11 @@ impl std::fmt::Debug for Error write!(formatter, "formula may not contain free variables (free variables in this formula: {})", free_variable_names_output) }, + Kind::NoCompletedDefinitionFound(ref predicate_declaration) => + write!(formatter, "no completed definition found for {}", predicate_declaration), + Kind::CannotHidePredicate(ref predicate_declaration_1, ref predicate_declaration_2) => + write!(formatter, "cannot hide predicate {} because it depends on {}", + predicate_declaration_1, predicate_declaration_2), Kind::RunVampire => write!(formatter, "could not run Vampire"), Kind::ProveProgram(exit_code, ref stdout, ref stderr) => { diff --git a/src/lib.rs b/src/lib.rs index d6a1413..09d86b2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,4 +1,5 @@ #![feature(trait_alias)] +#![feature(vec_remove_item)] pub mod commands; pub mod error; diff --git a/src/problem.rs b/src/problem.rs index fe8aaeb..debd40d 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -20,6 +20,9 @@ type VariableDeclarationIDs type InputConstantDeclarationDomains = std::collections::BTreeMap, crate::Domain>; +type VariableDeclarationDomains + = std::collections::BTreeMap, crate::Domain>; + struct FormatContext<'a, 'b> { pub program_variable_declaration_ids: std::cell::RefCell, @@ -28,9 +31,6 @@ struct FormatContext<'a, 'b> pub variable_declaration_domains: &'b VariableDeclarationDomains, } -type VariableDeclarationDomains - = std::collections::BTreeMap, crate::Domain>; - pub struct Problem { function_declarations: std::cell::RefCell, @@ -82,6 +82,64 @@ impl Problem section.push(statement); } + pub(crate) fn restrict_to_output_predicates(&mut self) -> Result<(), crate::Error> + { + let predicate_declarations = self.predicate_declarations.borrow(); + let input_predicate_declarations = self.input_predicate_declarations.borrow(); + let output_predicate_declarations = self.output_predicate_declarations.borrow(); + + // If no output statements were provided, show all predicates by default + if output_predicate_declarations.is_empty() + { + return Ok(()); + } + + let hidden_predicate_declarations = + predicate_declarations.iter().filter(|x| !output_predicate_declarations.contains(*x) + && !input_predicate_declarations.contains(*x)); + + let mut statements = self.statements.borrow_mut(); + + for hidden_predicate_declaration in hidden_predicate_declarations + { + let matches_completed_definition = + |(_, statement): &(_, &Statement)| match statement.kind + { + StatementKind::CompletedDefinition(ref predicate_declaration) => + predicate_declaration == hidden_predicate_declaration, + _ => false, + }; + + let completed_definitions = match statements.get_mut(&SectionKind::CompletedDefinitions) + { + Some(completed_definitions) => completed_definitions, + None => return Ok(()), + }; + + let completed_definition = match completed_definitions.iter().enumerate() + .find(matches_completed_definition) + { + Some((completed_definition_index, _)) => + completed_definitions.remove(completed_definition_index).formula, + None => return Err(crate::Error::new_no_completed_definition_found( + std::rc::Rc::clone(hidden_predicate_declaration))), + }; + + drop(completed_definitions); + + for (_, statements) in statements.iter_mut() + { + for statement in statements.iter_mut() + { + crate::utils::replace_predicate_in_formula_with_completed_definition( + &mut statement.formula, &completed_definition, self)?; + } + } + } + + Ok(()) + } + fn print_step_title(&self, step_title: &str, color: &termcolor::ColorSpec) { let longest_possible_key = " Finished"; @@ -216,17 +274,7 @@ impl Problem fn prove_unproven_statements(&self) -> Result { - let format_context = FormatContext - { - program_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - integer_variable_declaration_ids: - std::cell::RefCell::new(VariableDeclarationIDs::new()), - input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(), - variable_declaration_domains: &self.variable_declaration_domains.borrow(), - }; - - let display_statement = |statement: &Statement, format_context| + let display_statement = |statement: &Statement| { let step_title = match statement.proof_status { @@ -256,15 +304,17 @@ impl Problem self.shell.borrow_mut().print(&format!("{}: ", statement.kind), &termcolor::ColorSpec::new()); - match statement.kind + let format_context = FormatContext { - StatementKind::CompletedDefinition(_) - | StatementKind::IntegrityConstraint => - print!("{}", - foliage::format::display_formula(&statement.formula, format_context)), - _ => - print!("{}", statement.formula), - } + program_variable_declaration_ids: + std::cell::RefCell::new(VariableDeclarationIDs::new()), + integer_variable_declaration_ids: + std::cell::RefCell::new(VariableDeclarationIDs::new()), + input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(), + variable_declaration_domains: &self.variable_declaration_domains.borrow(), + }; + + print!("{}", foliage::format::display_formula(&statement.formula, &format_context)); }; // Show all statements that are assumed to be proven @@ -273,7 +323,7 @@ impl Problem for statement in statements.iter_mut() .filter(|statement| statement.proof_status == ProofStatus::AssumedProven) { - display_statement(statement, &format_context); + display_statement(statement); println!(""); } } @@ -286,7 +336,7 @@ impl Problem statement.proof_status = ProofStatus::ToProveNow; print!("\x1b[s"); - display_statement(statement, &format_context); + display_statement(statement); print!("\x1b[u"); use std::io::Write as _; @@ -309,7 +359,7 @@ impl Problem // TODO: make configurable again let (proof_result, proof_time_seconds) = run_vampire(&tptp_problem_to_prove_next_statement, - Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?; + Some(&["--mode", "casc", "--cores", "8", "--time_limit", "300"]))?; match self.next_unproven_statement_do_mut( |statement| @@ -323,7 +373,7 @@ impl Problem self.shell.borrow_mut().erase_line(); - display_statement(statement, &format_context); + display_statement(statement); match proof_result { @@ -591,6 +641,22 @@ impl crate::traits::AssignVariableDeclarationDomain for Problem } } +impl crate::traits::VariableDeclarationDomain for Problem +{ + fn variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc) + -> Option + { + self.variable_declaration_domains.borrow().iter().find_map( + |(x, domain)| + match x == variable_declaration + { + true => Some(*domain), + false => None, + }) + } +} + impl<'a, 'b> FormatContext<'a, 'b> { fn variable_declaration_id(&self, diff --git a/src/utils.rs b/src/utils.rs index 28519ee..27a58c5 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -1,8 +1,12 @@ mod arithmetic_terms; mod closures; +mod copy_formula; +mod output_predicates; pub(crate) use arithmetic_terms::*; pub(crate) use closures::*; +pub(crate) use copy_formula::*; +pub(crate) use output_predicates::*; #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] pub(crate) enum OperatorNotation diff --git a/src/utils/copy_formula.rs b/src/utils/copy_formula.rs new file mode 100644 index 0000000..748f8ed --- /dev/null +++ b/src/utils/copy_formula.rs @@ -0,0 +1,262 @@ +fn replace_variables_in_term(term: &mut foliage::Term, + old_variable_declarations: &foliage::VariableDeclarations, + new_variable_declarations: &foliage::VariableDeclarations) +{ + assert_eq!(old_variable_declarations.len(), new_variable_declarations.len()); + + use foliage::Term; + + match term + { + Term::BinaryOperation(binary_operation) => + { + replace_variables_in_term(&mut binary_operation.left, old_variable_declarations, + new_variable_declarations); + replace_variables_in_term(&mut binary_operation.right, old_variable_declarations, + new_variable_declarations); + }, + Term::Function(function) => + for mut argument in &mut function.arguments + { + replace_variables_in_term(&mut argument, old_variable_declarations, + new_variable_declarations); + }, + Term::UnaryOperation(unary_operation) => + replace_variables_in_term(&mut unary_operation.argument, old_variable_declarations, + new_variable_declarations), + Term::Variable(variable) => + if let Some(index) = old_variable_declarations.iter().enumerate() + .find_map( + |(index, variable_declaration)| + { + match *variable_declaration == variable.declaration + { + true => Some(index), + false => None, + } + }) + { + variable.declaration = std::rc::Rc::clone(&new_variable_declarations[index]); + }, + Term::Boolean(_) + | Term::Integer(_) + | Term::SpecialInteger(_) + | Term::String(_) => (), + } +} + +fn replace_variables_in_formula(formula: &mut foliage::Formula, + old_variable_declarations: &foliage::VariableDeclarations, + new_variable_declarations: &foliage::VariableDeclarations) +{ + use foliage::Formula; + + match formula + { + Formula::And(arguments) + | Formula::IfAndOnlyIf(arguments) + | Formula::Or(arguments) => + for argument in arguments + { + replace_variables_in_formula(argument, old_variable_declarations, + new_variable_declarations); + }, + Formula::Compare(compare) => + { + replace_variables_in_term(&mut compare.left, old_variable_declarations, + new_variable_declarations); + replace_variables_in_term(&mut compare.right, old_variable_declarations, + new_variable_declarations); + }, + Formula::Exists(quantified_formula) + | Formula::ForAll(quantified_formula) => + replace_variables_in_formula(&mut quantified_formula.argument, + old_variable_declarations, new_variable_declarations), + Formula::Implies(implies) => + { + replace_variables_in_formula(&mut implies.antecedent, old_variable_declarations, + new_variable_declarations); + replace_variables_in_formula(&mut implies.implication, old_variable_declarations, + new_variable_declarations); + }, + Formula::Not(argument) => + replace_variables_in_formula(argument, old_variable_declarations, + new_variable_declarations), + Formula::Predicate(predicate) => + for mut argument in &mut predicate.arguments + { + replace_variables_in_term(&mut argument, old_variable_declarations, + new_variable_declarations); + }, + Formula::Boolean(_) => (), + } +} + +fn replace_variable_in_term_with_term(term: &mut foliage::Term, + variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term) +{ + use foliage::Term; + + match term + { + Term::BinaryOperation(binary_operation) => + { + replace_variable_in_term_with_term(&mut binary_operation.left, variable_declaration, + replacement_term); + replace_variable_in_term_with_term(&mut binary_operation.right, variable_declaration, + replacement_term); + }, + Term::Function(function) => + for mut argument in &mut function.arguments + { + replace_variable_in_term_with_term(&mut argument, variable_declaration, + replacement_term); + }, + Term::UnaryOperation(unary_operation) => + replace_variable_in_term_with_term(&mut unary_operation.argument, variable_declaration, + replacement_term), + Term::Variable(variable) => + if *variable.declaration == *variable_declaration + { + *term = copy_term(replacement_term); + }, + Term::Boolean(_) + | Term::Integer(_) + | Term::SpecialInteger(_) + | Term::String(_) => (), + } +} + +pub(crate) fn replace_variable_in_formula_with_term(formula: &mut foliage::Formula, + variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term) +{ + use foliage::Formula; + + match formula + { + Formula::And(arguments) + | Formula::IfAndOnlyIf(arguments) + | Formula::Or(arguments) => + for argument in arguments + { + replace_variable_in_formula_with_term(argument, variable_declaration, + replacement_term); + }, + Formula::Compare(compare) => + { + replace_variable_in_term_with_term(&mut compare.left, variable_declaration, + replacement_term); + replace_variable_in_term_with_term(&mut compare.right, variable_declaration, + replacement_term); + }, + Formula::Exists(quantified_formula) + | Formula::ForAll(quantified_formula) => + replace_variable_in_formula_with_term(&mut quantified_formula.argument, + variable_declaration, replacement_term), + Formula::Implies(implies) => + { + replace_variable_in_formula_with_term(&mut implies.antecedent, variable_declaration, + replacement_term); + replace_variable_in_formula_with_term(&mut implies.implication, variable_declaration, + replacement_term); + }, + Formula::Not(argument) => + replace_variable_in_formula_with_term(argument, variable_declaration, replacement_term), + Formula::Predicate(predicate) => + for mut argument in &mut predicate.arguments + { + replace_variable_in_term_with_term(&mut argument, variable_declaration, + replacement_term); + }, + Formula::Boolean(_) => (), + } +} + +fn copy_term(term: &foliage::Term) -> foliage::Term +{ + use foliage::Term; + + match term + { + Term::BinaryOperation(binary_operation) => + Term::binary_operation(binary_operation.operator, + Box::new(copy_term(&binary_operation.left)), + Box::new(copy_term(&binary_operation.right))), + Term::Boolean(value) => Term::boolean(*value), + Term::Function(function) => Term::function(std::rc::Rc::clone(&function.declaration), + function.arguments.iter().map(|argument| copy_term(argument)).collect()), + Term::Integer(value) => Term::integer(*value), + Term::SpecialInteger(value) => Term::special_integer(*value), + Term::String(value) => Term::string(value.clone()), + Term::UnaryOperation(unary_operation) => Term::unary_operation(unary_operation.operator, + Box::new(copy_term(&unary_operation.argument))), + Term::Variable(variable) => Term::variable(std::rc::Rc::clone(&variable.declaration)), + } +} + +fn copy_quantified_formula(quantified_expression: &foliage::QuantifiedFormula, declarations: &D) + -> foliage::QuantifiedFormula +where + D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +{ + let copy_parameters = + quantified_expression.parameters.iter() + .map( + |parameter| + { + let copy_parameter = std::rc::Rc::new( + foliage::VariableDeclaration::new(parameter.name.clone())); + + if let Some(domain) = declarations.variable_declaration_domain(parameter) + { + declarations.assign_variable_declaration_domain(©_parameter, domain); + } + + copy_parameter + }) + .collect(); + let copy_parameters = std::rc::Rc::new(copy_parameters); + + let mut copy_argument = copy_formula(&quantified_expression.argument, declarations); + + replace_variables_in_formula(&mut copy_argument, &quantified_expression.parameters, + ©_parameters); + + foliage::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument)) +} + +pub(crate) fn copy_formula(formula: &foliage::Formula, declarations: &D) -> foliage::Formula +where + D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +{ + use foliage::Formula; + + match formula + { + Formula::And(arguments) => + Formula::and(arguments.iter().map( + |argument| copy_formula(argument, declarations)).collect()), + Formula::Boolean(value) => Formula::boolean(*value), + Formula::Compare(compare) => + Formula::compare(compare.operator, Box::new(copy_term(&compare.left)), + Box::new(copy_term(&compare.right))), + Formula::Exists(quantified_formula) => + Formula::Exists(copy_quantified_formula(quantified_formula, declarations)), + Formula::ForAll(quantified_formula) => + Formula::ForAll(copy_quantified_formula(quantified_formula, declarations)), + Formula::IfAndOnlyIf(arguments) => + Formula::if_and_only_if( + arguments.iter().map(|argument| copy_formula(argument, declarations)).collect()), + Formula::Implies(implies) => + Formula::implies(implies.direction, + Box::new(copy_formula(&implies.antecedent, declarations)), + Box::new(copy_formula(&implies.implication, declarations))), + Formula::Not(argument) => Formula::not(Box::new(copy_formula(&argument, declarations))), + Formula::Or(arguments) => + Formula::or(arguments.iter().map( + |argument| copy_formula(argument, declarations)).collect()), + Formula::Predicate(predicate) => + Formula::predicate(std::rc::Rc::clone(&predicate.declaration), + predicate.arguments.iter().map(|argument| copy_term(argument)).collect()), + } +} diff --git a/src/utils/output_predicates.rs b/src/utils/output_predicates.rs new file mode 100644 index 0000000..0ba885e --- /dev/null +++ b/src/utils/output_predicates.rs @@ -0,0 +1,127 @@ +fn formula_contains_predicate(formula: &foliage::Formula, + predicate_declaration: &foliage::PredicateDeclaration) + -> bool +{ + unimplemented!() +} + +fn replace_predicate_in_formula(formula: &mut foliage::Formula, + predicate_to_replace: &foliage::Predicate, replacement_formula: &foliage::Formula, + declarations: &D) +where + D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +{ + use foliage::{Formula, Term}; + + match formula + { + Formula::And(arguments) + | Formula::IfAndOnlyIf(arguments) + | Formula::Or(arguments) => + for mut argument in arguments + { + replace_predicate_in_formula(&mut argument, predicate_to_replace, + replacement_formula, declarations); + }, + Formula::Boolean(_) + | Formula::Compare(_) => (), + Formula::Exists(quantified_expression) + | Formula::ForAll(quantified_expression) => + replace_predicate_in_formula(&mut quantified_expression.argument, predicate_to_replace, + replacement_formula, declarations), + Formula::Implies(implies) => + { + replace_predicate_in_formula(&mut implies.antecedent, predicate_to_replace, + replacement_formula, declarations); + replace_predicate_in_formula(&mut implies.implication, predicate_to_replace, + replacement_formula, declarations); + }, + Formula::Not(argument) => + replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula, + declarations), + Formula::Predicate(predicate) => + if predicate.declaration == predicate_to_replace.declaration + { + let mut replacement_formula = + crate::utils::copy_formula(replacement_formula, declarations); + + for (index, argument) in predicate.arguments.iter().enumerate() + { + let variable_declaration = match &predicate_to_replace.arguments[index] + { + Term::Variable(variable) => &variable.declaration, + _ => panic!("invalid completed definition"), + }; + + crate::utils::replace_variable_in_formula_with_term(&mut replacement_formula, + &variable_declaration, argument); + } + + *formula = replacement_formula; + }, + } +} + +pub(crate) fn replace_predicate_in_formula_with_completed_definition( + formula: &mut foliage::Formula, completed_definition: &foliage::Formula, declarations: &D) + -> Result<(), crate::Error> +where + D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain, +{ + let false_ = foliage::Formula::false_(); + + // TODO: refactor + let (completed_definition_predicate, completed_definition) = match completed_definition + { + foliage::Formula::ForAll(quantified_expression) => match *quantified_expression.argument + { + foliage::Formula::IfAndOnlyIf(ref arguments) => + { + assert_eq!(arguments.len(), 2, "invalid completed definition"); + + match arguments[0] + { + foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]), + _ => panic!("invalid completed definition"), + } + }, + foliage::Formula::Not(ref argument) => match **argument + { + foliage::Formula::Predicate(ref predicate) => (predicate, &false_), + _ => panic!("invalid completed definition"), + }, + _ => panic!("invalid completed definition"), + }, + foliage::Formula::IfAndOnlyIf(ref arguments) => + { + assert_eq!(arguments.len(), 2, "invalid completed definition"); + + match arguments[0] + { + foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]), + _ => panic!("invalid completed definition"), + } + }, + foliage::Formula::Not(ref argument) => match **argument + { + foliage::Formula::Predicate(ref predicate) => (predicate, &false_), + _ => panic!("invalid completed definition"), + }, + _ => panic!("invalid completed definition"), + }; + + // Predicates can only be substituted by their completed definitions if there is no cycle. + // For example, if the completed definition of p/1 references q/1 and vice versa, neither can + // be replaced with the completed definition of the other + /*if formula_contains_predicate(completed_definition, predicate_declaration) + { + return Err(crate::Error::new()) + }*/ + + // TODO: detect cycles and warn accordingly + + replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition, + declarations); + + Ok(()) +}