Format option for translate command

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<PathBuf>,
     },
@@ -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,

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<Theory>, 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,36 @@ 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 transition_axioms = Theory {
+                        formulas: theory.prediates().into_iter().map(transition).collect(),
+                    };
                     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)
                 }
             }
 

src/syntax_tree/fol.rs

@@ -906,6 +906,14 @@ pub struct Theory {
 impl_node!(Theory, Format, TheoryParser);
 
 impl Theory {
+    pub fn prediates(&self) -> IndexSet<Predicate> {
+        let mut preds = IndexSet::new();
+        for formula in self {
+            preds.extend(formula.predicates())
+        }
+        preds
+    }
+
     pub fn replace_placeholders(self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
         self.into_iter()
             .map(|f| f.replace_placeholders(mapping))

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(),
         }
     }
 }