From f66f40912490226291d5af6c1f8b66e9ba6d7633 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 23 Aug 2018 11:05:38 -0700 Subject: Refactor ITE simplification preprocessing pass. (#2360) --- src/theory/ite_utilities.cpp | 1642 ------------------------------------------ 1 file changed, 1642 deletions(-) delete mode 100644 src/theory/ite_utilities.cpp (limited to 'src/theory/ite_utilities.cpp') diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp deleted file mode 100644 index 40a58cf57..000000000 --- a/src/theory/ite_utilities.cpp +++ /dev/null @@ -1,1642 +0,0 @@ -/********************* */ -/*! \file ite_utilities.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 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 - -#include "smt/smt_statistics_registry.h" -#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() : curr(), pos(0) {} - CTIVStackElement(TNode c) : curr(c), pos(0) {} -}; /* CTIVStackElement */ - -} /* CVC4::theory::ite */ - -ITEUtilities::ITEUtilities() - : d_containsVisitor(new ContainsTermITEVisitor()), - 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.get()); - } - 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& assertions){ - if(d_compressor == NULL){ - d_compressor = new ITECompressor(d_containsVisitor.get()); - } - 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(); - } - d_containsVisitor->garbageCollect(); -} - -/********************* */ -/* ContainsTermITEVisitor - */ -ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {} -ContainsTermITEVisitor::~ContainsTermITEVisitor(){} -bool ContainsTermITEVisitor::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 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 ContainsTermITEVisitor::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& assertions){ - std::vector 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(ContainsTermITEVisitor* contains) - : d_contains(contains) - , d_assertions(NULL) - , d_incoming(true, true) -{ - Assert(d_contains != NULL); - - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(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) -{ - smtStatisticsRegistry()->registerStat(&d_compressCalls); - smtStatisticsRegistry()->registerStat(&d_skolemsAdded); - -} -ITECompressor::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_compressCalls); - smtStatisticsRegistry()->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.eqNode(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() == 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& 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() : curr(), pos(0), maxChildHeight(0) {} - 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 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(ContainsTermITEVisitor* 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(true); - d_false = NodeManager::currentNM()->mkConst(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") -{ - smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded); - smtStatisticsRegistry()->registerStat(&d_unexpected); - smtStatisticsRegistry()->registerStat(&d_unsimplified); - smtStatisticsRegistry()->registerStat(&d_exactMatchFold); - smtStatisticsRegistry()->registerStat(&d_binaryPredFold); - smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds); - smtStatisticsRegistry()->registerStat(&d_simpITEVisits); - smtStatisticsRegistry()->registerStat(&d_inSmaller); -} - -ITESimplifier::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded); - smtStatisticsRegistry()->unregisterStat(&d_unexpected); - smtStatisticsRegistry()->unregisterStat(&d_unsimplified); - smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold); - smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold); - smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds); - smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits); - smtStatisticsRegistry()->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); - d_allocatedConstantLeaves.push_back(pair); - - (*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()); - d_allocatedConstantLeaves.push_back(both); - 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 visited; - set constants; - set 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 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 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().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(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("<" << res << endl; - return res; - } - std::pair 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 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 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; - } - - unordered_map::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(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(simpContext, iteNode)] = result; - return result; - } - - if (!containsTermITE(iteNode)) { - Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); - d_simpConstCache[pair(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(simpContext, iteNode)] = n; - return n; - } - return Node(); -} - - -Node ITESimplifier::getSimpVar(TypeNode t) -{ - std::unordered_map::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::unordered_set 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 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_careSetsOutstanding(0) - , d_usedSets() -{ - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); -} - -ITECareSimplifier::~ITECareSimplifier(){ - Assert(d_usedSets.empty()); - Assert(d_careSetsOutstanding == 0); -} - -void ITECareSimplifier::clear(){ - Assert(d_usedSets.empty()); - Assert(d_careSetsOutstanding == 0); -} - -ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet() -{ - if (d_usedSets.empty()) { - d_careSetsOutstanding++; - 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& 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; - - /* This extra block is to trigger the destructors for cs and cs2 - * before starting garbage collection. - */ - { - 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& css = cs.getCareSet(); - queue.erase(v); - - done = false; - set::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); - } - } - } - /* Perform garbage collection. */ - while (!d_usedSets.empty()) { - CareSetPtrVal* used = d_usedSets.back(); - d_usedSets.pop_back(); - Assert(used->safeToGarbageCollect()); - delete used; - Assert(d_careSetsOutstanding > 0); - d_careSetsOutstanding--; - } - - TNodeMap cache; - return substitute(e, substTable, cache); -} - -ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew( - ITECareSimplifier& simp) { - CareSetPtrVal* val = new CareSetPtrVal(simp); - return CareSetPtr(val); -} - - - -} /* namespace theory */ -} /* namespace CVC4 */ -- cgit v1.2.3