From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 29 Jul 2021 17:22:10 +0000 (-0300)
Subject: [proofs] Set BV solver to better proof-producing one when proofs on (#6903)
X-Git-Tag: cvc5-1.0.0~1428
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=63dfa2730bac42fed9dda6aa5fb3d57e6cadfcc0;p=cvc5.git

[proofs] Set BV solver to better proof-producing one when proofs on (#6903)

Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c7a2c8916..0a5c399ec 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -411,6 +411,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.bv.bvAssertInput = false;
   }
 
+  // If proofs are required and the user did not specify a specific BV solver,
+  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
+  if (options::produceProofs()
+      && options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL
+      && !opts.bv.bvSolverWasSetByUser
+      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+  {
+    Notice() << "Forcing internal bit-vector solver due to proof production."
+             << std::endl;
+    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+  }
+
   // whether we want to force safe unsat cores, i.e., if we are in the default
   // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =
diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2
index 741d77a19..3902f9c37 100644
--- a/test/regress/regress0/fp/issue-5524.smt2
+++ b/test/regress/regress0/fp/issue-5524.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --bv-solver=bitblast
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-fun fpv5 () Float32)
diff --git a/test/regress/regress1/aufbv/bug348.smtv1.smt2 b/test/regress/regress1/aufbv/bug348.smtv1.smt2
index 207da82c5..a1fc92d77 100644
--- a/test/regress/regress1/aufbv/bug348.smtv1.smt2
+++ b/test/regress/regress1/aufbv/bug348.smtv1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --bv-solver=bitblast
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)
diff --git a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
index d39ad79f4..7ef6ff8ef 100644
--- a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
+++ b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv
+; COMMAND-LINE: --cegqi-bv --bv-solver=bitblast
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
@@ -8,14 +8,13 @@
 (assert
  (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
  (exists ((v_nnf_34 (_ BitVec 32)))
-  (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6) 
+  (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6)
   (bvsle v_nnf_34 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_34) (_ bv1 32)))))))
 (assert
  (not
  (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
  (exists ((v_nnf_30 (_ BitVec 32)))
-  (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6) 
+  (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6)
   (bvsle v_nnf_30 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_30) (_ bv1 32))))))))
 (check-sat)
 (exit)
-
diff --git a/test/regress/regress2/bug394.smt2 b/test/regress/regress2/bug394.smt2
index c0c8ca48c..c32ca4ab8 100644
--- a/test/regress/regress2/bug394.smt2
+++ b/test/regress/regress2/bug394.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --bv-solver=bitblast
 ; EXPECT: sat
 ; EXPECT: unsat
 ; EXPECT: unsat