From: Aina Niemetz Date: Thu, 23 Aug 2018 18:05:38 +0000 (-0700) Subject: Refactor ITE simplification preprocessing pass. (#2360) X-Git-Tag: cvc5-1.0.0~4734 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f66f40912490226291d5af6c1f8b66e9ba6d7633;p=cvc5.git Refactor ITE simplification preprocessing pass. (#2360) --- diff --git a/src/Makefile.am b/src/Makefile.am index 6a21566e0..3b8a12fa5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -83,6 +83,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/ite_removal.cpp \ preprocessing/passes/ite_removal.h \ + preprocessing/passes/ite_simp.cpp \ + preprocessing/passes/ite_simp.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ preprocessing/passes/bool_to_bv.cpp \ @@ -115,6 +117,8 @@ libcvc4_la_SOURCES = \ preprocessing/preprocessing_pass_context.h \ preprocessing/preprocessing_pass_registry.cpp \ preprocessing/preprocessing_pass_registry.h \ + preprocessing/util/ite_utilities.cpp \ + preprocessing/util/ite_utilities.h \ printer/dagification_visitor.cpp \ printer/dagification_visitor.h \ printer/printer.cpp \ @@ -205,8 +209,6 @@ libcvc4_la_SOURCES = \ theory/evaluator.cpp \ theory/evaluator.h \ theory/interrupted.h \ - theory/ite_utilities.cpp \ - theory/ite_utilities.h \ theory/logic_info.cpp \ theory/logic_info.h \ theory/output_channel.h \ diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp new file mode 100644 index 000000000..137925f77 --- /dev/null +++ b/src/preprocessing/passes/ite_simp.cpp @@ -0,0 +1,263 @@ +/********************* */ +/*! \file ite_simp.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 ITE simplification preprocessing pass. + **/ + +#include "preprocessing/passes/ite_simp.h" + +#include "options/proof_options.h" +#include "smt/smt_statistics_registry.h" +#include "smt_util/nary_builder.h" +#include "theory/arith/arith_ite_utils.h" + +#include + +using namespace CVC4; +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/* -------------------------------------------------------------------------- */ + +namespace { + +Node simpITE(util::ITEUtilities* ite_utils, TNode assertion) +{ + if (!ite_utils->containsTermITE(assertion)) + { + return assertion; + } + else + { + Node result = ite_utils->simpITE(assertion); + Node res_rewritten = Rewriter::rewrite(result); + + if (options::simplifyWithCareEnabled()) + { + Chat() << "starting simplifyWithCare()" << endl; + Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten); + Chat() << "ending simplifyWithCare()" + << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; + result = Rewriter::rewrite(postSimpWithCare); + } + else + { + result = res_rewritten; + } + return result; + } +} + +/** + * Ensures the assertions asserted after index 'before' now effectively come + * before 'real_assertions_end'. + */ +void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, + size_t before) +{ + size_t cur_size = assertionsToPreprocess->size(); + if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0 + || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size) + { + return; + } + + // assertions + // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd()) + // can be modified + // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before) + // cannot be moved + // added [before, cur_size) + // can be modified + Assert(0 < assertionsToPreprocess->getRealAssertionsEnd()); + Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before); + Assert(before < cur_size); + + std::vector intoConjunction; + for (size_t i = before; i < cur_size; ++i) + { + intoConjunction.push_back((*assertionsToPreprocess)[i]); + } + assertionsToPreprocess->resize(before); + size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; + intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); + Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + assertionsToPreprocess->replace(lastBeforeItes, newLast); + Assert(assertionsToPreprocess->size() == before); +} + +} // namespace + +/* -------------------------------------------------------------------------- */ + +ITESimp::Statistics::Statistics() + : d_arithSubstitutionsAdded( + "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0) +{ + smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); +} + +ITESimp::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); +} + +bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) +{ + // This pass does not support dependency tracking yet + // (learns substitutions from all assertions so just + // adding addDependence is not enough) + if (options::unsatCores() || options::fewerPreprocessingHoles()) + { + return true; + } + bool result = true; + bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); + if (simpDidALotOfWork) + { + if (options::compressItes()) + { + result = d_iteUtilities.compress(assertionsToPreprocess->ref()); + } + + if (result) + { + // if false, don't bother to reclaim memory here. + NodeManager* nm = NodeManager::currentNM(); + if (nm->poolSize() >= options::zombieHuntThreshold()) + { + Chat() << "..ite simplifier did quite a bit of work.. " + << nm->poolSize() << endl; + Chat() << "....node manager contains " << nm->poolSize() + << " nodes before cleanup" << endl; + d_iteUtilities.clear(); + Rewriter::clearCaches(); + nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + Chat() << "....node manager contains " << nm->poolSize() + << " nodes after cleanup" << endl; + } + } + } + + // Do theory specific preprocessing passes + TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine(); + if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH) + && !options::incrementalSolving()) + { + if (!simpDidALotOfWork) + { + util::ContainsTermITEVisitor& contains = + *(d_iteUtilities.getContainsVisitor()); + arith::ArithIteUtils aiteu(contains, + d_preprocContext->getUserContext(), + theory_engine->getModel()); + bool anyItes = false; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + if (contains.containsTermITE(curr)) + { + anyItes = true; + Node res = aiteu.reduceVariablesInItes(curr); + Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl + << " ->" << res << endl; + if (curr != res) + { + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + if (!anyItes) + { + unsigned prevSubCount = aiteu.getSubCount(); + aiteu.learnSubstitutions(assertionsToPreprocess->ref()); + if (prevSubCount < aiteu.getSubCount()) + { + d_statistics.d_arithSubstitutionsAdded += + aiteu.getSubCount() - prevSubCount; + bool anySuccess = false; + for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + if (more != next) + { + anySuccess = true; + break; + } + } + for (size_t i = 0, N = assertionsToPreprocess->size(); + anySuccess && i < N; + ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + } + } + return result; +} + +/* -------------------------------------------------------------------------- */ + +ITESimp::ITESimp(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ite-simp") +{ +} + +PreprocessingPassResult ITESimp::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + d_preprocContext->spendResource(options::preprocessStep()); + + size_t nasserts = assertionsToPreprocess->size(); + for (size_t i = 0; i < nasserts; ++i) + { + d_preprocContext->spendResource(options::preprocessStep()); + Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]); + assertionsToPreprocess->replace(i, simp); + if (simp.isConst() && !simp.getConst()) + { + return PreprocessingPassResult::CONFLICT; + } + } + bool done = doneSimpITE(assertionsToPreprocess); + if (nasserts < assertionsToPreprocess->size()) + { + compressBeforeRealAssertions(assertionsToPreprocess, nasserts); + } + return done ? PreprocessingPassResult::NO_CONFLICT + : PreprocessingPassResult::CONFLICT; +} + +/* -------------------------------------------------------------------------- */ + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h new file mode 100644 index 000000000..2296d663e --- /dev/null +++ b/src/preprocessing/passes/ite_simp.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file ite_simp.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 ITE simplification preprocessing pass. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class ITESimp : public PreprocessingPass +{ + public: + ITESimp(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + struct Statistics + { + IntStat d_arithSubstitutionsAdded; + Statistics(); + ~Statistics(); + }; + + bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss); + + /** A collection of ite preprocessing passes. */ + util::ITEUtilities d_iteUtilities; + + Statistics d_statistics; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index b50421e6c..a289752fa 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -2,7 +2,7 @@ /*! \file preprocessing_pass_context.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Aina Niemetz, Mathias Preiner + ** Justin Xu, Andres Noetzli, Aina Niemetz ** 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. @@ -23,6 +23,7 @@ #include "context/context.h" #include "decision/decision_engine.h" +#include "preprocessing/util/ite_utilities.h" #include "smt/smt_engine.h" #include "smt/term_formula_removal.h" #include "theory/theory_engine.h" diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp new file mode 100644 index 000000000..66d9151df --- /dev/null +++ b/src/preprocessing/util/ite_utilities.cpp @@ -0,0 +1,1908 @@ +/********************* */ +/*! \file ite_utilities.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz, 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 "preprocessing/util/ite_utilities.h" + +#include + +#include "preprocessing/passes/rewrite.h" +#include "smt/smt_statistics_registry.h" +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace std; +namespace CVC4 { +namespace preprocessing { +namespace util { + +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 */ + +} // namespace 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 = theory::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 = theory::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(" << cite << ", " << constant + << ")" << endl; + if (cite.isConst()) + { + Node res = (cite == constant) ? d_true : d_false; + Debug("ite::constantIteEqualsConstant") << instance << "->" << 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, theory::TheoryId tid) +{ + Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) + || theory::Theory::theoryOf(e) != theory::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::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 = theory::Rewriter::rewrite(result); + d_simpConstCache[pair(simpContext, iteNode)] = result; + return result; + } + + if (!containsTermITE(iteNode)) + { + Node n = + theory::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 = theory::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 theory::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::Theory::theoryOf(current) != theory::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::Theory::theoryOf(result) != theory::THEORY_BOOL + && result.getType().isBoolean()) + { + result = simpITEAtom(result); + } + + // if(current != result && result.isConst()){ + // static int instance = 0; + // //cout << instance << " " << result << current << endl; + // } + + result = theory::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 util +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h new file mode 100644 index 000000000..e137749db --- /dev/null +++ b/src/preprocessing/util/ite_utilities.h @@ -0,0 +1,420 @@ +/********************* */ +/*! \file ite_utilities.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz, Paul Meng + ** 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 "cvc4_private.h" + +#ifndef __CVC4__ITE_UTILITIES_H +#define __CVC4__ITE_UTILITIES_H + +#include +#include + +#include "expr/node.h" +#include "util/hash.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace preprocessing { +namespace util { + +class IncomingArcCounter; +class TermITEHeightCounter; +class ITECompressor; +class ITESimplifier; +class ITECareSimplifier; + +/** + * A caching visitor that computes whether a node contains a term ite. + */ +class ContainsTermITEVisitor +{ + public: + ContainsTermITEVisitor(); + ~ContainsTermITEVisitor(); + + /** returns true if a node contains a term ite. */ + bool containsTermITE(TNode n); + + /** Garbage collects the cache. */ + void garbageCollect(); + + /** returns the size of the cache. */ + size_t cache_size() const { return d_cache.size(); } + + private: + typedef std::unordered_map NodeBoolMap; + NodeBoolMap d_cache; +}; + +class ITEUtilities +{ + public: + ITEUtilities(); + ~ITEUtilities(); + + Node simpITE(TNode assertion); + + bool simpIteDidALotOfWorkHeuristic() const; + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector& assertions); + + Node simplifyWithCare(TNode e); + + void clear(); + + ContainsTermITEVisitor* getContainsVisitor() + { + return d_containsVisitor.get(); + } + + bool containsTermITE(TNode n) + { + return d_containsVisitor->containsTermITE(n); + } + + private: + std::unique_ptr d_containsVisitor; + ITECompressor* d_compressor; + ITESimplifier* d_simplifier; + ITECareSimplifier* d_careSimp; +}; + +class IncomingArcCounter +{ + public: + IncomingArcCounter(bool skipVars = false, bool skipConstants = false); + ~IncomingArcCounter(); + void computeReachability(const std::vector& assertions); + + inline uint32_t lookupIncoming(Node n) const + { + NodeCountMap::const_iterator it = d_reachCount.find(n); + if (it == d_reachCount.end()) + { + return 0; + } + else + { + return (*it).second; + } + } + void clear(); + + private: + typedef std::unordered_map NodeCountMap; + NodeCountMap d_reachCount; + + bool d_skipVariables; + bool d_skipConstants; +}; + +class TermITEHeightCounter +{ + public: + TermITEHeightCounter(); + ~TermITEHeightCounter(); + + /** + * Compute and [potentially] cache the termITEHeight() of e. + * The term ite height equals the maximum number of term ites + * encountered on any path from e to a leaf. + * Inductively: + * - termITEHeight(leaves) = 0 + * - termITEHeight(e: term-ite(c, t, e) ) = + * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c + * - termITEHeight(e not term ite) = max_{c in children(e)) + * (termITEHeight(c)) + */ + uint32_t termITEHeight(TNode e); + + /** Clear the cache. */ + void clear(); + + /** Size of the cache. */ + size_t cache_size() const; + + private: + typedef std::unordered_map NodeCountMap; + NodeCountMap d_termITEHeight; +}; /* class TermITEHeightCounter */ + +/** + * A routine designed to undo the potentially large blow up + * due to expansion caused by the ite simplifier. + */ +class ITECompressor +{ + public: + ITECompressor(ContainsTermITEVisitor* contains); + ~ITECompressor(); + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector& assertions); + + /* garbage Collects the compressor. */ + void garbageCollect(); + + private: + Node d_true; /* Copy of true. */ + Node d_false; /* Copy of false. */ + ContainsTermITEVisitor* d_contains; + std::vector* d_assertions; + IncomingArcCounter d_incoming; + + typedef std::unordered_map NodeMap; + NodeMap d_compressed; + + void reset(); + + Node push_back_boolean(Node original, Node compressed); + bool multipleParents(TNode c); + Node compressBooleanITEs(Node toCompress); + Node compressTerm(Node toCompress); + Node compressBoolean(Node toCompress); + + class Statistics + { + public: + IntStat d_compressCalls; + IntStat d_skolemsAdded; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; /* class ITECompressor */ + +class ITESimplifier +{ + public: + ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); + ~ITESimplifier(); + + Node simpITE(TNode assertion); + + bool doneALotOfWorkHeuristic() const; + void clearSimpITECaches(); + + private: + Node d_true; + Node d_false; + + ContainsTermITEVisitor* d_containsVisitor; + inline bool containsTermITE(TNode n) + { + return d_containsVisitor->containsTermITE(n); + } + TermITEHeightCounter d_termITEHeight; + inline uint32_t termITEHeight(TNode e) + { + return d_termITEHeight.termITEHeight(e); + } + + // ConstantIte is a small inductive sublanguage: + // constant + // or termITE(cnd, ConstantIte, ConstantIte) + typedef std::vector NodeVec; + typedef std::unordered_map + ConstantLeavesMap; + ConstantLeavesMap d_constantLeaves; + + // d_constantLeaves satisfies the following invariants: + // not containsTermITE(x) then !isKey(x) + // containsTermITE(x): + // - not isKey(x) then this value is uncomputed + // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf + // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant + // leaf + bool isConstantIte(TNode e); + + /** If its not a constant and containsTermITE(ite), + * returns a sorted NodeVec of the leaves. */ + NodeVec* computeConstantLeaves(TNode ite); + + // Lists all of the vectors in d_constantLeaves for fast deletion. + std::vector d_allocatedConstantLeaves; + + /* transforms */ + Node transformAtom(TNode atom); + Node attemptConstantRemoval(TNode atom); + Node attemptLiftEquality(TNode atom); + Node attemptEagerRemoval(TNode atom); + + // Given ConstantIte trees lcite and rcite, + // return a boolean expression equivalent to (= lcite rcite) + Node intersectConstantIte(TNode lcite, TNode rcite); + + // Given ConstantIte tree cite and a constant c, + // return a boolean expression equivalent to (= lcite c) + Node constantIteEqualsConstant(TNode cite, TNode c); + uint32_t d_citeEqConstApplications; + + typedef std::pair NodePair; + using NodePairHashFunction = + PairHashFunction; + typedef std::unordered_map NodePairMap; + NodePairMap d_constantIteEqualsConstantCache; + NodePairMap d_replaceOverCache; + NodePairMap d_replaceOverTermIteCache; + Node replaceOver(Node n, Node replaceWith, Node simpVar); + Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); + + std::unordered_map d_leavesConstCache; + bool leavesAreConst(TNode e, theory::TheoryId tid); + bool leavesAreConst(TNode e); + + NodePairMap d_simpConstCache; + Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); + std::unordered_map d_simpVars; + Node getSimpVar(TypeNode t); + + typedef std::unordered_map NodeMap; + NodeMap d_simpContextCache; + Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); + + NodeMap d_simpITECache; + Node simpITEAtom(TNode atom); + + private: + class Statistics + { + public: + IntStat d_maxNonConstantsFolded; + IntStat d_unexpected; + IntStat d_unsimplified; + IntStat d_exactMatchFold; + IntStat d_binaryPredFold; + IntStat d_specialEqualityFolds; + IntStat d_simpITEVisits; + + HistogramStat d_inSmaller; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +class ITECareSimplifier +{ + public: + ITECareSimplifier(); + ~ITECareSimplifier(); + + Node simplifyWithCare(TNode e); + + void clear(); + + private: + /** + * This should always equal the number of care sets allocated by + * this object - the number of these that have been deleted. This is + * initially 0 and should always be 0 at the *start* of + * ~ITECareSimplifier(). + */ + unsigned d_careSetsOutstanding; + + Node d_true; + Node d_false; + + typedef std::unordered_map TNodeMap; + + class CareSetPtr; + class CareSetPtrVal + { + public: + bool safeToGarbageCollect() const { return d_refCount == 0; } + + private: + friend class ITECareSimplifier::CareSetPtr; + ITECareSimplifier& d_iteSimplifier; + unsigned d_refCount; + std::set d_careSet; + CareSetPtrVal(ITECareSimplifier& simp) + : d_iteSimplifier(simp), d_refCount(1) + { + } + }; /* class ITECareSimplifier::CareSetPtrVal */ + + std::vector d_usedSets; + void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); } + + class CareSetPtr + { + CareSetPtrVal* d_val; + CareSetPtr(CareSetPtrVal* val) : d_val(val) {} + + public: + CareSetPtr() : d_val(NULL) {} + CareSetPtr(const CareSetPtr& cs) + { + d_val = cs.d_val; + if (d_val != NULL) + { + ++(d_val->d_refCount); + } + } + ~CareSetPtr() + { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) + { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + } + CareSetPtr& operator=(const CareSetPtr& cs) + { + if (d_val != cs.d_val) + { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) + { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + d_val = cs.d_val; + if (d_val != NULL) + { + ++(d_val->d_refCount); + } + } + return *this; + } + std::set& getCareSet() { return d_val->d_careSet; } + + static CareSetPtr mkNew(ITECareSimplifier& simp); + static CareSetPtr recycle(CareSetPtrVal* val) + { + Assert(val != NULL && val->d_refCount == 0); + val->d_refCount = 1; + return CareSetPtr(val); + } + }; /* class ITECareSimplifier::CareSetPtr */ + + CareSetPtr getNewSet(); + + typedef std::map CareMap; + void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); + Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); +}; + +} // namespace util +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e7d52676..7b45bcb3c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,6 +82,7 @@ #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" +#include "preprocessing/passes/ite_simp.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" @@ -202,8 +203,6 @@ struct SmtEngineStatistics { /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; /** time spent in simplifying ITEs */ - TimerStat d_simpITETime; - /** time spent in simplifying ITEs */ TimerStat d_unconstrainedSimpTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; @@ -237,7 +236,6 @@ struct SmtEngineStatistics { d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_simpITETime("smt::SmtEngine::simpITETime"), d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), @@ -257,7 +255,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_simpITETime); smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); @@ -279,7 +276,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_simpITETime); smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); @@ -590,18 +586,9 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify ITE structure - bool simpITE(); - // Simplify based on unconstrained values void unconstrainedSimp(); - /** - * Ensures the assertions asserted after before now effectively come before - * d_realAssertionsEnd. - */ - void compressBeforeRealAssertions(size_t before); - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. @@ -2663,6 +2650,8 @@ void SmtEnginePrivate::finishInit() new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr intToBV( new IntToBV(d_preprocessingPassContext.get())); + std::unique_ptr iteSimp( + new ITESimp(d_preprocessingPassContext.get())); std::unique_ptr quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr pbProc( @@ -2705,6 +2694,7 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("global-negate", std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); + d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", @@ -3320,60 +3310,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -bool SmtEnginePrivate::simpITE() { - TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); - - spendResource(options::preprocessStep()); - - Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; - - unsigned numAssertionOnEntry = d_assertions.size(); - for (unsigned i = 0; i < d_assertions.size(); ++i) { - spendResource(options::preprocessStep()); - Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]); - d_assertions.replace(i, result); - if(result.isConst() && !result.getConst()){ - return false; - } - } - bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref()); - if(numAssertionOnEntry < d_assertions.size()){ - compressBeforeRealAssertions(numAssertionOnEntry); - } - return result; -} - -void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ - size_t curr = d_assertions.size(); - if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0 - || d_assertions.getRealAssertionsEnd() >= curr) - { - return; - } - - // assertions - // original: [0 ... d_assertions.getRealAssertionsEnd()) - // can be modified - // ites skolems [d_assertions.getRealAssertionsEnd(), before) - // cannot be moved - // added [before, curr) - // can be modified - Assert(0 < d_assertions.getRealAssertionsEnd()); - Assert(d_assertions.getRealAssertionsEnd() <= before); - Assert(before < curr); - - std::vector intoConjunction; - for(size_t i = before; id_unconstrainedSimpTime); spendResource(options::preprocessStep()); @@ -3845,11 +3781,14 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertions : " << d_assertions.size() << endl; // ITE simplification - if(options::doITESimp() && - (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) { + if (options::doITESimp() + && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) + { Chat() << "...doing ITE simplification..." << endl; - bool noConflict = simpITE(); - if(!noConflict){ + PreprocessingPassResult res = + d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions); + if (res == PreprocessingPassResult::CONFLICT) + { Chat() << "...ITE simplification found unsat..." << endl; return false; } diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index a683d2bbb..5b51e162d 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Kshitij Bansal + ** Tim King, Aina Niemetz, Kshitij Bansal ** 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. @@ -21,9 +21,9 @@ #include "base/output.h" #include "options/smt_options.h" +#include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" -#include "theory/ite_utilities.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_model.h" @@ -140,18 +140,19 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ Unreachable(); } -ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* uc, - TheoryModel* model) - : d_contains(contains) - , d_subs(NULL) - , d_model(model) - , d_one(1) - , d_subcount(uc, 0) - , d_skolems(uc) - , d_implies() - , d_skolemsAdded() - , d_orBinEqs() +ArithIteUtils::ArithIteUtils( + preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* uc, + TheoryModel* model) + : d_contains(contains), + d_subs(NULL), + d_model(model), + d_one(1), + d_subcount(uc, 0), + d_skolems(uc), + d_implies(), + d_skolemsAdded(), + d_orBinEqs() { d_subs = new SubstitutionMap(uc); } diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 7950ef05f..2c6a30758 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Aina Niemetz ** 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. @@ -29,15 +29,21 @@ #include "context/cdinsert_hashmap.h" namespace CVC4 { -namespace theory { +namespace preprocessing { +namespace util { class ContainsTermITEVisitor; +} +} // namespace preprocessing + +namespace theory { + class SubstitutionMap; class TheoryModel; namespace arith { class ArithIteUtils { - ContainsTermITEVisitor& d_contains; + preprocessing::util::ContainsTermITEVisitor& d_contains; SubstitutionMap* d_subs; TheoryModel* d_model; @@ -68,24 +74,24 @@ class ArithIteUtils { std::vector d_orBinEqs; public: - ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* userContext, - TheoryModel* model); - ~ArithIteUtils(); + ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* userContext, + TheoryModel* model); + ~ArithIteUtils(); - //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) + //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) - /** removes common sums variables sums from term ites. */ - Node reduceVariablesInItes(Node n); + /** removes common sums variables sums from term ites. */ + Node reduceVariablesInItes(Node n); - Node reduceConstantIteByGCD(Node n); + Node reduceConstantIteByGCD(Node n); - void clear(); + void clear(); - Node applySubstitutions(TNode f); - unsigned getSubCount() const; + Node applySubstitutions(TNode f); + unsigned getSubCount() const; - void learnSubstitutions(const std::vector& assertions); + void learnSubstitutions(const std::vector& assertions); private: /* applies this to all children of n and constructs the result */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 968970049..89550295a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -36,6 +36,7 @@ #include "expr/node_builder.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() +#include "preprocessing/util/ite_utilities.h" #include "smt/logic_exception.h" #include "smt/logic_request.h" #include "smt/smt_statistics_registry.h" @@ -59,7 +60,6 @@ #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" -#include "theory/ite_utilities.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -5374,7 +5374,7 @@ bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational } // TODO Speed up - ContainsTermITEVisitor ctv; + preprocessing::util::ContainsTermITEVisitor ctv; if(ctv.containsTermITE(t)){ return false; } 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 */ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h deleted file mode 100644 index bfce390eb..000000000 --- a/src/theory/ite_utilities.h +++ /dev/null @@ -1,389 +0,0 @@ -/********************* */ -/*! \file ite_utilities.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Paul Meng, 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 "cvc4_private.h" - -#ifndef __CVC4__ITE_UTILITIES_H -#define __CVC4__ITE_UTILITIES_H - -#include -#include - -#include "expr/node.h" -#include "util/hash.h" -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace theory { - -class IncomingArcCounter; -class TermITEHeightCounter; -class ITECompressor; -class ITESimplifier; -class ITECareSimplifier; - -/** - * A caching visitor that computes whether a node contains a term ite. - */ -class ContainsTermITEVisitor { -public: - ContainsTermITEVisitor(); - ~ContainsTermITEVisitor(); - - /** returns true if a node contains a term ite. */ - bool containsTermITE(TNode n); - - /** Garbage collects the cache. */ - void garbageCollect(); - - /** returns the size of the cache. */ - size_t cache_size() const { return d_cache.size(); } - -private: - typedef std::unordered_map NodeBoolMap; - NodeBoolMap d_cache; -}; - -class ITEUtilities -{ - public: - ITEUtilities(); - ~ITEUtilities(); - - Node simpITE(TNode assertion); - - bool simpIteDidALotOfWorkHeuristic() const; - - /* returns false if an assertion is discovered to be equal to false. */ - bool compress(std::vector& assertions); - - Node simplifyWithCare(TNode e); - - void clear(); - - ContainsTermITEVisitor* getContainsVisitor() - { - return d_containsVisitor.get(); - } - - bool containsTermITE(TNode n) - { - return d_containsVisitor->containsTermITE(n); - } - - private: - std::unique_ptr d_containsVisitor; - ITECompressor* d_compressor; - ITESimplifier* d_simplifier; - ITECareSimplifier* d_careSimp; -}; - -class IncomingArcCounter { -public: - IncomingArcCounter(bool skipVars = false, bool skipConstants = false); - ~IncomingArcCounter(); - void computeReachability(const std::vector& assertions); - - inline uint32_t lookupIncoming(Node n) const { - NodeCountMap::const_iterator it = d_reachCount.find(n); - if(it == d_reachCount.end()){ - return 0; - }else{ - return (*it).second; - } - } - void clear(); -private: - typedef std::unordered_map NodeCountMap; - NodeCountMap d_reachCount; - - bool d_skipVariables; - bool d_skipConstants; -}; - -class TermITEHeightCounter { -public: - TermITEHeightCounter(); - ~TermITEHeightCounter(); - - /** - * Compute and [potentially] cache the termITEHeight() of e. - * The term ite height equals the maximum number of term ites - * encountered on any path from e to a leaf. - * Inductively: - * - termITEHeight(leaves) = 0 - * - termITEHeight(e: term-ite(c, t, e) ) = - * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c - * - termITEHeight(e not term ite) = max_{c in children(e)) (termITEHeight(c)) - */ - uint32_t termITEHeight(TNode e); - - /** Clear the cache. */ - void clear(); - - /** Size of the cache. */ - size_t cache_size() const; - -private: - typedef std::unordered_map NodeCountMap; - NodeCountMap d_termITEHeight; -}; /* class TermITEHeightCounter */ - -/** - * A routine designed to undo the potentially large blow up - * due to expansion caused by the ite simplifier. - */ -class ITECompressor { -public: - ITECompressor(ContainsTermITEVisitor* contains); - ~ITECompressor(); - - /* returns false if an assertion is discovered to be equal to false. */ - bool compress(std::vector& assertions); - - /* garbage Collects the compressor. */ - void garbageCollect(); - -private: - - Node d_true; /* Copy of true. */ - Node d_false; /* Copy of false. */ - ContainsTermITEVisitor* d_contains; - std::vector* d_assertions; - IncomingArcCounter d_incoming; - - typedef std::unordered_map NodeMap; - NodeMap d_compressed; - - void reset(); - - Node push_back_boolean(Node original, Node compressed); - bool multipleParents(TNode c); - Node compressBooleanITEs(Node toCompress); - Node compressTerm(Node toCompress); - Node compressBoolean(Node toCompress); - - class Statistics { - public: - IntStat d_compressCalls; - IntStat d_skolemsAdded; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -}; /* class ITECompressor */ - -class ITESimplifier { -public: - ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); - ~ITESimplifier(); - - Node simpITE(TNode assertion); - - bool doneALotOfWorkHeuristic() const; - void clearSimpITECaches(); - -private: - Node d_true; - Node d_false; - - ContainsTermITEVisitor* d_containsVisitor; - inline bool containsTermITE(TNode n) { - return d_containsVisitor->containsTermITE(n); - } - TermITEHeightCounter d_termITEHeight; - inline uint32_t termITEHeight(TNode e) { - return d_termITEHeight.termITEHeight(e); - } - - // ConstantIte is a small inductive sublanguage: - // constant - // or termITE(cnd, ConstantIte, ConstantIte) - typedef std::vector NodeVec; - typedef std::unordered_map ConstantLeavesMap; - ConstantLeavesMap d_constantLeaves; - - // d_constantLeaves satisfies the following invariants: - // not containsTermITE(x) then !isKey(x) - // containsTermITE(x): - // - not isKey(x) then this value is uncomputed - // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf - // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant leaf - bool isConstantIte(TNode e); - - /** If its not a constant and containsTermITE(ite), - * returns a sorted NodeVec of the leaves. */ - NodeVec* computeConstantLeaves(TNode ite); - - // Lists all of the vectors in d_constantLeaves for fast deletion. - std::vector d_allocatedConstantLeaves; - - - /* transforms */ - Node transformAtom(TNode atom); - Node attemptConstantRemoval(TNode atom); - Node attemptLiftEquality(TNode atom); - Node attemptEagerRemoval(TNode atom); - - // Given ConstantIte trees lcite and rcite, - // return a boolean expression equivalent to (= lcite rcite) - Node intersectConstantIte(TNode lcite, TNode rcite); - - // Given ConstantIte tree cite and a constant c, - // return a boolean expression equivalent to (= lcite c) - Node constantIteEqualsConstant(TNode cite, TNode c); - uint32_t d_citeEqConstApplications; - - typedef std::pair NodePair; - using NodePairHashFunction = - PairHashFunction; - typedef std::unordered_map NodePairMap; - NodePairMap d_constantIteEqualsConstantCache; - NodePairMap d_replaceOverCache; - NodePairMap d_replaceOverTermIteCache; - Node replaceOver(Node n, Node replaceWith, Node simpVar); - Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); - - std::unordered_map d_leavesConstCache; - bool leavesAreConst(TNode e, theory::TheoryId tid); - bool leavesAreConst(TNode e); - - NodePairMap d_simpConstCache; - Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); - std::unordered_map d_simpVars; - Node getSimpVar(TypeNode t); - - typedef std::unordered_map NodeMap; - NodeMap d_simpContextCache; - Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); - - NodeMap d_simpITECache; - Node simpITEAtom(TNode atom); - - -private: - class Statistics { - public: - IntStat d_maxNonConstantsFolded; - IntStat d_unexpected; - IntStat d_unsimplified; - IntStat d_exactMatchFold; - IntStat d_binaryPredFold; - IntStat d_specialEqualityFolds; - IntStat d_simpITEVisits; - - HistogramStat d_inSmaller; - - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; -}; - -class ITECareSimplifier { -public: - ITECareSimplifier(); - ~ITECareSimplifier(); - - Node simplifyWithCare(TNode e); - - void clear(); -private: - - /** - * This should always equal the number of care sets allocated by - * this object - the number of these that have been deleted. This is - * initially 0 and should always be 0 at the *start* of - * ~ITECareSimplifier(). - */ - unsigned d_careSetsOutstanding; - - Node d_true; - Node d_false; - - typedef std::unordered_map TNodeMap; - - class CareSetPtr; - class CareSetPtrVal { - public: - bool safeToGarbageCollect() const { return d_refCount == 0; } - private: - friend class ITECareSimplifier::CareSetPtr; - ITECareSimplifier& d_iteSimplifier; - unsigned d_refCount; - std::set d_careSet; - CareSetPtrVal(ITECareSimplifier& simp) - : d_iteSimplifier(simp), d_refCount(1) {} - }; /* class ITECareSimplifier::CareSetPtrVal */ - - std::vector d_usedSets; - void careSetPtrGC(CareSetPtrVal* val) { - d_usedSets.push_back(val); - } - - class CareSetPtr { - CareSetPtrVal* d_val; - CareSetPtr(CareSetPtrVal* val) : d_val(val) {} - public: - CareSetPtr() : d_val(NULL) {} - CareSetPtr(const CareSetPtr& cs) { - d_val = cs.d_val; - if (d_val != NULL) { - ++(d_val->d_refCount); - } - } - ~CareSetPtr() { - if (d_val != NULL && (--(d_val->d_refCount) == 0)) { - d_val->d_iteSimplifier.careSetPtrGC(d_val); - } - } - CareSetPtr& operator=(const CareSetPtr& cs) { - if (d_val != cs.d_val) { - if (d_val != NULL && (--(d_val->d_refCount) == 0)) { - d_val->d_iteSimplifier.careSetPtrGC(d_val); - } - d_val = cs.d_val; - if (d_val != NULL) { - ++(d_val->d_refCount); - } - } - return *this; - } - std::set& getCareSet() { return d_val->d_careSet; } - - static CareSetPtr mkNew(ITECareSimplifier& simp); - static CareSetPtr recycle(CareSetPtrVal* val) { - Assert(val != NULL && val->d_refCount == 0); - val->d_refCount = 1; - return CareSetPtr(val); - } - }; /* class ITECareSimplifier::CareSetPtr */ - - CareSetPtr getNewSet(); - - typedef std::map CareMap; - void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); - Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); -}; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f5341b38b..c87a4be02 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -40,7 +40,6 @@ #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/care_graph.h" -#include "theory/ite_utilities.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -336,8 +335,6 @@ TheoryEngine::TheoryEngine(context::Context* context, ProofManager::currentPM()->initTheoryProofEngine(); #endif - d_iteUtilities = new ITEUtilities(); - smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } @@ -366,8 +363,6 @@ TheoryEngine::~TheoryEngine() { delete d_unconstrainedSimp; - delete d_iteUtilities; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2000,111 +1995,6 @@ void TheoryEngine::staticInitializeBVOptions( } } -Node TheoryEngine::ppSimpITE(TNode assertion) -{ - if (!d_iteUtilities->containsTermITE(assertion)) - { - return assertion; - } else { - Node result = d_iteUtilities->simpITE(assertion); - Node res_rewritten = Rewriter::rewrite(result); - - if(options::simplifyWithCareEnabled()){ - Chat() << "starting simplifyWithCare()" << endl; - Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten); - Chat() << "ending simplifyWithCare()" - << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; - result = Rewriter::rewrite(postSimpWithCare); - } else { - result = res_rewritten; - } - return result; - } -} - -bool TheoryEngine::donePPSimpITE(std::vector& assertions){ - // This pass does not support dependency tracking yet - // (learns substitutions from all assertions so just - // adding addDependence is not enough) - if (options::unsatCores() || options::fewerPreprocessingHoles()) { - return true; - } - bool result = true; - bool simpDidALotOfWork = d_iteUtilities->simpIteDidALotOfWorkHeuristic(); - if(simpDidALotOfWork){ - if(options::compressItes()){ - result = d_iteUtilities->compress(assertions); - } - - if(result){ - // if false, don't bother to reclaim memory here. - NodeManager* nm = NodeManager::currentNM(); - if(nm->poolSize() >= options::zombieHuntThreshold()){ - Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; - Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; - d_iteUtilities->clear(); - Rewriter::clearCaches(); - nm->reclaimZombiesUntil(options::zombieHuntThreshold()); - Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; - } - } - } - - // Do theory specific preprocessing passes - if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH) - && !options::incrementalSolving() ){ - if(!simpDidALotOfWork){ - ContainsTermITEVisitor& contains = - *(d_iteUtilities->getContainsVisitor()); - arith::ArithIteUtils aiteu(contains, d_userContext, getModel()); - bool anyItes = false; - for(size_t i = 0; i < assertions.size(); ++i){ - Node curr = assertions[i]; - if(contains.containsTermITE(curr)){ - anyItes = true; - Node res = aiteu.reduceVariablesInItes(curr); - Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl << " ->" << res << endl; - if(curr != res){ - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - assertions[i] = Rewriter::rewrite(more); - } - } - } - if(!anyItes){ - unsigned prevSubCount = aiteu.getSubCount(); - aiteu.learnSubstitutions(assertions); - if(prevSubCount < aiteu.getSubCount()){ - d_arithSubstitutionsAdded += aiteu.getSubCount() - prevSubCount; - bool anySuccess = false; - for(size_t i = 0, N = assertions.size(); i < N; ++i){ - Node curr = assertions[i]; - Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); - Node res = aiteu.reduceVariablesInItes(next); - Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl; - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - if(more != next){ - anySuccess = true; - break; - } - } - for(size_t i = 0, N = assertions.size(); anySuccess && i < N; ++i){ - Node curr = assertions[i]; - Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); - Node res = aiteu.reduceVariablesInItes(next); - Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl; - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - assertions[i] = Rewriter::rewrite(more); - } - } - } - } - } - return result; -} - void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5763114ca..71a0234ed 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -84,7 +84,6 @@ struct NodeTheoryPairHashFunction { namespace theory { class TheoryModel; class TheoryEngineModelBuilder; - class ITEUtilities; namespace eq { class EqualityEngine; @@ -828,12 +827,6 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** - * A collection of ite preprocessing passes. - */ - theory::ITEUtilities* d_iteUtilities; - - /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier* d_unconstrainedSimp;