naming TPTP formulas uniquely in a naive way (with counters)

potassco · Nov 28, 2024 · d53ef72 · d53ef72
1 parent 4efd319
commit d53ef72
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 10 deletions.
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
@@ -963,12 +963,8 @@ impl_node!(AnnotatedFormula, Format, AnnotatedFormulaParser);
 impl AnnotatedFormula {
     pub fn into_problem_formula(self, role: problem::Role) -> problem::AnnotatedFormula {
         problem::AnnotatedFormula {
-            name: if self.name.is_empty() {
-                // TODO: Revisit default naming scheme!
-                self.role.to_string()
-            } else {
-                self.name
-            },
+            // TODO: Revisit default naming scheme!
+            name: self.name,
             role,
             formula: self.formula,
         }

diff --git a/src/verifying/problem/mod.rs b/src/verifying/problem/mod.rs
@@ -136,6 +136,20 @@ impl Problem {
         self
     }
 
+    // TODO: Improve naming scheme for formulas
+    pub fn create_unique_formula_names(mut self) -> Self {
+        let mut formulas = vec![];
+        for (i, f) in self.formulas.into_iter().enumerate() {
+            formulas.push(AnnotatedFormula {
+                name: format!("formula_{i}_{}", f.name),
+                role: f.role,
+                formula: f.formula,
+            });
+        }
+        self.formulas = formulas;
+        self
+    }
+
     pub fn axioms(&self) -> Vec<AnnotatedFormula> {
         self.formulas
             .iter()

diff --git a/src/verifying/task/external_equivalence.rs b/src/verifying/task/external_equivalence.rs
@@ -704,7 +704,8 @@ impl Task for AssembledExternalEquivalenceTask {
                         Problem::with_name(format!("forward_outline_{i}_{j}"))
                             .add_annotated_formulas(axioms.clone())
                             .add_annotated_formulas(std::iter::once(conjecture.clone()))
-                            .rename_conflicting_symbols(),
+                            .rename_conflicting_symbols()
+                            .create_unique_formula_names(),
                     );
                 }
                 axioms.append(&mut lemma.consequences.clone());
@@ -722,6 +723,7 @@ impl Task for AssembledExternalEquivalenceTask {
                     )
                     .add_annotated_formulas(self.forward_conclusions)
                     .rename_conflicting_symbols()
+                    .create_unique_formula_names()
                     .decompose(self.decomposition),
             );
         }
@@ -745,7 +747,8 @@ impl Task for AssembledExternalEquivalenceTask {
                         Problem::with_name(format!("backward_outline_{i}_{j}"))
                             .add_annotated_formulas(axioms.clone())
                             .add_annotated_formulas(std::iter::once(conjecture.clone()))
-                            .rename_conflicting_symbols(),
+                            .rename_conflicting_symbols()
+                            .create_unique_formula_names(),
                     );
                 }
                 axioms.append(&mut lemma.consequences.clone());
@@ -763,6 +766,7 @@ impl Task for AssembledExternalEquivalenceTask {
                     )
                     .add_annotated_formulas(self.backward_conclusions)
                     .rename_conflicting_symbols()
+                    .create_unique_formula_names()
                     .decompose(self.decomposition),
             );
         }

diff --git a/src/verifying/task/strong_equivalence.rs b/src/verifying/task/strong_equivalence.rs
@@ -105,7 +105,8 @@ impl Task for StrongEquivalenceTask {
                         role: Role::Conjecture,
                         formula,
                     })
-                    .rename_conflicting_symbols(),
+                    .rename_conflicting_symbols()
+                    .create_unique_formula_names(),
             );
         }
         if matches!(
@@ -129,7 +130,8 @@ impl Task for StrongEquivalenceTask {
                         role: Role::Conjecture,
                         formula,
                     })
-                    .rename_conflicting_symbols(),
+                    .rename_conflicting_symbols()
+                    .create_unique_formula_names(),
             );
         }