From aacc90c1234c488f49814fae6dbf0e720e2dfa88 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Sep 2020 14:56:52 -0500
Subject: [PATCH] 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).
---
 src/smt/set_defaults.cpp                      |  6 +++++
 test/regress/CMakeLists.txt                   |  1 +
 ...ind_inv_eq_bvmul_4bit_withoutgrammar-v2.sy | 26 +++++++++++++++++++
 test/regress/regress1/sygus/max2-bv.sy        |  2 +-
 4 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4ad198a82..79490045b 100644
--- 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 bc45a3105..c7bf666d6 100644
--- 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
index 000000000..18a1426d5
--- /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 fa98ef26b..b8a23aba5 100644
--- 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))
-- 
2.30.2