From caab0a618e5e17229a177de6704debf8dbb2836e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 5 Feb 2020 01:10:33 +0100 Subject: [PATCH] Add option for input predicates --- src/error.rs | 8 ++ src/lib.rs | 1 + src/main.rs | 6 ++ src/output.rs | 2 +- src/translate/verify_properties.rs | 117 ++++++++++++--------- src/translate/verify_properties/context.rs | 5 + src/utils.rs | 32 ++++++ 7 files changed, 120 insertions(+), 51 deletions(-) diff --git a/src/error.rs b/src/error.rs index 8c6c942..4067f15 100644 --- a/src/error.rs +++ b/src/error.rs @@ -8,6 +8,7 @@ pub enum Kind DecodeIdentifier, Translate, ReadFile(std::path::PathBuf), + ParsePredicateDeclaration, } pub struct Error @@ -62,6 +63,11 @@ impl Error { Self::new(Kind::ReadFile(path)).with(source) } + + pub(crate) fn new_parse_predicate_declaration() -> Self + { + Self::new(Kind::ParsePredicateDeclaration) + } } impl std::fmt::Debug for Error @@ -79,6 +85,8 @@ 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::ParsePredicateDeclaration => write!(formatter, + "could not parse predicate declaration"), }?; if let Some(source) = &self.source diff --git a/src/lib.rs b/src/lib.rs index a192ad8..af4be3d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -8,3 +8,4 @@ mod utils; pub use error::Error; pub(crate) use utils::*; +pub use utils::parse_predicate_declaration; diff --git a/src/main.rs b/src/main.rs index 288cb31..bda6125 100644 --- a/src/main.rs +++ b/src/main.rs @@ -14,6 +14,10 @@ enum Command /// Output format (human-readable, tptp) #[structopt(long, default_value = "human-readable")] output_format: anthem::output::Format, + + /// Input predicates (examples: p/0, q/2) + #[structopt(long, parse(try_from_str = anthem::parse_predicate_declaration))] + input_predicates: Vec>, } } @@ -29,10 +33,12 @@ fn main() { input, output_format, + input_predicates, } => { if let Err(error) = anthem::translate::verify_properties::translate(&input, + input_predicates.into_iter().collect::(), output_format) { log::error!("could not translate input program: {}", error); diff --git a/src/output.rs b/src/output.rs index 74d2d8e..a52b3c9 100644 --- a/src/output.rs +++ b/src/output.rs @@ -1,7 +1,7 @@ pub(crate) mod human_readable; pub(crate) mod tptp; -#[derive(Debug)] +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] pub enum Format { HumanReadable, diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index bfb3814..ad2e816 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -54,13 +54,21 @@ impl clingo::Logger for Logger } } -pub fn translate

(program_paths: &[P], output_format: crate::output::Format) +pub fn translate

(program_paths: &[P], + input_predicate_declarations: foliage::PredicateDeclarations, + output_format: crate::output::Format) -> Result<(), crate::Error> where P: AsRef { 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; + + // Read all input programs for program_path in program_paths { let program = std::fs::read_to_string(program_path.as_ref()) @@ -68,6 +76,8 @@ where clingo::parse_program_with_logger(&program, &mut statement_handler, &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; @@ -147,69 +157,76 @@ where let predicate_declarations = context.predicate_declarations.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.variable_declaration_ids.borrow_mut().clear(); - match output_format + let print_formula = |formula: &foliage::Formula| { - crate::output::Format::HumanReadable => + match output_format { - let mut section_separator = ""; + crate::output::Format::HumanReadable => print!("{}", + crate::output::human_readable::display_formula(formula, None, &context)), + crate::output::Format::TPTP => print!("{}", + crate::output::tptp::display_formula(formula, &context)), + } + }; - if !predicate_declarations.is_empty() - { - println!("{}% completed definitions", section_separator); - section_separator = "\n"; - } + let mut section_separator = ""; - for (predicate_declaration, completed_definition) in completed_definitions - { - println!("%% completed definition of {}/{}\n{}", predicate_declaration.name, - predicate_declaration.arity, crate::output::human_readable::display_formula( - &completed_definition, None, &context)); - } - - if !context.integrity_constraints.borrow().is_empty() - { - println!("{}% integrity constraints", section_separator); - } - - for integrity_constraint in context.integrity_constraints.borrow().iter() - { - println!("{}", crate::output::human_readable::display_formula( - &integrity_constraint, None, &context)); - } - }, - crate::output::Format::TPTP => + for (i, (predicate_declaration, completed_definition)) in completed_definitions.enumerate() + { + if i == 0 { - let mut section_separator = ""; + println!("{}% completed definitions", section_separator); + } - if !predicate_declarations.is_empty() - { - println!("{}% completed definitions", section_separator); - section_separator = "\n"; - } + println!("%% completed definition of {}/{}", predicate_declaration.name, + predicate_declaration.arity); - for (predicate_declaration, completed_definition) in completed_definitions - { - println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name, - predicate_declaration.arity, crate::output::tptp::display_formula( - &completed_definition, &context)); - } + if output_format == crate::output::Format::TPTP + { + print!("tff(completion_{}_{}, axiom, ", predicate_declaration.name, + predicate_declaration.arity); + } - if !context.integrity_constraints.borrow().is_empty() - { - println!("{}% integrity constraints", section_separator); - } + print_formula(&completed_definition); - for integrity_constraint in context.integrity_constraints.borrow().iter() - { - println!("tff(integrity_constraint, axiom, {}).", - crate::output::tptp::display_formula(&integrity_constraint, &context)); - } - }, + if output_format == crate::output::Format::TPTP + { + print!(")."); + } + + println!(""); + + section_separator = "\n"; + } + + for (i, integrity_constraint) in context.integrity_constraints.borrow().iter().enumerate() + { + if i == 0 + { + println!("{}% integrity constraints", section_separator); + } + + 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!(""); + + section_separator = "\n"; } Ok(()) diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index 7781ecd..8458ec6 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -20,6 +20,8 @@ pub(crate) struct Context pub integrity_constraints: std::cell::RefCell, pub input_constant_declaration_domains: std::cell::RefCell, + pub input_predicate_declarations: std::cell::RefCell, + pub function_declarations: std::cell::RefCell, pub predicate_declarations: std::cell::RefCell, pub variable_declaration_stack: std::cell::RefCell, @@ -38,6 +40,9 @@ impl Context input_constant_declaration_domains: std::cell::RefCell::new(InputConstantDeclarationDomains::new()), + input_predicate_declarations: + std::cell::RefCell::new(foliage::PredicateDeclarations::new()), + function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()), predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()), variable_declaration_stack: diff --git a/src/utils.rs b/src/utils.rs index 7dc632c..3794f85 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -21,3 +21,35 @@ pub(crate) struct ScopedFormula pub free_variable_declarations: std::rc::Rc, pub formula: Box, } + +pub fn parse_predicate_declaration(input: &str) + -> Result, crate::Error> +{ + let mut parts = input.split("/"); + + let name = match parts.next() + { + Some(name) => name.to_string(), + None => return Err(crate::Error::new_parse_predicate_declaration()), + }; + + use std::str::FromStr; + + let arity = match parts.next() + { + Some(arity) + => usize::from_str(arity).map_err(|_| crate::Error::new_parse_predicate_declaration())?, + None => return Err(crate::Error::new_parse_predicate_declaration()), + }; + + if parts.next().is_some() + { + return Err(crate::Error::new_parse_predicate_declaration()); + } + + Ok(std::rc::Rc::new(foliage::PredicateDeclaration + { + name, + arity, + })) +}