bv: Refactor ppRewrite and move to TheoryBV. (#7271)

This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules.

Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse.

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 17c65c2902d4a352df133a831bba76e57ce9786c..dd7c1cd40af783b994c3d3f87b5e0242d84b377c 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -224,3 +224,11 @@ name   = "Bitvector Theory"
   default    = "false"
   help       = "assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver"
 
+
+[[option]]
+  name       = "rwExtendEq"
+  category   = "expert"
+  long       = "bv-rw-extend-eq"
+  type       = "bool"
+  default    = "false"
+  help       = "enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08)"

diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index b334a550d9da95f36116fb78de842082f243684d..fdc6d22d4d25b61f1a6a84ef0dce76abaa99e596 100644 (file)
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -72,13 +72,11 @@ bool BvIntroPow2::isPowerOfTwo(TNode node)
   if (t.getNumChildren() != 2) return false;
   TNode a = t[0];
   TNode b = t[1];
-  unsigned size = bv::utils::getSize(t);
-  if (size < 2) return false;
+  if (bv::utils::getSize(t) < 2) return false;
   Node diff =
       rewrite(NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b));
   return (diff.isConst()
-          && (diff == bv::utils::mkConst(size, 1u)
-              || diff == bv::utils::mkOnes(size)));
+          && (bv::utils::isOne(diff) || bv::utils::isOnes(diff)));
 }
 
 Node BvIntroPow2::rewritePowerOfTwo(TNode node)
@@ -87,11 +85,11 @@ Node BvIntroPow2::rewritePowerOfTwo(TNode node)
   TNode term = bv::utils::isZero(node[0]) ? node[1] : node[0];
   TNode a = term[0];
   TNode b = term[1];
-  unsigned size = bv::utils::getSize(term);
+  uint32_t size = bv::utils::getSize(term);
   Node diff = rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b));
   Assert(diff.isConst());
-  TNode x = diff == bv::utils::mkConst(size, 1u) ? a : b;
-  Node one = bv::utils::mkConst(size, 1u);
+  Node one = bv::utils::mkOne(size);
+  TNode x = diff == one ? a : b;
   Node sk = bv::utils::mkVar(size);
   Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk);
   Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh);

diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
index 0f39474da6e4f78360616acec222e4e739de29ab..b3e23f70c0817370aa2fcbe93cdd3179f2c9b208 100644 (file)
--- a/src/preprocessing/passes/bv_intro_pow2.h
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -51,7 +51,7 @@ class BvIntroPow2 : public PreprocessingPass
    * Only to be called on top level assertions.
    */
   Node rewritePowerOfTwo(TNode node);
-  /** Does the traversal of assertions and applies rweritePowerOfTwo. */
+  /** Does the traversal of assertions and applies rewritePowerOfTwo. */
   Node pow2Rewrite(Node node, std::unordered_map<Node, Node>& cache);
 };
 

diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp
index 682c556ccbba8523182f686adddc8eabf34bc11c..8427c1a50d6ca2fdf0d0183201f401a2191d3357 100644 (file)
--- a/src/theory/bv/bv_solver_layered.cpp
+++ b/src/theory/bv/bv_solver_layered.cpp
@@ -51,7 +51,6 @@ BVSolverLayered::BVSolverLayered(Env& env,
       d_subtheories(),
       d_subtheoryMap(),
       d_statistics(),
-      d_staticLearnCache(),
       d_lemmasAdded(c, false),
       d_conflict(c, false),
       d_invalidateModelCache(c, true),
@@ -391,103 +390,6 @@ void BVSolverLayered::propagate(Theory::Effort e)
   }
 }
 
-TrustNode BVSolverLayered::ppRewrite(TNode t)
-{
-  Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
-  Node res = t;
-  if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
-  {
-    Node result = RewriteRule<BitwiseEq>::run<false>(t);
-    res = rewrite(result);
-  }
-  else if (RewriteRule<UltAddOne>::applies(t))
-  {
-    Node result = RewriteRule<UltAddOne>::run<false>(t);
-    res = rewrite(result);
-  }
-  else if (res.getKind() == kind::EQUAL
-           && ((res[0].getKind() == kind::BITVECTOR_ADD
-                && RewriteRule<ConcatToMult>::applies(res[1]))
-               || (res[1].getKind() == kind::BITVECTOR_ADD
-                   && RewriteRule<ConcatToMult>::applies(res[0]))))
-  {
-    Node mult = RewriteRule<ConcatToMult>::applies(res[0])
-                    ? RewriteRule<ConcatToMult>::run<false>(res[0])
-                    : RewriteRule<ConcatToMult>::run<true>(res[1]);
-    Node factor = mult[0];
-    Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
-    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
-    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
-    if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
-    {
-      res = rewrite(rewr_eq);
-    }
-    else
-    {
-      res = t;
-    }
-  }
-  else if (RewriteRule<SignExtendEqConst>::applies(t))
-  {
-    res = RewriteRule<SignExtendEqConst>::run<false>(t);
-  }
-  else if (RewriteRule<ZeroExtendEqConst>::applies(t))
-  {
-    res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
-  }
-  else if (RewriteRule<NormalizeEqAddNeg>::applies(t))
-  {
-    res = RewriteRule<NormalizeEqAddNeg>::run<false>(t);
-  }
-
-  // if(t.getKind() == kind::EQUAL &&
-  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
-  //    kind::BITVECTOR_ADD) ||
-  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
-  //     kind::BITVECTOR_ADD))) {
-  //   // if we have an equality between a multiplication and addition
-  //   // try to express multiplication in terms of addition
-  //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
-  //   Node add = t[0].getKind() == kind::BITVECTOR_ADD? t[0] : t[1];
-  //   if (RewriteRule<MultSlice>::applies(mult)) {
-  //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
-  //     Node new_eq =
-  //     rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
-  //     new_mult, add));
-
-  //     // the simplification can cause the formula to blow up
-  //     // only apply if formula reduced
-  //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
-  //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
-  //       uint64_t old_size = bv->computeAtomWeight(t);
-  //       Assert (old_size);
-  //       uint64_t new_size = bv->computeAtomWeight(new_eq);
-  //       double ratio = ((double)new_size)/old_size;
-  //       if (ratio <= 0.4) {
-  //         ++(d_statistics.d_numMultSlice);
-  //         return new_eq;
-  //       }
-  //     }
-
-  //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
-  //       ++(d_statistics.d_numMultSlice);
-  //       return new_eq;
-  //     }
-  //   }
-  // }
-
-  if (options().bv.bvAbstraction && t.getType().isBoolean())
-  {
-    d_abstractionModule->addInputAtom(res);
-  }
-  Debug("bv-pp-rewrite") << "to   " << res << "\n";
-  if (res != t)
-  {
-    return TrustNode::mkTrustRewrite(t, res, nullptr);
-  }
-  return TrustNode::null();
-}
-
 void BVSolverLayered::presolve()
 {
   Debug("bitvector") << "BVSolverLayered::presolve" << std::endl;
@@ -611,56 +513,6 @@ EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
   ;
 }
 
-void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned)
-{
-  if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
-  {
-    return;
-  }
-  d_staticLearnCache.insert(in);
-
-  if (in.getKind() == kind::EQUAL)
-  {
-    if ((in[0].getKind() == kind::BITVECTOR_ADD
-         && in[1].getKind() == kind::BITVECTOR_SHL)
-        || (in[1].getKind() == kind::BITVECTOR_ADD
-            && in[0].getKind() == kind::BITVECTOR_SHL))
-    {
-      TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
-      TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
-
-      if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
-          && p[1].getKind() == kind::BITVECTOR_SHL)
-      {
-        unsigned size = utils::getSize(s);
-        Node one = utils::mkConst(size, 1u);
-        if (s[0] == one && p[0][0] == one && p[1][0] == one)
-        {
-          Node zero = utils::mkConst(size, 0u);
-          TNode b = p[0];
-          TNode c = p[1];
-          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
-          Node b_eq_0 = b.eqNode(zero);
-          Node c_eq_0 = c.eqNode(zero);
-          Node b_eq_c = b.eqNode(c);
-
-          Node dis = NodeManager::currentNM()->mkNode(
-              kind::OR, b_eq_0, c_eq_0, b_eq_c);
-          Node imp = in.impNode(dis);
-          learned << imp;
-        }
-      }
-    }
-  }
-  else if (in.getKind() == kind::AND)
-  {
-    for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
-    {
-      ppStaticLearn(in[i], learned);
-    }
-  }
-}
-
 bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
                                        std::vector<Node>& new_assertions)
 {

diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h
index 3b723b0520a64b33be1bd1f6f4de03350944f665..3870bc078348d4ba6a681f2fd75cf00cec788591 100644 (file)
--- a/src/theory/bv/bv_solver_layered.h
+++ b/src/theory/bv/bv_solver_layered.h
@@ -96,10 +96,6 @@ class BVSolverLayered : public BVSolver
     return std::string("BVSolverLayered");
   }
 
-  TrustNode ppRewrite(TNode t) override;
-
-  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
-
   void presolve() override;
 
   bool applyAbstraction(const std::vector<Node>& assertions,
@@ -127,7 +123,6 @@ class BVSolverLayered : public BVSolver
 
   typedef std::unordered_set<TNode> TNodeSet;
   typedef std::unordered_set<Node> NodeSet;
-  NodeSet d_staticLearnCache;
 
   typedef std::unordered_map<Node, Node> NodeToNode;
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index ba90c669ed781c8521992da4062ebfd64c5260bf..f027b56fefe0381f52f38e193a9e9796e84fc23e 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -22,6 +22,8 @@
 #include "theory/bv/bv_solver_bitblast.h"
 #include "theory/bv/bv_solver_bitblast_internal.h"
 #include "theory/bv/bv_solver_layered.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 #include "theory/trust_substitutions.h"
@@ -279,6 +281,37 @@ TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
   {
     return texp;
   }
+
+  Debug("theory-bv-pp-rewrite") << "ppRewrite " << t << "\n";
+  Node res = t;
+  if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
+  {
+    res = rewrite(RewriteRule<BitwiseEq>::run<false>(t));
+  }
+  // useful on QF_BV/space/ndist
+  else if (RewriteRule<UltAddOne>::applies(t))
+  {
+    res = rewrite(RewriteRule<UltAddOne>::run<false>(t));
+  }
+  // Useful for BV/2017-Preiner-scholl-smt08, but not for QF_BV
+  else if (options().bv.rwExtendEq)
+  {
+    if (RewriteRule<SignExtendEqConst>::applies(t))
+    {
+      res = RewriteRule<SignExtendEqConst>::run<false>(t);
+    }
+    else if (RewriteRule<ZeroExtendEqConst>::applies(t))
+    {
+      res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
+    }
+  }
+
+  Debug("theory-bv-pp-rewrite") << "to   " << res << "\n";
+  if (res != t)
+  {
+    return TrustNode::mkTrustRewrite(t, res, nullptr);
+  }
+
   return d_internal->ppRewrite(t);
 }
 
@@ -318,6 +351,47 @@ void TheoryBV::notifySharedTerm(TNode t)
 
 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
 {
+  if (in.getKind() == kind::EQUAL)
+  {
+    // Only useful in combination with --bv-intro-pow2 on
+    // QF_BV/pspace/power2sum benchmarks.
+    //
+    // Matches for equality:
+    //
+    // (= (bvadd (bvshl 1 x) (bvshl 1 y)) (bvshl 1 z))
+    //
+    // and does case analysis on the sum of two power of twos.
+    if ((in[0].getKind() == kind::BITVECTOR_ADD
+         && in[1].getKind() == kind::BITVECTOR_SHL)
+        || (in[1].getKind() == kind::BITVECTOR_ADD
+            && in[0].getKind() == kind::BITVECTOR_SHL))
+    {
+      TNode p = in[0].getKind() == kind::BITVECTOR_ADD ? in[0] : in[1];
+      TNode s = in[0].getKind() == kind::BITVECTOR_ADD ? in[1] : in[0];
+
+      if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
+          && p[1].getKind() == kind::BITVECTOR_SHL)
+      {
+        if (utils::isOne(s[0]) && utils::isOne(p[0][0])
+            && utils::isOne(p[1][0]))
+        {
+          Node zero = utils::mkZero(utils::getSize(s));
+          TNode b = p[0];
+          TNode c = p[1];
+          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
+          Node b_eq_0 = b.eqNode(zero);
+          Node c_eq_0 = c.eqNode(zero);
+          Node b_eq_c = b.eqNode(c);
+
+          Node dis = NodeManager::currentNM()->mkNode(
+              kind::OR, b_eq_0, c_eq_0, b_eq_c);
+          Node imp = in.impNode(dis);
+          learned << imp;
+        }
+      }
+    }
+  }
+
   d_internal->ppStaticLearn(in, learned);
 }