bv: Enable bitblast solver by default. (#6660)

This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index e5b96b54ae7b02ca700a89134329b14cadd58965..fcad51cebebeaf395ce88c84922fb8a67c06c9b2 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -227,7 +227,7 @@ name   = "Bitvector Theory"
   category   = "regular"
   long       = "bv-solver=MODE"
   type       = "BVSolver"
-  default    = "LAZY"
+  default    = "BITBLAST"
   help       = "choose bit-vector solver, see --bv-solver=help"
   help_mode  = "Bit-vector solvers."
 [[option.mode.BITBLAST]]

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 463a937fd218e340d25971cbd50afa174fe998a4..dc2c7e2a39f66b6165f0ec431f305b2dce0b8ac6 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -253,6 +253,28 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m,
       return false;
     }
   }
+
+  // In eager bitblast mode we also have to collect the model values for
+  // Boolean variables in the CNF stream.
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::vector<TNode> vars;
+    d_cnfStream->getBooleanVariables(vars);
+    for (TNode var : vars)
+    {
+      Assert(d_cnfStream->hasLiteral(var));
+      prop::SatLiteral bit = d_cnfStream->getLiteral(var);
+      prop::SatValue value = d_satSolver->value(bit);
+      Assert(value != prop::SAT_VALUE_UNKNOWN);
+      if (!m->assertEquality(
+              var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
+      {
+        return false;
+      }
+    }
+  }
+
   return true;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6036b021b4177da774a0d50e41b7c58c414762f1..707e5e43dc91f231b064b351f4416ac14fb99e1c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -235,6 +235,16 @@ set(regress_0_tests
   regress0/bv/bug440.smtv1.smt2
   regress0/bv/bug733.smt2
   regress0/bv/bug734.smt2
+  regress0/bv/bv-abstr-bug.smt2
+  regress0/bv/bv-abstr-bug2.smt2
+  regress0/bv/bv-int-collapse1.smt2
+  regress0/bv/bv-int-collapse2.smt2
+  regress0/bv/bv-options4.smt2
+  regress0/bv/bv-to-bool1.smtv1.smt2
+  regress0/bv/bv-to-bool2.smt2
+  regress0/bv/bv2nat-ground-c.smt2
+  regress0/bv/bv2nat-simp-range.smt2
+  regress0/bv/bv_to_int1.smt2
   regress0/bv/bv_to_int_5230_binary.smt2
   regress0/bv/bv_to_int_5230_missing_op.smt2
   regress0/bv/bv_to_int_5230_shift_const.smt2
@@ -242,20 +252,10 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5293_1.smt2
   regress0/bv/bv_to_int_5293_2.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+  regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
   regress0/bv/bv_to_int_zext.smt2
-  regress0/bv/bv_to_int1.smt2
-  regress0/bv/bv-abstr-bug.smt2
-  regress0/bv/bv-abstr-bug2.smt2
-  regress0/bv/bv-int-collapse1.smt2
-  regress0/bv/bv-int-collapse2.smt2
-  regress0/bv/bv-options4.smt2
-  regress0/bv/bv-to-bool1.smtv1.smt2
-  regress0/bv/bv-to-bool2.smt2
-  regress0/bv/bv2nat-ground-c.smt2
-  regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvcomp.cvc
   regress0/bv/bvmul-pow2-only.smt2
   regress0/bv/bvsimple.cvc
@@ -421,6 +421,7 @@ set(regress_0_tests
   regress0/bv/issue-4076.smt2
   regress0/bv/issue-4130.smt2
   regress0/bv/issue3621.smt2
+  regress0/bv/issue5396.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
@@ -660,6 +661,9 @@ set(regress_0_tests
   regress0/issue5540-2-dump-model.smt2
   regress0/issue5540-model-decls.smt2
   regress0/issue5550-num-children.smt2
+  regress0/issue5736.smt2
+  regress0/issue5743.smt2
+  regress0/issue5947.smt2
   regress0/issue6605-2-abd-triv.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
@@ -1501,6 +1505,7 @@ set(regress_1_tests
   regress1/bv/incorrect1.smtv1.smt2
   regress1/bv/issue3654.smt2
   regress1/bv/issue3776.smt2
+  regress1/bv/issue3958.smt2
   regress1/bv/min-pp-rewrite-error.smt2
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2

diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2
index a31036f7169d8e94ff733fe741a50acc321bcad2..1f5015d140518028b80f3bf51452624bea1f2165 100644 (file)
--- a/test/regress/regress0/bv/bv-int-collapse1.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)

diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2
index 5cf6a600c5d49fafa890c32316422f869b246fdb..d56188dad26b15e99e200f169663f0b43a8511d9 100644 (file)
--- a/test/regress/regress0/bv/bv-int-collapse2.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)

diff --git a/test/regress/regress0/bv/issue5396.smt2 b/test/regress/regress0/bv/issue5396.smt2
new file mode 100644 (file)
index 0000000..7f6d3ab
--- /dev/null
+++ b/test/regress/regress0/bv/issue5396.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-fun a () Int)
+(assert (= (bv2nat (bvor ((_ int2bv 3) a) ((_ int2bv 3) a))) 0))
+(assert (distinct ((_ extract 0 0) (bvsdiv ((_ int2bv 3) (bv2nat (bvmul ((_ int2bv 3) a) ((_ int2bv 3) a)))) ((_ int2bv 3) 1))) (_ bv0 1)))
+(check-sat)

diff --git a/test/regress/regress0/issue5736.smt2 b/test/regress/regress0/issue5736.smt2
new file mode 100644 (file)
index 0000000..dd4d4f9
--- /dev/null
+++ b/test/regress/regress0/issue5736.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q --check-unsat-cores --check-models
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-fun c () (_ BitVec 32))
+(declare-fun d () (_ BitVec 32))
+(declare-fun e () (_ BitVec 32))
+(declare-fun f () (_ BitVec 32))
+(declare-fun g () (Array (_ BitVec 32) (_ BitVec 32)))
+(assert (= (= d e) (= (select a c) f)))
+(assert (= g (store b (bvxor (_ bv4 32) f) (_ bv0 32))))
+(check-sat)

diff --git a/test/regress/regress0/issue5743.smt2 b/test/regress/regress0/issue5743.smt2
new file mode 100644 (file)
index 0000000..b53f0fb
--- /dev/null
+++ b/test/regress/regress0/issue5743.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --check-models -q
+(set-logic QF_AUFBV)
+(set-info :status sat)
+(declare-fun bv_22-0 () (_ BitVec 1))
+(declare-fun arr-8324605531633220487_-1461211092162269148-0 () (Array (_ BitVec 1) Bool))
+(assert (select arr-8324605531633220487_-1461211092162269148-0 (bvlshr bv_22-0 bv_22-0)))
+(check-sat)

diff --git a/test/regress/regress0/issue5947.smt2 b/test/regress/regress0/issue5947.smt2
new file mode 100644 (file)
index 0000000..4fbcfb0
--- /dev/null
+++ b/test/regress/regress0/issue5947.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q --check-models
+(set-logic QF_UFBVLIA)
+(set-info :status sat)
+(declare-fun f ((_ BitVec 3)) Int)
+(declare-fun x () (_ BitVec 3))
+(declare-fun y () (_ BitVec 3))
+(assert (not (= (f (bvxor x y)) (f (bvxnor x y)))))
+(check-sat)

diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2
index 50550f530d54e195cc655862fd647e4d4234d5dc..7e0da282ed2067e5f7c1c88c97a023ca442f35a0 100644 (file)
--- a/test/regress/regress1/bv/bv2nat-ground.smt2
+++ b/test/regress/regress1/bv/bv2nat-ground.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic QF_BVLIA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/bv/issue3958.smt2 b/test/regress/regress1/bv/issue3958.smt2
new file mode 100644 (file)
index 0000000..5ed7163
--- /dev/null
+++ b/test/regress/regress1/bv/issue3958.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const v4 Bool)
+(declare-const v8 Bool)
+(declare-const bv_21-0 (_ BitVec 21))
+(assert (or (= bv_21-0 bv_21-0 bv_21-0 (_ bv0 21) bv_21-0) v4))
+(assert (or (= (_ bv0 21) (bvudiv bv_21-0 bv_21-0) (_ bv0 21) (_ bv0 21)) v8))
+(check-sat)

diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 094a327726b23ac4378a16f45501bac0f81547e5..150320824b9d06ba349e7d586953629bec4405a3 100644 (file)
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -45,6 +45,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
   d_smtEngine->setLogic("QF_BV");
 
   d_smtEngine->setOption("bitblast", "eager");
+  d_smtEngine->setOption("bv-solver", "lazy");
   d_smtEngine->setOption("incremental", "false");
   // Notice that this unit test uses the theory engine of a created SMT
   // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized