diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
tree | 39695fe22d387bc84bc49d20831a19648d55011f /src/theory/quantifiers/bv_inverter.cpp | |
parent | be11fae39055f213586058ec9129d1276f724b0e (diff) |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 222 |
1 files changed, 46 insertions, 176 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 957385a14..d777dc4f8 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -52,21 +52,7 @@ Node BvInverter::getSolveVariable(TypeNode tn) std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn); if (its == d_solve_var.end()) { - std::stringstream ss; - if (tn.isFunction()) - { - Assert(tn.getNumChildren() == 2); - Assert(tn[0].isBoolean()); - ss << "slv_f"; - } - else - { - ss << "slv"; - } - Node k = NodeManager::currentNM()->mkSkolem(ss.str(), tn); - // marked as a virtual term (it is eligible for instantiation) - VirtualTermSkolemAttribute vtsa; - k.setAttribute(vtsa, true); + Node k = NodeManager::currentNM()->mkSkolem("slv", tn); d_solve_var[tn] = k; return k; } @@ -76,75 +62,50 @@ Node BvInverter::getSolveVariable(TypeNode tn) } } -Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn) +Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) { // condition should be rewritten - Assert(Rewriter::rewrite(cond) == cond); - std::unordered_map<Node, Node, NodeHashFunction>::iterator it = - d_inversion_skolem_cache.find(cond); - if (it == d_inversion_skolem_cache.end()) + Node new_cond = Rewriter::rewrite(cond); + if (new_cond != cond) { - Node skv; - if (cond.getKind() == EQUAL) + Trace("cegqi-bv-skvinv-debug") << "Condition " << cond + << " was rewritten to " << new_cond + << std::endl; + } + Node c; + // optimization : if condition is ( x = v ) should just return v and not + // introduce a Skolem this can happen when we ask for the multiplicative + // inversion with bv1 + TNode solve_var = getSolveVariable(tn); + if (new_cond.getKind() == EQUAL) + { + for (unsigned i = 0; i < 2; i++) { - // optimization : if condition is ( x = v ) should just return v and not - // introduce a Skolem this can happen when we ask for the multiplicative - // inversion with bv1 - Node x = getSolveVariable(tn); - for (unsigned i = 0; i < 2; i++) + if (new_cond[i] == solve_var) { - if (cond[i] == x) - { - skv = cond[1 - i]; - Trace("cegqi-bv-skvinv") - << "SKVINV : " << skv << " is trivially associated with conditon " - << cond << std::endl; - break; - } + c = new_cond[1 - i]; + Trace("cegqi-bv-skvinv") << "SKVINV : " << c + << " is trivially associated with conditon " + << new_cond << std::endl; + break; } } - if (skv.isNull()) - { - // TODO : compute the value if the condition is deterministic, e.g. calc - // multiplicative inverse of 2 constants - skv = NodeManager::currentNM()->mkSkolem( - "skvinv", tn, "created for BvInverter"); - Trace("cegqi-bv-skvinv") - << "SKVINV : " << skv << " is the skolem associated with conditon " - << cond << std::endl; - // marked as a virtual term (it is eligible for instantiation) - VirtualTermSkolemAttribute vtsa; - skv.setAttribute(vtsa, true); - } - d_inversion_skolem_cache[cond] = skv; - return skv; - } - else - { - Assert(it->second.getType() == tn); - return it->second; } -} - -Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn) -{ - NodeManager* nm = NodeManager::currentNM(); - // function maps conditions to skolems - TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn); - return getSolveVariable(ftn); -} - -Node BvInverter::getInversionNode(Node cond, TypeNode tn) -{ - // condition should be rewritten - Node new_cond = Rewriter::rewrite(cond); - if (new_cond != cond) + // TODO : compute the value if the condition is deterministic, e.g. calc + // multiplicative inverse of 2 constants + if (c.isNull()) { - Trace("bv-invert-debug") << "Condition " << cond << " was rewritten to " - << new_cond << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Node x = m->getBoundVariable(tn); + Node ccond = new_cond.substitute(solve_var, x); + c = nm->mkNode(kind::CHOICE, nm->mkNode(BOUND_VAR_LIST, x), ccond); + Trace("cegqi-bv-skvinv") << "SKVINV : Make " << c << " for " << new_cond + << std::endl; } - Node f = getInversionSkolemFunctionFor(tn); - return NodeManager::currentNM()->mkNode(kind::APPLY_UF, f, new_cond); + // currently shouldn't cache since + // the return value depends on the + // state of m (which bound variable is returned). + return c; } bool BvInverter::isInvertible(Kind k, unsigned index) @@ -219,97 +180,6 @@ Node BvInverter::getPathToPv( return Node::null(); } -Node BvInverter::eliminateSkolemFunctions(TNode n, - std::vector<Node>& side_conditions) -{ - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; - std::stack<TNode> visit; - TNode cur; - - visit.push(n); - 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()) - { - Trace("bv-invert-debug") - << "eliminateSkolemFunctions from " << cur << "..." << std::endl; - - Node ret = cur; - bool childChanged = false; - std::vector<Node> children; - if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - 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); - } - if (childChanged) - { - ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); - } - // now, check if it is a skolem function - if (ret.getKind() == APPLY_UF) - { - Node op = ret.getOperator(); - TypeNode tnp = op.getType(); - // is this a skolem function? - std::map<TypeNode, Node>::iterator its = d_solve_var.find(tnp); - if (its != d_solve_var.end() && its->second == op) - { - Assert(ret.getNumChildren() == 1); - Assert(ret[0].getType().isBoolean()); - - Node cond = ret[0]; - // must rewrite now to ensure we lookup the correct skolem - cond = Rewriter::rewrite(cond); - - // if so, we replace by the (finalized) skolem variable - // Notice that since we are post-rewriting, skolem functions are - // already eliminated from cond - ret = getInversionSkolemFor(cond, ret.getType()); - - // also must add (substituted) side condition to vector - // substitute ( solve variable -> inversion skolem ) - TNode solve_var = getSolveVariable(ret.getType()); - TNode tret = ret; - cond = cond.substitute(solve_var, tret); - if (std::find(side_conditions.begin(), side_conditions.end(), cond) - == side_conditions.end()) - { - side_conditions.push_back(cond); - } - } - } - Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << cur - << " returned " << ret << std::endl; - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path) { @@ -329,7 +199,7 @@ Node BvInverter::getPathToPv( Node BvInverter::solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& path, - BvInverterModelQuery* m, + BvInverterQuery* m, BvInverterStatus& status) { Assert(!path.empty()); @@ -413,7 +283,7 @@ Node BvInverter::solve_bv_lit(Node sv, } status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -469,7 +339,7 @@ Node BvInverter::solve_bv_lit(Node sv, } status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -502,7 +372,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -599,7 +469,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; @@ -641,7 +511,7 @@ Node BvInverter::solve_bv_lit(Node sv, } Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; break; } @@ -694,7 +564,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; @@ -713,7 +583,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; break; } @@ -749,7 +619,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; } else @@ -793,7 +663,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; } else @@ -863,7 +733,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; |