summaryrefslogtreecommitdiff
path: root/src/util/ite_removal.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r--src/util/ite_removal.cpp138
1 files changed, 72 insertions, 66 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 0dfea4399..1ceedc688 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -18,7 +18,6 @@
#include "util/ite_removal.h"
#include "expr/command.h"
-#include "theory/quantifiers/options.h"
#include "theory/ite_utilities.h"
using namespace CVC4;
@@ -29,7 +28,7 @@ namespace CVC4 {
RemoveITE::RemoveITE(context::UserContext* u)
: d_iteCache(u)
{
- d_containsVisitor = new theory::ContainsTermITEVistor();
+ d_containsVisitor = new theory::ContainsTermITEVisitor();
}
RemoveITE::~RemoveITE(){
@@ -40,7 +39,7 @@ void RemoveITE::garbageCollect(){
d_containsVisitor->garbageCollect();
}
-theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){
+theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
return d_containsVisitor;
}
@@ -51,22 +50,20 @@ size_t RemoveITE::collectedCacheSizes() const{
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- std::vector<Node> quantVar;
// Do this in two steps to avoid Node problems(?)
// Appears related to bug 512, splitting this into two lines
// fixes the bug on clang on Mac OS
- Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false);
output[i] = itesRemoved;
}
}
-bool RemoveITE::containsTermITE(TNode e){
+bool RemoveITE::containsTermITE(TNode e) const {
return d_containsVisitor->containsTermITE(e);
}
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap,
- std::vector<Node>& quantVar) {
+ IteSkolemMap& iteSkolemMap, bool inQuant) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
@@ -76,35 +73,28 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
}
// The result may be cached already
+ std::pair<Node, bool> cacheKey(node, inQuant);
NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(node);
+ ITECache::const_iterator i = d_iteCache.find(cacheKey);
if(i != d_iteCache.end()) {
Node cached = (*i).second;
Debug("ite") << "removeITEs: in-cache: " << cached << endl;
return cached.isNull() ? Node(node) : cached;
}
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
// If an ITE replace it
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
- if(!nodeType.isBoolean()) {
+ if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl;
Node skolem;
// Make the skolem to represent the ITE
- if( quantVar.empty() ){
- skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
- }else{
- //if in the scope of free variables, make a skolem operator
- vector< TypeNode > argTypes;
- for( size_t i=0; i<quantVar.size(); i++ ){
- argTypes.push_back( quantVar[i].getType() );
- }
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
- Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
- vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
- skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
- }
+ skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
// The new assertion
Node newAssertion =
@@ -113,18 +103,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- d_iteCache.insert(node, skolem);
+ d_iteCache.insert(cacheKey, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
-
- if( !quantVar.empty() ){
- //if in the scope of free variables, it is a quantified assertion
- vector< Node > children;
- children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
- children.push_back( newAssertion );
- newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
- }
+ newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
@@ -135,42 +117,66 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
}
// If not an ITE, go deep
- if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
- node.getKind() != kind::EXISTS &&
- node.getKind() != kind::REWRITE_RULE ) {
- std::vector< Node > newQuantVar;
- newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
- if( node.getKind()==kind::FORALL ){
- for( size_t i=0; i<node[0].getNumChildren(); i++ ){
- newQuantVar.push_back( node[0][i] );
- }
- }
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Remove the ITEs from the children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Remove the ITEs from the children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = run(*it, output, iteSkolemMap, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
- // If changes, we rewrite
- if(somethingChanged) {
- Node cached = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache.insert(node, cached);
- return cached;
- } else {
- d_iteCache.insert(node, Node::null());
- return node;
- }
+ // If changes, we rewrite
+ if(somethingChanged) {
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(cacheKey, cached);
+ return cached;
} else {
- d_iteCache.insert(node, Node::null());
+ d_iteCache.insert(cacheKey, Node::null());
return node;
}
}
+Node RemoveITE::replace(TNode node, bool inQuant) const {
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
+ // Check the cache
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Replace in children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = replace(*it, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ return nodeManager->mkNode(node.getKind(), newChildren);
+ } else {
+ return node;
+ }
+}
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback