From: Andrew Reynolds Date: Wed, 11 Oct 2017 13:51:05 +0000 (-0500) Subject: Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remov... X-Git-Tag: cvc5-1.0.0~5565 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f34a6307e4bb7ec01574a8f9e813bd5fc92a30a;p=cvc5.git Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remove non-invertible operators. Add regression. (#1222) --- 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 +#include 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 visited; + // whether the visited term contains pv + std::unordered_map visited_contains_pv; + std::unordered_map::iterator it; + std::stack 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 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)