summaryrefslogtreecommitdiff
path: root/src/theory/ite_utilities.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/ite_utilities.cpp')
-rw-r--r--src/theory/ite_utilities.cpp1613
1 files changed, 1613 insertions, 0 deletions
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
new file mode 100644
index 000000000..facd5f4f0
--- /dev/null
+++ b/src/theory/ite_utilities.cpp
@@ -0,0 +1,1613 @@
+/********************* */
+/*! \file ite_simplifier.cpp
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Simplifications for ITE expressions
+ **
+ ** This module implements preprocessing phases designed to simplify ITE
+ ** expressions. Based on:
+ ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
+ ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
+ **/
+
+
+#include "theory/ite_utilities.h"
+#include <utility>
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace std;
+namespace CVC4 {
+namespace theory {
+
+namespace ite {
+inline static bool isTermITE(TNode e) {
+ return (e.getKind() == kind::ITE && !e.getType().isBoolean());
+}
+
+inline static bool triviallyContainsNoTermITEs(TNode e) {
+ return e.isConst() || e.isVar();
+}
+
+static bool isTheoryAtom(TNode a){
+ using namespace kind;
+ switch(a.getKind()){
+ case EQUAL:
+ case DISTINCT:
+ return !(a[0].getType().isBoolean());
+
+ /* from uf */
+ case APPLY_UF:
+ return a.getType().isBoolean();
+ case CARDINALITY_CONSTRAINT:
+ case DIVISIBLE:
+ case LT:
+ case LEQ:
+ case GT:
+ case GEQ:
+ case IS_INTEGER:
+ case BITVECTOR_COMP:
+ case BITVECTOR_ULT:
+ case BITVECTOR_ULE:
+ case BITVECTOR_UGT:
+ case BITVECTOR_UGE:
+ case BITVECTOR_SLT:
+ case BITVECTOR_SLE:
+ case BITVECTOR_SGT:
+ case BITVECTOR_SGE:
+ return true;
+ default:
+ return false;
+ }
+}
+
+struct CTIVStackElement {
+ TNode curr;
+ unsigned pos;
+ CTIVStackElement(){}
+ CTIVStackElement(TNode c) : curr(c), pos(0){ }
+};/* CTIVStackElement */
+
+} /* CVC4::theory::ite */
+
+
+
+ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+ : d_containsVisitor(containsVisitor)
+ , d_compressor(NULL)
+ , d_simplifier(NULL)
+ , d_careSimp(NULL)
+{
+ Assert(d_containsVisitor != NULL);
+}
+
+ITEUtilities::~ITEUtilities(){
+
+ if(d_simplifier != NULL){
+ delete d_simplifier;
+ }
+ if(d_compressor != NULL){
+ delete d_compressor;
+ }
+ if(d_careSimp != NULL){
+ delete d_careSimp;
+ }
+}
+
+Node ITEUtilities::simpITE(TNode assertion){
+ if(d_simplifier == NULL){
+ d_simplifier = new ITESimplifier(d_containsVisitor);
+ }
+ return d_simplifier->simpITE(assertion);
+}
+
+bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const{
+ if(d_simplifier == NULL){
+ return false;
+ }else{
+ return d_simplifier->doneALotOfWorkHeuristic();
+ }
+}
+
+/* returns false if an assertion is discovered to be equal to false. */
+bool ITEUtilities::compress(std::vector<Node>& assertions){
+ if(d_compressor == NULL){
+ d_compressor = new ITECompressor(d_containsVisitor);
+ }
+ return d_compressor->compress(assertions);
+}
+
+Node ITEUtilities::simplifyWithCare(TNode e){
+ if(d_careSimp == NULL){
+ d_careSimp = new ITECareSimplifier();
+ }
+ return d_careSimp->simplifyWithCare(e);
+}
+
+void ITEUtilities::clear(){
+ if(d_simplifier != NULL){
+ d_simplifier->clearSimpITECaches();
+ }
+ if(d_compressor != NULL){
+ d_compressor->garbageCollect();
+ }
+ if(d_careSimp != NULL){
+ d_careSimp->clear();
+ }
+}
+
+/********************* */
+/* ContainsTermITEVistor
+ */
+ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
+ContainsTermITEVistor::~ContainsTermITEVistor(){}
+bool ContainsTermITEVistor::containsTermITE(TNode e){
+ /* throughout execution skip through NOT nodes. */
+ e = (e.getKind() == kind::NOT) ? e[0] : e;
+ if(ite::triviallyContainsNoTermITEs(e)){ return false; }
+
+ NodeBoolMap::const_iterator end = d_cache.end();
+ NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
+ if(tmp_it != end){
+ return (*tmp_it).second;
+ }
+
+ bool foundTermIte = false;
+ std::vector<ite::CTIVStackElement> stack;
+ stack.push_back(ite::CTIVStackElement(e));
+ while(!foundTermIte && !stack.empty()){
+ ite::CTIVStackElement& top = stack.back();
+ TNode curr = top.curr;
+ if(top.pos >= curr.getNumChildren()){
+ // all of the children have been visited
+ // no term ites were found
+ d_cache[curr] = false;
+ stack.pop_back();
+ }else{
+ // this is someone's child
+ TNode child = curr[top.pos];
+ child = (child.getKind() == kind::NOT) ? child[0] : child;
+ ++top.pos;
+ if(ite::triviallyContainsNoTermITEs(child)){
+ // skip
+ }else{
+ tmp_it = d_cache.find(child);
+ if(tmp_it != end){
+ foundTermIte = (*tmp_it).second;
+ }else{
+ stack.push_back(ite::CTIVStackElement(child));
+ foundTermIte = ite::isTermITE(child);
+ }
+ }
+ }
+ }
+ if(foundTermIte){
+ while(!stack.empty()){
+ TNode curr = stack.back().curr;
+ stack.pop_back();
+ d_cache[curr] = true;
+ }
+ }
+ return foundTermIte;
+}
+void ContainsTermITEVistor::garbageCollect() {
+ d_cache.clear();
+}
+
+/********************* */
+/* IncomingArcCounter
+ */
+IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
+ : d_reachCount()
+ , d_skipVariables(skipVars)
+ , d_skipConstants(skipConstants)
+{}
+IncomingArcCounter::~IncomingArcCounter(){}
+
+void IncomingArcCounter::computeReachability(const std::vector<Node>& assertions){
+ std::vector<TNode> tovisit(assertions.begin(), assertions.end());
+
+ while(!tovisit.empty()){
+ TNode back = tovisit.back();
+ tovisit.pop_back();
+
+ bool skip = false;
+ switch(back.getMetaKind()){
+ case kind::metakind::CONSTANT:
+ skip = d_skipConstants;
+ break;
+ case kind::metakind::VARIABLE:
+ skip = d_skipVariables;
+ break;
+ default:
+ break;
+ }
+
+ if(skip) { continue; }
+ if(d_reachCount.find(back) != d_reachCount.end()){
+ d_reachCount[back] = 1 + d_reachCount[back];
+ }else{
+ d_reachCount[back] = 1;
+ for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){
+ tovisit.push_back(*cit);
+ }
+ }
+ }
+}
+
+void IncomingArcCounter::clear() {
+ d_reachCount.clear();
+}
+
+/********************* */
+/* ITECompressor
+ */
+ITECompressor::ITECompressor(ContainsTermITEVistor* contains)
+ : d_contains(contains)
+ , d_assertions(NULL)
+ , d_incoming(true, true)
+{
+ Assert(d_contains != NULL);
+
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECompressor::~ITECompressor() {
+ reset();
+}
+
+void ITECompressor::reset(){
+ d_incoming.clear();
+ d_compressed.clear();
+}
+
+void ITECompressor::garbageCollect(){
+ reset();
+}
+
+ITECompressor::Statistics::Statistics():
+ d_compressCalls("ite-simp::compressCalls", 0),
+ d_skolemsAdded("ite-simp::skolems", 0)
+{
+ StatisticsRegistry::registerStat(&d_compressCalls);
+ StatisticsRegistry::registerStat(&d_skolemsAdded);
+
+}
+ITECompressor::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_compressCalls);
+ StatisticsRegistry::unregisterStat(&d_skolemsAdded);
+}
+
+Node ITECompressor::push_back_boolean(Node original, Node compressed){
+ Node rewritten = Rewriter::rewrite(compressed);
+ // There is a bug if the rewritter takes a pure boolean expression
+ // and changes its theory
+ if(rewritten.isConst()){
+ d_compressed[compressed] = rewritten;
+ d_compressed[original] = rewritten;
+ d_compressed[rewritten] = rewritten;
+ return rewritten;
+ }else if(d_compressed.find(rewritten) != d_compressed.end()){
+ Node res = d_compressed[rewritten];
+ d_compressed[original] = res;
+ d_compressed[compressed] = res;
+ return res;
+ }else if(rewritten.isVar() ||
+ (rewritten.getKind() == kind::NOT && rewritten[0].isVar())){
+ d_compressed[original] = rewritten;
+ d_compressed[compressed] = rewritten;
+ d_compressed[rewritten] = rewritten;
+ return rewritten;
+ }else{
+ NodeManager* nm = NodeManager::currentNM();
+ Node skolem = nm->mkSkolem("compress_$$", nm->booleanType());
+ d_compressed[rewritten] = skolem;
+ d_compressed[original] = skolem;
+ d_compressed[compressed] = skolem;
+
+ Node iff = skolem.iffNode(rewritten);
+ d_assertions->push_back(iff);
+ ++(d_statistics.d_skolemsAdded);
+ return skolem;
+ }
+}
+
+bool ITECompressor::multipleParents(TNode c){
+ return d_incoming.lookupIncoming(c) >= 2;
+}
+
+Node ITECompressor::compressBooleanITEs(Node toCompress){
+ Assert(toCompress.getKind() == kind::ITE);
+ Assert(toCompress.getType().isBoolean());
+
+ if(!(toCompress[1] == d_false || toCompress[2] == d_false)){
+ Node cmpCnd = compressBoolean(toCompress[0]);
+ if(cmpCnd.isConst()){
+ Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
+ Node res = compressBoolean(branch);
+ d_compressed[toCompress] = res;
+ return res;
+ }else{
+ Node cmpThen = compressBoolean(toCompress[1]);
+ Node cmpElse = compressBoolean(toCompress[2]);
+ Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
+ if(multipleParents(toCompress)){
+ return push_back_boolean(toCompress, newIte);
+ }else{
+ return newIte;
+ }
+ }
+ }
+
+ NodeBuilder<> nb(kind::AND);
+ Node curr = toCompress;
+ while(curr.getKind() == kind::ITE &&
+ (curr[1] == d_false || curr[2] == d_false) &&
+ (!multipleParents(curr) || curr == toCompress)){
+
+ bool negateCnd = (curr[1] == d_false);
+ Node compressCnd = compressBoolean(curr[0]);
+ if(compressCnd.isConst()){
+ if(compressCnd.getConst<bool>() == negateCnd){
+ return push_back_boolean(toCompress, d_false);
+ }else{
+ // equivalent to true don't push back
+ }
+ }else{
+ Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
+ nb << pb;
+ }
+ curr = negateCnd ? curr[2] : curr[1];
+ }
+ Assert(toCompress != curr);
+
+ nb << compressBoolean(curr);
+ Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
+ return push_back_boolean(toCompress, res);
+}
+
+Node ITECompressor::compressTerm(Node toCompress){
+ if(toCompress.isConst() || toCompress.isVar()){
+ return toCompress;
+ }
+
+ if(d_compressed.find(toCompress) != d_compressed.end()){
+ return d_compressed[toCompress];
+ }
+ if(toCompress.getKind() == kind::ITE){
+ Node cmpCnd = compressBoolean(toCompress[0]);
+ if(cmpCnd.isConst()){
+ Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
+ Node res = compressTerm(toCompress);
+ d_compressed[toCompress] = res;
+ return res;
+ }else{
+ Node cmpThen = compressTerm(toCompress[1]);
+ Node cmpElse = compressTerm(toCompress[2]);
+ Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
+ d_compressed[toCompress] = newIte;
+ return newIte;
+ }
+ }
+
+ NodeBuilder<> nb(toCompress.getKind());
+
+ if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << (toCompress.getOperator());
+ }
+ for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+ nb << compressTerm(*it);
+ }
+ Node compressed = (Node)nb;
+ if(multipleParents(toCompress)){
+ d_compressed[toCompress] = compressed;
+ }
+ return compressed;
+}
+
+Node ITECompressor::compressBoolean(Node toCompress){
+ static int instance = 0;
+ ++instance;
+ if(toCompress.isConst() || toCompress.isVar()){
+ return toCompress;
+ }
+ if(d_compressed.find(toCompress) != d_compressed.end()){
+ return d_compressed[toCompress];
+ }else if(toCompress.getKind() == kind::ITE){
+ return compressBooleanITEs(toCompress);
+ }else{
+ bool ta = ite::isTheoryAtom(toCompress);
+ NodeBuilder<> nb(toCompress.getKind());
+ if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << (toCompress.getOperator());
+ }
+ for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+ Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
+ nb << pb;
+ }
+ Node compressed = nb;
+ if(ta || multipleParents(toCompress)){
+ return push_back_boolean(toCompress, compressed);
+ }else{
+ return compressed;
+ }
+ }
+}
+
+
+
+bool ITECompressor::compress(std::vector<Node>& assertions){
+ reset();
+
+ d_assertions = &assertions;
+ d_incoming.computeReachability(assertions);
+
+ ++(d_statistics.d_compressCalls);
+ Chat() << "Computed reachability" << endl;
+
+ bool nofalses = true;
+ size_t original_size = assertions.size();
+ Chat () << "compressing " << original_size << endl;
+ for(size_t i = 0; i < original_size && nofalses; ++i){
+ Node assertion = assertions[i];
+ Node compressed = compressBoolean(assertion);
+ Node rewritten = Rewriter::rewrite(compressed);
+ assertions[i] = rewritten;
+ Assert(!d_contains->containsTermITE(rewritten));
+
+ nofalses = (rewritten != d_false);
+ }
+
+ d_assertions = NULL;
+
+ return nofalses;
+}
+
+TermITEHeightCounter::TermITEHeightCounter()
+ :d_termITEHeight()
+{}
+
+TermITEHeightCounter::~TermITEHeightCounter(){}
+
+void TermITEHeightCounter::clear(){
+ d_termITEHeight.clear();
+}
+
+size_t TermITEHeightCounter::cache_size() const{
+ return d_termITEHeight.size();
+}
+
+namespace ite {
+struct TITEHStackElement {
+ TNode curr;
+ unsigned pos;
+ uint32_t maxChildHeight;
+ TITEHStackElement(){}
+ TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0){ }
+};
+} /* namespace ite */
+
+uint32_t TermITEHeightCounter::termITEHeight(TNode e){
+
+ if(ite::triviallyContainsNoTermITEs(e)){ return 0; }
+
+ NodeCountMap::const_iterator end = d_termITEHeight.end();
+ NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
+ if(tmp_it != end){
+ return (*tmp_it).second;
+ }
+
+
+ uint32_t returnValue = 0;
+ // This is initially 0 as the very first call this is included in the max,
+ // but this has no effect.
+ std::vector<ite::TITEHStackElement> stack;
+ stack.push_back(ite::TITEHStackElement(e));
+ while(!stack.empty()){
+ ite::TITEHStackElement& top = stack.back();
+ top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
+ TNode curr = top.curr;
+ if(top.pos >= curr.getNumChildren()){
+ // done with the current node
+ returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
+ d_termITEHeight[curr] = returnValue;
+ stack.pop_back();
+ continue;
+ }else{
+ if(top.pos == 0 && curr.getKind() == kind::ITE){
+ ++top.pos;
+ returnValue = 0;
+ continue;
+ }
+ // this is someone's child
+ TNode child = curr[top.pos];
+ ++top.pos;
+ if(ite::triviallyContainsNoTermITEs(child)){
+ returnValue = 0;
+ }else{
+ tmp_it = d_termITEHeight.find(child);
+ if(tmp_it != end){
+ returnValue = (*tmp_it).second;
+ }else{
+ stack.push_back(ite::TITEHStackElement(child));
+ }
+ }
+ }
+ }
+ return returnValue;
+}
+
+
+
+ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains)
+ : d_containsVisitor(contains)
+ , d_termITEHeight()
+ , d_constantLeaves()
+ , d_allocatedConstantLeaves()
+ , d_citeEqConstApplications(0)
+ , d_constantIteEqualsConstantCache()
+ , d_replaceOverCache()
+ , d_replaceOverTermIteCache()
+ , d_leavesConstCache()
+ , d_simpConstCache()
+ , d_simpContextCache()
+ , d_simpITECache()
+{
+ Assert(d_containsVisitor != NULL);
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITESimplifier::~ITESimplifier() {
+ clearSimpITECaches();
+ Assert(d_constantLeaves.empty());
+ Assert(d_allocatedConstantLeaves.empty());
+}
+
+bool ITESimplifier::leavesAreConst(TNode e){
+ return leavesAreConst(e, theory::Theory::theoryOf(e));
+}
+
+void ITESimplifier::clearSimpITECaches(){
+ Chat() << "clear ite caches " << endl;
+ for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){
+ NodeVec* curr = d_allocatedConstantLeaves[i];
+ delete curr;
+ }
+ d_citeEqConstApplications = 0;
+ d_constantLeaves.clear();
+ d_allocatedConstantLeaves.clear();
+ d_termITEHeight.clear();
+ d_constantIteEqualsConstantCache.clear();
+ d_replaceOverCache.clear();
+ d_replaceOverTermIteCache.clear();
+ d_simpITECache.clear();
+ d_simpVars.clear();
+ d_simpConstCache.clear();
+ d_leavesConstCache.clear();
+ d_simpContextCache.clear();
+}
+
+bool ITESimplifier::doneALotOfWorkHeuristic() const {
+ static const size_t SIZE_BOUND = 1000;
+ Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl;
+ return (d_citeEqConstApplications > SIZE_BOUND);
+}
+
+ITESimplifier::Statistics::Statistics():
+ d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
+ d_unexpected("ite-simp::unexpected", 0),
+ d_unsimplified("ite-simp::unsimplified", 0),
+ d_exactMatchFold("ite-simp::exactMatchFold", 0),
+ d_binaryPredFold("ite-simp::binaryPredFold", 0),
+ d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
+ d_simpITEVisits("ite-simp::simpITE.visits", 0),
+ d_inSmaller("ite-simp::inSmaller")
+{
+ StatisticsRegistry::registerStat(&d_maxNonConstantsFolded);
+ StatisticsRegistry::registerStat(&d_unexpected);
+ StatisticsRegistry::registerStat(&d_unsimplified);
+ StatisticsRegistry::registerStat(&d_exactMatchFold);
+ StatisticsRegistry::registerStat(&d_binaryPredFold);
+ StatisticsRegistry::registerStat(&d_specialEqualityFolds);
+ StatisticsRegistry::registerStat(&d_simpITEVisits);
+ StatisticsRegistry::registerStat(&d_inSmaller);
+}
+
+ITESimplifier::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded);
+ StatisticsRegistry::unregisterStat(&d_unexpected);
+ StatisticsRegistry::unregisterStat(&d_unsimplified);
+ StatisticsRegistry::unregisterStat(&d_exactMatchFold);
+ StatisticsRegistry::unregisterStat(&d_binaryPredFold);
+ StatisticsRegistry::unregisterStat(&d_specialEqualityFolds);
+ StatisticsRegistry::unregisterStat(&d_simpITEVisits);
+ StatisticsRegistry::unregisterStat(&d_inSmaller);
+}
+
+bool ITESimplifier::isConstantIte(TNode e){
+ if(e.isConst()){
+ return true;
+ }else if(ite::isTermITE(e)){
+ NodeVec* constants = computeConstantLeaves(e);
+ return constants != NULL;
+ }else{
+ return false;
+ }
+}
+
+ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
+ Assert(ite::isTermITE(ite));
+ ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
+ ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
+ if(it != end){
+ return (*it).second;
+ }
+ TNode thenB = ite[1];
+ TNode elseB = ite[2];
+
+ // special case 2 constant children
+ if(thenB.isConst() && elseB.isConst()){
+ NodeVec* pair = new NodeVec(2);
+ (*pair)[0] = std::min(thenB, elseB);
+ (*pair)[1] = std::max(thenB, elseB);
+ d_constantLeaves[ite] = pair;
+ return pair;
+ }
+ // At least 1 is an ITE
+ if(!(thenB.isConst() || thenB.getKind() == kind::ITE) ||
+ !(elseB.isConst() || elseB.getKind() == kind::ITE)){
+ // Cannot be a termITE tree
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ // At least 1 is not a constant
+ TNode definitelyITE = thenB.isConst() ? elseB : thenB;
+ TNode maybeITE = thenB.isConst() ? thenB : elseB;
+
+ NodeVec* defChildren = computeConstantLeaves(definitelyITE);
+ if(defChildren == NULL){
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ NodeVec scratch;
+ NodeVec* maybeChildren = NULL;
+ if(maybeITE.getKind() == kind::ITE){
+ maybeChildren = computeConstantLeaves(maybeITE);
+ }else{
+ scratch.push_back(maybeITE);
+ maybeChildren = &scratch;
+ }
+ if(maybeChildren == NULL){
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size());
+ NodeVec::iterator newEnd;
+ newEnd = std::set_union(defChildren->begin(), defChildren->end(),
+ maybeChildren->begin(), maybeChildren->end(),
+ both->begin());
+ both->resize(newEnd - both->begin());
+ d_constantLeaves[ite] = both;
+ return both;
+}
+
+// This is uncached! Better for protoyping or getting limited size examples
+struct IteTreeSearchData{
+ set<Node> visited;
+ set<Node> constants;
+ set<Node> nonConstants;
+ int maxConstants;
+ int maxNonconstants;
+ int maxDepth;
+ bool failure;
+ IteTreeSearchData()
+ : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
+ {}
+};
+void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){
+ if(search.maxDepth >= 0 && depth > search.maxDepth){
+ search.failure = true;
+ }
+ if(search.failure){
+ return;
+ }
+ if(search.visited.find(e) != search.visited.end()){
+ return;
+ }else{
+ search.visited.insert(e);
+ }
+
+ if(e.isConst()){
+ search.constants.insert(e);
+ if(search.maxConstants >= 0 &&
+ search.constants.size() > (unsigned)search.maxConstants){
+ search.failure = true;
+ }
+ }else if(e.getKind() == kind::ITE){
+ iteTreeSearch(e[1], depth+1, search);
+ iteTreeSearch(e[2], depth+1, search);
+ }else{
+ search.nonConstants.insert(e);
+ if(search.maxNonconstants >= 0 &&
+ search.nonConstants.size() > (unsigned)search.maxNonconstants){
+ search.failure = true;
+ }
+ }
+}
+
+Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){
+ if(n == simpVar){
+ return replaceWith;
+ }else if(n.getNumChildren() == 0){
+ return n;
+ }
+ Assert(n.getNumChildren() > 0);
+ Assert(!n.isVar());
+
+ pair<Node, Node> p = make_pair(n, replaceWith);
+ if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){
+ return d_replaceOverCache[p];
+ }
+
+ NodeBuilder<> builder(n.getKind());
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << n.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < n.getNumChildren(); ++ i) {
+ Node newChild = replaceOver(n[i], replaceWith, simpVar);
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_replaceOverCache[p] = result;
+ return result;
+}
+
+Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){
+ if(e.getKind() == kind::ITE){
+ pair<Node, Node> p = make_pair(e, simpAtom);
+ if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){
+ return d_replaceOverTermIteCache[p];
+ }
+ Assert(!e.getType().isBoolean());
+ Node cnd = e[0];
+ Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
+ Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
+ Node newIte = cnd.iteNode(newThen, newElse);
+ d_replaceOverTermIteCache[p] = newIte;
+ return newIte;
+ }else{
+ return replaceOver(simpAtom, e, simpVar);
+ }
+}
+
+Node ITESimplifier::attemptLiftEquality(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if((left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
+ !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
+
+ // exactly 1 is an ite
+ TNode ite = left.getKind() == kind::ITE ? left :right;
+ TNode notIte = left.getKind() == kind::ITE ? right : left;
+
+ if(notIte == ite[1]){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
+ }else if(notIte == ite[2]){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
+ }
+ if(notIte.isConst() &&
+ (ite[1].isConst() || ite[2].isConst())){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
+ }
+ }
+ }
+
+ // try a similar more relaxed version for non-equality operators
+ if(atom.getMetaKind() == kind::metakind::OPERATOR &&
+ atom.getNumChildren() == 2 &&
+ !atom[1].getType().isBoolean()){
+
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if( (left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
+ !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
+ // exactly 1 is an ite
+ bool leftIsIte = left.getKind() == kind::ITE;
+ Node ite = leftIsIte ? left :right;
+ Node notIte = leftIsIte ? right : left;
+
+ if(notIte.isConst()){
+ IteTreeSearchData search;
+ search.maxNonconstants = 2;
+ iteTreeSearch(ite, 0, search);
+ if(!search.failure){
+ d_statistics.d_maxNonConstantsFolded.maxAssign(search.nonConstants.size());
+ Debug("ite::simpite") << "used " << search.nonConstants.size() << " nonconstants" << endl;
+ NodeManager* nm = NodeManager::currentNM();
+ Node simpVar = getSimpVar(notIte.getType());
+ TNode newLeft = leftIsIte ? simpVar : notIte;
+ TNode newRight = leftIsIte ? notIte : simpVar;
+ Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
+
+ ++(d_statistics.d_binaryPredFold);
+ return replaceOverTermIte(ite, newAtom, simpVar);
+ }
+ }
+ }
+ }
+
+ // TODO "This is way too tailored. Must generalize!"
+ if(atom.getKind() == kind::EQUAL &&
+ atom.getNumChildren() == 2 &&
+ ite::isTermITE(atom[0]) &&
+ atom[1].getKind() == kind::MULT &&
+ atom[1].getNumChildren() == 2 &&
+ atom[1][0].isConst() &&
+ atom[1][0].getConst<Rational>().isNegativeOne() &&
+ ite::isTermITE(atom[1][1]) &&
+ d_termITEHeight.termITEHeight(atom[0]) == 1 &&
+ d_termITEHeight.termITEHeight(atom[1][1]) == 1 &&
+ (atom[0][1].isConst() || atom[0][2].isConst()) &&
+ (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){
+ // expand all 4 cases
+
+ Node negOne = atom[1][0];
+
+ Node lite = atom[0];
+ Node lC = lite[0];
+ Node lT = lite[1];
+ Node lE = lite[2];
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node negRite = atom[1][1];
+ Node rC = negRite[0];
+ Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
+ Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
+
+ // (ite lC lT lE) = (ite rC rT rE)
+ // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
+ // (ite lc (ite rC (= lT rT) (= lT rE))
+ // (ite rC (= lE rT) (= lE rE)))
+
+ Node eqTT = lT.eqNode(rT);
+ Node eqTE = lT.eqNode(rE);
+ Node eqET = lE.eqNode(rT);
+ Node eqEE = lE.eqNode(rE);
+ Node thenLC = rC.iteNode(eqTT, eqTE);
+ Node elseLC = rC.iteNode(eqET, eqEE);
+ Node newIte = lC.iteNode(thenLC, elseLC);
+
+ ++(d_statistics.d_specialEqualityFolds);
+ return newIte;
+ }
+ return Node::null();
+}
+
+// Interesting classes of atoms:
+// 2. Contains constants and 1 constant term ite
+// 3. Contains 2 constant term ites
+Node ITESimplifier::transformAtom(TNode atom){
+ if(! d_containsVisitor->containsTermITE(atom)){
+ if(atom.getKind() == kind::EQUAL &&
+ atom[0].isConst() && atom[1].isConst()){
+ // constant equality
+ return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
+ }
+ return Node::null();
+ }else{
+ Node acr = attemptConstantRemoval(atom);
+ if(!acr.isNull()){
+ return acr;
+ }
+ // Node ale = attemptLiftEquality(atom);
+ // if(!ale.isNull()){
+ // //return ale;
+ // }
+ return Node::null();
+ }
+}
+
+static unsigned numBranches = 0;
+static unsigned numFalseBranches = 0;
+static unsigned itesMade = 0;
+
+Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
+ static int instance = 0;
+ ++instance;
+ Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<<cite << ", " << constant<<")"<< endl;
+ if(cite.isConst()){
+ Node res = (cite == constant) ? d_true : d_false;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
+ return res;
+ }
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+
+ NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
+ if(eq_pos != d_constantIteEqualsConstantCache.end()){
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl;
+ return (*eq_pos).second;
+ }
+
+ ++d_citeEqConstApplications;
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if(std::binary_search(leaves->begin(), leaves->end(), constant)){
+ if(leaves->size() == 1){
+ // probably unreachable
+ d_constantIteEqualsConstantCache[pair] = d_true;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << d_true << endl;
+ return d_true;
+ }else{
+ Assert(cite.getKind() == kind::ITE);
+ TNode cnd = cite[0];
+ TNode tB = cite[1];
+ TNode fB = cite[2];
+ Node tEqs = constantIteEqualsConstant(tB, constant);
+ Node fEqs = constantIteEqualsConstant(fB, constant);
+ Node boolIte = cnd.iteNode(tEqs, fEqs);
+ if(!(tEqs.isConst() || fEqs.isConst())){
+ ++numBranches;
+ }
+ if(!(tEqs == d_false || fEqs == d_false)){
+ ++numFalseBranches;
+ }
+ ++itesMade;
+ d_constantIteEqualsConstantCache[pair] = boolIte;
+ //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl;
+ return boolIte;
+ }
+ }else{
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl;
+ return d_false;
+ }
+}
+
+
+Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
+ // intersect the constant ite trees lcite and rcite
+
+ if(lcite.isConst() || rcite.isConst()){
+ bool lIsConst = lcite.isConst();
+ TNode constant = lIsConst ? lcite : rcite;
+ TNode cite = lIsConst ? rcite : lcite;
+
+ (d_statistics.d_inSmaller)<< 1;
+ unsigned preItesMade = itesMade;
+ unsigned preNumBranches = numBranches;
+ unsigned preNumFalseBranches = numFalseBranches;
+ Node bterm = constantIteEqualsConstant(cite, constant);
+ Debug("intersectConstantIte")
+ << (numBranches - preNumBranches)
+ << " " << (numFalseBranches - preNumFalseBranches)
+ << " " << (itesMade - preItesMade) << endl;
+ return bterm;
+ }
+ Assert(lcite.getKind() == kind::ITE);
+ Assert(rcite.getKind() == kind::ITE);
+
+ NodeVec* leftValues = computeConstantLeaves(lcite);
+ NodeVec* rightValues = computeConstantLeaves(rcite);
+
+ uint32_t smaller = std::min(leftValues->size(), rightValues->size());
+
+ (d_statistics.d_inSmaller)<< smaller;
+ NodeVec intersection(smaller, Node::null());
+ NodeVec::iterator newEnd;
+ newEnd = std::set_intersection(leftValues->begin(), leftValues->end(),
+ rightValues->begin(), rightValues->end(),
+ intersection.begin());
+ intersection.resize(newEnd - intersection.begin());
+ if(intersection.empty()){
+ return d_false;
+ }else{
+ NodeBuilder<> nb(kind::OR);
+ NodeVec::const_iterator it = intersection.begin(), end=intersection.end();
+ for(; it != end; ++it){
+ Node inBoth = *it;
+ Node lefteq = constantIteEqualsConstant(lcite, inBoth);
+ Node righteq = constantIteEqualsConstant(rcite, inBoth);
+ Node bothHold = lefteq.andNode(righteq);
+ nb << bothHold;
+ }
+ Node result = (nb.getNumChildren() >= 1) ? (Node)nb : nb[0];
+ return result;
+ }
+}
+
+
+Node ITESimplifier::attemptEagerRemoval(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if((left.isConst() &&
+ right.getKind() == kind::ITE && isConstantIte(right)) ||
+ (right.isConst() &&
+ left.getKind() == kind::ITE && isConstantIte(left))){
+ TNode constant = left.isConst() ? left : right;
+ TNode cite = left.isConst() ? right : left;
+
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+ NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
+ if(eq_pos != d_constantIteEqualsConstantCache.end()){
+ Node ret = (*eq_pos).second;
+ if(ret.isConst()){
+ return ret;
+ }else{
+ return Node::null();
+ }
+ }
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if(!std::binary_search(leaves->begin(), leaves->end(), constant)){
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ return d_false;
+ }
+ }
+ }
+ return Node::null();
+}
+
+Node ITESimplifier::attemptConstantRemoval(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if(isConstantIte(left) && isConstantIte(right)){
+ return intersectConstantIte(left, right);
+ }
+ }
+ return Node::null();
+}
+
+
+bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
+{
+ Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
+ Theory::theoryOf(e) != THEORY_BOOL);
+ if (e.isConst()) {
+ return true;
+ }
+
+ hash_map<Node, bool, NodeHashFunction>::iterator it;
+ it = d_leavesConstCache.find(e);
+ if (it != d_leavesConstCache.end()) {
+ return (*it).second;
+ }
+
+ if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
+ d_leavesConstCache[e] = false;
+ return false;
+ }
+
+ Assert(e.getNumChildren() > 0);
+ size_t k = 0, sz = e.getNumChildren();
+
+ if (e.getKind() == kind::ITE) {
+ k = 1;
+ }
+
+ for (; k < sz; ++k) {
+ if (!leavesAreConst(e[k], tid)) {
+ d_leavesConstCache[e] = false;
+ return false;
+ }
+ }
+ d_leavesConstCache[e] = true;
+ return true;
+}
+
+
+Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar)
+{
+ NodePairMap::iterator it;
+ it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode));
+ if (it != d_simpConstCache.end()) {
+ return (*it).second;
+ }
+
+ if (iteNode.getKind() == kind::ITE) {
+ NodeBuilder<> builder(kind::ITE);
+ builder << iteNode[0];
+ unsigned i = 1;
+ for (; i < iteNode.getNumChildren(); ++ i) {
+ Node n = simpConstants(simpContext, iteNode[i], simpVar);
+ if (n.isNull()) {
+ return n;
+ }
+ builder << n;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ result = Rewriter::rewrite(result);
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
+ return result;
+ }
+
+ if (!containsTermITE(iteNode)) {
+ Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+
+ Node iteNode2;
+ Node simpVar2;
+ d_simpContextCache.clear();
+ Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
+ if (!simpContext2.isNull()) {
+ Assert(!iteNode2.isNull());
+ simpContext2 = simpContext.substitute(simpVar, simpContext2);
+ Node n = simpConstants(simpContext2, iteNode2, simpVar2);
+ if (n.isNull()) {
+ return n;
+ }
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+ return Node();
+}
+
+
+Node ITESimplifier::getSimpVar(TypeNode t)
+{
+ std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+ it = d_simpVars.find(t);
+ if (it != d_simpVars.end()) {
+ return (*it).second;
+ }
+ else {
+ Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification");
+ d_simpVars[t] = var;
+ return var;
+ }
+}
+
+
+Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
+{
+ NodeMap::iterator it;
+ it = d_simpContextCache.find(c);
+ if (it != d_simpContextCache.end()) {
+ return (*it).second;
+ }
+
+ if (!containsTermITE(c)) {
+ d_simpContextCache[c] = c;
+ return c;
+ }
+
+ if (c.getKind() == kind::ITE && !c.getType().isBoolean()) {
+ // Currently only support one ite node in a simp context
+ // Return Null if more than one is found
+ if (!iteNode.isNull()) {
+ return Node();
+ }
+ simpVar = getSimpVar(c.getType());
+ if (simpVar.isNull()) {
+ return Node();
+ }
+ d_simpContextCache[c] = simpVar;
+ iteNode = c;
+ return simpVar;
+ }
+
+ NodeBuilder<> builder(c.getKind());
+ if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << c.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < c.getNumChildren(); ++ i) {
+ Node newChild = createSimpContext(c[i], iteNode, simpVar);
+ if (newChild.isNull()) {
+ return newChild;
+ }
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_simpContextCache[c] = result;
+ return result;
+}
+typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
+ if(visited.find(x) != visited.end()){
+ return;
+ }
+ visited.insert(x);
+ if(x.getKind() == k){
+ ++reached;
+ }
+ for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){
+ countReachable_(x[i], k, visited, reached);
+ }
+}
+
+uint32_t countReachable(TNode x, Kind k){
+ NodeSet visited;
+ uint32_t reached = 0;
+ countReachable_(x, k, visited, reached);
+ return reached;
+}
+
+Node ITESimplifier::simpITEAtom(TNode atom)
+{
+ static int CVC4_UNUSED instance = 0;
+ Debug("ite::atom") << "still simplifying " << (++instance) << endl;
+ Node attempt = transformAtom(atom);
+ Debug("ite::atom") << " finished " << instance << endl;
+ if(!attempt.isNull()){
+ Node rewritten = Rewriter::rewrite(attempt);
+ Debug("ite::print-success")
+ << instance << " "
+ << "rewriting " << countReachable(rewritten, kind::ITE)
+ << " from " << countReachable(atom, kind::ITE) << endl
+ << "\t rewritten " << rewritten << endl
+ << "\t input " << atom << endl;
+ return rewritten;
+ }
+
+ if (leavesAreConst(atom)) {
+ Node iteNode;
+ Node simpVar;
+ d_simpContextCache.clear();
+ Node simpContext = createSimpContext(atom, iteNode, simpVar);
+ if (!simpContext.isNull()) {
+ if (iteNode.isNull()) {
+ Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
+ ++(d_statistics.d_unexpected);
+ Debug("ite::simpite") << instance << " "
+ << "how about?" << atom << endl;
+ Debug("ite::simpite") << instance << " "
+ << "\t" << simpContext << endl;
+ return Rewriter::rewrite(simpContext);
+ }
+ Node n = simpConstants(simpContext, iteNode, simpVar);
+ if (!n.isNull()) {
+ ++(d_statistics.d_unexpected);
+ Debug("ite::simpite") << instance << " "
+ << "here?" << atom << endl;
+ Debug("ite::simpite") << instance << " "
+ << "\t" << n << endl;
+ return n;
+ }
+ }
+ }
+ if(Debug.isOn("ite::simpite")){
+ if(countReachable(atom, kind::ITE) > 0){
+ Debug("ite::simpite") << instance << " "
+ << "remaining " << atom << endl;
+ }
+ }
+ ++(d_statistics.d_unsimplified);
+ return atom;
+}
+
+
+struct preprocess_stack_element {
+ TNode node;
+ bool children_added;
+ preprocess_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};/* struct preprocess_stack_element */
+
+
+Node ITESimplifier::simpITE(TNode assertion)
+{
+ // Do a topological sort of the subexpressions and substitute them
+ vector<preprocess_stack_element> toVisit;
+ toVisit.push_back(assertion);
+
+ static int call = 0;
+ ++call;
+ int iteration = 0;
+
+ while (!toVisit.empty())
+ {
+ iteration ++;
+ //cout << "call " << call << " : " << iteration << endl;
+ // The current node we are processing
+ preprocess_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
+
+ // If node has no ITE's or already in the cache we're done, pop from the stack
+ if (current.getNumChildren() == 0 ||
+ (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) {
+ d_simpITECache[current] = current;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ continue;
+ }
+
+ NodeMap::iterator find = d_simpITECache.find(current);
+ if (find != d_simpITECache.end()) {
+ toVisit.pop_back();
+ continue;
+ }
+
+ // Not yet substituted, so process
+ if (stackHead.children_added) {
+ // Children have been processed, so substitute
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
+ Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
+ Node child = current[i];
+ Node childRes = d_simpITECache[current[i]];
+ builder << childRes;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+
+ // If this is an atom, we process it
+ if (Theory::theoryOf(result) != THEORY_BOOL &&
+ result.getType().isBoolean()) {
+ result = simpITEAtom(result);
+ }
+
+ // if(current != result && result.isConst()){
+ // static int instance = 0;
+ // //cout << instance << " " << result << current << endl;
+ // }
+
+ result = Rewriter::rewrite(result);
+ d_simpITECache[current] = result;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ } else {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0) {
+ stackHead.children_added = true;
+ // We need to add the children
+ for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+ TNode childNode = *child_it;
+ NodeMap::iterator childFind = d_simpITECache.find(childNode);
+ if (childFind == d_simpITECache.end()) {
+ toVisit.push_back(childNode);
+ }
+ }
+ } else {
+ // No children, so we're done
+ d_simpITECache[current] = current;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ }
+ }
+ }
+ return d_simpITECache[assertion];
+}
+
+ITECareSimplifier::ITECareSimplifier()
+ : d_usedSets()
+{
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECareSimplifier::~ITECareSimplifier(){}
+
+void ITECareSimplifier::clear(){
+ d_usedSets.clear();
+}
+
+ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
+{
+ if (d_usedSets.empty()) {
+ return ITECareSimplifier::CareSetPtr::mkNew(*this);
+ }
+ else {
+ ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
+ cs.getCareSet().clear();
+ d_usedSets.pop_back();
+ return cs;
+ }
+}
+
+
+void ITECareSimplifier::updateQueue(CareMap& queue,
+ TNode e,
+ ITECareSimplifier::CareSetPtr& careSet)
+{
+ CareMap::iterator it = queue.find(e), iend = queue.end();
+ if (it != iend) {
+ set<Node>& cs2 = (*it).second.getCareSet();
+ ITECareSimplifier::CareSetPtr csNew = getNewSet();
+ set_intersection(careSet.getCareSet().begin(),
+ careSet.getCareSet().end(),
+ cs2.begin(), cs2.end(),
+ inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
+ (*it).second = csNew;
+ }
+ else {
+ queue[e] = careSet;
+ }
+}
+
+
+Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
+{
+ TNodeMap::iterator it = cache.find(e), iend = cache.end();
+ if (it != iend) {
+ return it->second;
+ }
+
+ // do substitution?
+ it = substTable.find(e);
+ iend = substTable.end();
+ if (it != iend) {
+ Node result = substitute(it->second, substTable, cache);
+ cache[e] = result;
+ return result;
+ }
+
+ size_t sz = e.getNumChildren();
+ if (sz == 0) {
+ cache[e] = e;
+ return e;
+ }
+
+ NodeBuilder<> builder(e.getKind());
+ if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << e.getOperator();
+ }
+ for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
+ builder << substitute(e[i], substTable, cache);
+ }
+
+ Node result = builder;
+ // it = substTable.find(result);
+ // if (it != iend) {
+ // result = substitute(it->second, substTable, cache);
+ // }
+ cache[e] = result;
+ return result;
+}
+
+
+Node ITECareSimplifier::simplifyWithCare(TNode e)
+{
+ TNodeMap substTable;
+ CareMap queue;
+ CareMap::iterator it;
+ ITECareSimplifier::CareSetPtr cs = getNewSet();
+ ITECareSimplifier::CareSetPtr cs2;
+ queue[e] = cs;
+
+ TNode v;
+ bool done;
+ unsigned i;
+
+ while (!queue.empty()) {
+ it = queue.end();
+ --it;
+ v = it->first;
+ cs = it->second;
+ set<Node>& css = cs.getCareSet();
+ queue.erase(v);
+
+ done = false;
+ set<Node>::iterator iCare, iCareEnd = css.end();
+
+ switch (v.getKind()) {
+ case kind::ITE: {
+ iCare = css.find(v[0]);
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[1];
+ updateQueue(queue, v[1], cs);
+ done = true;
+ break;
+ }
+ else {
+ iCare = css.find(v[0].negate());
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[2];
+ updateQueue(queue, v[2], cs);
+ done = true;
+ break;
+ }
+ }
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ updateQueue(queue, v[1], cs2);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ updateQueue(queue, v[2], cs2);
+ done = true;
+ break;
+ }
+ case kind::AND: {
+ for (i = 0; i < v.getNumChildren(); ++i) {
+ iCare = css.find(v[i].negate());
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_false;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ for (i = 1; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ case kind::OR: {
+ for (i = 0; i < v.getNumChildren(); ++i) {
+ iCare = css.find(v[i]);
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_true;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ for (i = 1; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ default:
+ break;
+ }
+
+ if (done) {
+ continue;
+ }
+
+ for (unsigned i = 0; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs);
+ }
+ }
+ while (!d_usedSets.empty()) {
+ delete d_usedSets.back();
+ d_usedSets.pop_back();
+ }
+
+ TNodeMap cache;
+ return substitute(e, substTable, cache);
+}
+
+
+} /* namespace theory */
+} /* namespace CVC4 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback