From 290f2a718a8ebe9532239fa53fabc9763564b5dc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 21 Aug 2018 12:10:38 -0500
Subject: [PATCH] Use cbqi-full for sygus (#2346)

---
 src/smt/smt_engine.cpp                        |  6 ++++
 .../sygus/ce_guided_instantiation.cpp         | 32 +++++++++++++------
 test/regress/Makefile.tests                   |  1 +
 test/regress/regress1/sygus/max2-bv.sy        | 26 +++++++++++++++
 4 files changed, 55 insertions(+), 10 deletions(-)
 create mode 100644 test/regress/regress1/sygus/max2-bv.sy

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1e8ae4033..cabe825be 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1934,6 +1934,7 @@ void SmtEngine::setDefaults() {
       options::ceGuidedInst.set( true );
     }
   }
+  // if sygus is enabled, set the defaults for sygus
   if( options::ceGuidedInst() ){
     //counterexample-guided instantiation for sygus
     if( !options::cegqiSingleInvMode.wasSetByUser() ){
@@ -1945,6 +1946,11 @@ void SmtEngine::setDefaults() {
     if( !options::instNoEntail.wasSetByUser() ){
       options::instNoEntail.set( false );
     }
+    if (!options::cbqiFullEffort.wasSetByUser())
+    {
+      // should use full effort cbqi for single invocation and repair const
+      options::cbqiFullEffort.set(true);
+    }
     if (options::sygusRew())
     {
       options::sygusRewSynth.set(true);
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index b3cb98bc5..1e0b36a3c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -267,20 +267,32 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
   if( !conj->needsRefinement() ){
     Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
-    std::vector<Node> clems;
-    conj->doSingleInvCheck(clems);
-    if (!clems.empty())
+    if (conj->isSingleInvocation())
     {
-      d_last_inst_si = true;
-      for (const Node& lem : clems)
+      std::vector<Node> clems;
+      conj->doSingleInvCheck(clems);
+      if (!clems.empty())
       {
-        Trace("cegqi-lemma")
-            << "Cegqi::Lemma : single invocation instantiation : " << lem
+        d_last_inst_si = true;
+        for (const Node& lem : clems)
+        {
+          Trace("cegqi-lemma")
+              << "Cegqi::Lemma : single invocation instantiation : " << lem
+              << std::endl;
+          d_quantEngine->addLemma(lem);
+        }
+        d_statistics.d_cegqi_si_lemmas += clems.size();
+        Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
+      }
+      else
+      {
+        // This can happen for non-monotonic instantiation strategies. We
+        // set --cbqi-full to ensure that for most strategies (e.g. BV), we
+        // are using a monotonic strategy.
+        Trace("cegqi-warn")
+            << "  ...FAILED to add cbqi instantiation for single invocation!"
             << std::endl;
-        d_quantEngine->addLemma(lem);
       }
-      d_statistics.d_cegqi_si_lemmas += clems.size();
-      Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
       return;
     }
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 08f64a925..e773bf698 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1549,6 +1549,7 @@ REG1_TESTS = \
 	regress1/sygus/list-head-x.sy \
 	regress1/sygus/logiccell_help.sy \
 	regress1/sygus/max.sy \
+	regress1/sygus/max2-bv.sy \
 	regress1/sygus/multi-fun-polynomial2.sy \
 	regress1/sygus/nflat-fwd-3.sy \
 	regress1/sygus/nflat-fwd.sy \
diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy
new file mode 100644
index 000000000..297bd9179
--- /dev/null
+++ b/test/regress/regress1/sygus/max2-bv.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic BV)
+
+(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32)
+)
+
+(declare-var x (BitVec 32))
+
+(declare-var y (BitVec 32))
+
+(constraint 
+(bvuge (max2 x y) x)
+)
+
+(constraint 
+(bvuge (max2 x y) y)
+)
+
+(constraint 
+(or (= x (max2 x y)) (= y (max2 x y)))
+)
+
+(check-synth)
+
+
-- 
2.30.2