From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 4 Jun 2021 13:30:35 +0000 (-0700)
Subject: bv: Enable bitblast solver by default. (#6660)
X-Git-Tag: cvc5-1.0.0~1641
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=125b1c56d64b6dde1638565152b86950ef3c1342;p=cvc5.git

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 e5b96b54a..fcad51ceb 100644
--- 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 463a937fd..dc2c7e2a3 100644
--- 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 6036b021b..707e5e43d 100644
--- 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 a31036f71..1f5015d14 100644
--- 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 5cf6a600c..d56188dad 100644
--- 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
index 000000000..7f6d3ab38
--- /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
index 000000000..dd4d4f951
--- /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
index 000000000..b53f0fbef
--- /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
index 000000000..4fbcfb00b
--- /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 50550f530..7e0da282e 100644
--- 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
index 000000000..5ed71630d
--- /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 094a32772..150320824 100644
--- 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