Add tests for #241

This adds the test cases from #241.

tests/issue241_a.lisp

@@ -0,0 +1,7 @@
+(defcolumns X)
+
+(defconstraint constraint-1 () (is-not-zero! (if (is-zero 1) 1 1)))
+(defconstraint constraint-2 () (eq! (is-not-zero! (if (is-zero X) 1 X)) 0))
+(defconstraint constraint-3 () (eq! (~and! (is-not-zero! (if (is-zero 0) 1 0)) 0) 0))
+(defconstraint constraint-4 () (is-not-zero! (if (is-zero 0) 1 0)))
+(defconstraint constraint-5 () (is-not-zero! (if (is-zero X) 1 X)))

tests/issue241_b.lisp

@@ -0,0 +1,6 @@
+(defcolumns X ST)
+
+;; ST ==> x != 1
+(defconstraint constraint-6 () (if-not-zero ST (neq! 1 (if (is-zero 0) X X))))
+;; ST ==> x != 0
+(defconstraint constraint-7 () (if-not-zero ST (neq! 0 (if (is-zero X) X X))))

tests/models.rs

@@ -230,6 +230,16 @@ static MODELS: &[Model] = &[
         cols: &["X"],
         oracle: Some(|_| false),
     },
+    Model {
+        name: "issue241_a",
+        cols: &["X"],
+        oracle: Some(|_| true),
+    },
+    Model {
+        name: "issue241_b",
+        cols: &["ST", "X"],
+        oracle: Some(issue241_b_oracle),
+    },
 ];
 
 // ===================================================================
@@ -251,9 +261,9 @@ fn arrays_1_oracle(tr: &Trace) -> bool {
     true
 }
 
-// // ===================================================================
-// // IsZero
-// // ===================================================================
+// ===================================================================
+// IsZero
+// ===================================================================
 
 #[allow(non_snake_case)]
 fn iszero_oracle(tr: &Trace) -> bool {
@@ -267,9 +277,9 @@ fn iszero_oracle(tr: &Trace) -> bool {
     true
 }
 
-// // ===================================================================
-// // Shift
-// // ===================================================================
+// ===================================================================
+// Shift
+// ===================================================================
 
 #[allow(non_snake_case)]
 fn shift_1_oracle(tr: &Trace) -> bool {
@@ -323,3 +333,20 @@ fn shift_5_oracle(tr: &Trace) -> bool {
     }
     true
 }
+
+// ===================================================================
+// Issue 241
+// ===================================================================
+
+#[allow(non_snake_case)]
+fn issue241_b_oracle(tr: &Trace) -> bool {
+    let (X, ST) = (tr.col("X"), tr.col("ST"));
+    for k in 0..tr.height() {
+        let c1 = ST[k] == 0 || X[k] != 1;
+        let c2 = ST[k] == 0 || X[k] != 0;
+        if !c1 || !c2 {
+            return false;
+        }
+    }
+    true
+}