Cegis-specific infrastructure (#1933)

3 files changed, 76 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c0f1cf315..f8fdd4a18 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1480,6 +1480,7 @@ REG1_TESTS = \
 	regress1/sygus/dt-test-ns.sy \
 	regress1/sygus/dup-op.sy \
 	regress1/sygus/fg_polynomial3.sy \
+	regress1/sygus/find_sc_bvult_bvnot.sy \
 	regress1/sygus/hd-01-d1-prog.sy \
 	regress1/sygus/hd-19-d1-prog-dup-op.sy \
 	regress1/sygus/hd-sdiv.sy \
diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
index 32e4723aa..ce437bc34 100644
--- a/test/regress/regress1/sygus/VC22_a.sy
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --cegis-sample=use
 (set-logic LIA)
 
 (synth-fun f ((x1 Int) (x2 Int)) Int
diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy
new file mode 100644
index 000000000..e994c2a5b
--- /dev/null
+++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy
@@ -0,0 +1,74 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --cegis-sample=trust
+(set-logic BV)
+
+; we test --cegis-sample=trust since we can exhaustively sample BV4
+
+(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool
+  ((Start Bool (
+     true
+     false
+     (not Start)
+     (and Start Start)
+     (or Start Start)
+;     (=> Start Start)
+     (= StartBv StartBv)
+     (bvult StartBv StartBv)
+     (bvslt StartBv StartBv)
+     (bvuge StartBv StartBv)
+     (bvsge StartBv StartBv)
+   ))
+   (StartBv (BitVec 4) (
+     s
+     t
+     #x0
+     #x8 ; min_val
+     #x7 ; max_val
+     (bvneg  StartBv)
+     (bvnot  StartBv)
+     (bvadd  StartBv StartBv)
+     (bvsub  StartBv StartBv)
+     (bvand  StartBv StartBv)
+     (bvlshr StartBv StartBv)
+     (bvor   StartBv StartBv)
+     (bvshl  StartBv StartBv)
+   ))
+))
+
+(declare-var s (BitVec 4))
+(declare-var t (BitVec 4))
+(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+  (ite (= b #x0) #xF (bvudiv a b))
+)
+(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
+  (ite (= b #x0) a (bvurem a b))
+)
+(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool
+(bvult (bvnot x) t)
+)
+(constraint
+  (=
+   (or
+    (case #x0 s t)
+    (case #x1 s t)
+    (case #x2 s t)
+    (case #x3 s t)
+    (case #x4 s t)
+    (case #x5 s t)
+    (case #x6 s t)
+    (case #x7 s t)
+    (case #x8 s t)
+    (case #x9 s t)
+    (case #xA s t)
+    (case #xB s t)
+    (case #xC s t)
+    (case #xD s t)
+    (case #xE s t)
+    (case #xF s t)
+   )
+   (SC s t)
+  )
+)
+
+(check-synth)