From b14f6202355a02e0f5c17a94d376901b277a38a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 6 May 2020 00:13:43 +0200 Subject: [PATCH] Implement proof mechanism --- Cargo.toml | 2 +- src/commands.rs | 2 +- src/commands/verify_specification.rs | 49 ------ src/error.rs | 7 + src/input/specification.rs | 9 +- src/main.rs | 4 +- src/problem.rs | 245 ++++++++++++++++++++++++++- 7 files changed, 262 insertions(+), 56 deletions(-) delete mode 100644 src/commands/verify_specification.rs diff --git a/Cargo.toml b/Cargo.toml index 2680d97..8f2a010 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "anthem" -version = "0.3.0" +version = "0.3.0-beta.1" authors = ["Patrick Lühne "] edition = "2018" diff --git a/src/commands.rs b/src/commands.rs index 00cf6ae..9864c02 100644 --- a/src/commands.rs +++ b/src/commands.rs @@ -1 +1 @@ -pub mod verify_specification; +pub mod verify_program; diff --git a/src/commands/verify_specification.rs b/src/commands/verify_specification.rs deleted file mode 100644 index 1b3f319..0000000 --- a/src/commands/verify_specification.rs +++ /dev/null @@ -1,49 +0,0 @@ -pub fn run

(program_path: P, specification_path: P, output_format: crate::output::Format) -where - P: AsRef -{ - //let context = crate::translate::verify_properties::Context::new(); - let mut problem = crate::Problem::new(); - - log::info!("reading specification “{}”", specification_path.as_ref().display()); - - let specification_content = match std::fs::read_to_string(specification_path.as_ref()) - { - Ok(specification_content) => specification_content, - Err(error) => - { - log::error!("could not access specification file: {}", error); - std::process::exit(1) - }, - }; - - // TODO: rename to read_specification - match crate::input::parse_specification(&specification_content, &mut problem) - { - Ok(_) => (), - Err(error) => - { - log::error!("could not read specification: {}", error); - std::process::exit(1) - } - } - - log::info!("read specification “{}”", specification_path.as_ref().display()); - - log::info!("reading input program “{}”", program_path.as_ref().display()); - - // TODO: make consistent with specification call (path vs. content) - match crate::translate::verify_properties::Translator::new(&mut problem).translate(program_path) - { - Ok(_) => (), - Err(error) => - { - log::error!("could not translate input program: {}", error); - std::process::exit(1) - } - } - - problem.prove(crate::ProofDirection::Both); - - log::info!("done"); -} diff --git a/src/error.rs b/src/error.rs index 83bd941..5ae306b 100644 --- a/src/error.rs +++ b/src/error.rs @@ -20,6 +20,7 @@ pub enum Kind UnknownProofDirection(String), UnknownDomainIdentifier(String), VariableNameNotAllowed(String), + WriteTPTPProgram, } pub struct Error @@ -129,6 +130,11 @@ impl Error { Self::new(Kind::VariableNameNotAllowed(variable_name)) } + + pub(crate) fn new_write_tptp_program>(source: S) -> Self + { + Self::new(Kind::WriteTPTPProgram).with(source) + } } impl std::fmt::Debug for Error @@ -168,6 +174,7 @@ impl std::fmt::Debug for Error Kind::VariableNameNotAllowed(ref variable_name) => write!(formatter, "variable name “{}” not allowed (program variables must start with X, Y, or Z and integer variables with I, J, K, L, M, or N)", variable_name), + Kind::WriteTPTPProgram => write!(formatter, "error writing TPTP program"), }?; if let Some(source) = &self.source diff --git a/src/input/specification.rs b/src/input/specification.rs index 4ae0769..f1add07 100644 --- a/src/input/specification.rs +++ b/src/input/specification.rs @@ -245,6 +245,8 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) crate::Domain::Program }; + log::debug!("domain: {:?}", domain); + let mut input_constant_declarations = problem.input_constant_declarations.borrow_mut(); @@ -253,7 +255,12 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) let constant_declaration = problem.find_or_create_function_declaration(constant_or_predicate_name, 0); - input_constant_declarations.insert(constant_declaration); + input_constant_declarations.insert(std::rc::Rc::clone(&constant_declaration)); + + let mut input_constant_declaration_domains = + problem.input_constant_declaration_domains.borrow_mut(); + + input_constant_declaration_domains.insert(constant_declaration, domain); let mut input_characters = input.chars(); diff --git a/src/main.rs b/src/main.rs index dad793c..0444f09 100644 --- a/src/main.rs +++ b/src/main.rs @@ -24,7 +24,7 @@ enum Command fn main() { - pretty_env_logger::init(); + pretty_env_logger::init_custom_env("ANTHEM_LOG"); let command = Command::from_args(); @@ -36,7 +36,7 @@ fn main() specification_path, output_format, } - => anthem::commands::verify_specification::run(&program_path, &specification_path, + => anthem::commands::verify_program::run(&program_path, &specification_path, output_format), } } diff --git a/src/problem.rs b/src/problem.rs index 9c83485..0df2add 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -6,6 +6,7 @@ pub enum StatementKind Assertion, } +#[derive(Copy, Clone, Eq, PartialEq)] enum ProofStatus { AssumedProven, @@ -151,10 +152,86 @@ impl Problem drop(statements); - self.display(crate::output::Format::HumanReadable); + self.prove_unproven_statements(); log::info!("finished forward proof"); } + + if proof_direction == crate::ProofDirection::Backward + || proof_direction == crate::ProofDirection::Both + { + log::info!("performing backward proof"); + + let mut statements = self.statements.borrow_mut(); + + // Initially reset all proof statuses + for (_, statements) in statements.iter_mut() + { + for statement in statements.iter_mut() + { + match statement.kind + { + StatementKind::Axiom + | StatementKind::Assertion + => statement.proof_status = ProofStatus::AssumedProven, + _ => statement.proof_status = ProofStatus::ToProve, + } + } + } + + drop(statements); + + self.prove_unproven_statements(); + + log::info!("finished backward proof"); + } + } + + fn prove_unproven_statements(&self) -> Result<(), crate::Error> + { + while self.statements.borrow() + .iter() + .find(|section| + section.1.iter().find(|x| x.proof_status == ProofStatus::ToProve).is_some()) + .is_some() + { + let mut tptp_problem_to_prove_next_statement = "".to_string(); + + self.write_tptp_problem_to_prove_next_statement( + &mut tptp_problem_to_prove_next_statement) + .map_err(|error| crate::Error::new_write_tptp_program(error))?; + + log::info!("proving program:\n{}", &tptp_problem_to_prove_next_statement); + + // TODO: refactor + let mut conjecture_found = false; + + for section in self.statements.borrow_mut().iter_mut() + { + for statement in section.1.iter_mut() + { + if statement.proof_status == ProofStatus::ToProve + { + conjecture_found = true; + statement.proof_status = ProofStatus::AssumedProven; + } + + if conjecture_found + { + break; + } + } + + if conjecture_found + { + break; + } + } + + log::info!("program proven!"); + } + + Ok(()) } fn display(&self, output_format: crate::output::Format) @@ -306,7 +383,8 @@ impl Problem if output_format == crate::output::Format::TPTP { - print!("tff({}, , ", name); + // TODO: add proper statement type + print!("tff({}, axiom, ", name); } print_formula(&statement.formula); @@ -320,6 +398,169 @@ impl Problem } } } + + fn write_tptp_problem_to_prove_next_statement(&self, formatter: &mut String) -> std::fmt::Result + { + use std::fmt::Write as _; + use std::io::Write as _; + + 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 write_title = |formatter: &mut String, title, section_separator| -> std::fmt::Result + { + write!(formatter, "{}{}", section_separator, "%".repeat(72))?; + write!(formatter, "\n% {}", title)?; + writeln!(formatter, "\n{}", "%".repeat(72)) + }; + + let mut section_separator = ""; + + write_title(formatter, "anthem types", section_separator)?; + section_separator = "\n"; + + let tptp_preamble_anthem_types + = include_str!("output/tptp/preamble_types.tptp").trim_end(); + writeln!(formatter, "{}", tptp_preamble_anthem_types)?; + + write_title(formatter, "anthem axioms", section_separator)?; + + let tptp_preamble_anthem_types + = include_str!("output/tptp/preamble_axioms.tptp").trim_end(); + writeln!(formatter, "{}", tptp_preamble_anthem_types)?; + + if !self.predicate_declarations.borrow().is_empty() + || !self.function_declarations.borrow().is_empty() + { + write_title(formatter, "types", section_separator)?; + + if !self.predicate_declarations.borrow().is_empty() + { + writeln!(formatter, "% predicate types")?; + } + + for predicate_declaration in self.predicate_declarations.borrow().iter() + { + writeln!(formatter, "tff(type, type, {}).", + crate::output::tptp::display_predicate_declaration(predicate_declaration))?; + } + + if !self.function_declarations.borrow().is_empty() + { + writeln!(formatter, "% function types")?; + } + + for function_declaration in self.function_declarations.borrow().iter() + { + writeln!(formatter, "tff(type, type, {}).", + crate::output::tptp::display_function_declaration(function_declaration, + &format_context))?; + } + } + + let function_declarations = self.function_declarations.borrow(); + let symbolic_constants = function_declarations.iter().filter( + |x| !self.input_constant_declaration_domains.borrow().contains_key(*x)); + + let mut last_symbolic_constant: Option> = + None; + + for (i, symbolic_constant) in symbolic_constants.enumerate() + { + // Order axioms are only necessary with two or more symbolic constants + if i == 1 + { + writeln!(formatter, "% axioms for order of symbolic constants")?; + } + + if symbolic_constant.arity > 0 + { + // TODO: refactor + unimplemented!("n-ary function declarations aren’t supported"); + } + + if let Some(last_symbolic_constant) = last_symbolic_constant + { + writeln!(formatter, "tff(symbolic_constant_order, axiom, p__less__({}, {})).", + last_symbolic_constant.name, symbolic_constant.name)?; + } + + last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant)); + } + + let mut conjecture_found = false; + + for (section_kind, statements) in self.statements.borrow().iter() + { + if statements.is_empty() + { + continue; + } + + let title = match section_kind + { + SectionKind::CompletedDefinitions => "completed definitions", + SectionKind::IntegrityConstraints => "integrity constraints", + SectionKind::Axioms => "axioms", + SectionKind::Assumptions => "assumptions", + SectionKind::Lemmas => "lemmas", + SectionKind::Assertions => "assertions", + }; + + write_title(formatter, title, section_separator)?; + section_separator = "\n"; + + let mut i = 0; + + for statement in statements.iter() + { + // Only prove one statement at a time + if conjecture_found && statement.proof_status == ProofStatus::ToProve + { + continue; + } + + if let Some(ref description) = statement.description + { + writeln!(formatter, "% {}", description)?; + } + + let name = match &statement.name + { + // TODO: refactor + Some(name) => name.clone(), + None => + { + i += 1; + format!("statement_{}", i) + }, + }; + + let statement_type = match statement.proof_status + { + ProofStatus::AssumedProven => "axiom", + ProofStatus::ToProve => + { + conjecture_found = true; + "conjecture" + }, + }; + + // TODO: add proper statement type + writeln!(formatter, "tff({}, {}, {}).", name, statement_type, + crate::output::tptp::display_formula(&statement.formula, &format_context))?; + } + } + + Ok(()) + } } impl foliage::FindOrCreateFunctionDeclaration for Problem