diff --git a/examples/example-2.spec b/examples/example-2.spec index d217fa7..064833b 100644 --- a/examples/example-2.spec +++ b/examples/example-2.spec @@ -1,9 +1,8 @@ -axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3). - -axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)). - input: n -> integer. +axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3). +axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)). + assume: n >= 0. assert: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n). @@ -16,6 +15,8 @@ lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))). lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > n). lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)). + + lemma(forward): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))). lemma(forward): exists N2 p(N2). lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2). diff --git a/src/problem.rs b/src/problem.rs index 38c9125..9f038aa 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -133,6 +133,17 @@ impl Problem pub fn prove(&self, proof_direction: crate::ProofDirection) -> Result<(), crate::Error> { + // TODO: refactor + 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(), + }; + if proof_direction == crate::ProofDirection::Forward || proof_direction == crate::ProofDirection::Both { @@ -141,7 +152,7 @@ impl Problem let mut statements = self.statements.borrow_mut(); // Initially reset all proof statuses - for (_, statements) in statements.iter_mut() + for (section_kind, statements) in statements.iter_mut() { for statement in statements.iter_mut() { @@ -149,10 +160,34 @@ impl Problem { StatementKind::Axiom | StatementKind::Assumption - | StatementKind::Program - => statement.proof_status = ProofStatus::AssumedProven, - StatementKind::Lemma(crate::ProofDirection::Backward) - => statement.proof_status = ProofStatus::Ignored, + | StatementKind::Program => + { + // TODO: avoid code duplication + let statement_type_output = match section_kind + { + SectionKind::CompletedDefinitions => "completed definition", + SectionKind::IntegrityConstraints => "integrity constraint", + SectionKind::Axioms => "axiom", + SectionKind::Assumptions => "assumption", + SectionKind::Lemmas => "lemma", + SectionKind::Assertions => "assertion", + }; + + // TODO: refactor + match statement.kind + { + StatementKind::Program => println!(" - {}: {}", + statement_type_output, + foliage::format::display_formula(&statement.formula, + &format_context)), + _ => println!(" - {}: {}", statement_type_output, + statement.formula), + } + + statement.proof_status = ProofStatus::AssumedProven; + }, + StatementKind::Lemma(crate::ProofDirection::Backward) => + statement.proof_status = ProofStatus::Ignored, _ => statement.proof_status = ProofStatus::ToProveLater, } } @@ -173,7 +208,7 @@ impl Problem let mut statements = self.statements.borrow_mut(); // Initially reset all proof statuses - for (_, statements) in statements.iter_mut() + for (section_kind, statements) in statements.iter_mut() { for statement in statements.iter_mut() { @@ -181,10 +216,34 @@ impl Problem { StatementKind::Axiom | StatementKind::Assumption - | StatementKind::Assertion - => statement.proof_status = ProofStatus::AssumedProven, - StatementKind::Lemma(crate::ProofDirection::Forward) - => statement.proof_status = ProofStatus::Ignored, + | StatementKind::Assertion => + { + // TODO: avoid code duplication + let statement_type_output = match section_kind + { + SectionKind::CompletedDefinitions => "completed definition", + SectionKind::IntegrityConstraints => "integrity constraint", + SectionKind::Axioms => "axiom", + SectionKind::Assumptions => "assumption", + SectionKind::Lemmas => "lemma", + SectionKind::Assertions => "assertion", + }; + + // TODO: refactor + match statement.kind + { + StatementKind::Program => println!(" - {}: {}", + statement_type_output, + foliage::format::display_formula(&statement.formula, + &format_context)), + _ => println!(" - {}: {}", statement_type_output, + statement.formula), + } + + statement.proof_status = ProofStatus::AssumedProven; + }, + StatementKind::Lemma(crate::ProofDirection::Forward) => + statement.proof_status = ProofStatus::Ignored, _ => statement.proof_status = ProofStatus::ToProveLater, } } @@ -248,8 +307,14 @@ impl Problem SectionKind::Assertions => "assertion", }; - println!("- verifying {}: {}", statement_type_output, - foliage::format::display_formula(&statement.formula, &format_context)); + match statement.kind + { + StatementKind::Program => println!(" - verifying {}: {}", + statement_type_output, + foliage::format::display_formula(&statement.formula, &format_context)), + _ => println!(" - verifying {}: {}", statement_type_output, + statement.formula), + } }) { Some(_) => (), @@ -262,7 +327,7 @@ impl Problem &mut tptp_problem_to_prove_next_statement) .map_err(|error| crate::Error::new_write_tptp_program(error))?; - log::trace!("TPTP program :\n{}", &tptp_problem_to_prove_next_statement); + log::trace!("TPTP program:\n{}", &tptp_problem_to_prove_next_statement); // TODO: make configurable again let (proof_result, proof_time_seconds) = @@ -273,13 +338,13 @@ impl Problem { ProofResult::NotProven => { - println!(" → could not prove statement"); + println!(" → could not prove statement"); return Ok(()); }, ProofResult::Disproven => { - println!(" → statement disproven"); + println!(" → statement disproven"); return Ok(()); }, @@ -295,9 +360,9 @@ impl Problem match proof_time_seconds { - None => println!(" → statement proven"), + None => println!(" → statement proven"), Some(proof_time_seconds) => - println!(" → statement proven in {} seconds", proof_time_seconds), + println!(" → statement proven in {} seconds", proof_time_seconds), } } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index e957ad7..8b5642a 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -155,6 +155,12 @@ impl<'p> Translator<'p> for predicate_declaration in self.problem.predicate_declarations.borrow().iter() { + // Don’t perform completion for input predicates + if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration) + { + continue; + } + let completed_definition = completed_definition(predicate_declaration, &mut self.definitions, self.problem);