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

Work in progress

This commit is contained in:
Patrick Lühne 2020-05-13 02:24:13 +02:00
parent 4d00fbeb97
commit 0dbf30bb1b
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 51 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/problem.rs
View File

@ -4,11 +4,12 @@ mod section_kind;
pub use proof_direction::ProofDirection;
pub use section_kind::SectionKind;
#[derive(Copy, Clone, Eq, PartialEq)]
#[derive(Eq, PartialEq)]
pub enum StatementKind
{
Axiom,
Program,
CompletedDefinition(std::rc::Rc<foliage::PredicateDeclaration>),
IntegrityConstraint,
Assumption,
Lemma(ProofDirection),
Assertion,
@ -155,7 +156,7 @@ impl Problem
{
self.print_step_title("Started",
termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)));
self.shell.borrow_mut().println(&"verification of assertions from completed definitions",
self.shell.borrow_mut().println(&"verification of assertions from translated program",
&termcolor::ColorSpec::new());
let mut statements = self.statements.borrow_mut();
@ -169,7 +170,8 @@ impl Problem
{
StatementKind::Axiom
| StatementKind::Assumption
| StatementKind::Program =>
| StatementKind::CompletedDefinition(_)
| StatementKind::IntegrityConstraint =>
statement.proof_status = ProofStatus::AssumedProven,
StatementKind::Lemma(ProofDirection::Backward) =>
statement.proof_status = ProofStatus::Ignored,
@ -193,7 +195,7 @@ impl Problem
};
self.print_step_title("Finished", &step_title_color);
println!("verification of assertions from completed definitions");
println!("verification of assertions from translated program");
}
if proof_direction == ProofDirection::Both
@ -206,7 +208,7 @@ impl Problem
{
self.print_step_title("Started",
termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)));
self.shell.borrow_mut().println(&"verification of completed definitions from assertions",
self.shell.borrow_mut().println(&"verification of translated program from assertions",
&termcolor::ColorSpec::new());
let mut statements = self.statements.borrow_mut();
@ -244,7 +246,7 @@ impl Problem
};
self.print_step_title("Finished", &step_title_color);
println!("verification of completed definitions from assertions");
println!("verification of translated program from assertions");
}
Ok(())
@ -313,7 +315,8 @@ impl Problem
match statement.kind
{
StatementKind::Program =>
StatementKind::CompletedDefinition(_)
| StatementKind::IntegrityConstraint =>
print!("{}",
foliage::format::display_formula(&statement.formula, format_context)),
_ =>

49
src/translate/verify_properties.rs
View File

@ -141,19 +141,50 @@ impl<'p> Translator<'p>
}
};
for predicate_declaration in self.problem.predicate_declarations.borrow().iter()
// TODO: refactor
let predicate_declarations = self.problem.predicate_declarations.borrow();
let input_predicate_declarations = self.problem.input_predicate_declarations.borrow();
let mut definitions = &mut self.definitions;
let problem = &self.problem;
let completed_definitions = predicate_declarations.iter()
.filter_map(
|predicate_declaration|
{
// Don’t perform completion for input predicates
if input_predicate_declarations.contains(predicate_declaration)
{
return None;
}
let completed_definition = completed_definition(predicate_declaration,
&mut definitions, problem);
Some((std::rc::Rc::clone(predicate_declaration), completed_definition))
})
.collect::<std::collections::BTreeMap<_, _>>();
// Replace occurrences of hidden predicates with their completed definitions
let output_predicate_declarations = self.problem.output_predicate_declarations.borrow();
// If no output statements are present, don’t hide any predicates by default
if !output_predicate_declarations.is_empty()
{
// Don’t perform completion for input predicates
if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration)
let hidden_predicate_declarations =
predicate_declarations.difference(&output_predicate_declarations);
for hidden_predicate_declaration in hidden_predicate_declarations
{
continue;
log::debug!("hidden: {}", hidden_predicate_declaration);
}
}
let completed_definition =
completed_definition(predicate_declaration, &mut self.definitions, self.problem);
for (predicate_declaration, completed_definition) in completed_definitions.into_iter()
{
let statement_kind = crate::problem::StatementKind::CompletedDefinition(
std::rc::Rc::clone(&predicate_declaration));
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Program, completed_definition)
let statement = crate::problem::Statement::new(statement_kind, completed_definition)
.with_name(format!("completed_definition_{}_{}", predicate_declaration.name,
predicate_declaration.arity))
.with_description(format!("completed definition of {}/{}",
@ -295,7 +326,7 @@ impl<'p> Translator<'p>
let integrity_constraint = crate::universal_closure(open_formula);
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Program, integrity_constraint)
crate::problem::StatementKind::IntegrityConstraint, integrity_constraint)
.with_name("integrity_constraint".to_string())
.with_description("integrity constraint".to_string());