adding representation of empty clauses

ufmg-smite · Nov 2, 2024 · 363c3aa · 363c3aa
1 parent b89bc0f
commit 363c3aa
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 9 deletions.
diff --git a/carcara/src/translation/alethe_signature/theory.rs b/carcara/src/translation/alethe_signature/theory.rs
@@ -8,6 +8,8 @@ use std::string::String;
 pub struct AletheTheory {
     // Built-in operators.
     pub cl: Symbol,
+    // To represent the empty clause.
+    pub empty_cl: Symbol,
     pub ite: Symbol,
 
     // Logical operators.
@@ -37,6 +39,7 @@ impl AletheTheory {
     pub fn new() -> Self {
         AletheTheory {
             cl: String::from("@cl"),
+            empty_cl: String::from("@empty_cl"),
             ite: String::from("ite"),
 
             // Logical operators.

diff --git a/carcara/src/translation/eunoia.rs b/carcara/src/translation/eunoia.rs
@@ -50,10 +50,10 @@ impl EunoiaTranslator {
 
     fn translate_commands(&mut self, command_list: &[ProofCommand]) {
         // To get a ProofIter object
+        // TODO: improve this
         let proof = Proof {
             premises: IndexSet::new(),
             constant_definitions: Vec::new(),
-            // TODO: ugly?
             commands: command_list.to_vec(),
         };
         // ProofIter objects to get commands indexed by pairs
@@ -451,13 +451,18 @@ impl EunoiaTranslator {
         // Vec<Rc<Term>>, though it represents an
         // invocation of Alethe's cl operator
         // TODO: we are always adding the conclusion clause
-        let conclusion: EunoiaTerm = EunoiaTerm::App(
-            self.alethe_signature.cl.clone(),
-            clause
-                .iter()
-                .map(|term| self.translate_term(term))
-                .collect(),
-        );
+        let conclusion: EunoiaTerm = if clause.is_empty() {
+            EunoiaTerm::Id(self.alethe_signature.empty_cl.clone())
+        } else {
+            // {!clause.is_empty()}
+            EunoiaTerm::App(
+                self.alethe_signature.cl.clone(),
+                clause
+                    .iter()
+                    .map(|term| self.translate_term(term))
+                    .collect(),
+            )
+        };
 
         // NOTE: not adding conclusion clause to this list
         let mut eunoia_arguments: Vec<EunoiaTerm> = Vec::new();

diff --git a/carcara/src/translation/tests/alethe_signature/theory.eo b/carcara/src/translation/tests/alethe_signature/theory.eo
@@ -4,6 +4,9 @@
 
 ; The famous Alethe cl
 (declare-const @cl (-> Bool Bool Bool) :right-assoc-nil false)
+; TODO: some better way to deal with empty clauses?
+(declare-const @empty_cl Bool)
+
 
 (declare-const ite (-> (! Type :var A :implicit) Bool A A A))
 (declare-const not (-> Bool Bool))

diff --git a/carcara/src/translation/tests/test_translate.rs b/carcara/src/translation/tests/test_translate.rs
@@ -86,7 +86,7 @@ fn test_small_example() {
          (step t2 (@cl (<= a 5.0) (> a 5.0)) :rule la_generic :args ( 1.0 1.0 ))\n\
          (assume h2 (not (= b 10.0)))\n\
          (assume h3 (not (<= a 5.0)))\n\
-         (step t3 (@cl) :rule resolution :premises ( t1 t2 h2 h3 ))\n",
+         (step t3 @empty_cl :rule resolution :premises ( t1 t2 h2 h3 ))\n",
         std::str::from_utf8(&buf_proof).unwrap()
     );
 }