Fixes for cbqi-bv (#1449)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e7736ebfca27592b73f0d0bcf87107282d976263..4336b7a0503a20ceecfb2a7fb8eded8f52c1d7cf 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1937,7 +1937,7 @@ void SmtEngine::setDefaults() {
       }
     }else{
       // only supported in pure arithmetic or pure BV
-      if (d_logic.isPure(THEORY_BV))
+      if (!d_logic.isPure(THEORY_BV))
       {
         options::cbqiNestedQE.set(false);
       }

diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index e4bc9adb84817937d999437c2372364a4e89bdd9..8a0412a800257fed59dbe487a57af589bcd6184d 100644 (file)
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -1887,66 +1887,62 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
     }
     for (std::pair<const Node, std::vector<Node> >& es : extract_map)
     {
-      if (es.second.size() > 1)
-      {
-        // sort based on the extract start position
-        std::vector<Node>& curr_vec = es.second;
+      // sort based on the extract start position
+      std::vector<Node>& curr_vec = es.second;
 
-        SortBvExtractInterval sbei;
-        std::sort(curr_vec.begin(), curr_vec.end(), sbei);
+      SortBvExtractInterval sbei;
+      std::sort(curr_vec.begin(), curr_vec.end(), sbei);
 
-        unsigned width = es.first.getType().getBitVectorSize();
+      unsigned width = es.first.getType().getBitVectorSize();
 
-        // list of points b such that:
-        //   b>0 and we must start a segment at (b-1)  or  b==0
-        std::vector<unsigned> boundaries;
-        boundaries.push_back(width);
-        boundaries.push_back(0);
+      // list of points b such that:
+      //   b>0 and we must start a segment at (b-1)  or  b==0
+      std::vector<unsigned> boundaries;
+      boundaries.push_back(width);
+      boundaries.push_back(0);
 
-        Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
-        for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+      Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
+      for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+      {
+        Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
+        BitVectorExtract e =
+            curr_vec[i].getOperator().getConst<BitVectorExtract>();
+        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+            == boundaries.end())
         {
-          Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i]
-                               << std::endl;
-          BitVectorExtract e =
-              curr_vec[i].getOperator().getConst<BitVectorExtract>();
-          if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
-              == boundaries.end())
-          {
-            boundaries.push_back(e.high + 1);
-          }
-          if (std::find(boundaries.begin(), boundaries.end(), e.low)
-              == boundaries.end())
-          {
-            boundaries.push_back(e.low);
-          }
+          boundaries.push_back(e.high + 1);
         }
-        std::sort(boundaries.rbegin(), boundaries.rend());
-
-        // make the extract variables
-        std::vector<Node> children;
-        for (unsigned i = 1; i < boundaries.size(); i++)
+        if (std::find(boundaries.begin(), boundaries.end(), e.low)
+            == boundaries.end())
         {
-          Assert(boundaries[i - 1] > 0);
-          Node ex = bv::utils::mkExtract(
-              es.first, boundaries[i - 1] - 1, boundaries[i]);
-          Node var =
-              nm->mkSkolem("ek",
-                           ex.getType(),
-                           "variable to represent disjoint extract region");
-          Node ceq_lem = var.eqNode(ex);
-          Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl;
-          new_lems.push_back(ceq_lem);
-          children.push_back(var);
-          vars.push_back(var);
+          boundaries.push_back(e.low);
         }
+      }
+      std::sort(boundaries.rbegin(), boundaries.rend());
 
-        Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
-        Assert(conc.getType() == es.first.getType());
-        Node eq_lem = conc.eqNode(es.first);
-        Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
-        new_lems.push_back(eq_lem);
+      // make the extract variables
+      std::vector<Node> children;
+      for (unsigned i = 1; i < boundaries.size(); i++)
+      {
+        Assert(boundaries[i - 1] > 0);
+        Node ex = bv::utils::mkExtract(
+            es.first, boundaries[i - 1] - 1, boundaries[i]);
+        Node var =
+            nm->mkSkolem("ek",
+                         ex.getType(),
+                         "variable to represent disjoint extract region");
+        Node ceq_lem = var.eqNode(ex);
+        Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl;
+        new_lems.push_back(ceq_lem);
+        children.push_back(var);
+        vars.push_back(var);
       }
+
+      Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
+      Assert(conc.getType() == es.first.getType());
+      Node eq_lem = conc.eqNode(es.first);
+      Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
+      new_lems.push_back(eq_lem);
       Trace("cegqi-bv-pp") << "...finished processing extracts for term "
                             << es.first << std::endl;
     }

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 668593842abe8024433cc0f74f95ce8bf04a2e32..bd2b8e78e1f38180b6f7214b838eb77f159d899e 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -744,7 +744,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
     }else{
       //this should never happen for monotonic selection strategies
       Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
-      Assert( !options::cbqiNestedQE() || options::cbqiAll() );
       return false;
     }
   }

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index bb43d6c1c6eea141c9f94d8f1d7ec044738ac76f..a8c25ae5a75115e46cbf7f2a498394963beb35b4 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -134,7 +134,8 @@ TESTS =     \
        javafe.ast.WhileStmt.447.smt2 \
        clock-10.smt2 \
        javafe.tc.FlowInsensitiveChecks.682.smt2 \
-       javafe.tc.CheckCompilationUnit.001.smt2
+       javafe.tc.CheckCompilationUnit.001.smt2 \
+       model_6_1_bv.smt2
  
 
 # regression can be solved with --finite-model-find --fmf-inst-engine

diff --git a/test/regress/regress0/quantifiers/model_6_1_bv.smt2 b/test/regress/regress0/quantifiers/model_6_1_bv.smt2
new file mode 100644 (file)
index 0000000..011430b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/model_6_1_bv.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --cbqi-nested-qe
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun lambda () (_ BitVec 32))
+(declare-fun lambdaprime () (_ BitVec 32))
+(declare-fun x5 () (_ BitVec 32))
+(declare-fun x4 () (_ BitVec 32))
+(declare-fun bool.b22 () Bool)
+(declare-fun bool.b7 () Bool)
+(declare-fun bool.b5 () Bool)
+(declare-fun bool.b6 () Bool)
+(assert (forall ((?lambda (_ BitVec 32))) (or (or (exists ((?lambdaprime (_ BitVec 32))) (let ((?v_1 (not bool.b22)) (?v_3 (not bool.b7)) (?v_4 (not bool.b5))) (let ((?v_2 (and ?v_4 (not bool.b6))) (?v_0 (bvmul (bvneg (_ bv1 32)) (bvadd x4 (bvmul (_ bv30 32) ?lambdaprime))))) (and (and (bvsle (_ bv0 32) ?lambdaprime) (bvsle ?lambdaprime ?lambda)) (not (and (not (bvsle (bvmul (bvneg (_ bv1 32)) (bvadd x5 (bvmul (_ bv1 32) ?lambdaprime))) (bvneg (_ bv10 32)))) (and (and (not (and (bvsle ?v_0 (bvneg (_ bv4100 32))) (and ?v_1 (and ?v_3 ?v_2)))) (not (and (bvsle ?v_0 (bvneg (_ bv4500 32))) (and ?v_1 (and bool.b7 ?v_2))))) (not (and (bvsle ?v_0 (bvneg (_ bv4910 32))) (and ?v_1 (and ?v_3 (and ?v_4 bool.b6)))))))))))) (bvslt ?lambda (_ bv0 32))) (not (and (not bool.b22) (and (not bool.b7) (and bool.b5 (not bool.b6))))))))
+(check-sat)
+(exit)