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 \
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 \
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 \
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+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<Node> 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<bool>())
+ {
+ 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
--- /dev/null
+/********************* */
+/*! \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
/*! \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.
#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"
--- /dev/null
+/********************* */
+/*! \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 <utility>
+
+#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<Node>& 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<ite::CTIVStackElement> stack;
+ stack.push_back(ite::CTIVStackElement(e));
+ while (!foundTermIte && !stack.empty())
+ {
+ ite::CTIVStackElement& top = stack.back();
+ TNode curr = top.curr;
+ if (top.pos >= curr.getNumChildren())
+ {
+ // all of the children have been visited
+ // no term ites were found
+ d_cache[curr] = false;
+ stack.pop_back();
+ }
+ else
+ {
+ // this is someone's child
+ TNode child = curr[top.pos];
+ child = (child.getKind() == kind::NOT) ? child[0] : child;
+ ++top.pos;
+ if (ite::triviallyContainsNoTermITEs(child))
+ {
+ // skip
+ }
+ else
+ {
+ tmp_it = d_cache.find(child);
+ if (tmp_it != end)
+ {
+ foundTermIte = (*tmp_it).second;
+ }
+ else
+ {
+ stack.push_back(ite::CTIVStackElement(child));
+ foundTermIte = ite::isTermITE(child);
+ }
+ }
+ }
+ }
+ if (foundTermIte)
+ {
+ while (!stack.empty())
+ {
+ TNode curr = stack.back().curr;
+ stack.pop_back();
+ d_cache[curr] = true;
+ }
+ }
+ return foundTermIte;
+}
+void 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<Node>& assertions)
+{
+ std::vector<TNode> tovisit(assertions.begin(), assertions.end());
+
+ while (!tovisit.empty())
+ {
+ TNode back = tovisit.back();
+ tovisit.pop_back();
+
+ bool skip = false;
+ switch (back.getMetaKind())
+ {
+ case kind::metakind::CONSTANT: skip = d_skipConstants; break;
+ case kind::metakind::VARIABLE: skip = d_skipVariables; break;
+ default: break;
+ }
+
+ if (skip)
+ {
+ continue;
+ }
+ if (d_reachCount.find(back) != d_reachCount.end())
+ {
+ d_reachCount[back] = 1 + d_reachCount[back];
+ }
+ else
+ {
+ d_reachCount[back] = 1;
+ for (TNode::iterator cit = back.begin(), end = back.end(); cit != end;
+ ++cit)
+ {
+ tovisit.push_back(*cit);
+ }
+ }
+ }
+}
+
+void IncomingArcCounter::clear() { d_reachCount.clear(); }
+
+/********************* */
+/* ITECompressor
+ */
+ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
+ : d_contains(contains), d_assertions(NULL), d_incoming(true, true)
+{
+ Assert(d_contains != NULL);
+
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECompressor::~ITECompressor() { reset(); }
+
+void ITECompressor::reset()
+{
+ d_incoming.clear();
+ d_compressed.clear();
+}
+
+void ITECompressor::garbageCollect() { reset(); }
+
+ITECompressor::Statistics::Statistics()
+ : d_compressCalls("ite-simp::compressCalls", 0),
+ d_skolemsAdded("ite-simp::skolems", 0)
+{
+ 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<bool>() == negateCnd)
+ {
+ return push_back_boolean(toCompress, d_false);
+ }
+ else
+ {
+ // equivalent to true don't push back
+ }
+ }
+ else
+ {
+ Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
+ nb << pb;
+ }
+ curr = negateCnd ? curr[2] : curr[1];
+ }
+ Assert(toCompress != curr);
+
+ nb << compressBoolean(curr);
+ Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
+ return push_back_boolean(toCompress, res);
+}
+
+Node ITECompressor::compressTerm(Node toCompress)
+{
+ if (toCompress.isConst() || toCompress.isVar())
+ {
+ return toCompress;
+ }
+
+ if (d_compressed.find(toCompress) != d_compressed.end())
+ {
+ return d_compressed[toCompress];
+ }
+ if (toCompress.getKind() == kind::ITE)
+ {
+ Node cmpCnd = compressBoolean(toCompress[0]);
+ if (cmpCnd.isConst())
+ {
+ Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
+ Node res = compressTerm(toCompress);
+ d_compressed[toCompress] = res;
+ return res;
+ }
+ else
+ {
+ Node cmpThen = compressTerm(toCompress[1]);
+ Node cmpElse = compressTerm(toCompress[2]);
+ Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
+ d_compressed[toCompress] = newIte;
+ return newIte;
+ }
+ }
+
+ NodeBuilder<> nb(toCompress.getKind());
+
+ if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ nb << (toCompress.getOperator());
+ }
+ for (Node::iterator it = toCompress.begin(), end = toCompress.end();
+ it != end;
+ ++it)
+ {
+ nb << compressTerm(*it);
+ }
+ Node compressed = (Node)nb;
+ if (multipleParents(toCompress))
+ {
+ d_compressed[toCompress] = compressed;
+ }
+ return compressed;
+}
+
+Node ITECompressor::compressBoolean(Node toCompress)
+{
+ static int instance = 0;
+ ++instance;
+ if (toCompress.isConst() || toCompress.isVar())
+ {
+ return toCompress;
+ }
+ if (d_compressed.find(toCompress) != d_compressed.end())
+ {
+ return d_compressed[toCompress];
+ }
+ else if (toCompress.getKind() == kind::ITE)
+ {
+ return compressBooleanITEs(toCompress);
+ }
+ else
+ {
+ bool ta = ite::isTheoryAtom(toCompress);
+ NodeBuilder<> nb(toCompress.getKind());
+ if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ nb << (toCompress.getOperator());
+ }
+ for (Node::iterator it = toCompress.begin(), end = toCompress.end();
+ it != end;
+ ++it)
+ {
+ Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
+ nb << pb;
+ }
+ Node compressed = nb;
+ if (ta || multipleParents(toCompress))
+ {
+ return push_back_boolean(toCompress, compressed);
+ }
+ else
+ {
+ return compressed;
+ }
+ }
+}
+
+bool ITECompressor::compress(std::vector<Node>& assertions)
+{
+ reset();
+
+ d_assertions = &assertions;
+ d_incoming.computeReachability(assertions);
+
+ ++(d_statistics.d_compressCalls);
+ Chat() << "Computed reachability" << endl;
+
+ bool nofalses = true;
+ size_t original_size = assertions.size();
+ Chat() << "compressing " << original_size << endl;
+ for (size_t i = 0; i < original_size && nofalses; ++i)
+ {
+ Node assertion = assertions[i];
+ Node compressed = compressBoolean(assertion);
+ Node rewritten = 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<ite::TITEHStackElement> stack;
+ stack.push_back(ite::TITEHStackElement(e));
+ while (!stack.empty())
+ {
+ ite::TITEHStackElement& top = stack.back();
+ top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
+ TNode curr = top.curr;
+ if (top.pos >= curr.getNumChildren())
+ {
+ // done with the current node
+ returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
+ d_termITEHeight[curr] = returnValue;
+ stack.pop_back();
+ continue;
+ }
+ else
+ {
+ if (top.pos == 0 && curr.getKind() == kind::ITE)
+ {
+ ++top.pos;
+ returnValue = 0;
+ continue;
+ }
+ // this is someone's child
+ TNode child = curr[top.pos];
+ ++top.pos;
+ if (ite::triviallyContainsNoTermITEs(child))
+ {
+ returnValue = 0;
+ }
+ else
+ {
+ tmp_it = d_termITEHeight.find(child);
+ if (tmp_it != end)
+ {
+ returnValue = (*tmp_it).second;
+ }
+ else
+ {
+ stack.push_back(ite::TITEHStackElement(child));
+ }
+ }
+ }
+ }
+ return returnValue;
+}
+
+ITESimplifier::ITESimplifier(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<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITESimplifier::~ITESimplifier()
+{
+ clearSimpITECaches();
+ Assert(d_constantLeaves.empty());
+ Assert(d_allocatedConstantLeaves.empty());
+}
+
+bool ITESimplifier::leavesAreConst(TNode e)
+{
+ return leavesAreConst(e, theory::Theory::theoryOf(e));
+}
+
+void ITESimplifier::clearSimpITECaches()
+{
+ Chat() << "clear ite caches " << endl;
+ for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
+ {
+ NodeVec* curr = d_allocatedConstantLeaves[i];
+ delete curr;
+ }
+ d_citeEqConstApplications = 0;
+ d_constantLeaves.clear();
+ d_allocatedConstantLeaves.clear();
+ d_termITEHeight.clear();
+ d_constantIteEqualsConstantCache.clear();
+ d_replaceOverCache.clear();
+ d_replaceOverTermIteCache.clear();
+ d_simpITECache.clear();
+ d_simpVars.clear();
+ d_simpConstCache.clear();
+ d_leavesConstCache.clear();
+ d_simpContextCache.clear();
+}
+
+bool ITESimplifier::doneALotOfWorkHeuristic() const
+{
+ static const size_t SIZE_BOUND = 1000;
+ Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications
+ << endl;
+ return (d_citeEqConstApplications > SIZE_BOUND);
+}
+
+ITESimplifier::Statistics::Statistics()
+ : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
+ d_unexpected("ite-simp::unexpected", 0),
+ d_unsimplified("ite-simp::unsimplified", 0),
+ d_exactMatchFold("ite-simp::exactMatchFold", 0),
+ d_binaryPredFold("ite-simp::binaryPredFold", 0),
+ d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
+ d_simpITEVisits("ite-simp::simpITE.visits", 0),
+ d_inSmaller("ite-simp::inSmaller")
+{
+ 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<Node> visited;
+ set<Node> constants;
+ set<Node> nonConstants;
+ int maxConstants;
+ int maxNonconstants;
+ int maxDepth;
+ bool failure;
+ IteTreeSearchData()
+ : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
+ {
+ }
+};
+void iteTreeSearch(Node e, int depth, IteTreeSearchData& search)
+{
+ if (search.maxDepth >= 0 && depth > search.maxDepth)
+ {
+ search.failure = true;
+ }
+ if (search.failure)
+ {
+ return;
+ }
+ if (search.visited.find(e) != search.visited.end())
+ {
+ return;
+ }
+ else
+ {
+ search.visited.insert(e);
+ }
+
+ if (e.isConst())
+ {
+ search.constants.insert(e);
+ if (search.maxConstants >= 0
+ && search.constants.size() > (unsigned)search.maxConstants)
+ {
+ search.failure = true;
+ }
+ }
+ else if (e.getKind() == kind::ITE)
+ {
+ iteTreeSearch(e[1], depth + 1, search);
+ iteTreeSearch(e[2], depth + 1, search);
+ }
+ else
+ {
+ search.nonConstants.insert(e);
+ if (search.maxNonconstants >= 0
+ && search.nonConstants.size() > (unsigned)search.maxNonconstants)
+ {
+ search.failure = true;
+ }
+ }
+}
+
+Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
+{
+ if (n == simpVar)
+ {
+ return replaceWith;
+ }
+ else if (n.getNumChildren() == 0)
+ {
+ return n;
+ }
+ Assert(n.getNumChildren() > 0);
+ Assert(!n.isVar());
+
+ pair<Node, Node> p = make_pair(n, replaceWith);
+ if (d_replaceOverCache.find(p) != d_replaceOverCache.end())
+ {
+ return d_replaceOverCache[p];
+ }
+
+ NodeBuilder<> builder(n.getKind());
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << n.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < n.getNumChildren(); ++i)
+ {
+ Node newChild = replaceOver(n[i], replaceWith, simpVar);
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_replaceOverCache[p] = result;
+ return result;
+}
+
+Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar)
+{
+ if (e.getKind() == kind::ITE)
+ {
+ pair<Node, Node> p = make_pair(e, simpAtom);
+ if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end())
+ {
+ return d_replaceOverTermIteCache[p];
+ }
+ Assert(!e.getType().isBoolean());
+ Node cnd = e[0];
+ Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
+ Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
+ Node newIte = cnd.iteNode(newThen, newElse);
+ d_replaceOverTermIteCache[p] = newIte;
+ return newIte;
+ }
+ else
+ {
+ return replaceOver(simpAtom, e, simpVar);
+ }
+}
+
+Node ITESimplifier::attemptLiftEquality(TNode atom)
+{
+ if (atom.getKind() == kind::EQUAL)
+ {
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
+ && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
+ {
+ // exactly 1 is an ite
+ TNode ite = left.getKind() == kind::ITE ? left : right;
+ TNode notIte = left.getKind() == kind::ITE ? right : left;
+
+ if (notIte == ite[1])
+ {
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
+ }
+ else if (notIte == ite[2])
+ {
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
+ }
+ if (notIte.isConst() && (ite[1].isConst() || ite[2].isConst()))
+ {
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
+ }
+ }
+ }
+
+ // try a similar more relaxed version for non-equality operators
+ if (atom.getMetaKind() == kind::metakind::OPERATOR
+ && atom.getNumChildren() == 2 && !atom[1].getType().isBoolean())
+ {
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if ((left.getKind() == kind::ITE || right.getKind() == kind::ITE)
+ && !(left.getKind() == kind::ITE && right.getKind() == kind::ITE))
+ {
+ // exactly 1 is an ite
+ bool leftIsIte = left.getKind() == kind::ITE;
+ Node ite = leftIsIte ? left : right;
+ Node notIte = leftIsIte ? right : left;
+
+ if (notIte.isConst())
+ {
+ IteTreeSearchData search;
+ search.maxNonconstants = 2;
+ iteTreeSearch(ite, 0, search);
+ if (!search.failure)
+ {
+ d_statistics.d_maxNonConstantsFolded.maxAssign(
+ search.nonConstants.size());
+ Debug("ite::simpite") << "used " << search.nonConstants.size()
+ << " nonconstants" << endl;
+ NodeManager* nm = NodeManager::currentNM();
+ Node simpVar = getSimpVar(notIte.getType());
+ TNode newLeft = leftIsIte ? simpVar : notIte;
+ TNode newRight = leftIsIte ? notIte : simpVar;
+ Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
+
+ ++(d_statistics.d_binaryPredFold);
+ return replaceOverTermIte(ite, newAtom, simpVar);
+ }
+ }
+ }
+ }
+
+ // TODO "This is way too tailored. Must generalize!"
+ if (atom.getKind() == kind::EQUAL && atom.getNumChildren() == 2
+ && ite::isTermITE(atom[0]) && atom[1].getKind() == kind::MULT
+ && atom[1].getNumChildren() == 2 && atom[1][0].isConst()
+ && atom[1][0].getConst<Rational>().isNegativeOne()
+ && ite::isTermITE(atom[1][1])
+ && d_termITEHeight.termITEHeight(atom[0]) == 1
+ && d_termITEHeight.termITEHeight(atom[1][1]) == 1
+ && (atom[0][1].isConst() || atom[0][2].isConst())
+ && (atom[1][1][1].isConst() || atom[1][1][2].isConst()))
+ {
+ // expand all 4 cases
+
+ Node negOne = atom[1][0];
+
+ Node lite = atom[0];
+ Node lC = lite[0];
+ Node lT = lite[1];
+ Node lE = lite[2];
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node negRite = atom[1][1];
+ Node rC = negRite[0];
+ Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
+ Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
+
+ // (ite lC lT lE) = (ite rC rT rE)
+ // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
+ // (ite lc (ite rC (= lT rT) (= lT rE))
+ // (ite rC (= lE rT) (= lE rE)))
+
+ Node eqTT = lT.eqNode(rT);
+ Node eqTE = lT.eqNode(rE);
+ Node eqET = lE.eqNode(rT);
+ Node eqEE = lE.eqNode(rE);
+ Node thenLC = rC.iteNode(eqTT, eqTE);
+ Node elseLC = rC.iteNode(eqET, eqEE);
+ Node newIte = lC.iteNode(thenLC, elseLC);
+
+ ++(d_statistics.d_specialEqualityFolds);
+ return newIte;
+ }
+ return Node::null();
+}
+
+// Interesting classes of atoms:
+// 2. Contains constants and 1 constant term ite
+// 3. Contains 2 constant term ites
+Node ITESimplifier::transformAtom(TNode atom)
+{
+ if (!d_containsVisitor->containsTermITE(atom))
+ {
+ if (atom.getKind() == kind::EQUAL && atom[0].isConst() && atom[1].isConst())
+ {
+ // constant equality
+ return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
+ }
+ return Node::null();
+ }
+ else
+ {
+ Node acr = attemptConstantRemoval(atom);
+ if (!acr.isNull())
+ {
+ return acr;
+ }
+ // Node ale = attemptLiftEquality(atom);
+ // if(!ale.isNull()){
+ // //return ale;
+ // }
+ return Node::null();
+ }
+}
+
+static unsigned numBranches = 0;
+static unsigned numFalseBranches = 0;
+static unsigned itesMade = 0;
+
+Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant)
+{
+ static int instance = 0;
+ ++instance;
+ Debug("ite::constantIteEqualsConstant")
+ << instance << "constantIteEqualsConstant(" << cite << ", " << constant
+ << ")" << endl;
+ if (cite.isConst())
+ {
+ Node res = (cite == constant) ? d_true : d_false;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
+ return res;
+ }
+ std::pair<Node, Node> pair = make_pair(cite, constant);
+
+ NodePairMap::const_iterator eq_pos =
+ d_constantIteEqualsConstantCache.find(pair);
+ if (eq_pos != d_constantIteEqualsConstantCache.end())
+ {
+ Debug("ite::constantIteEqualsConstant")
+ << instance << "->" << (*eq_pos).second << endl;
+ return (*eq_pos).second;
+ }
+
+ ++d_citeEqConstApplications;
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if (std::binary_search(leaves->begin(), leaves->end(), constant))
+ {
+ if (leaves->size() == 1)
+ {
+ // probably unreachable
+ d_constantIteEqualsConstantCache[pair] = d_true;
+ Debug("ite::constantIteEqualsConstant")
+ << instance << "->" << d_true << endl;
+ return d_true;
+ }
+ else
+ {
+ Assert(cite.getKind() == kind::ITE);
+ TNode cnd = cite[0];
+ TNode tB = cite[1];
+ TNode fB = cite[2];
+ Node tEqs = constantIteEqualsConstant(tB, constant);
+ Node fEqs = constantIteEqualsConstant(fB, constant);
+ Node boolIte = cnd.iteNode(tEqs, fEqs);
+ if (!(tEqs.isConst() || fEqs.isConst()))
+ {
+ ++numBranches;
+ }
+ if (!(tEqs == d_false || fEqs == d_false))
+ {
+ ++numFalseBranches;
+ }
+ ++itesMade;
+ d_constantIteEqualsConstantCache[pair] = boolIte;
+ // Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte
+ // << endl;
+ return boolIte;
+ }
+ }
+ else
+ {
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ Debug("ite::constantIteEqualsConstant")
+ << instance << "->" << d_false << endl;
+ return d_false;
+ }
+}
+
+Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
+{
+ // intersect the constant ite trees lcite and rcite
+
+ if (lcite.isConst() || rcite.isConst())
+ {
+ bool lIsConst = lcite.isConst();
+ TNode constant = lIsConst ? lcite : rcite;
+ TNode cite = lIsConst ? rcite : lcite;
+
+ (d_statistics.d_inSmaller) << 1;
+ unsigned preItesMade = itesMade;
+ unsigned preNumBranches = numBranches;
+ unsigned preNumFalseBranches = numFalseBranches;
+ Node bterm = constantIteEqualsConstant(cite, constant);
+ Debug("intersectConstantIte") << (numBranches - preNumBranches) << " "
+ << (numFalseBranches - preNumFalseBranches)
+ << " " << (itesMade - preItesMade) << endl;
+ return bterm;
+ }
+ Assert(lcite.getKind() == kind::ITE);
+ Assert(rcite.getKind() == kind::ITE);
+
+ NodeVec* leftValues = computeConstantLeaves(lcite);
+ NodeVec* rightValues = computeConstantLeaves(rcite);
+
+ uint32_t smaller = std::min(leftValues->size(), rightValues->size());
+
+ (d_statistics.d_inSmaller) << smaller;
+ NodeVec intersection(smaller, Node::null());
+ NodeVec::iterator newEnd;
+ newEnd = std::set_intersection(leftValues->begin(),
+ leftValues->end(),
+ rightValues->begin(),
+ rightValues->end(),
+ intersection.begin());
+ intersection.resize(newEnd - intersection.begin());
+ if (intersection.empty())
+ {
+ return d_false;
+ }
+ else
+ {
+ NodeBuilder<> nb(kind::OR);
+ NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
+ for (; it != end; ++it)
+ {
+ Node inBoth = *it;
+ Node lefteq = constantIteEqualsConstant(lcite, inBoth);
+ Node righteq = constantIteEqualsConstant(rcite, inBoth);
+ Node bothHold = lefteq.andNode(righteq);
+ nb << bothHold;
+ }
+ Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
+ return result;
+ }
+}
+
+Node ITESimplifier::attemptEagerRemoval(TNode atom)
+{
+ if (atom.getKind() == kind::EQUAL)
+ {
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if ((left.isConst() && right.getKind() == kind::ITE && isConstantIte(right))
+ || (right.isConst() && left.getKind() == kind::ITE
+ && isConstantIte(left)))
+ {
+ TNode constant = left.isConst() ? left : right;
+ TNode cite = left.isConst() ? right : left;
+
+ std::pair<Node, Node> pair = make_pair(cite, constant);
+ NodePairMap::const_iterator eq_pos =
+ d_constantIteEqualsConstantCache.find(pair);
+ if (eq_pos != d_constantIteEqualsConstantCache.end())
+ {
+ Node ret = (*eq_pos).second;
+ if (ret.isConst())
+ {
+ return ret;
+ }
+ else
+ {
+ return Node::null();
+ }
+ }
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if (!std::binary_search(leaves->begin(), leaves->end(), constant))
+ {
+ std::pair<Node, Node> pair = make_pair(cite, constant);
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ return d_false;
+ }
+ }
+ }
+ return Node::null();
+}
+
+Node ITESimplifier::attemptConstantRemoval(TNode atom)
+{
+ if (atom.getKind() == kind::EQUAL)
+ {
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if (isConstantIte(left) && isConstantIte(right))
+ {
+ return intersectConstantIte(left, right);
+ }
+ }
+ return Node::null();
+}
+
+bool ITESimplifier::leavesAreConst(TNode e, 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<Node, bool, NodeHashFunction>::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<Node, Node>(simpContext, iteNode));
+ if (it != d_simpConstCache.end())
+ {
+ return (*it).second;
+ }
+
+ if (iteNode.getKind() == kind::ITE)
+ {
+ NodeBuilder<> builder(kind::ITE);
+ builder << iteNode[0];
+ unsigned i = 1;
+ for (; i < iteNode.getNumChildren(); ++i)
+ {
+ Node n = simpConstants(simpContext, iteNode[i], simpVar);
+ if (n.isNull())
+ {
+ return n;
+ }
+ builder << n;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ result = theory::Rewriter::rewrite(result);
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
+ return result;
+ }
+
+ if (!containsTermITE(iteNode))
+ {
+ Node n =
+ theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+
+ Node iteNode2;
+ Node simpVar2;
+ d_simpContextCache.clear();
+ Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
+ if (!simpContext2.isNull())
+ {
+ Assert(!iteNode2.isNull());
+ simpContext2 = simpContext.substitute(simpVar, simpContext2);
+ Node n = simpConstants(simpContext2, iteNode2, simpVar2);
+ if (n.isNull())
+ {
+ return n;
+ }
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+ return Node();
+}
+
+Node ITESimplifier::getSimpVar(TypeNode t)
+{
+ std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+ it = d_simpVars.find(t);
+ if (it != d_simpVars.end())
+ {
+ return (*it).second;
+ }
+ else
+ {
+ Node var = NodeManager::currentNM()->mkSkolem(
+ "iteSimp", t, "is a variable resulting from ITE simplification");
+ d_simpVars[t] = var;
+ return var;
+ }
+}
+
+Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
+{
+ NodeMap::iterator it;
+ it = d_simpContextCache.find(c);
+ if (it != d_simpContextCache.end())
+ {
+ return (*it).second;
+ }
+
+ if (!containsTermITE(c))
+ {
+ d_simpContextCache[c] = c;
+ return c;
+ }
+
+ if (c.getKind() == kind::ITE && !c.getType().isBoolean())
+ {
+ // Currently only support one ite node in a simp context
+ // Return Null if more than one is found
+ if (!iteNode.isNull())
+ {
+ return Node();
+ }
+ simpVar = getSimpVar(c.getType());
+ if (simpVar.isNull())
+ {
+ return Node();
+ }
+ d_simpContextCache[c] = simpVar;
+ iteNode = c;
+ return simpVar;
+ }
+
+ NodeBuilder<> builder(c.getKind());
+ if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << c.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < c.getNumChildren(); ++i)
+ {
+ Node newChild = createSimpContext(c[i], iteNode, simpVar);
+ if (newChild.isNull())
+ {
+ return newChild;
+ }
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_simpContextCache[c] = result;
+ return result;
+}
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
+{
+ if (visited.find(x) != visited.end())
+ {
+ return;
+ }
+ visited.insert(x);
+ if (x.getKind() == k)
+ {
+ ++reached;
+ }
+ for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i)
+ {
+ countReachable_(x[i], k, visited, reached);
+ }
+}
+
+uint32_t countReachable(TNode x, Kind k)
+{
+ NodeSet visited;
+ uint32_t reached = 0;
+ countReachable_(x, k, visited, reached);
+ return reached;
+}
+
+Node ITESimplifier::simpITEAtom(TNode atom)
+{
+ static int CVC4_UNUSED instance = 0;
+ Debug("ite::atom") << "still simplifying " << (++instance) << endl;
+ Node attempt = transformAtom(atom);
+ Debug("ite::atom") << " finished " << instance << endl;
+ if (!attempt.isNull())
+ {
+ Node rewritten = 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<preprocess_stack_element> toVisit;
+ toVisit.push_back(assertion);
+
+ static int call = 0;
+ ++call;
+ int iteration = 0;
+
+ while (!toVisit.empty())
+ {
+ iteration++;
+ // cout << "call " << call << " : " << iteration << endl;
+ // The current node we are processing
+ preprocess_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
+
+ // If node has no ITE's or already in the cache we're done, pop from the
+ // stack
+ if (current.getNumChildren() == 0
+ || (theory::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<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(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<Node>& cs2 = (*it).second.getCareSet();
+ ITECareSimplifier::CareSetPtr csNew = getNewSet();
+ set_intersection(careSet.getCareSet().begin(),
+ careSet.getCareSet().end(),
+ cs2.begin(),
+ cs2.end(),
+ inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
+ (*it).second = csNew;
+ }
+ else
+ {
+ queue[e] = careSet;
+ }
+}
+
+Node ITECareSimplifier::substitute(TNode e,
+ TNodeMap& substTable,
+ TNodeMap& cache)
+{
+ TNodeMap::iterator it = cache.find(e), iend = cache.end();
+ if (it != iend)
+ {
+ return it->second;
+ }
+
+ // do substitution?
+ it = substTable.find(e);
+ iend = substTable.end();
+ if (it != iend)
+ {
+ Node result = substitute(it->second, substTable, cache);
+ cache[e] = result;
+ return result;
+ }
+
+ size_t sz = e.getNumChildren();
+ if (sz == 0)
+ {
+ cache[e] = e;
+ return e;
+ }
+
+ NodeBuilder<> builder(e.getKind());
+ if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << e.getOperator();
+ }
+ for (unsigned i = 0; i < e.getNumChildren(); ++i)
+ {
+ builder << substitute(e[i], substTable, cache);
+ }
+
+ Node result = builder;
+ // it = substTable.find(result);
+ // if (it != iend) {
+ // result = substitute(it->second, substTable, cache);
+ // }
+ cache[e] = result;
+ return result;
+}
+
+Node ITECareSimplifier::simplifyWithCare(TNode e)
+{
+ TNodeMap substTable;
+
+ /* 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<Node>& css = cs.getCareSet();
+ queue.erase(v);
+
+ done = false;
+ set<Node>::iterator iCare, iCareEnd = css.end();
+
+ switch (v.getKind())
+ {
+ case kind::ITE:
+ {
+ iCare = css.find(v[0]);
+ if (iCare != iCareEnd)
+ {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[1];
+ updateQueue(queue, v[1], cs);
+ done = true;
+ break;
+ }
+ else
+ {
+ iCare = css.find(v[0].negate());
+ if (iCare != iCareEnd)
+ {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[2];
+ updateQueue(queue, v[2], cs);
+ done = true;
+ break;
+ }
+ }
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ updateQueue(queue, v[1], cs2);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ updateQueue(queue, v[2], cs2);
+ done = true;
+ break;
+ }
+ case kind::AND:
+ {
+ for (i = 0; i < v.getNumChildren(); ++i)
+ {
+ iCare = css.find(v[i].negate());
+ if (iCare != iCareEnd)
+ {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_false;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ for (i = 1; i < v.getNumChildren(); ++i)
+ {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ case kind::OR:
+ {
+ for (i = 0; i < v.getNumChildren(); ++i)
+ {
+ iCare = css.find(v[i]);
+ if (iCare != iCareEnd)
+ {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_true;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ for (i = 1; i < v.getNumChildren(); ++i)
+ {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ default: break;
+ }
+
+ if (done)
+ {
+ continue;
+ }
+
+ for (unsigned i = 0; i < v.getNumChildren(); ++i)
+ {
+ updateQueue(queue, v[i], cs);
+ }
+ }
+ }
+ /* 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
--- /dev/null
+/********************* */
+/*! \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 <unordered_map>
+#include <vector>
+
+#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<Node, bool, NodeHashFunction> 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<Node>& 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<ContainsTermITEVisitor> 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<Node>& 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<Node, uint32_t, NodeHashFunction> 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<Node, uint32_t, NodeHashFunction> 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<Node>& 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<Node>* d_assertions;
+ IncomingArcCounter d_incoming;
+
+ typedef std::unordered_map<Node, Node, NodeHashFunction> 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<Node> NodeVec;
+ typedef std::unordered_map<Node, NodeVec*, NodeHashFunction>
+ 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<NodeVec*> 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<Node, Node> NodePair;
+ using NodePairHashFunction =
+ PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>;
+ typedef std::unordered_map<NodePair, Node, NodePairHashFunction> 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<Node, bool, NodeHashFunction> 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<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+ Node getSimpVar(TypeNode t);
+
+ typedef std::unordered_map<Node, Node, NodeHashFunction> 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<uint32_t> 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<TNode, Node, TNodeHashFunction> 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<Node> d_careSet;
+ CareSetPtrVal(ITECareSimplifier& simp)
+ : d_iteSimplifier(simp), d_refCount(1)
+ {
+ }
+ }; /* class ITECareSimplifier::CareSetPtrVal */
+
+ std::vector<CareSetPtrVal*> 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<Node>& 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<TNode, CareSetPtr> CareMap;
+ void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
+ Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
+};
+
+} // namespace util
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif
#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"
/** 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;
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"),
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);
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);
*/
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.
new GlobalNegate(d_preprocessingPassContext.get()));
std::unique_ptr<IntToBV> intToBV(
new IntToBV(d_preprocessingPassContext.get()));
+ std::unique_ptr<ITESimp> iteSimp(
+ new ITESimp(d_preprocessingPassContext.get()));
std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
new QuantifiersPreprocess(d_preprocessingPassContext.get()));
std::unique_ptr<PseudoBooleanProcessor> pbProc(
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",
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<bool>()){
- 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<Node> intoConjunction;
- for(size_t i = before; i<curr; ++i){
- intoConjunction.push_back(d_assertions[i]);
- }
- d_assertions.resize(before);
- size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1;
- intoConjunction.push_back(d_assertions[lastBeforeItes]);
- Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
- d_assertions.replace(lastBeforeItes, newLast);
- Assert(d_assertions.size() == before);
-}
-
void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
spendResource(options::preprocessStep());
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;
}
/*! \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.
#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"
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);
}
/*! \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.
#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;
std::vector<Node> 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<Node>& assertions);
+ void learnSubstitutions(const std::vector<Node>& assertions);
private:
/* applies this to all children of n and constructs the result */
#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"
#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"
}
// TODO Speed up
- ContainsTermITEVisitor ctv;
+ preprocessing::util::ContainsTermITEVisitor ctv;
if(ctv.containsTermITE(t)){
return false;
}
+++ /dev/null
-/********************* */
-/*! \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 <utility>
-
-#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<Node>& 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<ite::CTIVStackElement> stack;
- stack.push_back(ite::CTIVStackElement(e));
- while(!foundTermIte && !stack.empty()){
- ite::CTIVStackElement& top = stack.back();
- TNode curr = top.curr;
- if(top.pos >= curr.getNumChildren()){
- // all of the children have been visited
- // no term ites were found
- d_cache[curr] = false;
- stack.pop_back();
- }else{
- // this is someone's child
- TNode child = curr[top.pos];
- child = (child.getKind() == kind::NOT) ? child[0] : child;
- ++top.pos;
- if(ite::triviallyContainsNoTermITEs(child)){
- // skip
- }else{
- tmp_it = d_cache.find(child);
- if(tmp_it != end){
- foundTermIte = (*tmp_it).second;
- }else{
- stack.push_back(ite::CTIVStackElement(child));
- foundTermIte = ite::isTermITE(child);
- }
- }
- }
- }
- if(foundTermIte){
- while(!stack.empty()){
- TNode curr = stack.back().curr;
- stack.pop_back();
- d_cache[curr] = true;
- }
- }
- return foundTermIte;
-}
-void 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<Node>& assertions){
- std::vector<TNode> tovisit(assertions.begin(), assertions.end());
-
- while(!tovisit.empty()){
- TNode back = tovisit.back();
- tovisit.pop_back();
-
- bool skip = false;
- switch(back.getMetaKind()){
- case kind::metakind::CONSTANT:
- skip = d_skipConstants;
- break;
- case kind::metakind::VARIABLE:
- skip = d_skipVariables;
- break;
- default:
- break;
- }
-
- if(skip) { continue; }
- if(d_reachCount.find(back) != d_reachCount.end()){
- d_reachCount[back] = 1 + d_reachCount[back];
- }else{
- d_reachCount[back] = 1;
- for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){
- tovisit.push_back(*cit);
- }
- }
- }
-}
-
-void IncomingArcCounter::clear() {
- d_reachCount.clear();
-}
-
-/********************* */
-/* ITECompressor
- */
-ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
- : d_contains(contains)
- , d_assertions(NULL)
- , d_incoming(true, true)
-{
- Assert(d_contains != NULL);
-
- d_true = NodeManager::currentNM()->mkConst<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-ITECompressor::~ITECompressor() {
- reset();
-}
-
-void ITECompressor::reset(){
- d_incoming.clear();
- d_compressed.clear();
-}
-
-void ITECompressor::garbageCollect(){
- reset();
-}
-
-ITECompressor::Statistics::Statistics():
- d_compressCalls("ite-simp::compressCalls", 0),
- d_skolemsAdded("ite-simp::skolems", 0)
-{
- 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<bool>() == negateCnd){
- return push_back_boolean(toCompress, d_false);
- }else{
- // equivalent to true don't push back
- }
- }else{
- Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
- nb << pb;
- }
- curr = negateCnd ? curr[2] : curr[1];
- }
- Assert(toCompress != curr);
-
- nb << compressBoolean(curr);
- Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
- return push_back_boolean(toCompress, res);
-}
-
-Node ITECompressor::compressTerm(Node toCompress){
- if(toCompress.isConst() || toCompress.isVar()){
- return toCompress;
- }
-
- if(d_compressed.find(toCompress) != d_compressed.end()){
- return d_compressed[toCompress];
- }
- if(toCompress.getKind() == kind::ITE){
- Node cmpCnd = compressBoolean(toCompress[0]);
- if(cmpCnd.isConst()){
- Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
- Node res = compressTerm(toCompress);
- d_compressed[toCompress] = res;
- return res;
- }else{
- Node cmpThen = compressTerm(toCompress[1]);
- Node cmpElse = compressTerm(toCompress[2]);
- Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
- d_compressed[toCompress] = newIte;
- return newIte;
- }
- }
-
- NodeBuilder<> nb(toCompress.getKind());
-
- if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
- nb << (toCompress.getOperator());
- }
- for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
- nb << compressTerm(*it);
- }
- Node compressed = (Node)nb;
- if(multipleParents(toCompress)){
- d_compressed[toCompress] = compressed;
- }
- return compressed;
-}
-
-Node ITECompressor::compressBoolean(Node toCompress){
- static int instance = 0;
- ++instance;
- if(toCompress.isConst() || toCompress.isVar()){
- return toCompress;
- }
- if(d_compressed.find(toCompress) != d_compressed.end()){
- return d_compressed[toCompress];
- }else if(toCompress.getKind() == kind::ITE){
- return compressBooleanITEs(toCompress);
- }else{
- bool ta = ite::isTheoryAtom(toCompress);
- NodeBuilder<> nb(toCompress.getKind());
- if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
- nb << (toCompress.getOperator());
- }
- for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
- Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
- nb << pb;
- }
- Node compressed = nb;
- if(ta || multipleParents(toCompress)){
- return push_back_boolean(toCompress, compressed);
- }else{
- return compressed;
- }
- }
-}
-
-
-
-bool ITECompressor::compress(std::vector<Node>& assertions){
- reset();
-
- d_assertions = &assertions;
- d_incoming.computeReachability(assertions);
-
- ++(d_statistics.d_compressCalls);
- Chat() << "Computed reachability" << endl;
-
- bool nofalses = true;
- size_t original_size = assertions.size();
- Chat () << "compressing " << original_size << endl;
- for(size_t i = 0; i < original_size && nofalses; ++i){
- Node assertion = assertions[i];
- Node compressed = compressBoolean(assertion);
- Node rewritten = Rewriter::rewrite(compressed);
- assertions[i] = rewritten;
- Assert(!d_contains->containsTermITE(rewritten));
-
- nofalses = (rewritten != d_false);
- }
-
- d_assertions = NULL;
-
- return nofalses;
-}
-
-TermITEHeightCounter::TermITEHeightCounter()
- :d_termITEHeight()
-{}
-
-TermITEHeightCounter::~TermITEHeightCounter(){}
-
-void TermITEHeightCounter::clear(){
- d_termITEHeight.clear();
-}
-
-size_t TermITEHeightCounter::cache_size() const{
- return d_termITEHeight.size();
-}
-
-namespace ite {
-struct TITEHStackElement {
- TNode curr;
- unsigned pos;
- uint32_t maxChildHeight;
- TITEHStackElement() : 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<ite::TITEHStackElement> stack;
- stack.push_back(ite::TITEHStackElement(e));
- while(!stack.empty()){
- ite::TITEHStackElement& top = stack.back();
- top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
- TNode curr = top.curr;
- if(top.pos >= curr.getNumChildren()){
- // done with the current node
- returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
- d_termITEHeight[curr] = returnValue;
- stack.pop_back();
- continue;
- }else{
- if(top.pos == 0 && curr.getKind() == kind::ITE){
- ++top.pos;
- returnValue = 0;
- continue;
- }
- // this is someone's child
- TNode child = curr[top.pos];
- ++top.pos;
- if(ite::triviallyContainsNoTermITEs(child)){
- returnValue = 0;
- }else{
- tmp_it = d_termITEHeight.find(child);
- if(tmp_it != end){
- returnValue = (*tmp_it).second;
- }else{
- stack.push_back(ite::TITEHStackElement(child));
- }
- }
- }
- }
- return returnValue;
-}
-
-
-
-ITESimplifier::ITESimplifier(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<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-ITESimplifier::~ITESimplifier() {
- clearSimpITECaches();
- Assert(d_constantLeaves.empty());
- Assert(d_allocatedConstantLeaves.empty());
-}
-
-bool ITESimplifier::leavesAreConst(TNode e){
- return leavesAreConst(e, theory::Theory::theoryOf(e));
-}
-
-void ITESimplifier::clearSimpITECaches(){
- Chat() << "clear ite caches " << endl;
- for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){
- NodeVec* curr = d_allocatedConstantLeaves[i];
- delete curr;
- }
- d_citeEqConstApplications = 0;
- d_constantLeaves.clear();
- d_allocatedConstantLeaves.clear();
- d_termITEHeight.clear();
- d_constantIteEqualsConstantCache.clear();
- d_replaceOverCache.clear();
- d_replaceOverTermIteCache.clear();
- d_simpITECache.clear();
- d_simpVars.clear();
- d_simpConstCache.clear();
- d_leavesConstCache.clear();
- d_simpContextCache.clear();
-}
-
-bool ITESimplifier::doneALotOfWorkHeuristic() const {
- static const size_t SIZE_BOUND = 1000;
- Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl;
- return (d_citeEqConstApplications > SIZE_BOUND);
-}
-
-ITESimplifier::Statistics::Statistics():
- d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
- d_unexpected("ite-simp::unexpected", 0),
- d_unsimplified("ite-simp::unsimplified", 0),
- d_exactMatchFold("ite-simp::exactMatchFold", 0),
- d_binaryPredFold("ite-simp::binaryPredFold", 0),
- d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
- d_simpITEVisits("ite-simp::simpITE.visits", 0),
- d_inSmaller("ite-simp::inSmaller")
-{
- 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<Node> visited;
- set<Node> constants;
- set<Node> nonConstants;
- int maxConstants;
- int maxNonconstants;
- int maxDepth;
- bool failure;
- IteTreeSearchData()
- : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
- {}
-};
-void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){
- if(search.maxDepth >= 0 && depth > search.maxDepth){
- search.failure = true;
- }
- if(search.failure){
- return;
- }
- if(search.visited.find(e) != search.visited.end()){
- return;
- }else{
- search.visited.insert(e);
- }
-
- if(e.isConst()){
- search.constants.insert(e);
- if(search.maxConstants >= 0 &&
- search.constants.size() > (unsigned)search.maxConstants){
- search.failure = true;
- }
- }else if(e.getKind() == kind::ITE){
- iteTreeSearch(e[1], depth+1, search);
- iteTreeSearch(e[2], depth+1, search);
- }else{
- search.nonConstants.insert(e);
- if(search.maxNonconstants >= 0 &&
- search.nonConstants.size() > (unsigned)search.maxNonconstants){
- search.failure = true;
- }
- }
-}
-
-Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){
- if(n == simpVar){
- return replaceWith;
- }else if(n.getNumChildren() == 0){
- return n;
- }
- Assert(n.getNumChildren() > 0);
- Assert(!n.isVar());
-
- pair<Node, Node> p = make_pair(n, replaceWith);
- if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){
- return d_replaceOverCache[p];
- }
-
- NodeBuilder<> builder(n.getKind());
- if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << n.getOperator();
- }
- unsigned i = 0;
- for (; i < n.getNumChildren(); ++ i) {
- Node newChild = replaceOver(n[i], replaceWith, simpVar);
- builder << newChild;
- }
- // Mark the substitution and continue
- Node result = builder;
- d_replaceOverCache[p] = result;
- return result;
-}
-
-Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){
- if(e.getKind() == kind::ITE){
- pair<Node, Node> p = make_pair(e, simpAtom);
- if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){
- return d_replaceOverTermIteCache[p];
- }
- Assert(!e.getType().isBoolean());
- Node cnd = e[0];
- Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
- Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
- Node newIte = cnd.iteNode(newThen, newElse);
- d_replaceOverTermIteCache[p] = newIte;
- return newIte;
- }else{
- return replaceOver(simpAtom, e, simpVar);
- }
-}
-
-Node ITESimplifier::attemptLiftEquality(TNode atom){
- if(atom.getKind() == kind::EQUAL){
- TNode left = atom[0];
- TNode right = atom[1];
- if((left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
- !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
-
- // exactly 1 is an ite
- TNode ite = left.getKind() == kind::ITE ? left :right;
- TNode notIte = left.getKind() == kind::ITE ? right : left;
-
- if(notIte == ite[1]){
- ++(d_statistics.d_exactMatchFold);
- return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
- }else if(notIte == ite[2]){
- ++(d_statistics.d_exactMatchFold);
- return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
- }
- if(notIte.isConst() &&
- (ite[1].isConst() || ite[2].isConst())){
- ++(d_statistics.d_exactMatchFold);
- return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
- }
- }
- }
-
- // try a similar more relaxed version for non-equality operators
- if(atom.getMetaKind() == kind::metakind::OPERATOR &&
- atom.getNumChildren() == 2 &&
- !atom[1].getType().isBoolean()){
-
- TNode left = atom[0];
- TNode right = atom[1];
- if( (left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
- !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
- // exactly 1 is an ite
- bool leftIsIte = left.getKind() == kind::ITE;
- Node ite = leftIsIte ? left :right;
- Node notIte = leftIsIte ? right : left;
-
- if(notIte.isConst()){
- IteTreeSearchData search;
- search.maxNonconstants = 2;
- iteTreeSearch(ite, 0, search);
- if(!search.failure){
- d_statistics.d_maxNonConstantsFolded.maxAssign(search.nonConstants.size());
- Debug("ite::simpite") << "used " << search.nonConstants.size() << " nonconstants" << endl;
- NodeManager* nm = NodeManager::currentNM();
- Node simpVar = getSimpVar(notIte.getType());
- TNode newLeft = leftIsIte ? simpVar : notIte;
- TNode newRight = leftIsIte ? notIte : simpVar;
- Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
-
- ++(d_statistics.d_binaryPredFold);
- return replaceOverTermIte(ite, newAtom, simpVar);
- }
- }
- }
- }
-
- // TODO "This is way too tailored. Must generalize!"
- if(atom.getKind() == kind::EQUAL &&
- atom.getNumChildren() == 2 &&
- ite::isTermITE(atom[0]) &&
- atom[1].getKind() == kind::MULT &&
- atom[1].getNumChildren() == 2 &&
- atom[1][0].isConst() &&
- atom[1][0].getConst<Rational>().isNegativeOne() &&
- ite::isTermITE(atom[1][1]) &&
- d_termITEHeight.termITEHeight(atom[0]) == 1 &&
- d_termITEHeight.termITEHeight(atom[1][1]) == 1 &&
- (atom[0][1].isConst() || atom[0][2].isConst()) &&
- (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){
- // expand all 4 cases
-
- Node negOne = atom[1][0];
-
- Node lite = atom[0];
- Node lC = lite[0];
- Node lT = lite[1];
- Node lE = lite[2];
-
- NodeManager* nm = NodeManager::currentNM();
- Node negRite = atom[1][1];
- Node rC = negRite[0];
- Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
- Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
-
- // (ite lC lT lE) = (ite rC rT rE)
- // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
- // (ite lc (ite rC (= lT rT) (= lT rE))
- // (ite rC (= lE rT) (= lE rE)))
-
- Node eqTT = lT.eqNode(rT);
- Node eqTE = lT.eqNode(rE);
- Node eqET = lE.eqNode(rT);
- Node eqEE = lE.eqNode(rE);
- Node thenLC = rC.iteNode(eqTT, eqTE);
- Node elseLC = rC.iteNode(eqET, eqEE);
- Node newIte = lC.iteNode(thenLC, elseLC);
-
- ++(d_statistics.d_specialEqualityFolds);
- return newIte;
- }
- return Node::null();
-}
-
-// Interesting classes of atoms:
-// 2. Contains constants and 1 constant term ite
-// 3. Contains 2 constant term ites
-Node ITESimplifier::transformAtom(TNode atom){
- if(! d_containsVisitor->containsTermITE(atom)){
- if(atom.getKind() == kind::EQUAL &&
- atom[0].isConst() && atom[1].isConst()){
- // constant equality
- return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
- }
- return Node::null();
- }else{
- Node acr = attemptConstantRemoval(atom);
- if(!acr.isNull()){
- return acr;
- }
- // Node ale = attemptLiftEquality(atom);
- // if(!ale.isNull()){
- // //return ale;
- // }
- return Node::null();
- }
-}
-
-static unsigned numBranches = 0;
-static unsigned numFalseBranches = 0;
-static unsigned itesMade = 0;
-
-Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
- static int instance = 0;
- ++instance;
- Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<<cite << ", " << constant<<")"<< endl;
- if(cite.isConst()){
- Node res = (cite == constant) ? d_true : d_false;
- Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
- return res;
- }
- std::pair<Node,Node> pair = make_pair(cite, constant);
-
- NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
- if(eq_pos != d_constantIteEqualsConstantCache.end()){
- Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl;
- return (*eq_pos).second;
- }
-
- ++d_citeEqConstApplications;
-
- NodeVec* leaves = computeConstantLeaves(cite);
- Assert(leaves != NULL);
- if(std::binary_search(leaves->begin(), leaves->end(), constant)){
- if(leaves->size() == 1){
- // probably unreachable
- d_constantIteEqualsConstantCache[pair] = d_true;
- Debug("ite::constantIteEqualsConstant") << instance << "->" << d_true << endl;
- return d_true;
- }else{
- Assert(cite.getKind() == kind::ITE);
- TNode cnd = cite[0];
- TNode tB = cite[1];
- TNode fB = cite[2];
- Node tEqs = constantIteEqualsConstant(tB, constant);
- Node fEqs = constantIteEqualsConstant(fB, constant);
- Node boolIte = cnd.iteNode(tEqs, fEqs);
- if(!(tEqs.isConst() || fEqs.isConst())){
- ++numBranches;
- }
- if(!(tEqs == d_false || fEqs == d_false)){
- ++numFalseBranches;
- }
- ++itesMade;
- d_constantIteEqualsConstantCache[pair] = boolIte;
- //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl;
- return boolIte;
- }
- }else{
- d_constantIteEqualsConstantCache[pair] = d_false;
- Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl;
- return d_false;
- }
-}
-
-
-Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
- // intersect the constant ite trees lcite and rcite
-
- if(lcite.isConst() || rcite.isConst()){
- bool lIsConst = lcite.isConst();
- TNode constant = lIsConst ? lcite : rcite;
- TNode cite = lIsConst ? rcite : lcite;
-
- (d_statistics.d_inSmaller)<< 1;
- unsigned preItesMade = itesMade;
- unsigned preNumBranches = numBranches;
- unsigned preNumFalseBranches = numFalseBranches;
- Node bterm = constantIteEqualsConstant(cite, constant);
- Debug("intersectConstantIte")
- << (numBranches - preNumBranches)
- << " " << (numFalseBranches - preNumFalseBranches)
- << " " << (itesMade - preItesMade) << endl;
- return bterm;
- }
- Assert(lcite.getKind() == kind::ITE);
- Assert(rcite.getKind() == kind::ITE);
-
- NodeVec* leftValues = computeConstantLeaves(lcite);
- NodeVec* rightValues = computeConstantLeaves(rcite);
-
- uint32_t smaller = std::min(leftValues->size(), rightValues->size());
-
- (d_statistics.d_inSmaller)<< smaller;
- NodeVec intersection(smaller, Node::null());
- NodeVec::iterator newEnd;
- newEnd = std::set_intersection(leftValues->begin(), leftValues->end(),
- rightValues->begin(), rightValues->end(),
- intersection.begin());
- intersection.resize(newEnd - intersection.begin());
- if(intersection.empty()){
- return d_false;
- }else{
- NodeBuilder<> nb(kind::OR);
- NodeVec::const_iterator it = intersection.begin(), end=intersection.end();
- for(; it != end; ++it){
- Node inBoth = *it;
- Node lefteq = constantIteEqualsConstant(lcite, inBoth);
- Node righteq = constantIteEqualsConstant(rcite, inBoth);
- Node bothHold = lefteq.andNode(righteq);
- nb << bothHold;
- }
- Node result = (nb.getNumChildren() > 1) ? (Node)nb : nb[0];
- return result;
- }
-}
-
-
-Node ITESimplifier::attemptEagerRemoval(TNode atom){
- if(atom.getKind() == kind::EQUAL){
- TNode left = atom[0];
- TNode right = atom[1];
- if((left.isConst() &&
- right.getKind() == kind::ITE && isConstantIte(right)) ||
- (right.isConst() &&
- left.getKind() == kind::ITE && isConstantIte(left))){
- TNode constant = left.isConst() ? left : right;
- TNode cite = left.isConst() ? right : left;
-
- std::pair<Node,Node> pair = make_pair(cite, constant);
- NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
- if(eq_pos != d_constantIteEqualsConstantCache.end()){
- Node ret = (*eq_pos).second;
- if(ret.isConst()){
- return ret;
- }else{
- return Node::null();
- }
- }
-
- NodeVec* leaves = computeConstantLeaves(cite);
- Assert(leaves != NULL);
- if(!std::binary_search(leaves->begin(), leaves->end(), constant)){
- std::pair<Node,Node> pair = make_pair(cite, constant);
- d_constantIteEqualsConstantCache[pair] = d_false;
- return d_false;
- }
- }
- }
- return Node::null();
-}
-
-Node ITESimplifier::attemptConstantRemoval(TNode atom){
- if(atom.getKind() == kind::EQUAL){
- TNode left = atom[0];
- TNode right = atom[1];
- if(isConstantIte(left) && isConstantIte(right)){
- return intersectConstantIte(left, right);
- }
- }
- return Node::null();
-}
-
-
-bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
-{
- Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
- Theory::theoryOf(e) != THEORY_BOOL);
- if (e.isConst()) {
- return true;
- }
-
- unordered_map<Node, bool, NodeHashFunction>::iterator it;
- it = d_leavesConstCache.find(e);
- if (it != d_leavesConstCache.end()) {
- return (*it).second;
- }
-
- if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
- d_leavesConstCache[e] = false;
- return false;
- }
-
- Assert(e.getNumChildren() > 0);
- size_t k = 0, sz = e.getNumChildren();
-
- if (e.getKind() == kind::ITE) {
- k = 1;
- }
-
- for (; k < sz; ++k) {
- if (!leavesAreConst(e[k], tid)) {
- d_leavesConstCache[e] = false;
- return false;
- }
- }
- d_leavesConstCache[e] = true;
- return true;
-}
-
-
-Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar)
-{
- NodePairMap::iterator it;
- it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode));
- if (it != d_simpConstCache.end()) {
- return (*it).second;
- }
-
- if (iteNode.getKind() == kind::ITE) {
- NodeBuilder<> builder(kind::ITE);
- builder << iteNode[0];
- unsigned i = 1;
- for (; i < iteNode.getNumChildren(); ++ i) {
- Node n = simpConstants(simpContext, iteNode[i], simpVar);
- if (n.isNull()) {
- return n;
- }
- builder << n;
- }
- // Mark the substitution and continue
- Node result = builder;
- result = Rewriter::rewrite(result);
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
- return result;
- }
-
- if (!containsTermITE(iteNode)) {
- Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
- return n;
- }
-
- Node iteNode2;
- Node simpVar2;
- d_simpContextCache.clear();
- Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
- if (!simpContext2.isNull()) {
- Assert(!iteNode2.isNull());
- simpContext2 = simpContext.substitute(simpVar, simpContext2);
- Node n = simpConstants(simpContext2, iteNode2, simpVar2);
- if (n.isNull()) {
- return n;
- }
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
- return n;
- }
- return Node();
-}
-
-
-Node ITESimplifier::getSimpVar(TypeNode t)
-{
- std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
- it = d_simpVars.find(t);
- if (it != d_simpVars.end()) {
- return (*it).second;
- }
- else {
- Node var = NodeManager::currentNM()->mkSkolem("iteSimp", t, "is a variable resulting from ITE simplification");
- d_simpVars[t] = var;
- return var;
- }
-}
-
-
-Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
-{
- NodeMap::iterator it;
- it = d_simpContextCache.find(c);
- if (it != d_simpContextCache.end()) {
- return (*it).second;
- }
-
- if (!containsTermITE(c)) {
- d_simpContextCache[c] = c;
- return c;
- }
-
- if (c.getKind() == kind::ITE && !c.getType().isBoolean()) {
- // Currently only support one ite node in a simp context
- // Return Null if more than one is found
- if (!iteNode.isNull()) {
- return Node();
- }
- simpVar = getSimpVar(c.getType());
- if (simpVar.isNull()) {
- return Node();
- }
- d_simpContextCache[c] = simpVar;
- iteNode = c;
- return simpVar;
- }
-
- NodeBuilder<> builder(c.getKind());
- if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << c.getOperator();
- }
- unsigned i = 0;
- for (; i < c.getNumChildren(); ++ i) {
- Node newChild = createSimpContext(c[i], iteNode, simpVar);
- if (newChild.isNull()) {
- return newChild;
- }
- builder << newChild;
- }
- // Mark the substitution and continue
- Node result = builder;
- d_simpContextCache[c] = result;
- return result;
-}
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
- if(visited.find(x) != visited.end()){
- return;
- }
- visited.insert(x);
- if(x.getKind() == k){
- ++reached;
- }
- for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){
- countReachable_(x[i], k, visited, reached);
- }
-}
-
-uint32_t countReachable(TNode x, Kind k){
- NodeSet visited;
- uint32_t reached = 0;
- countReachable_(x, k, visited, reached);
- return reached;
-}
-
-Node ITESimplifier::simpITEAtom(TNode atom)
-{
- static int CVC4_UNUSED instance = 0;
- Debug("ite::atom") << "still simplifying " << (++instance) << endl;
- Node attempt = transformAtom(atom);
- Debug("ite::atom") << " finished " << instance << endl;
- if(!attempt.isNull()){
- Node rewritten = Rewriter::rewrite(attempt);
- Debug("ite::print-success")
- << instance << " "
- << "rewriting " << countReachable(rewritten, kind::ITE)
- << " from " << countReachable(atom, kind::ITE) << endl
- << "\t rewritten " << rewritten << endl
- << "\t input " << atom << endl;
- return rewritten;
- }
-
- if (leavesAreConst(atom)) {
- Node iteNode;
- Node simpVar;
- d_simpContextCache.clear();
- Node simpContext = createSimpContext(atom, iteNode, simpVar);
- if (!simpContext.isNull()) {
- if (iteNode.isNull()) {
- Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
- ++(d_statistics.d_unexpected);
- Debug("ite::simpite") << instance << " "
- << "how about?" << atom << endl;
- Debug("ite::simpite") << instance << " "
- << "\t" << simpContext << endl;
- return Rewriter::rewrite(simpContext);
- }
- Node n = simpConstants(simpContext, iteNode, simpVar);
- if (!n.isNull()) {
- ++(d_statistics.d_unexpected);
- Debug("ite::simpite") << instance << " "
- << "here?" << atom << endl;
- Debug("ite::simpite") << instance << " "
- << "\t" << n << endl;
- return n;
- }
- }
- }
- if(Debug.isOn("ite::simpite")){
- if(countReachable(atom, kind::ITE) > 0){
- Debug("ite::simpite") << instance << " "
- << "remaining " << atom << endl;
- }
- }
- ++(d_statistics.d_unsimplified);
- return atom;
-}
-
-
-struct preprocess_stack_element {
- TNode node;
- bool children_added;
- preprocess_stack_element(TNode node)
- : node(node), children_added(false) {}
-};/* struct preprocess_stack_element */
-
-
-Node ITESimplifier::simpITE(TNode assertion)
-{
- // Do a topological sort of the subexpressions and substitute them
- vector<preprocess_stack_element> toVisit;
- toVisit.push_back(assertion);
-
- static int call = 0;
- ++call;
- int iteration = 0;
-
- while (!toVisit.empty())
- {
- iteration ++;
- //cout << "call " << call << " : " << iteration << endl;
- // The current node we are processing
- preprocess_stack_element& stackHead = toVisit.back();
- TNode current = stackHead.node;
-
- // If node has no ITE's or already in the cache we're done, pop from the stack
- if (current.getNumChildren() == 0 ||
- (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) {
- d_simpITECache[current] = current;
- ++(d_statistics.d_simpITEVisits);
- toVisit.pop_back();
- continue;
- }
-
- NodeMap::iterator find = d_simpITECache.find(current);
- if (find != d_simpITECache.end()) {
- toVisit.pop_back();
- continue;
- }
-
- // Not yet substituted, so process
- if (stackHead.children_added) {
- // Children have been processed, so substitute
- NodeBuilder<> builder(current.getKind());
- if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << current.getOperator();
- }
- for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
- Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
- Node child = current[i];
- Node childRes = d_simpITECache[current[i]];
- builder << childRes;
- }
- // Mark the substitution and continue
- Node result = builder;
-
- // If this is an atom, we process it
- if (Theory::theoryOf(result) != THEORY_BOOL &&
- result.getType().isBoolean()) {
- result = simpITEAtom(result);
- }
-
- // if(current != result && result.isConst()){
- // static int instance = 0;
- // //cout << instance << " " << result << current << endl;
- // }
-
- result = Rewriter::rewrite(result);
- d_simpITECache[current] = result;
- ++(d_statistics.d_simpITEVisits);
- toVisit.pop_back();
- } else {
- // Mark that we have added the children if any
- if (current.getNumChildren() > 0) {
- stackHead.children_added = true;
- // We need to add the children
- for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
- TNode childNode = *child_it;
- NodeMap::iterator childFind = d_simpITECache.find(childNode);
- if (childFind == d_simpITECache.end()) {
- toVisit.push_back(childNode);
- }
- }
- } else {
- // No children, so we're done
- d_simpITECache[current] = current;
- ++(d_statistics.d_simpITEVisits);
- toVisit.pop_back();
- }
- }
- }
- return d_simpITECache[assertion];
-}
-
-ITECareSimplifier::ITECareSimplifier()
- : d_careSetsOutstanding(0)
- , d_usedSets()
-{
- d_true = NodeManager::currentNM()->mkConst<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(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<Node>& cs2 = (*it).second.getCareSet();
- ITECareSimplifier::CareSetPtr csNew = getNewSet();
- set_intersection(careSet.getCareSet().begin(),
- careSet.getCareSet().end(),
- cs2.begin(), cs2.end(),
- inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
- (*it).second = csNew;
- }
- else {
- queue[e] = careSet;
- }
-}
-
-
-Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
-{
- TNodeMap::iterator it = cache.find(e), iend = cache.end();
- if (it != iend) {
- return it->second;
- }
-
- // do substitution?
- it = substTable.find(e);
- iend = substTable.end();
- if (it != iend) {
- Node result = substitute(it->second, substTable, cache);
- cache[e] = result;
- return result;
- }
-
- size_t sz = e.getNumChildren();
- if (sz == 0) {
- cache[e] = e;
- return e;
- }
-
- NodeBuilder<> builder(e.getKind());
- if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << e.getOperator();
- }
- for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
- builder << substitute(e[i], substTable, cache);
- }
-
- Node result = builder;
- // it = substTable.find(result);
- // if (it != iend) {
- // result = substitute(it->second, substTable, cache);
- // }
- cache[e] = result;
- return result;
-}
-
-
-Node ITECareSimplifier::simplifyWithCare(TNode e)
-{
- TNodeMap substTable;
-
- /* 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<Node>& css = cs.getCareSet();
- queue.erase(v);
-
- done = false;
- set<Node>::iterator iCare, iCareEnd = css.end();
-
- switch (v.getKind()) {
- case kind::ITE: {
- iCare = css.find(v[0]);
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = v[1];
- updateQueue(queue, v[1], cs);
- done = true;
- break;
- }
- else {
- iCare = css.find(v[0].negate());
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = v[2];
- updateQueue(queue, v[2], cs);
- done = true;
- break;
- }
- }
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0]);
- updateQueue(queue, v[1], cs2);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0].negate());
- updateQueue(queue, v[2], cs2);
- done = true;
- break;
- }
- case kind::AND: {
- for (i = 0; i < v.getNumChildren(); ++i) {
- iCare = css.find(v[i].negate());
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = d_false;
- done = true;
- break;
- }
- }
- if (done) break;
-
- Assert(v.getNumChildren() > 1);
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0]);
- for (i = 1; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs2);
- }
- done = true;
- break;
- }
- case kind::OR: {
- for (i = 0; i < v.getNumChildren(); ++i) {
- iCare = css.find(v[i]);
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = d_true;
- done = true;
- break;
- }
- }
- if (done) break;
-
- Assert(v.getNumChildren() > 1);
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0].negate());
- for (i = 1; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs2);
- }
- done = true;
- break;
- }
- default:
- break;
- }
-
- if (done) {
- continue;
- }
-
- for (unsigned i = 0; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs);
- }
- }
- }
- /* 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 */
+++ /dev/null
-/********************* */
-/*! \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 <unordered_map>
-#include <vector>
-
-#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<Node, bool, NodeHashFunction> 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<Node>& 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<ContainsTermITEVisitor> 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<Node>& 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<Node, uint32_t, NodeHashFunction> 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<Node, uint32_t, NodeHashFunction> 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<Node>& 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<Node>* d_assertions;
- IncomingArcCounter d_incoming;
-
- typedef std::unordered_map<Node, Node, NodeHashFunction> 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<Node> NodeVec;
- typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > 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<NodeVec*> 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<Node, Node> NodePair;
- using NodePairHashFunction =
- PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>;
- typedef std::unordered_map<NodePair, Node, NodePairHashFunction> 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<Node, bool, NodeHashFunction> 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<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
- Node getSimpVar(TypeNode t);
-
- typedef std::unordered_map<Node, Node, NodeHashFunction> 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<uint32_t> 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<TNode, Node, TNodeHashFunction> 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<Node> d_careSet;
- CareSetPtrVal(ITECareSimplifier& simp)
- : d_iteSimplifier(simp), d_refCount(1) {}
- }; /* class ITECareSimplifier::CareSetPtrVal */
-
- std::vector<CareSetPtrVal*> 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<Node>& 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<TNode, CareSetPtr> CareMap;
- void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
- Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
#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"
ProofManager::currentPM()->initTheoryProofEngine();
#endif
- d_iteUtilities = new ITEUtilities();
-
smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
}
delete d_unconstrainedSimp;
- delete d_iteUtilities;
-
smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
}
}
-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<Node>& 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<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
Assert(explanationVector.size() > 0);
namespace theory {
class TheoryModel;
class TheoryEngineModelBuilder;
- class ITEUtilities;
namespace eq {
class EqualityEngine;
/** 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;
projects / cvc5.git / commitdiff