Add pivots when elaborate drup

Author: Tiago Campos

carcara.code-workspace

@@ -1,9 +1,11 @@
 {
 	"folders": [
 		{
+			"name": "carcara",
 			"path": "."
 		},
 		{
+			"name": "cvc5",
 			"path": "../cvc5"
 		}
 	],

carcara/src/checker/rules/drup.rs

@@ -17,3 +17,59 @@ pub fn drup(
         Err(err) => Err(CheckerError::DrupFormatError(err))
     }
 }
+
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn drup() {
+        test_cases! {
+            definitions = "
+                (declare-const a Bool)
+                (declare-const b Bool)
+                (declare-const c Bool)
+                (declare-const d Bool)
+                (declare-const e Bool)
+            ",
+            "Simple working examples" {
+                "(assume a0 (or a c))
+                (assume a1 (or a (not c) d))
+                (assume a2 (or (not d) e))
+                (assume a3 (or (not d) (not e)))
+                (assume a4 (not a))
+                (assume a5 (not b))
+                (step t0 (cl a c) :rule or :premises (a0))
+                (step t1 (cl a (not c) d) :rule or :premises (a1))
+                (step t2 (cl (not d) e) :rule or :premises (a2))
+                (step t3 (cl (not d) (not e)) :rule or :premises (a3))
+                (step t4 (cl a b) :rule drup :premises (t0 t1 t2 t3) :args ((cl a b)))": true,
+
+                "
+                (assume a1 (not a))
+                (assume a2 (not b))
+                (assume a3 (or a b))
+                (step t0 (cl a b) :rule or :premises (a3))
+                (step t1 (cl) :rule drup :premises (a1 a2 t0) :args ((cl)))": true,
+            }
+
+            "Simple false-working examples" {
+                "(assume a0 (or a c))
+                (assume a1 (or a (not c) d))
+                (assume a2 (or (not d) e))
+                (assume a4 (not a))
+                (assume a5 (not b))
+                (step t0 (cl a c) :rule or :premises (a0))
+                (step t1 (cl a (not c) d) :rule or :premises (a1))
+                (step t2 (cl (not d) e) :rule or :premises (a2))
+                (step t4 (cl a) :rule drup :premises (t0 t1 t2) :args ((cl a b)))": false,
+
+                "
+                (assume a1 (not a))
+                (assume a3 (or a b))
+                (step t0 (cl a b) :rule or :premises (a3))
+                (step t1 (cl) :rule drup :premises (a1 t0) :args ((cl)))": false,
+            }
+
+        }
+    }
+}

carcara/src/drup.rs

@@ -31,10 +31,10 @@ pub enum DrupFormatError {
     #[error("couldn't find conclusion term in the premise clauses")]
     NoConclusionInPremise,
     #[error(
-        "couldn't elaborate drup because bottom wasn't derived from the premises and argument"
+        "couldn't elaborate drup because bottom wasn't derived from the premises and the argument"
     )]
     NoFinalBottomInDrup,
-    #[error("couldn't elaborate drup because the argument might not be in RUP or the premises derive bottom alone")]
+    #[error("couldn't elaborate drup because the argument might not be in RUP")]
     PotentialNoDrupFormat,
 }
 

carcara/src/elaborator/drup.rs

@@ -13,6 +13,7 @@ pub fn elaborate_drup(
     #[derive(Debug)]
     enum ResolutionStep<'a> {
         Resolvent(
+            &'a(bool, Rc<Term>),
             u64,
             u64,
             (Vec<Rc<Term>>, IndexSet<(bool, &'a Rc<Term>)>, u64),
@@ -95,6 +96,7 @@ pub fn elaborate_drup(
                         let resolvent_hash = hash_term(pool, resolvent.as_slice());
 
                         resolutions.push(ResolutionStep::Resolvent(
+                            pivot,
                             rup[i].1,
                             rup[i + 1].1,
                             (resolvent, resolvent_indexset.clone(), resolvent_hash),
@@ -108,7 +110,7 @@ pub fn elaborate_drup(
                 }
 
                 match &resolutions[resolutions.len() - 1] {
-                    ResolutionStep::Resolvent(_, _, (resolvent, _, _)) => {
+                    ResolutionStep::Resolvent(_, _, _, (resolvent, _, _)) => {
                         if resolvent.len() > 0 {
                             return Err(CheckerError::DrupFormatError(
                                 DrupFormatError::NoFinalBottomInDrup,
@@ -125,7 +127,7 @@ pub fn elaborate_drup(
                 }
 
                 resolutions.retain(|step| match step {
-                    ResolutionStep::Resolvent(_, _, (resolvent, _, _)) => {
+                    ResolutionStep::Resolvent(_, _, _, (resolvent, _, _)) => {
                         resolvent.len() > 0 || rup_clause.len() == 0
                     }
                     ResolutionStep::UnChanged(_, _) => false, // Since unchanged are trivally avaliable we can ignore them
@@ -134,6 +136,7 @@ pub fn elaborate_drup(
                 for (i, resolution_step) in resolutions.iter().enumerate() {
                     match resolution_step {
                         ResolutionStep::Resolvent(
+                            pivot,
                             c,
                             d,
                             (resolvent, resolvent_indexset, resolvent_hash),
@@ -151,7 +154,7 @@ pub fn elaborate_drup(
                                     (*premises.get(d).unwrap()).clone(),
                                 ],
                                 discharge: Vec::new(),
-                                args: Vec::new(),
+                                args: vec![pivot.1.clone(), pool.bool_constant(pivot.0)],
                                 previous_step: None,
                             }));
 

cli/src/main.rs

@@ -239,7 +239,7 @@ struct ElaborationOptions {
         arg_enum,
         long,
         multiple = true,
-        default_values = &["polyeq", "lia-generic", "reordering", "local", "uncrowd", "hole"]
+        default_values = &["polyeq", "lia-generic", "local", "uncrowd", "reordering", "hole"]
     )]
     pipeline: Vec<ElaborationStep>,
 }