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 b0bc70cd7aa987dcccbde4a2756a4d95b7350f48..8a1d674ed1182ecc8ee8ff92a76eaa72be2046e4 100755 (executable)
--- 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 f98c9ee84869e1ce0ba398aab4f9d1648a2923db..c887d1895e03de407b7b1c902eadd98adb125189 100644 (file)
--- 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)