diff --git a/Cargo.toml b/Cargo.toml index f282b0e..2680d97 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ authors = ["Patrick Lühne "] edition = "2018" [dependencies] -foliage = {git = "https://github.com/pluehne/foliage", branch = "parser"} +foliage = {git = "https://github.com/pluehne/foliage", branch = "parser-new"} log = "0.4" pretty_env_logger = "0.4" structopt = "0.3" diff --git a/src/commands.rs b/src/commands.rs new file mode 100644 index 0000000..00cf6ae --- /dev/null +++ b/src/commands.rs @@ -0,0 +1 @@ +pub mod verify_specification; diff --git a/src/commands/verify_specification.rs b/src/commands/verify_specification.rs new file mode 100644 index 0000000..1b3f319 --- /dev/null +++ b/src/commands/verify_specification.rs @@ -0,0 +1,49 @@ +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 4c5213f..83bd941 100644 --- a/src/error.rs +++ b/src/error.rs @@ -8,8 +8,18 @@ pub enum Kind DecodeIdentifier, Translate, ReadFile(std::path::PathBuf), + ExpectedStatement, + ExpectedColon, + UnknownStatement(String), + UnmatchedParenthesis, + MissingStatementTerminator, + ParseFormula, + ExpectedIdentifier, ParsePredicateDeclaration, - ParseConstantDeclaration, + //ParseConstantDeclaration, + UnknownProofDirection(String), + UnknownDomainIdentifier(String), + VariableNameNotAllowed(String), } pub struct Error @@ -65,14 +75,59 @@ impl Error Self::new(Kind::ReadFile(path)).with(source) } + pub(crate) fn new_expected_statement() -> Self + { + Self::new(Kind::ExpectedStatement) + } + + pub(crate) fn new_expected_colon() -> Self + { + Self::new(Kind::ExpectedColon) + } + + pub(crate) fn new_unknown_statement(statement_name: String) -> Self + { + Self::new(Kind::UnknownStatement(statement_name)) + } + + pub(crate) fn new_unmatched_parenthesis() -> Self + { + Self::new(Kind::UnmatchedParenthesis) + } + + pub(crate) fn new_missing_statement_terminator() -> Self + { + Self::new(Kind::MissingStatementTerminator) + } + + pub(crate) fn new_parse_formula>(source: S) -> Self + { + Self::new(Kind::ParseFormula).with(source) + } + + pub(crate) fn new_expected_identifier() -> Self + { + Self::new(Kind::ExpectedIdentifier) + } + pub(crate) fn new_parse_predicate_declaration() -> Self { Self::new(Kind::ParsePredicateDeclaration) } - pub(crate) fn new_parse_constant_declaration() -> Self + pub(crate) fn new_unknown_proof_direction(proof_direction: String) -> Self { - Self::new(Kind::ParseConstantDeclaration) + Self::new(Kind::UnknownProofDirection(proof_direction)) + } + + pub(crate) fn new_unknown_domain_identifier(domain_identifier: String) -> Self + { + Self::new(Kind::UnknownDomainIdentifier(domain_identifier)) + } + + pub(crate) fn new_variable_name_not_allowed(variable_name: String) -> Self + { + Self::new(Kind::VariableNameNotAllowed(variable_name)) } } @@ -91,10 +146,28 @@ impl std::fmt::Debug for Error Kind::DecodeIdentifier => write!(formatter, "could not decode identifier"), Kind::Translate => write!(formatter, "could not translate input program"), Kind::ReadFile(path) => write!(formatter, "could not read file “{}”", path.display()), + Kind::ExpectedStatement => write!(formatter, + "expected statement (axiom, assert, assume, input, lemma)"), + Kind::ExpectedColon => write!(formatter, "expected ‘:’"), + Kind::UnknownStatement(ref statement_name) => write!(formatter, + "unknown statement “{}” (allowed: axiom, assert, assume, input, lemma)", + statement_name), + Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis"), Kind::ParsePredicateDeclaration => write!(formatter, "could not parse predicate declaration"), - Kind::ParseConstantDeclaration => write!(formatter, - "could not parse constant declaration"), + Kind::ParseFormula => write!(formatter, "could not parse formula"), + Kind::ExpectedIdentifier => write!(formatter, "expected constant or predicate name"), + Kind::ParsePredicateDeclaration => write!(formatter, + "could not parse predicate declaration"), + Kind::MissingStatementTerminator => write!(formatter, + "statement not terminated with ‘.’ character"), + Kind::UnknownProofDirection(ref proof_direction) => write!(formatter, + "unknown proof direction “{}” (allowed: integer, program)", proof_direction), + Kind::UnknownDomainIdentifier(ref domain_identifier) => write!(formatter, + "unknown domain identifier “{}” (allowed: int, program)", domain_identifier), + 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), }?; if let Some(source) = &self.source diff --git a/src/input.rs b/src/input.rs new file mode 100644 index 0000000..32758ae --- /dev/null +++ b/src/input.rs @@ -0,0 +1,3 @@ +pub(crate) mod specification; + +pub(crate) use specification::parse_specification; diff --git a/src/input/specification.rs b/src/input/specification.rs new file mode 100644 index 0000000..4ae0769 --- /dev/null +++ b/src/input/specification.rs @@ -0,0 +1,404 @@ +// TODO: refactor +fn term_assign_variable_declaration_domains(term: &foliage::Term, declarations: &D) + -> Result<(), crate::Error> +where + D: crate::traits::AssignVariableDeclarationDomain, +{ + match term + { + foliage::Term::BinaryOperation(binary_operation) => + { + term_assign_variable_declaration_domains(&binary_operation.left, declarations)?; + term_assign_variable_declaration_domains(&binary_operation.right, declarations)?; + }, + foliage::Term::Function(function) => + for argument in &function.arguments + { + term_assign_variable_declaration_domains(&argument, declarations)?; + }, + foliage::Term::UnaryOperation(unary_operation) => + term_assign_variable_declaration_domains(&unary_operation.argument, declarations)?, + foliage::Term::Variable(variable) => + { + let domain = match variable.declaration.name.chars().next() + { + Some('X') + | Some('Y') + | Some('Z') => crate::Domain::Program, + Some('I') + | Some('J') + | Some('K') + | Some('L') + | Some('M') + | Some('N') => crate::Domain::Integer, + // TODO: improve error handling + Some(other) => return Err( + crate::Error::new_variable_name_not_allowed(variable.declaration.name.clone())), + None => unreachable!(), + }; + + declarations.assign_variable_declaration_domain(&variable.declaration, domain); + }, + _ => (), + } + + Ok(()) +} + +fn formula_assign_variable_declaration_domains(formula: &foliage::Formula, declarations: &D) + -> Result<(), crate::Error> +where + D: crate::traits::AssignVariableDeclarationDomain, +{ + match formula + { + foliage::Formula::And(arguments) + | foliage::Formula::Or(arguments) + | foliage::Formula::IfAndOnlyIf(arguments) => + for argument in arguments + { + formula_assign_variable_declaration_domains(&argument, declarations)?; + }, + foliage::Formula::Compare(compare) => + { + term_assign_variable_declaration_domains(&compare.left, declarations)?; + term_assign_variable_declaration_domains(&compare.right, declarations)?; + }, + foliage::Formula::Exists(quantified_formula) + | foliage::Formula::ForAll(quantified_formula) => + formula_assign_variable_declaration_domains(&quantified_formula.argument, + declarations)?, + foliage::Formula::Implies(implies) => + { + formula_assign_variable_declaration_domains(&implies.antecedent, declarations)?; + formula_assign_variable_declaration_domains(&implies.implication, declarations)?; + } + foliage::Formula::Not(argument) => + formula_assign_variable_declaration_domains(&argument, declarations)?, + foliage::Formula::Predicate(predicate) => + for argument in &predicate.arguments + { + term_assign_variable_declaration_domains(&argument, declarations)?; + }, + _ => (), + } + + Ok(()) +} + +fn closed_formula<'i, D>(input: &'i str, declarations: &D) + -> Result<(crate::ScopedFormula, &'i str), crate::Error> +where + D: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration + + crate::traits::AssignVariableDeclarationDomain, +{ + let terminator_position = match input.find('.') + { + None => return Err(crate::Error::new_missing_statement_terminator()), + Some(terminator_position) => terminator_position, + }; + + let (formula_input, remaining_input) = input.split_at(terminator_position); + let mut remaining_input_characters = remaining_input.chars(); + remaining_input_characters.next(); + let remaining_input = remaining_input_characters.as_str(); + + let closed_formula = foliage::parse::formula(formula_input, declarations) + .map_err(|error| crate::Error::new_parse_formula(error))?; + + formula_assign_variable_declaration_domains(&closed_formula.formula, declarations)?; + + // TODO: get rid of ScopedFormula + let scoped_formula = crate::ScopedFormula + { + free_variable_declarations: closed_formula.free_variable_declarations, + formula: closed_formula.formula, + }; + + Ok((scoped_formula, remaining_input)) +} + +fn variable_free_formula<'i, D>(input: &'i str, declarations: &D) + -> Result<(foliage::Formula, &'i str), crate::Error> +where + D: foliage::FindOrCreateFunctionDeclaration + + foliage::FindOrCreatePredicateDeclaration + + crate::traits::AssignVariableDeclarationDomain, +{ + let (closed_formula, input) = closed_formula(input, declarations)?; + + if !closed_formula.free_variable_declarations.is_empty() + { + // TODO: improve + panic!("formula may not contain free variables"); + } + + Ok((closed_formula.formula, input)) +} + +fn formula_statement_body<'i>(input: &'i str, problem: &crate::Problem) + -> Result<(foliage::Formula, &'i str), crate::Error> +{ + let input = input.trim_start(); + + let mut input_characters = input.chars(); + + let remaining_input = match input_characters.next() + { + Some(':') => input_characters.as_str(), + _ => return Err(crate::Error::new_expected_colon()), + }; + + let input = remaining_input; + + variable_free_formula(input, problem) +} + +fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem) + -> Result<&'i str, crate::Error> +{ + input = input.trim_start(); + + let mut input_characters = input.chars(); + + let remaining_input = match input_characters.next() + { + Some(':') => input_characters.as_str(), + _ => return Err(crate::Error::new_expected_colon()), + }; + + input = remaining_input; + + loop + { + input = input.trim_start(); + + let (constant_or_predicate_name, remaining_input) = + foliage::parse::tokens::identifier(input) + .ok_or_else(|| crate::Error::new_expected_identifier())?; + + input = remaining_input.trim_start(); + + let mut input_characters = input.chars(); + + match input_characters.next() + { + // Parse input predicate specifiers + Some('/') => + { + input = input_characters.as_str().trim_start(); + + let (arity, remaining_input) = foliage::parse::tokens::number(input) + .map_err(|error| crate::Error::new_parse_predicate_declaration().with(error))? + .ok_or_else(|| crate::Error::new_parse_predicate_declaration())?; + + input = remaining_input.trim_start(); + + let mut input_predicate_declarations = + problem.input_predicate_declarations.borrow_mut(); + + use foliage::FindOrCreatePredicateDeclaration; + + let predicate_declaration = + problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity); + + input_predicate_declarations.insert(predicate_declaration); + + let mut input_characters = input.chars(); + + match input_characters.next() + { + Some(',') => input = input_characters.as_str(), + _ => break, + } + }, + // Parse input constant specifiers + Some(_) + | None => + { + let domain = + if input.starts_with("->") + { + let mut input_characters = input.chars(); + input_characters.next(); + input_characters.next(); + + input = input_characters.as_str().trim_start(); + + let (identifier, remaining_input) = + foliage::parse::tokens::identifier(input) + .ok_or_else(|| crate::Error::new_expected_identifier())?; + + input = remaining_input; + + match identifier + { + "integer" => crate::Domain::Integer, + "program" => crate::Domain::Program, + _ => return Err(crate::Error::new_unknown_domain_identifier( + identifier.to_string())), + } + } + else + { + crate::Domain::Program + }; + + let mut input_constant_declarations = + problem.input_constant_declarations.borrow_mut(); + + use foliage::FindOrCreateFunctionDeclaration; + + let constant_declaration = + problem.find_or_create_function_declaration(constant_or_predicate_name, 0); + + input_constant_declarations.insert(constant_declaration); + + let mut input_characters = input.chars(); + + match input_characters.next() + { + Some(',') => input = input_characters.as_str(), + _ => break, + } + } + } + } + + input = input.trim_start(); + + let mut input_characters = input.chars(); + + if input_characters.next() != Some('.') + { + return Err(crate::Error::new_missing_statement_terminator()) + } + + input = input_characters.as_str(); + + Ok(input) +} + +pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem) + -> Result<(), crate::Error> +{ + loop + { + input = input.trim_start(); + + if input.is_empty() + { + return Ok(()); + } + + let (identifier, remaining_input) = match foliage::parse::tokens::identifier(input) + { + Some(identifier) => identifier, + None => return Err(crate::Error::new_expected_statement()), + }; + + input = remaining_input; + + match identifier + { + "axiom" => + { + let (formula, remaining_input) = formula_statement_body(input, problem)?; + input = remaining_input; + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Axiom, formula); + + problem.add_statement(crate::problem::SectionKind::Axioms, statement); + + continue; + }, + "assume" => + { + let (formula, remaining_input) = formula_statement_body(input, problem)?; + input = remaining_input; + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Assumption, formula); + + problem.add_statement(crate::problem::SectionKind::Assumptions, statement); + + continue; + }, + "lemma" => + { + input = input.trim_start(); + + let mut input_characters = input.chars(); + + let (proof_direction, remaining_input) = match input_characters.next() + { + Some('(') => + { + // TODO: refactor + input = input_characters.as_str().trim_start(); + + let (proof_direction, remaining_input) = match + foliage::parse::tokens::identifier(input) + { + Some(("forward", remaining_input)) => + (crate::ProofDirection::Forward, remaining_input), + Some(("backward", remaining_input)) => + (crate::ProofDirection::Backward, remaining_input), + Some(("both", remaining_input)) => + (crate::ProofDirection::Both, remaining_input), + Some((identifier, _)) => + return Err(crate::Error::new_unknown_proof_direction( + identifier.to_string())), + None => (crate::ProofDirection::Both, input), + }; + + input = remaining_input.trim_start(); + + let mut input_characters = input.chars(); + + if input_characters.next() != Some(')') + { + return Err(crate::Error::new_unmatched_parenthesis()); + } + + input = input_characters.as_str(); + + (proof_direction, input) + }, + Some(_) + | None => (crate::ProofDirection::Both, remaining_input), + }; + + input = remaining_input; + + let (formula, remaining_input) = formula_statement_body(input, problem)?; + + input = remaining_input; + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Lemma(proof_direction), formula); + + problem.add_statement(crate::problem::SectionKind::Lemmas, statement); + + continue; + }, + "assert" => + { + let (formula, remaining_input) = formula_statement_body(input, problem)?; + + input = remaining_input; + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Assertion, formula); + + problem.add_statement(crate::problem::SectionKind::Assertions, statement); + + continue; + }, + "input" => input = input_statement_body(input, problem)?, + identifier => return Err(crate::Error::new_unknown_statement(identifier.to_string())), + } + } +} diff --git a/src/lib.rs b/src/lib.rs index e0da604..0c0845f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,12 +1,15 @@ #![feature(trait_alias)] +pub mod commands; pub mod error; +pub mod input; pub mod output; +pub mod problem; pub(crate) mod traits; pub mod translate; mod utils; pub use error::Error; +pub use problem::Problem; pub(crate) use utils::*; -pub use utils::{Domain, InputConstantDeclarationDomains, parse_predicate_declaration, - parse_constant_declaration}; +pub use utils::{Domain, InputConstantDeclarationDomains}; diff --git a/src/main.rs b/src/main.rs index 3ef44a9..dad793c 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,25 +5,20 @@ use structopt::StructOpt as _; enum Command { #[structopt(about = "Verifies a logic program against a specification")] - #[structopt(aliases = &["verify-specification", "verify-spec", "vspec"])] + #[structopt(aliases = &["vprog"])] VerifyProgram { - /// ASP input program (one or multiple files) - #[structopt(parse(from_os_str), required(true))] - input: Vec, + /// ASP input program file path + #[structopt(name = "program", parse(from_os_str), required(true))] + program_path: std::path::PathBuf, + + #[structopt(name = "specification", parse(from_os_str), required(true))] + /// Specification file path + specification_path: std::path::PathBuf, /// Output format (human-readable, tptp) #[structopt(long, default_value = "human-readable")] output_format: anthem::output::Format, - - /// Input predicates (examples: p, q/2) - #[structopt(long, parse(try_from_str = anthem::parse_predicate_declaration))] - input_predicates: Vec>, - - /// Input constants (example: c, integer(n)) - #[structopt(long, parse(try_from_str = anthem::parse_constant_declaration))] - input_constants: Vec< - (std::rc::Rc, anthem::Domain)>, } } @@ -37,21 +32,11 @@ fn main() { Command::VerifyProgram { - input, + program_path, + specification_path, output_format, - input_predicates, - input_constants, } - => - { - if let Err(error) = anthem::translate::verify_properties::translate(&input, - input_predicates.into_iter().collect::(), - input_constants.into_iter().collect::>(), - output_format) - { - log::error!("could not translate input program: {}", error); - std::process::exit(1) - } - }, + => anthem::commands::verify_specification::run(&program_path, &specification_path, + output_format), } } diff --git a/src/output/human_readable.rs b/src/output/human_readable.rs index 48ad178..715d258 100644 --- a/src/output/human_readable.rs +++ b/src/output/human_readable.rs @@ -1,4 +1,4 @@ -pub(crate) fn display_variable_declaration(context: &C, formatter: &mut std::fmt::Formatter, +/*pub(crate) fn display_variable_declaration(context: &C, formatter: &mut std::fmt::Formatter, variable_declaration: &std::rc::Rc) -> std::fmt::Result where C: @@ -15,4 +15,4 @@ where C: }; write!(formatter, "{}{}", prefix, id + 1) -} +}*/ diff --git a/src/problem.rs b/src/problem.rs new file mode 100644 index 0000000..9c83485 --- /dev/null +++ b/src/problem.rs @@ -0,0 +1,502 @@ +pub enum StatementKind +{ + Axiom, + Assumption, + Lemma(crate::ProofDirection), + Assertion, +} + +enum ProofStatus +{ + AssumedProven, + ToProve, +} + +pub enum ProofResult +{ + Proven, + NotProven, + Disproven, +} + +pub struct Statement +{ + kind: StatementKind, + name: Option, + description: Option, + formula: foliage::Formula, + proof_status: ProofStatus, +} + +type VariableDeclarationIDs + = std::collections::BTreeMap::, usize>; + +struct FormatContext<'a, 'b> +{ + pub program_variable_declaration_ids: std::cell::RefCell, + pub integer_variable_declaration_ids: std::cell::RefCell, + pub input_constant_declaration_domains: &'a crate::InputConstantDeclarationDomains, + pub variable_declaration_domains: &'b VariableDeclarationDomains, +} + +impl Statement +{ + pub fn new(kind: StatementKind, formula: foliage::Formula) -> Self + { + Self + { + kind, + name: None, + description: None, + formula, + proof_status: ProofStatus::ToProve, + } + } + + pub fn with_name(mut self, name: String) -> Self + { + self.name = Some(name); + self + } + + pub fn with_description(mut self, description: String) -> Self + { + self.description = Some(description); + self + } +} + +#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)] +pub enum SectionKind +{ + CompletedDefinitions, + IntegrityConstraints, + Axioms, + Assumptions, + Lemmas, + Assertions, +} + +type VariableDeclarationDomains + = std::collections::BTreeMap, crate::Domain>; + +pub struct Problem +{ + function_declarations: std::cell::RefCell, + pub predicate_declarations: std::cell::RefCell, + + statements: std::cell::RefCell>>, + + pub input_constant_declarations: std::cell::RefCell, + pub input_constant_declaration_domains: + std::cell::RefCell, + pub input_predicate_declarations: std::cell::RefCell, + // TODO: clean up as variable declarations are dropped + variable_declaration_domains: std::cell::RefCell, +} + +impl Problem +{ + pub fn new() -> Self + { + Self + { + function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()), + predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()), + + statements: std::cell::RefCell::new(std::collections::BTreeMap::new()), + + input_constant_declarations: + std::cell::RefCell::new(foliage::FunctionDeclarations::new()), + input_constant_declaration_domains: + std::cell::RefCell::new(crate::InputConstantDeclarationDomains::new()), + input_predicate_declarations: + std::cell::RefCell::new(foliage::PredicateDeclarations::new()), + variable_declaration_domains: + std::cell::RefCell::new(VariableDeclarationDomains::new()), + } + } + + pub fn add_statement(&self, section_kind: SectionKind, statement: Statement) + { + let mut statements = self.statements.borrow_mut(); + let section = statements.entry(section_kind).or_insert(vec![]); + + section.push(statement); + } + + pub fn prove(&self, proof_direction: crate::ProofDirection) + { + if proof_direction == crate::ProofDirection::Forward + || proof_direction == crate::ProofDirection::Both + { + log::info!("performing forward 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::Assumption + => statement.proof_status = ProofStatus::AssumedProven, + _ => statement.proof_status = ProofStatus::ToProve, + } + } + } + + drop(statements); + + self.display(crate::output::Format::HumanReadable); + + log::info!("finished forward proof"); + } + } + + fn display(&self, output_format: crate::output::Format) + { + 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 print_title = |title, section_separator| + { + print!("{}{}", section_separator, "%".repeat(72)); + print!("\n% {}", title); + println!("\n{}", "%".repeat(72)); + }; + + let print_formula = |formula: &foliage::Formula| + { + match output_format + { + crate::output::Format::HumanReadable => print!("{}", + foliage::format::display_formula(formula, &format_context)), + crate::output::Format::TPTP => print!("{}", + crate::output::tptp::display_formula(formula, &format_context)), + } + }; + + let mut section_separator = ""; + + if output_format == crate::output::Format::TPTP + { + print_title("anthem types", section_separator); + section_separator = "\n"; + + let tptp_preamble_anthem_types + = include_str!("output/tptp/preamble_types.tptp").trim_end(); + println!("{}", tptp_preamble_anthem_types); + + print_title("anthem axioms", section_separator); + + let tptp_preamble_anthem_types + = include_str!("output/tptp/preamble_axioms.tptp").trim_end(); + println!("{}", tptp_preamble_anthem_types); + + if !self.predicate_declarations.borrow().is_empty() + || !self.function_declarations.borrow().is_empty() + { + print_title("types", section_separator); + + if !self.predicate_declarations.borrow().is_empty() + { + println!("% predicate types") + } + + for predicate_declaration in self.predicate_declarations.borrow().iter() + { + println!("tff(type, type, {}).", + crate::output::tptp::display_predicate_declaration(predicate_declaration)); + } + + if !self.function_declarations.borrow().is_empty() + { + println!("% function types") + } + + for function_declaration in self.function_declarations.borrow().iter() + { + println!("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 + { + println!("% axioms for order of symbolic constants") + } + + if symbolic_constant.arity > 0 + { + // TODO: refactor + panic!("unexpected n-ary function declaration"); + } + + if let Some(last_symbolic_constant) = last_symbolic_constant + { + println!("tff(symbolic_constant_order, axiom, p__less__({}, {})).", + last_symbolic_constant.name, symbolic_constant.name); + } + + last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant)); + } + } + + 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", + }; + + print_title(title, section_separator); + section_separator = "\n"; + + let mut i = 0; + + for statement in statements.iter() + { + if let Some(ref description) = statement.description + { + println!("% {}", description); + } + + let name = match &statement.name + { + // TODO: refactor + Some(name) => name.clone(), + None => + { + i += 1; + format!("statement_{}", i) + }, + }; + + if output_format == crate::output::Format::TPTP + { + print!("tff({}, , ", name); + } + + print_formula(&statement.formula); + + if output_format == crate::output::Format::TPTP + { + print!(")."); + } + + println!(""); + } + } + } +} + +impl foliage::FindOrCreateFunctionDeclaration for Problem +{ + fn find_or_create_function_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc + { + let mut function_declarations = self.function_declarations.borrow_mut(); + + match function_declarations.iter().find(|x| x.name == name && x.arity == arity) + { + Some(declaration) => std::rc::Rc::clone(&declaration), + None => + { + let declaration = foliage::FunctionDeclaration + { + name: name.to_string(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); + + function_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new function declaration: {}/{}", name, arity); + + declaration + }, + } + } +} + +impl foliage::FindOrCreatePredicateDeclaration for Problem +{ + fn find_or_create_predicate_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc + { + let mut predicate_declarations = self.predicate_declarations.borrow_mut(); + + match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity) + { + Some(declaration) => std::rc::Rc::clone(&declaration), + None => + { + let declaration = foliage::PredicateDeclaration + { + name: name.to_string(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); + + predicate_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new predicate declaration: {}/{}", name, arity); + + declaration + }, + } + } +} + +impl crate::traits::AssignVariableDeclarationDomain for Problem +{ + fn assign_variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc, domain: crate::Domain) + { + let mut variable_declaration_domains = self.variable_declaration_domains.borrow_mut(); + + match variable_declaration_domains.get(variable_declaration) + { + Some(current_domain) => assert_eq!(*current_domain, domain, + "inconsistent variable declaration domain"), + None => + { + variable_declaration_domains + .insert(std::rc::Rc::clone(variable_declaration).into(), domain); + }, + } + } +} + +impl<'a, 'b> FormatContext<'a, 'b> +{ + fn variable_declaration_id(&self, + variable_declaration: &std::rc::Rc) + -> usize + { + let mut variable_declaration_ids = match self.variable_declaration_domains + .get(variable_declaration) + { + Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(), + Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(), + None => unreachable!("all variables should be declared at this point"), + }; + + match variable_declaration_ids.get(variable_declaration) + { + Some(id) => *id, + None => + { + let id = variable_declaration_ids.len(); + variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); + id + }, + } + } +} + +impl<'a, 'b> crate::traits::InputConstantDeclarationDomain for FormatContext<'a, 'b> +{ + fn input_constant_declaration_domain(&self, + declaration: &std::rc::Rc) -> crate::Domain + { + // Assume the program domain if not specified otherwise + self.input_constant_declaration_domains.get(declaration).map(|x| *x) + .unwrap_or(crate::Domain::Program) + } +} + +impl<'a, 'b> crate::traits::VariableDeclarationDomain for FormatContext<'a, 'b> +{ + fn variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc) + -> Option + { + self.variable_declaration_domains.get(variable_declaration) + .map(|x| *x) + } +} + +impl<'a, 'b> crate::traits::VariableDeclarationID for FormatContext<'a, 'b> +{ + fn variable_declaration_id(&self, + variable_declaration: &std::rc::Rc) + -> usize + { + use crate::traits::VariableDeclarationDomain; + + let mut variable_declaration_ids = match self.variable_declaration_domain( + variable_declaration) + { + Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(), + Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(), + None => panic!("all variables should be declared at this point"), + }; + + match variable_declaration_ids.get(variable_declaration) + { + Some(id) => + { + *id + } + None => + { + let id = variable_declaration_ids.len(); + variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id); + id + }, + } + } +} + +impl<'a, 'b> foliage::format::Format for FormatContext<'a, 'b> +{ + fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter, + variable_declaration: &std::rc::Rc) + -> std::fmt::Result + { + let id = self.variable_declaration_id(variable_declaration); + let domain = self.variable_declaration_domains.get(variable_declaration) + .expect("unspecified variable domain"); + + let prefix = match domain + { + crate::Domain::Integer => "N", + crate::Domain::Program => "X", + }; + + write!(formatter, "{}{}", prefix, id + 1) + } +} diff --git a/src/specification.rs b/src/specification.rs new file mode 100644 index 0000000..b73a1e4 --- /dev/null +++ b/src/specification.rs @@ -0,0 +1,36 @@ +/*#[derive(Clone, Copy, Eq, Hash, PartialEq)] +pub enum ProofDirection +{ + Forward, + Backward, +} + +#[derive(Eq, Hash, PartialEq)] +pub enum CompletionTarget +{ + Predicate(std::rc::Rc), + Constraint, +} + +pub struct CompletionFormula +{ + pub target: CompletionTarget, + pub formula: foliage::Formula, +} + +pub struct Lemma +{ + pub direction: Option, + pub formula: foliage::Formula, +} + +pub struct Specification +{ + pub axioms: foliage::Formulas, + pub lemmas: Vec, + pub assumptions: foliage::Formulas, + pub assertions: foliage::Formulas, + + pub input_constants: foliage::FunctionDeclarations, + pub input_predicates: foliage::PredicateDeclarations, +}*/ diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 6893980..c073975 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -1,47 +1,23 @@ -mod context; mod head_type; mod translate_body; -use context::*; use head_type::*; use translate_body::*; use crate::traits::AssignVariableDeclarationDomain as _; -struct StatementHandler +struct PredicateDefinitions { - context: Context, + pub parameters: std::rc::Rc, + pub definitions: Vec, } -impl StatementHandler -{ - fn new() -> Self - { - Self - { - context: Context::new(), - } - } -} +type Definitions = + std::collections::BTreeMap::, PredicateDefinitions>; -impl clingo::StatementHandler for StatementHandler +pub(crate) struct Translator<'p> { - fn on_statement(&mut self, statement: &clingo::ast::Statement) -> bool - { - match statement.statement_type() - { - clingo::ast::StatementType::Rule(ref rule) => - { - if let Err(error) = read_rule(rule, &self.context) - { - log::error!("could not translate input program: {}", error); - return false; - } - }, - _ => log::debug!("read statement (other kind)"), - } - - true - } + problem: &'p mut crate::Problem,// TODO: refactor + definitions: Definitions, } struct Logger; @@ -54,418 +30,301 @@ impl clingo::Logger for Logger } } -pub fn translate

(program_paths: &[P], - input_predicate_declarations: foliage::PredicateDeclarations, - input_constant_declaration_domains: crate::InputConstantDeclarationDomains, - output_format: crate::output::Format) - -> Result<(), crate::Error> -where - P: AsRef +impl<'p> clingo::StatementHandler for Translator<'p> { - let mut statement_handler = StatementHandler::new(); - - *statement_handler.context.input_predicate_declarations.borrow_mut() - = input_predicate_declarations.clone(); - *statement_handler.context.predicate_declarations.borrow_mut() - = input_predicate_declarations; - *statement_handler.context.function_declarations.borrow_mut() - = input_constant_declaration_domains.keys().map(std::rc::Rc::clone).collect(); - *statement_handler.context.input_constant_declaration_domains.borrow_mut() - = input_constant_declaration_domains; - - for input_predicate_declaration in statement_handler.context.input_predicate_declarations - .borrow().iter() + fn on_statement(&mut self, statement: &clingo::ast::Statement) -> bool { - log::info!("input predicate: {}/{}", input_predicate_declaration.name, - input_predicate_declaration.arity); + match statement.statement_type() + { + clingo::ast::StatementType::Rule(ref rule) => + { + if let Err(error) = self.read_rule(rule) + { + log::error!("could not translate input program: {}", error); + return false; + } + }, + _ => log::debug!("read statement (other kind)"), + } + + true + } +} + +impl<'p> Translator<'p> +{ + pub fn new(problem: &'p mut crate::Problem) -> Self + { + Self + { + problem, + definitions: Definitions::new(), + } } - for (input_constant_declaration, domain) in statement_handler.context - .input_constant_declaration_domains.borrow().iter() - { - log::info!("input constant: {} (domain: {:?})", input_constant_declaration.name, domain); - } - - // Read all input programs - for program_path in program_paths + pub fn translate

(&mut self, program_path: P) -> Result<(), crate::Error> + where + P: AsRef { + // Read input program let program = std::fs::read_to_string(program_path.as_ref()) - .map_err(|error| crate::Error::new_read_file(program_path.as_ref().to_path_buf(), error))?; + .map_err( + |error| crate::Error::new_read_file(program_path.as_ref().to_path_buf(), error))?; - clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX) + clingo::parse_program_with_logger(&program, self, &mut Logger, std::u32::MAX) .map_err(|error| crate::Error::new_translate(error))?; log::info!("read input program “{}”", program_path.as_ref().display()); - } - let context = statement_handler.context; - - for (predicate_declaration, definitions) in context.definitions.borrow().iter() - { - for definition in definitions.definitions.iter() + // TODO: reimplement + /* + for (predicate_declaration, predicate_definitions) in self.definitions.iter() { - log::debug!("definition({}/{}): {}.", predicate_declaration.name, predicate_declaration.arity, - foliage::format::display_formula(&definition.formula, &context)); - } - } - - let completed_definition = |predicate_declaration| - { - match context.definitions.borrow_mut().remove(predicate_declaration) - { - // This predicate symbol has at least one definition, so build the disjunction of those - Some(definitions) => + for definition in predicate_definitions.definitions.iter() { - let or_arguments = definitions.definitions.into_iter() - .map(|x| crate::existential_closure(x)) - .collect::>(); - let or = foliage::Formula::or(or_arguments); + log::debug!("definition({}/{}): {}.", predicate_declaration.name, + predicate_declaration.arity, + foliage::format::display_formula(&definition.formula, self.problem)); + } + }*/ - let head_arguments = definitions.head_atom_parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) - .collect::>(); + let completed_definition = |predicate_declaration, definitions: &mut Definitions, + problem: &crate::Problem| + { + match definitions.remove(predicate_declaration) + { + // This predicate symbol has at least one definition, so build the disjunction of those + Some(predicate_definitions) => + { + let or_arguments = predicate_definitions.definitions.into_iter() + .map(|x| crate::existential_closure(x)) + .collect::>(); + let or = foliage::Formula::or(or_arguments); - let head_predicate = foliage::Formula::predicate( - std::rc::Rc::clone(predicate_declaration), head_arguments); + let head_arguments = predicate_definitions.parameters.iter() + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .collect::>(); - let completed_definition = - foliage::Formula::if_and_only_if(vec![head_predicate, or]); + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(predicate_declaration), head_arguments); + + let completed_definition = + foliage::Formula::if_and_only_if(vec![head_predicate, or]); + + let scoped_formula = crate::ScopedFormula + { + free_variable_declarations: predicate_definitions.parameters, + formula: completed_definition, + }; + + crate::universal_closure(scoped_formula) + }, + // This predicate has no definitions, so universally falsify it + None => + { + let parameters = std::rc::Rc::new((0..predicate_declaration.arity) + .map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + problem.assign_variable_declaration_domain(&variable_declaration, + crate::Domain::Program); + variable_declaration + }) + .collect::>()); + + let head_arguments = parameters.iter() + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .collect(); + + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(predicate_declaration), head_arguments); + + let not = foliage::Formula::not(Box::new(head_predicate)); + + let scoped_formula = crate::ScopedFormula + { + free_variable_declarations: parameters, + formula: not, + }; + + crate::universal_closure(scoped_formula) + }, + } + }; + + for predicate_declaration in self.problem.predicate_declarations.borrow().iter() + { + let completed_definition = + completed_definition(predicate_declaration, &mut self.definitions, self.problem); + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Assumption, completed_definition) + .with_name(format!("completed_definition_{}_{}", predicate_declaration.name, + predicate_declaration.arity)) + .with_description(format!("completed definition of {}/{}", + predicate_declaration.name, predicate_declaration.arity)); + + self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions, + statement); + } + + Ok(()) + } + + fn read_rule(&mut self, rule: &clingo::ast::Rule) + -> Result<(), crate::Error> + { + let head_type = determine_head_type(rule.head(), self.problem)?; + + match &head_type + { + HeadType::SingleAtom(head_atom) + | HeadType::ChoiceWithSingleAtom(head_atom) => + { + if !self.definitions.contains_key(&head_atom.predicate_declaration) + { + let parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity) + .map(|_| + { + let variable_declaration = std::rc::Rc::new( + foliage::VariableDeclaration::new("".to_string())); + self.problem.assign_variable_declaration_domain(&variable_declaration, + crate::Domain::Program); + variable_declaration + }) + .collect()); + + self.definitions.insert( + std::rc::Rc::clone(&head_atom.predicate_declaration), + PredicateDefinitions + { + parameters, + definitions: vec![], + }); + } + + // TODO: refactor + let predicate_definitions = + self.definitions.get_mut(&head_atom.predicate_declaration).unwrap(); + + let parameters = std::rc::Rc::clone(&predicate_definitions.parameters); + let free_variable_declarations = std::cell::RefCell::new(vec![]); + let free_layer = + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); + let parameters_layer = + foliage::VariableDeclarationStackLayer::bound(&free_layer, parameters); + + let mut definition_arguments = + translate_body(rule.body(), self.problem, ¶meters_layer)?; + + // TODO: refactor + assert_eq!(predicate_definitions.parameters.len(), head_atom.arguments.len()); + + if let HeadType::ChoiceWithSingleAtom(_) = head_type + { + let head_arguments = predicate_definitions.parameters.iter() + .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) + .collect::>(); + + let head_predicate = foliage::Formula::predicate( + std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments); + + definition_arguments.push(head_predicate); + } + + let mut head_atom_arguments_iterator = head_atom.arguments.iter(); + + for parameter in predicate_definitions.parameters.iter() + { + let head_atom_argument = head_atom_arguments_iterator.next().unwrap(); + + let translated_head_term = crate::translate::common::choose_value_in_term( + head_atom_argument, std::rc::Rc::clone(parameter), self.problem, + ¶meters_layer)?; + + definition_arguments.push(translated_head_term); + } + + // TODO: refactor + let free_variable_declarations = match free_layer + { + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + => free_variable_declarations.into_inner(), + _ => unreachable!(), + }; + + let definition = match definition_arguments.len() + { + 1 => definition_arguments.pop().unwrap(), + 0 => foliage::Formula::true_(), + _ => foliage::Formula::and(definition_arguments), + }; + + let definition = crate::ScopedFormula + { + free_variable_declarations: std::rc::Rc::new(free_variable_declarations), + formula: definition, + }; + + // TODO: refactor + // TODO: reimplement + /* + log::debug!("translated rule with single atom in head: {}", + foliage::format::display_formula(&definition.formula, self.problem)); + */ + + predicate_definitions.definitions.push(definition); + }, + HeadType::IntegrityConstraint => + { + let free_variable_declarations = std::cell::RefCell::new(vec![]); + let free_layer = + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); + + let mut arguments = translate_body(rule.body(), self.problem, &free_layer)?; + + // TODO: refactor + let free_variable_declarations = match free_layer + { + foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) + => free_variable_declarations.into_inner(), + _ => unreachable!(), + }; + + let formula = match arguments.len() + { + 1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())), + 0 => foliage::Formula::false_(), + _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), + }; let scoped_formula = crate::ScopedFormula { - free_variable_declarations: definitions.head_atom_parameters, - formula: completed_definition, + free_variable_declarations: std::rc::Rc::new(free_variable_declarations), + formula, }; - crate::universal_closure(scoped_formula) + let integrity_constraint = crate::universal_closure(scoped_formula); + + // TODO: refactor + // TODO: reimplement + /* + log::debug!("translated integrity constraint: {}", + foliage::format::display_formula(&integrity_constraint, self.problem)); + */ + + let statement = crate::problem::Statement::new( + crate::problem::StatementKind::Assumption, integrity_constraint) + .with_name("integrity_constraint".to_string()) + .with_description("integrity constraint".to_string()); + + self.problem.add_statement(crate::problem::SectionKind::IntegrityConstraints, + statement); }, - // This predicate has no definitions, so universally falsify it - None => - { - let head_atom_parameters = std::rc::Rc::new((0..predicate_declaration.arity) - .map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) - .collect::>()); - - let head_arguments = head_atom_parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) - .collect(); - - let head_predicate = foliage::Formula::predicate( - std::rc::Rc::clone(predicate_declaration), head_arguments); - - let not = foliage::Formula::not(Box::new(head_predicate)); - - let scoped_formula = crate::ScopedFormula - { - free_variable_declarations: head_atom_parameters, - formula: not, - }; - - crate::universal_closure(scoped_formula) - }, - } - }; - - let predicate_declarations = context.predicate_declarations.borrow(); - let function_declarations = context.function_declarations.borrow(); - let input_constant_declaration_domains = context.input_constant_declaration_domains.borrow(); - let completed_definitions = predicate_declarations.iter() - // Don’t perform completion for any input predicate - .filter(|x| !context.input_predicate_declarations.borrow().contains(*x)) - .map(|x| (std::rc::Rc::clone(x), completed_definition(x))); - - // Earlier log messages may have assigned IDs to the variable declarations, so reset them - context.program_variable_declaration_ids.borrow_mut().clear(); - context.integer_variable_declaration_ids.borrow_mut().clear(); - - let print_title = |title, section_separator| - { - print!("{}{}", section_separator, "%".repeat(80)); - print!("\n% {}", title); - println!("\n{}", "%".repeat(80)); - }; - - let print_formula = |formula: &foliage::Formula| - { - match output_format - { - crate::output::Format::HumanReadable => print!("{}", - foliage::format::display_formula(formula, &context)), - crate::output::Format::TPTP => print!("{}", - crate::output::tptp::display_formula(formula, &context)), - } - }; - - let mut section_separator = ""; - - if output_format == crate::output::Format::TPTP - { - print_title("anthem types", section_separator); - section_separator = "\n"; - - let tptp_preamble_anthem_types - = include_str!("../output/tptp/preamble_types.tptp").trim_end(); - println!("{}", tptp_preamble_anthem_types); - - print_title("anthem axioms", section_separator); - - let tptp_preamble_anthem_types - = include_str!("../output/tptp/preamble_axioms.tptp").trim_end(); - println!("{}", tptp_preamble_anthem_types); - - if !predicate_declarations.is_empty() || !function_declarations.is_empty() - { - print_title("types", section_separator); - - if !predicate_declarations.is_empty() - { - println!("% predicate types") - } - - for predicate_declaration in &*predicate_declarations - { - println!("tff(type, type, {}).", - crate::output::tptp::display_predicate_declaration(predicate_declaration)); - } - - if !function_declarations.is_empty() - { - println!("% function types") - } - - for function_declaration in &*function_declarations - { - println!("tff(type, type, {}).", - crate::output::tptp::display_function_declaration(function_declaration, - &context)); - } + HeadType::Trivial => log::info!("skipping trivial rule"), } - let symbolic_constants = function_declarations.iter().filter( - |x| !input_constant_declaration_domains.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 - { - println!("% axioms for order of symbolic constants") - } - - if symbolic_constant.arity > 0 - { - return Err(crate::Error::new_logic("unexpected n-ary function declaration")); - } - - if let Some(last_symbolic_constant) = last_symbolic_constant - { - println!("tff(symbolic_constant_order, axiom, p__less__({}, {})).", - last_symbolic_constant.name, symbolic_constant.name); - } - - last_symbolic_constant = Some(std::rc::Rc::clone(symbolic_constant)); - } + Ok(()) } - - for (i, (predicate_declaration, completed_definition)) in completed_definitions.enumerate() - { - if i == 0 - { - print_title("completed definitions", section_separator); - } - - section_separator = "\n"; - - println!("% completed definition of {}/{}", predicate_declaration.name, - predicate_declaration.arity); - - if output_format == crate::output::Format::TPTP - { - print!("tff(completion_{}_{}, axiom, ", predicate_declaration.name, - predicate_declaration.arity); - } - - print_formula(&completed_definition); - - if output_format == crate::output::Format::TPTP - { - print!(")."); - } - - println!(""); - } - - for (i, integrity_constraint) in context.integrity_constraints.borrow().iter().enumerate() - { - if i == 0 - { - print_title("integrity constraints", section_separator); - } - - section_separator = "\n"; - - if output_format == crate::output::Format::TPTP - { - print!("tff(integrity_constraint, axiom, "); - } - - print_formula(&integrity_constraint); - - if output_format == crate::output::Format::TPTP - { - print!(")."); - } - - println!(""); - } - - Ok(()) -} - -fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::Error> -{ - let head_type = determine_head_type(rule.head(), context)?; - - match &head_type - { - HeadType::SingleAtom(head_atom) - | HeadType::ChoiceWithSingleAtom(head_atom) => - { - if !context.definitions.borrow().contains_key(&head_atom.predicate_declaration) - { - let head_atom_parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity) - .map(|_| - { - let variable_declaration = std::rc::Rc::new( - foliage::VariableDeclaration::new("".to_string())); - context.assign_variable_declaration_domain(&variable_declaration, - crate::Domain::Program); - variable_declaration - }) - .collect()); - - context.definitions.borrow_mut().insert( - std::rc::Rc::clone(&head_atom.predicate_declaration), - Definitions - { - head_atom_parameters, - definitions: vec![], - }); - } - - let mut definitions = context.definitions.borrow_mut(); - let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap(); - - let head_atom_parameters = std::rc::Rc::clone(&definitions.head_atom_parameters); - let free_variable_declarations = std::cell::RefCell::new(vec![]); - let free_layer = - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); - let head_atom_parameters_layer = foliage::VariableDeclarationStackLayer::bound( - &free_layer, head_atom_parameters); - - let mut definition_arguments = translate_body(rule.body(), context, - &head_atom_parameters_layer)?; - - assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len()); - - if let HeadType::ChoiceWithSingleAtom(_) = head_type - { - let head_arguments = definitions.head_atom_parameters.iter() - .map(|x| foliage::Term::variable(std::rc::Rc::clone(x))) - .collect::>(); - - let head_predicate = foliage::Formula::predicate( - std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments); - - definition_arguments.push(head_predicate); - } - - let mut head_atom_arguments_iterator = head_atom.arguments.iter(); - - for head_atom_parameter in definitions.head_atom_parameters.iter() - { - let head_atom_argument = head_atom_arguments_iterator.next().unwrap(); - - let translated_head_term = crate::translate::common::choose_value_in_term( - head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context, - &head_atom_parameters_layer)?; - - definition_arguments.push(translated_head_term); - } - - // TODO: refactor - let free_variable_declarations = match free_layer - { - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) - => free_variable_declarations.into_inner(), - _ => unreachable!(), - }; - - let definition = match definition_arguments.len() - { - 1 => definition_arguments.pop().unwrap(), - 0 => foliage::Formula::true_(), - _ => foliage::Formula::and(definition_arguments), - }; - - let definition = crate::ScopedFormula - { - free_variable_declarations: std::rc::Rc::new(free_variable_declarations), - formula: definition, - }; - - log::debug!("translated rule with single atom in head: {}", - foliage::format::display_formula(&definition.formula, context)); - - definitions.definitions.push(definition); - }, - HeadType::IntegrityConstraint => - { - let free_variable_declarations = std::cell::RefCell::new(vec![]); - let free_layer = - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations); - - let mut arguments = translate_body(rule.body(), context, &free_layer)?; - - // TODO: refactor - let free_variable_declarations = match free_layer - { - foliage::VariableDeclarationStackLayer::Free(free_variable_declarations) - => free_variable_declarations.into_inner(), - _ => unreachable!(), - }; - - let formula = match arguments.len() - { - 1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())), - 0 => foliage::Formula::false_(), - _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), - }; - - let scoped_formula = crate::ScopedFormula - { - free_variable_declarations: std::rc::Rc::new(free_variable_declarations), - formula, - }; - - let integrity_constraint = crate::universal_closure(scoped_formula); - - log::debug!("translated integrity constraint: {}", - foliage::format::display_formula(&integrity_constraint, context)); - - context.integrity_constraints.borrow_mut().push(integrity_constraint); - }, - HeadType::Trivial => log::info!("skipping trivial rule"), - } - - Ok(()) } diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index 4d1b3b5..1f0a1db 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -1,4 +1,4 @@ -pub(crate) struct Definitions +/*pub(crate) struct Definitions { pub head_atom_parameters: std::rc::Rc, pub definitions: Vec, @@ -192,4 +192,4 @@ impl foliage::format::Format for Context crate::output::human_readable::display_variable_declaration(self, formatter, variable_declaration) } -} +}*/ diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 9103d23..db60d46 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,3 +1,4 @@ +// TODO: rename context pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer) -> Result diff --git a/src/utils.rs b/src/utils.rs index b17d0ab..b7fed68 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -36,6 +36,14 @@ impl std::fmt::Display for Domain } } +#[derive(Clone, Copy, Eq, Hash, PartialEq)] +pub enum ProofDirection +{ + Forward, + Backward, + Both, +} + pub(crate) struct ScopedFormula { pub free_variable_declarations: std::rc::Rc, @@ -62,7 +70,7 @@ pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage } } -pub fn parse_predicate_declaration(input: &str) +/*pub fn parse_predicate_declaration(input: &str) -> Result, crate::Error> { let mut parts = input.split("/"); @@ -88,12 +96,12 @@ pub fn parse_predicate_declaration(input: &str) name: name.to_string(), arity, })) -} +}*/ pub type InputConstantDeclarationDomains = std::collections::BTreeMap, Domain>; -pub fn parse_constant_declaration(input: &str) +/*pub fn parse_constant_declaration(input: &str) -> Result<(std::rc::Rc, crate::Domain), crate::Error> { let mut parts = input.split(":"); @@ -123,4 +131,4 @@ pub fn parse_constant_declaration(input: &str) }); Ok((constant_declaration, domain)) -} +}*/