Use cbqi-full for sygus (#2346)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1e8ae40339356b08d3b6264768ea0376a9a4e6e7..cabe825be87a1a2647c4055bbe96fcf7f1d79d3b 100644 (file)
--- 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 b3cb98bc523666ef9928dbf3dc33b30e7119fe56..1e0b36a3ca39051811c7e5df664a67ed0565caf0 100644 (file)
--- 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 08f64a92584c217ceafcb03419966a0f09d7c785..e773bf698791389eaa5d6ac06dbb5e2478e06d1e 100644 (file)
--- 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 (file)
index 0000000..297bd91
--- /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)
+
+