From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Apr 2020 13:45:52 +0000 (-0500)
Subject: Allow eager bitblasting with solve bv as int in QF_NIA (#4373)
X-Git-Tag: cvc5-1.0.0~3344
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=286ed8f8a3d6aece0469e983e87626a25107608d;p=cvc5.git

Allow eager bitblasting with solve bv as int in QF_NIA (#4373)

This also updates the SMT COMP script to revert to our previous behavior.

This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.
---

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index b0bc70cd7..8a1d674ed 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -39,11 +39,11 @@ QF_NIA)
   trywith 60 --nl-ext-tplanes --decision=justification
   trywith 60 --no-nl-ext-tplanes --decision=internal
   # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
-  trywith 600 --solve-int-as-bv=2   --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=4   --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=8   --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=16  --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 1200 --solve-int-as-bv=32 --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   finishwith --nl-ext-tplanes --decision=internal
   ;;
 QF_NRA)
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index f98c9ee84..c887d1895 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -133,8 +133,19 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
 
   if (options::solveIntAsBV() > 0)
   {
+    // not compatible with incremental
+    if (options::incrementalSolving())
+    {
+      throw OptionException(
+          "solving integers as bitvectors is currently not supported "
+          "when solving incrementally.");
+    }
+    // Int to BV currently always eliminates arithmetic completely (or otherwise
+    // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
+    // are required.
     logic = logic.getUnlockedCopy();
     logic.enableTheory(THEORY_BV);
+    logic.disableTheory(THEORY_ARITH);
     logic.lock();
   }
 
@@ -565,7 +576,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       || logic.isTheoryEnabled(THEORY_SETS)
       // Non-linear arithmetic requires UF to deal with division/mod because
       // their expansion introduces UFs for the division/mod-by-zero case.
-      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())
+      // If we are eliminating non-linear arithmetic via solve-int-as-bv,
+      // then this is not required, since non-linear arithmetic will be
+      // eliminated altogether (or otherwise fail at preprocessing).
+      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+          && options::solveIntAsBV() == 0)
       // If division/mod-by-zero is not treated as a constant value in BV, we
       // need UF.
       || (logic.isTheoryEnabled(THEORY_BV)