Disable cegqi-bv when using sygus (#5124)

This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.

I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4ad198a82fe108ad83ad074ef1f0602e4a89d38a..79490045b3a73cc571b4c2c0e8d2a0c55a999391 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -963,6 +963,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::cegqiMidpoint.set(true);
     }
+    // must disable cegqi-bv since it may introduce witness terms, which
+    // cannot appear in synthesis solutions
+    if (!options::cegqiBv.wasSetByUser())
+    {
+      options::cegqiBv.set(false);
+    }
     if (options::sygusRepairConst())
     {
       if (!options::cegqi.wasSetByUser())

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bc45a3105a94508bd440e7adea511c180d878bee..c7bf666d657b84ed10e5cc4f414cf33bbbb7c0d0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1939,6 +1939,7 @@ set(regress_1_tests
   regress1/sygus/extract.sy
   regress1/sygus/fast-enum-backtrack.sy
   regress1/sygus/fg_polynomial3.sy
+  regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
   regress1/sygus/hd-01-d1-prog.sy
   regress1/sygus/hd-19-d1-prog-dup-op.sy

diff --git a/test/regress/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy b/test/regress/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
new file mode 100644 (file)
index 0000000..18a1426
--- /dev/null
+++ b/test/regress/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+
+(set-logic BV)
+
+(synth-fun inv ((s (_ BitVec 4)) (t (_ BitVec 4))) (_ BitVec 4))
+
+(declare-var s (_ BitVec 4))
+(declare-var t (_ BitVec 4))
+
+
+(define-fun l ( (s (_ BitVec 4)) (t (_ BitVec 4))) Bool 
+     (= (bvmul (inv s t) s) t)
+)
+(define-fun SC ((s (_ BitVec 4)) (t (_ BitVec 4))) Bool 
+    (= (bvand (bvor (bvneg s) s) t) t)
+)
+(constraint
+  (=> 
+    (SC s t)
+    (l s t)
+  )
+)
+
+; should not generate witness terms in solution
+(check-synth)

diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy
index fa98ef26be55a18a36022dceb21fd5a946550e6a..b8a23aba5a6e38f45caf71782e7e5de32b29c865 100644 (file)
--- a/test/regress/regress1/sygus/max2-bv.sy
+++ b/test/regress/regress1/sygus/max2-bv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-bv
 (set-logic BV)
 
 (synth-fun max2 ((x (_ BitVec 32)) (y (_ BitVec 32))) (_ BitVec 32))