From fad765a539f8732461340980477ffe3f8c672fb2 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 2 Oct 2017 12:35:28 -0700 Subject: [PATCH] Address comments from PR #1164. (#1174) Make eliminateSkolemFunctions(...) iterative and some more minor fixes. --- src/theory/quantifiers/bv_inverter.cpp | 135 ++++++++++++++----------- src/theory/quantifiers/bv_inverter.h | 7 +- 2 files changed, 75 insertions(+), 67 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index a0b78d6d4..5152b2917 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/bv_inverter.h" #include +#include #include "theory/quantifiers/term_database.h" @@ -87,9 +88,9 @@ Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn) { } Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn) { + NodeManager* nm = NodeManager::currentNM(); // function maps conditions to skolems - TypeNode ftn = NodeManager::currentNM()->mkFunctionType( - NodeManager::currentNM()->booleanType(), tn); + TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn); return getSolveVariable(ftn); } @@ -144,71 +145,83 @@ Node BvInverter::getPathToPv( return Node::null(); } -Node BvInverter::eliminateSkolemFunctions( - TNode n, std::vector& side_conditions, - std::unordered_map& visited) { - std::unordered_map::iterator it = - visited.find(n); - if (it == visited.end()) { - Trace("bv-invert-debug") - << "eliminateSkolemFunctions from " << n << "..." << std::endl; - Node ret = n; - bool childChanged = false; - std::vector children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back(n.getOperator()); - } - for (unsigned i = 0; i < n.getNumChildren(); i++) { - Node nc = eliminateSkolemFunctions(n[i], side_conditions, visited); - childChanged = childChanged || n[i] != nc; - children.push_back(nc); - } - if (childChanged) { - ret = NodeManager::currentNM()->mkNode(n.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::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 BvInverter::eliminateSkolemFunctions(TNode n, + std::vector& side_conditions) { + std::unordered_map visited; + std::unordered_map::iterator it; + std::stack visit; + TNode cur; + + visit.push(n); + do { + cur = visit.top(); + visit.pop(); + it = visited.find(cur); - Node cond = ret[0]; - // must rewrite now to ensure we lookup the correct skolem - cond = Rewriter::rewrite(cond); + 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; - // 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()); + Node ret = cur; + bool childChanged = false; + std::vector 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::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()); - // 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); + 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; } - Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << n - << " returned " << ret << std::endl; - visited[n] = ret; - return ret; - } else { - return it->second; - } -} - -Node BvInverter::eliminateSkolemFunctions(TNode n, - std::vector& side_conditions) { - std::unordered_map visited; - return eliminateSkolemFunctions(n, side_conditions, visited); + } 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, diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index ca6c97f83..724b3b7a7 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -42,7 +42,7 @@ class BvInverterStatus { BvInverterStatus() : d_status(0) {} ~BvInverterStatus() {} int d_status; - // TODO : may not need this (conditions are now appear explicitly in solved + // TODO : may not need this (conditions now appear explicitly in solved // forms) side conditions std::vector d_conds; }; @@ -111,11 +111,6 @@ class BvInverter { Node getPathToPv(Node lit, Node pv, Node sv, std::vector& path, std::unordered_set& visited); - /** helper function for eliminateSkolemFunctions */ - Node eliminateSkolemFunctions( - TNode n, std::vector& side_conditions, - std::unordered_map& visited); - // is operator k invertible? bool isInvertible(Kind k); -- 2.30.2