diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 15:24:07 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 15:24:07 -0600 |
commit | 96b699bc6cccd1ade32e2d5ef73ce004063b8201 (patch) | |
tree | 8128f4bd212c87cc193f11648a136bd4236fbf83 /src/smt/term_formula_removal.cpp | |
parent | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (diff) |
Minor cleanup and reorganization related to last commit.
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
-rw-r--r-- | src/smt/term_formula_removal.cpp | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp new file mode 100644 index 000000000..3fd333cc5 --- /dev/null +++ b/src/smt/term_formula_removal.cpp @@ -0,0 +1,235 @@ +/********************* */ +/*! \file term_formula_removal.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Removal of term formulas + ** + ** Removal of term formulas. + **/ +#include "smt/term_formula_removal.h" + +#include <vector> + +#include "options/proof_options.h" +#include "proof/proof_manager.h" +#include "theory/ite_utilities.h" + +using namespace std; + +namespace CVC4 { + +RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVisitor(); +} + +RemoveTermFormulas::~RemoveTermFormulas(){ + delete d_containsVisitor; +} + +void RemoveTermFormulas::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { + return d_containsVisitor; +} + +size_t RemoveTermFormulas::collectedCacheSizes() const{ + return d_containsVisitor->cache_size() + d_iteCache.size(); +} + +void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +{ + size_t n = output.size(); + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + // 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, false, false); + // In some calling contexts, not necessary to report dependence information. + if (reportDeps && + (options::unsatCores() || options::fewerPreprocessingHoles())) { + // new assertions have a dependence on the node + PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) + while(n < output.size()) { + PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) + ++n; + } + } + output[i] = itesRemoved; + } +} + +bool RemoveTermFormulas::containsTermITE(TNode e) const { + return d_containsVisitor->containsTermITE(e); +} + +Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) { + // Current node + Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; + + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ + return Node(node); + } + + // The result may be cached already + int cv = cacheVal( inQuant, inTerm ); + std::pair<Node, int> cacheKey(node, cv); + NodeManager *nodeManager = NodeManager::currentNM(); + 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; + } + + + // If an ITE, replace it + TypeNode nodeType = node.getType(); + if(node.getKind() == kind::ITE) { + if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { + Node skolem; + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); + + // The new assertion + Node newAssertion = + nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), + skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the 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, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + } + //if a non-variable Boolean term, replace it + if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ + Node skolem; + // Make the skolem to represent the Boolean term + //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); + skolem = nodeManager->mkBooleanTermVariable(); + + // The new assertion + Node newAssertion = skolem.eqNode( node ); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the 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, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && + node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ + // Remember if we're inside a term + Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; + inTerm = true; + } + + // If not an ITE, go deep + 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, inTerm); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(cacheKey, cached); + return cached; + } else { + d_iteCache.insert(cacheKey, Node::null()); + return node; + } +} + +Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ + return Node(node); + } + + // Check the cache + NodeManager *nodeManager = NodeManager::currentNM(); + int cv = cacheVal( inQuant, inTerm ); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + return cached.isNull() ? Node(node) : cached; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ + // Remember if we're inside a term + inTerm = 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, inTerm); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + return nodeManager->mkNode(node.getKind(), newChildren); + } else { + return node; + } +} + +}/* CVC4 namespace */ |