diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
commit | 97555307af3415d6fbbac3fc9dccdafec51056b7 (patch) | |
tree | 56b47f809268d5b8ae21594d22cbec7ced8f46aa /src/util | |
parent | 9ac1cb18f03a5edf4b50532d29e195f74d6a83c2 (diff) |
Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/ite_removal.cpp | 14 | ||||
-rw-r--r-- | src/util/ite_removal.h | 11 |
2 files changed, 18 insertions, 7 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index dfa6e3cba..9d2524170 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -30,13 +30,15 @@ namespace CVC4 { struct IteRewriteAttrTag {}; typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; -void RemoveITE::run(std::vector<Node>& output) { +void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) +{ for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - output[i] = run(output[i], output); + output[i] = run(output[i], output, iteSkolemMap); } } -Node RemoveITE::run(TNode node, std::vector<Node>& output) { +Node RemoveITE::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -67,7 +69,9 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) { nodeManager->setAttribute(node, IteRewriteAttr(), skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output - output.push_back(run(newAssertion, output)); + newAssertion = run(newAssertion, output, iteSkolemMap); + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); // The representation is now the skolem return skolem; @@ -82,7 +86,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) { } // Remove the ITEs from the children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output); + Node newChild = run(*it, output, iteSkolemMap); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index bfb0d4ac8..248ce4efa 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -26,19 +26,26 @@ namespace CVC4 { +typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; + class RemoveITE { public: /** * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions. + * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new + * Boolean ite created in conjunction with that skolem variable. */ - static void run(std::vector<Node>& assertions); + static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap); /** * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions. + * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new + * Boolean ite created in conjunction with that skolem variable. */ - static Node run(TNode node, std::vector<Node>& additionalAssertions); + static Node run(TNode node, std::vector<Node>& additionalAssertions, + IteSkolemMap& iteSkolemMap); };/* class RemoveTTE */ |