Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)

7 files changed, 173 insertions, 10 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index d209c4d73..9b84c8ecf 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -22,10 +22,11 @@
 #include "theory/bv/theory_bv_utils.h"
 
 
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 /* Drop child at given index from expression.
  * E.g., dropChild((x + y + z), 1) -> (x + z)  */
@@ -270,11 +271,22 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
 
     /* inversions  */
     if (k == BITVECTOR_CONCAT) {
-      // TODO
-      Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term "
-                         << k
-                         << ", from " << sv_t << std::endl;
-      return Node::null();
+      /* x = t[upper:lower]
+       * where
+       * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
+       * lower = getSize(sv_t[i]) for i > index
+       */
+      unsigned upper, lower;
+      upper = bv::utils::getSize(t) - 1;
+      lower = 0;
+      NodeBuilder<> nb(nm, BITVECTOR_CONCAT);
+      for (unsigned i = 0; i < sv_t.getNumChildren(); i++) {
+        if (i < index)
+          upper -= bv::utils::getSize(sv_t[i]);
+        else if (i > index)
+          lower += bv::utils::getSize(sv_t[i]);
+      }
+      t = bv::utils::mkExtract(t, upper, lower);
     } else {
       Node s = sv_t.getNumChildren() == 2
         ? sv_t[1 - index]
@@ -396,10 +408,100 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
                              << ", from " << sv_t << std::endl;
           return Node::null();
         }
+      } else if (k == BITVECTOR_UDIV_TOTAL) {
+        TypeNode solve_tn = sv_t[index].getType();
+        Node x = getSolveVariable(solve_tn);
+        Node s = sv_t[1 - index];
+        unsigned w = bv::utils::getSize(s);
+        Node scl, scr;
+        Node zero = bv::utils::mkConst(w, 0u);
+
+        /* x udiv s = t */
+        if (index == 0) {
+          /* with side conditions:
+           * !umulo(s * t)
+           */
+          scl = nm->mkNode(NOT, bv::utils::mkUmulo(s, t));
+          scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, x, s), t);
+        /* s udiv x = t */
+        } else {
+          /* with side conditions:
+           * (t = 0 && (s = 0 || s != 2^w-1))
+           * || s >= t
+           * || t = 2^w-1
+           */
+          Node ones = bv::utils::mkOnes(w);
+          Node t_eq_zero = nm->mkNode(EQUAL, t, zero);
+          Node s_eq_zero = nm->mkNode(EQUAL, s, zero);
+          Node s_ne_ones = nm->mkNode(DISTINCT, s, ones);
+          Node s_ge_t = nm->mkNode(BITVECTOR_UGE, s, t);
+          Node t_eq_ones = nm->mkNode(EQUAL, t, ones);
+          scl = nm->mkNode(
+              OR,
+              nm->mkNode(AND, t_eq_zero, nm->mkNode(OR, s_eq_zero, s_ne_ones)),
+              s_ge_t, t_eq_ones);
+          scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, x), t);
+        }
+
+        /* overall side condition */
+        Node sc = nm->mkNode(IMPLIES, scl, scr);
+        /* add side condition */
+        status.d_conds.push_back(sc);
+
+        /* get the skolem node for this side condition*/
+        Node skv = getInversionNode(sc, solve_tn);
+        /* now solving with the skolem node as the RHS */
+        t = skv;
+      } else if (k == BITVECTOR_SHL) {
+        TypeNode solve_tn = sv_t[index].getType();
+        Node x = getSolveVariable(solve_tn);
+        Node s = sv_t[1 - index];
+        unsigned w = bv::utils::getSize(s);
+        Node scl, scr;
+
+        /* x << s = t */
+        if (index == 0) {
+          /* with side conditions:
+           * (s = 0 || ctz(t) >= s)
+           * <->
+           * (s = 0 || ((t o z) >> (z o s))[w-1:0] = z)
+           *
+           * where
+           * w = getSize(s) = getSize(t) = getSize (z) && z = 0
+           */
+          Node zero = bv::utils::mkConst(w, 0u);
+          Node s_eq_zero = nm->mkNode(EQUAL, s, zero);
+          Node t_conc_zero = nm->mkNode(BITVECTOR_CONCAT, t, zero);
+          Node zero_conc_s = nm->mkNode(BITVECTOR_CONCAT, zero, s);
+          Node shr_s = nm->mkNode(BITVECTOR_LSHR, t_conc_zero, zero_conc_s);
+          Node extr_shr_s = bv::utils::mkExtract(shr_s, w - 1, 0);
+          Node ctz_t_ge_s = nm->mkNode(EQUAL, extr_shr_s, zero);
+          scl = nm->mkNode(OR, s_eq_zero, ctz_t_ge_s);
+          scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_SHL, x, s), t);
+          /* s << x = t */
+        } else {
+          /* with side conditions:
+           * (s = 0 && t = 0)
+           * || (ctz(t) >= ctz(s)
+           *     && (t = 0 ||
+           *         "remaining shifted bits in t match corresponding bits in s"))
+           */
+          Trace("bv-invert") << "bv-invert : Unsupported for index " << index
+                             << ", from " << sv_t << std::endl;
+          return Node::null();
+        }
+
+        /* overall side condition */
+        Node sc = nm->mkNode(IMPLIES, scl, scr);
+        /* add side condition */
+        status.d_conds.push_back(sc);
+
+        /* get the skolem node for this side condition*/
+        Node skv = getInversionNode(sc, solve_tn);
+        /* now solving with the skolem node as the RHS */
+        t = skv;
       } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) {
         t = NodeManager::currentNM()->mkNode(k, t);
-        //}else if( k==BITVECTOR_CONCAT ){
-        // TODO
         //}else if( k==BITVECTOR_ASHR ){
         // TODO
       } else {
@@ -472,3 +574,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node lit, bool pol,
   }
   return Node::null();
 }
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index eb33e2c82..e045ad44c 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -92,6 +92,11 @@ TESTS =	\
 	bug822.smt2 \
 	qbv-test-invert-mul.smt2 \
 	qbv-simple-2vars-vo.smt2 \
+	qbv-test-invert-concat-0.smt2 \
+	qbv-test-invert-concat-1.smt2 \
+	qbv-test-invert-shl.smt2 \
+	qbv-test-invert-udiv-0.smt2 \
+	qbv-test-invert-udiv-1.smt2 \
 	qbv-test-urem-rewrite.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
new file mode 100644
index 000000000..f4e19fc52
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 64))
+
+(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
new file mode 100644
index 000000000..827e74605
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 64))
+
+(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
new file mode 100644
index 000000000..97a0662eb
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+
+(assert (forall ((x (_ BitVec 32))) (not (= (bvshl x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
new file mode 100644
index 000000000..becfc5315
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+
+(assert (distinct a b (_ bv0 16)))
+(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
new file mode 100644
index 000000000..0373cf8f3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+
+(assert (distinct a b (_ bv0 16)))
+(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv a x) b))))
+
+(check-sat)