Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remove non-invertible operators. Add regression. (#1222)

4 files changed, 101 insertions, 4 deletions

diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 642ec8fcc..981d33c2f 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -28,6 +28,7 @@
 #include "util/bitvector.h"
 
 #include <algorithm>
+#include <stack>
 
 using namespace std;
 using namespace CVC4;
@@ -899,10 +900,18 @@ bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf,
 }
 
 bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
-  Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl;
+  // if option enabled, use approach for word-level inversion for BV instantiation
   if( options::cbqiBv() ){
-    // if option enabled, use approach for word-level inversion for BV instantiation
-    processLiteral( ci, sf, pv, lit, effort );
+    // get the best rewritten form of lit for solving for pv 
+    //   this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible
+    Node rlit = rewriteAssertionForSolvePv( pv, lit );
+    if( Trace.isOn("cegqi-bv") ){
+      Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl;
+      if( lit!=rlit ){
+        Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
+      }
+    }
+    processLiteral( ci, sf, pv, rlit, effort );
   }
   return false;
 }
@@ -994,3 +1003,76 @@ bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci,
 
   return true;
 }
+  
+Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) {
+  NodeManager* nm = NodeManager::currentNM();
+  // result of rewriting the visited term
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  // whether the visited term contains pv
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::stack<TNode> visit;
+  TNode cur;
+  visit.push(lit);
+  do {
+    cur = visit.top();
+    visit.pop();
+    it = visited.find(cur);
+
+    if (it == visited.end()) {
+      visited[cur] = Node::null();
+      visit.push(cur);
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        visit.push(cur[i]);
+      }
+    } else if (it->second.isNull()) {
+      Node ret;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back(cur.getOperator());
+      }
+      bool contains_pv = ( cur==pv );
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        it = visited.find(cur[i]);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur[i] != it->second;
+        children.push_back(it->second);
+        contains_pv = contains_pv || visited_contains_pv[cur[i]];
+      }
+      
+      // [1] rewrite cases of non-invertible operators
+      
+      // if cur is urem( x, y ) where x contains pv but y does not, then
+      // rewrite urem( x, y ) ---> x - udiv( x, y )*y
+      if (cur.getKind()==BITVECTOR_UREM_TOTAL) {
+        if( visited_contains_pv[cur[0]] && !visited_contains_pv[cur[1]] ){
+          ret = nm->mkNode( BITVECTOR_SUB, children[0], 
+                  nm->mkNode( BITVECTOR_MULT,
+                    nm->mkNode( BITVECTOR_UDIV_TOTAL, children[0], children[1] ),
+                    children[1] ) );
+        }
+      }
+      
+      // [2] try to rewrite non-linear literals -> linear literals
+      
+      
+      // return original if the above steps do not produce a result
+      if (ret.isNull()) {
+        if (childChanged) {
+          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+        }else{
+          ret = cur;
+        }
+      }
+      visited[cur] = ret;
+      // careful that rewrites above do not affect whether this term contains pv
+      visited_contains_pv[cur] = contains_pv;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(lit) != visited.end());
+  Assert(!visited.find(lit)->second.isNull());
+  return visited[lit];
+}
+
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index fff608b82..0880fe878 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -91,6 +91,10 @@ private:
   std::unordered_map< unsigned, BvInverterStatus > d_inst_id_to_status;
   // variable to current id we are processing
   std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
+  /** rewrite assertion for solve pv
+  * returns a literal that is equivalent to lit that leads to best solved form for pv
+  */
+  Node rewriteAssertionForSolvePv( Node pv, Node lit );
 private:
   void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
 public:
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index a4bd40df5..eb33e2c82 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -91,7 +91,8 @@ TESTS =	\
 	psyco-001-bv.smt2 \
 	bug822.smt2 \
 	qbv-test-invert-mul.smt2 \
-	qbv-simple-2vars-vo.smt2
+	qbv-simple-2vars-vo.smt2 \
+	qbv-test-urem-rewrite.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
new file mode 100644
index 000000000..6df69d80b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+
+(assert (forall ((x (_ BitVec 4))) (not (= (bvurem x a) b))))
+
+(check-sat)