From 17683839737e8c7f34dda3a445398d3462aaaa41 Mon Sep 17 00:00:00 2001 From: janheuer Date: Wed, 25 Sep 2024 16:39:43 +0200 Subject: [PATCH 1/4] add predicates function to theory --- src/syntax_tree/fol.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index c501ecbd..ac596ce0 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -876,6 +876,14 @@ pub struct Theory { impl_node!(Theory, Format, TheoryParser); impl Theory { + pub fn prediates(&self) -> IndexSet { + let mut preds = IndexSet::new(); + for formula in self { + preds.extend(formula.predicates()) + } + preds + } + pub fn replace_placeholders(self, mapping: &IndexMap) -> Self { self.into_iter() .map(|f| f.replace_placeholders(mapping)) From c3334f5d5a1ce6aa2e28ea4e25512be62adfc658 Mon Sep 17 00:00:00 2001 From: janheuer Date: Wed, 25 Sep 2024 16:47:40 +0200 Subject: [PATCH 2/4] make transition public and change input --- src/verifying/task/strong_equivalence.rs | 33 ++++++++++++------------ 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/verifying/task/strong_equivalence.rs b/src/verifying/task/strong_equivalence.rs index 363b4d39..6f1fbc5d 100644 --- a/src/verifying/task/strong_equivalence.rs +++ b/src/verifying/task/strong_equivalence.rs @@ -28,29 +28,30 @@ pub struct StrongEquivalenceTask { pub break_equivalences: bool, } -impl StrongEquivalenceTask { - fn transition_axioms(&self) -> fol::Theory { - fn transition(p: asp::Predicate) -> fol::Formula { - let p: fol::Predicate = p.into(); - - let hp = gamma::here(p.clone().to_formula()); - let tp = gamma::there(p.to_formula()); +pub fn transition(p: fol::Predicate) -> fol::Formula { + let hp = gamma::here(p.clone().to_formula()); + let tp = gamma::there(p.to_formula()); - let variables = hp.free_variables(); + let variables = hp.free_variables(); - fol::Formula::BinaryFormula { - connective: fol::BinaryConnective::Implication, - lhs: hp.into(), - rhs: tp.into(), - } - .quantify(fol::Quantifier::Forall, variables.into_iter().collect()) - } + fol::Formula::BinaryFormula { + connective: fol::BinaryConnective::Implication, + lhs: hp.into(), + rhs: tp.into(), + } + .quantify(fol::Quantifier::Forall, variables.into_iter().collect()) +} +impl StrongEquivalenceTask { + fn transition_axioms(&self) -> fol::Theory { let mut predicates = self.left.predicates(); predicates.extend(self.right.predicates()); fol::Theory { - formulas: predicates.into_iter().map(transition).collect(), + formulas: predicates + .into_iter() + .map(|p| transition(p.into())) + .collect(), } } } From eb2780c17e5cd842d4ab38a8d09c5548bcee2861 Mon Sep 17 00:00:00 2001 From: janheuer Date: Wed, 25 Sep 2024 16:53:10 +0200 Subject: [PATCH 3/4] add format argument to translate command --- src/command_line/arguments.rs | 22 ++++++++++++ src/command_line/procedures.rs | 63 ++++++++++++++++++++++++++++++---- 2 files changed, 78 insertions(+), 7 deletions(-) diff --git a/src/command_line/arguments.rs b/src/command_line/arguments.rs index 219136a7..4ffe5160 100644 --- a/src/command_line/arguments.rs +++ b/src/command_line/arguments.rs @@ -28,6 +28,14 @@ pub enum Command { #[arg(long, value_enum)] with: Translation, + /// Output format + #[arg(long, value_enum, default_value_t)] + format: Format, + + /// Role of output formulas (only used for TPTP output) + #[arg(long, value_enum, default_value_t)] + role: Role, + /// The file to translate input: Option, }, @@ -100,6 +108,20 @@ pub enum Translation { TauStar, } +#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, ValueEnum)] +pub enum Format { + #[default] + Default, + TPTP, +} + +#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, ValueEnum)] +pub enum Role { + #[default] + Axiom, + Conjecture, +} + #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, ValueEnum)] pub enum Equivalence { Strong, diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index d4be68e6..83c2cb38 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -2,16 +2,22 @@ use { crate::{ analyzing::tightness::Tightness, command_line::{ - arguments::{Arguments, Command, Equivalence, Property, Translation}, + arguments::{Arguments, Command, Equivalence, Format, Property, Role, Translation}, files::Files, }, - syntax_tree::{asp, fol, Node as _}, + syntax_tree::{ + asp, + fol::{self, Theory}, + Node as _, + }, translating::{completion::completion, gamma::gamma, tau_star::tau_star}, verifying::{ + problem, prover::{vampire::Vampire, Prover, Report, Status, Success}, task::{ external_equivalence::ExternalEquivalenceTask, - strong_equivalence::StrongEquivalenceTask, Task, + strong_equivalence::{transition, StrongEquivalenceTask}, + Task, }, }, }, @@ -20,6 +26,40 @@ use { either::Either, }; +fn output_theory(theory: Theory, helper_axioms: Option, format: Format, role: Role) { + match format { + Format::Default => print!("{theory}"), + Format::TPTP => { + let role_string = match role { + Role::Axiom => "axiom", + Role::Conjecture => "conjecture", + }; + + let axioms = match helper_axioms { + Some(x) => x, + None => Theory { formulas: vec![] }, + }; + + let problem = problem::Problem::with_name("theory") + .add_theory(axioms, |i, formula| problem::AnnotatedFormula { + name: format!("helper_axiom_{i}"), + role: problem::Role::Axiom, + formula, + }) + .add_theory(theory, |i, formula| problem::AnnotatedFormula { + name: format!("{role_string}_{i}"), + role: match role { + Role::Axiom => problem::Role::Axiom, + Role::Conjecture => problem::Role::Conjecture, + }, + formula, + }); + + print!("{problem}"); + } + } +} + pub fn main() -> Result<()> { match Arguments::parse().command { Command::Analyze { property, input } => { @@ -35,28 +75,37 @@ pub fn main() -> Result<()> { Ok(()) } - Command::Translate { with, input } => { + Command::Translate { + with, + input, + format, + role, + } => { match with { Translation::Completion => { let theory = input.map_or_else(fol::Theory::from_stdin, fol::Theory::from_file)?; let completed_theory = completion(theory).context("the given theory is not completable")?; - print!("{completed_theory}") + output_theory(completed_theory, None, format, role) } Translation::Gamma => { let theory = input.map_or_else(fol::Theory::from_stdin, fol::Theory::from_file)?; + let mut transition_axioms = Theory { formulas: vec![] }; + for p in theory.prediates() { + transition_axioms.formulas.push(transition(p)); + } let gamma_theory = gamma(theory); - print!("{gamma_theory}") + output_theory(gamma_theory, Some(transition_axioms), format, role) } Translation::TauStar => { let program = input.map_or_else(asp::Program::from_stdin, asp::Program::from_file)?; let theory = tau_star(program); - print!("{theory}") + output_theory(theory, None, format, role) } } From 02148e2c94b7b2ea9661f0a0596047be8224ec29 Mon Sep 17 00:00:00 2001 From: janheuer Date: Tue, 1 Oct 2024 16:22:32 +0200 Subject: [PATCH 4/4] change computation of transition axioms --- src/command_line/procedures.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index 83c2cb38..07c03d57 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -93,10 +93,9 @@ pub fn main() -> Result<()> { Translation::Gamma => { let theory = input.map_or_else(fol::Theory::from_stdin, fol::Theory::from_file)?; - let mut transition_axioms = Theory { formulas: vec![] }; - for p in theory.prediates() { - transition_axioms.formulas.push(transition(p)); - } + let transition_axioms = Theory { + formulas: theory.prediates().into_iter().map(transition).collect(), + }; let gamma_theory = gamma(theory); output_theory(gamma_theory, Some(transition_axioms), format, role) }