patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Improve output

Browse Source
This commit is contained in:
Patrick Lühne 2020-05-07 17:19:42 +02:00
parent 5469f7d7b2
commit 753cc3e5a8
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 93 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
examples/example-2.spec
View File

@ -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).

89
src/problem.rs
View File

@ -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(_) => (),

6
src/translate/verify_properties.rs
View File

@ -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);