Int2BV fail on demand (#4079)

This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 4c781d47cf1fd17541e321245860ab11e6909e52..b46253851bdf07a3544935a5574f3906926e785e 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 --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
+  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
   finishwith --nl-ext-tplanes --decision=internal
   ;;
 QF_NRA)

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 372df90ced1949be60edd826c63dc529b55517aa..9fa9a0c05fa6f06e0b6bb96be8031b88d32d97ae 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -44,6 +44,20 @@ struct intToBV_stack_element
   intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {}
 }; /* struct intToBV_stack_element */
 
+bool childrenTypesChanged(Node n, NodeMap& cache) {
+  bool result = false;
+  for (Node child : n) {
+    TypeNode originalType = child.getType();
+    TypeNode newType = cache[child].getType();
+    if (! newType.isSubtypeOf(originalType)) {
+      result = true;
+      break;
+    }
+  }
+  return result;
+}
+
+
 Node intToBVMakeBinary(TNode n, NodeMap& cache)
 {
   // Do a topological sort of the subexpressions and substitute them
@@ -84,6 +98,10 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
       else
       {
         NodeBuilder<> builder(current.getKind());
+        if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          builder << current.getOperator();
+        }
+
         for (unsigned i = 0; i < current.getNumChildren(); ++i)
         {
           Assert(cache.find(current[i]) != cache.end());
@@ -203,13 +221,12 @@ Node intToBV(TNode n, NodeMap& cache)
           case kind::EQUAL:
           case kind::ITE: break;
           default:
-            if (Theory::theoryOf(current) == THEORY_BOOL)
-            {
-              break;
-            }
-            throw TypeCheckingException(
+            if (childrenTypesChanged(current, cache)) {
+              throw TypeCheckingException(
                 current.toExpr(),
                 string("Cannot translate to BV: ") + current.toString());
+            }
+            break;
         }
         for (unsigned i = 0; i < children.size(); ++i)
         {
@@ -229,6 +246,9 @@ Node intToBV(TNode n, NodeMap& cache)
         }
       }
       NodeBuilder<> builder(newKind);
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        builder << current.getOperator();
+      }
       for (unsigned i = 0; i < children.size(); ++i)
       {
         builder << children[i];
@@ -271,10 +291,6 @@ Node intToBV(TNode n, NodeMap& cache)
                                   nm->mkBitVectorType(size),
                                   "Variable introduced in intToBV pass");
           }
-          else
-          {
-            AlwaysAssert(current.getType() == nm->booleanType());
-          }
         }
         else if (current.isConst())
         {
@@ -283,25 +299,21 @@ Node intToBV(TNode n, NodeMap& cache)
             case kind::CONST_RATIONAL:
             {
               Rational constant = current.getConst<Rational>();
-              AlwaysAssert(constant.isIntegral());
-              AlwaysAssert(constant >= 0);
-              BitVector bv(size, constant.getNumerator());
-              if (bv.toSignedInteger() != constant.getNumerator())
-              {
-                throw TypeCheckingException(
-                    current.toExpr(),
-                    string("Not enough bits for constant in intToBV: ")
-                        + current.toString());
+              if (constant.isIntegral()) {
+                AlwaysAssert(constant >= 0);
+                BitVector bv(size, constant.getNumerator());
+                if (bv.toSignedInteger() != constant.getNumerator())
+                {
+                  throw TypeCheckingException(
+                      current.toExpr(),
+                      string("Not enough bits for constant in intToBV: ")
+                          + current.toString());
+                }
+                result = nm->mkConst(bv);
               }
-              result = nm->mkConst(bv);
               break;
             }
-            case kind::CONST_BOOLEAN: break;
-            default:
-              throw TypeCheckingException(
-                  current.toExpr(),
-                  string("Cannot translate const to BV: ")
-                      + current.toString());
+            default: break;
           }
         }
         else
@@ -325,7 +337,7 @@ IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult IntToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  unordered_map<Node, Node, NodeHashFunction> cache;
+  NodeMap cache;
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     assertionsToPreprocess->replace(

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a367c846928516ea2ee58ad7910cd4c176070486..7d78e93f9b24ce59ca87a0ae65b385af95650603 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1192,13 +1192,9 @@ void SmtEngine::setDefaults() {
 
   if (options::solveIntAsBV() > 0)
   {
-    if (!(d_logic <= LogicInfo("QF_NIA")))
-    {
-      throw OptionException(
-          "--solve-int-as-bv=X only supported for pure integer logics (QF_NIA, "
-          "QF_LIA, QF_IDL)");
-    }
-    d_logic = LogicInfo("QF_BV");
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableTheory(THEORY_BV);
+    d_logic.lock();
   }
 
   if (options::solveBVAsInt() > 0)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4cd3c70d2c3c79298f97e1f79807528063f39fbe..0eb6bc2d2a40992a9f2ebc287647ff9a34e12067 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -358,6 +358,7 @@ set(regress_0_tests
   regress0/bv/fuzz40.smtv1.smt2
   regress0/bv/fuzz41.smtv1.smt2
   regress0/bv/issue3621.smt2
+  regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2

diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2
index 939439adf2cc3e9fb13c359f783d1af2d5041c19..1c8f9b1df341341436cc2da19315c05c1b5b3907 100644 (file)
--- a/test/regress/regress0/bv/bv-abstr-bug2.smt2
+++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager
+; COMMAND-LINE: --solve-int-as-bv=32 
 (set-logic QF_NIA)
 (set-info :status sat)
 (declare-fun _substvar_7_ () Bool)

diff --git a/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
new file mode 100644 (file)
index 0000000..1ef63f3
--- /dev/null
+++ b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models 
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun A () (Array S S))
+(declare-fun f ((_ BitVec 4)) S)
+
+(assert (distinct (select A (f (_ bv0 4))) (select A (f (_ bv1 4)))))
+(check-sat)