From f66f40912490226291d5af6c1f8b66e9ba6d7633 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 23 Aug 2018 11:05:38 -0700 Subject: [PATCH] Refactor ITE simplification preprocessing pass. (#2360) --- src/Makefile.am | 6 +- src/preprocessing/passes/ite_simp.cpp | 263 ++++ src/preprocessing/passes/ite_simp.h | 56 + .../preprocessing_pass_context.h | 3 +- .../util}/ite_utilities.cpp | 1196 ++++++++++------- .../util}/ite_utilities.h | 143 +- src/smt/smt_engine.cpp | 83 +- src/theory/arith/arith_ite_utils.cpp | 29 +- src/theory/arith/arith_ite_utils.h | 36 +- src/theory/arith/theory_arith_private.cpp | 4 +- src/theory/theory_engine.cpp | 110 -- src/theory/theory_engine.h | 7 - 12 files changed, 1192 insertions(+), 744 deletions(-) create mode 100644 src/preprocessing/passes/ite_simp.cpp create mode 100644 src/preprocessing/passes/ite_simp.h rename src/{theory => preprocessing/util}/ite_utilities.cpp (62%) rename src/{theory => preprocessing/util}/ite_utilities.h (85%) diff --git a/src/Makefile.am b/src/Makefile.am index 6a21566e0..3b8a12fa5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -83,6 +83,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/ite_removal.cpp \ preprocessing/passes/ite_removal.h \ + preprocessing/passes/ite_simp.cpp \ + preprocessing/passes/ite_simp.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ preprocessing/passes/bool_to_bv.cpp \ @@ -115,6 +117,8 @@ libcvc4_la_SOURCES = \ preprocessing/preprocessing_pass_context.h \ preprocessing/preprocessing_pass_registry.cpp \ preprocessing/preprocessing_pass_registry.h \ + preprocessing/util/ite_utilities.cpp \ + preprocessing/util/ite_utilities.h \ printer/dagification_visitor.cpp \ printer/dagification_visitor.h \ printer/printer.cpp \ @@ -205,8 +209,6 @@ libcvc4_la_SOURCES = \ theory/evaluator.cpp \ theory/evaluator.h \ theory/interrupted.h \ - theory/ite_utilities.cpp \ - theory/ite_utilities.h \ theory/logic_info.cpp \ theory/logic_info.h \ theory/output_channel.h \ diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp new file mode 100644 index 000000000..137925f77 --- /dev/null +++ b/src/preprocessing/passes/ite_simp.cpp @@ -0,0 +1,263 @@ +/********************* */ +/*! \file ite_simp.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ITE simplification preprocessing pass. + **/ + +#include "preprocessing/passes/ite_simp.h" + +#include "options/proof_options.h" +#include "smt/smt_statistics_registry.h" +#include "smt_util/nary_builder.h" +#include "theory/arith/arith_ite_utils.h" + +#include + +using namespace CVC4; +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/* -------------------------------------------------------------------------- */ + +namespace { + +Node simpITE(util::ITEUtilities* ite_utils, TNode assertion) +{ + if (!ite_utils->containsTermITE(assertion)) + { + return assertion; + } + else + { + Node result = ite_utils->simpITE(assertion); + Node res_rewritten = Rewriter::rewrite(result); + + if (options::simplifyWithCareEnabled()) + { + Chat() << "starting simplifyWithCare()" << endl; + Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten); + Chat() << "ending simplifyWithCare()" + << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; + result = Rewriter::rewrite(postSimpWithCare); + } + else + { + result = res_rewritten; + } + return result; + } +} + +/** + * Ensures the assertions asserted after index 'before' now effectively come + * before 'real_assertions_end'. + */ +void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, + size_t before) +{ + size_t cur_size = assertionsToPreprocess->size(); + if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0 + || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size) + { + return; + } + + // assertions + // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd()) + // can be modified + // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before) + // cannot be moved + // added [before, cur_size) + // can be modified + Assert(0 < assertionsToPreprocess->getRealAssertionsEnd()); + Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before); + Assert(before < cur_size); + + std::vector intoConjunction; + for (size_t i = before; i < cur_size; ++i) + { + intoConjunction.push_back((*assertionsToPreprocess)[i]); + } + assertionsToPreprocess->resize(before); + size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; + intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); + Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + assertionsToPreprocess->replace(lastBeforeItes, newLast); + Assert(assertionsToPreprocess->size() == before); +} + +} // namespace + +/* -------------------------------------------------------------------------- */ + +ITESimp::Statistics::Statistics() + : d_arithSubstitutionsAdded( + "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0) +{ + smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); +} + +ITESimp::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); +} + +bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) +{ + // This pass does not support dependency tracking yet + // (learns substitutions from all assertions so just + // adding addDependence is not enough) + if (options::unsatCores() || options::fewerPreprocessingHoles()) + { + return true; + } + bool result = true; + bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); + if (simpDidALotOfWork) + { + if (options::compressItes()) + { + result = d_iteUtilities.compress(assertionsToPreprocess->ref()); + } + + if (result) + { + // if false, don't bother to reclaim memory here. + NodeManager* nm = NodeManager::currentNM(); + if (nm->poolSize() >= options::zombieHuntThreshold()) + { + Chat() << "..ite simplifier did quite a bit of work.. " + << nm->poolSize() << endl; + Chat() << "....node manager contains " << nm->poolSize() + << " nodes before cleanup" << endl; + d_iteUtilities.clear(); + Rewriter::clearCaches(); + nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + Chat() << "....node manager contains " << nm->poolSize() + << " nodes after cleanup" << endl; + } + } + } + + // Do theory specific preprocessing passes + TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine(); + if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH) + && !options::incrementalSolving()) + { + if (!simpDidALotOfWork) + { + util::ContainsTermITEVisitor& contains = + *(d_iteUtilities.getContainsVisitor()); + arith::ArithIteUtils aiteu(contains, + d_preprocContext->getUserContext(), + theory_engine->getModel()); + bool anyItes = false; + for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + if (contains.containsTermITE(curr)) + { + anyItes = true; + Node res = aiteu.reduceVariablesInItes(curr); + Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl + << " ->" << res << endl; + if (curr != res) + { + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + if (!anyItes) + { + unsigned prevSubCount = aiteu.getSubCount(); + aiteu.learnSubstitutions(assertionsToPreprocess->ref()); + if (prevSubCount < aiteu.getSubCount()) + { + d_statistics.d_arithSubstitutionsAdded += + aiteu.getSubCount() - prevSubCount; + bool anySuccess = false; + for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + if (more != next) + { + anySuccess = true; + break; + } + } + for (size_t i = 0, N = assertionsToPreprocess->size(); + anySuccess && i < N; + ++i) + { + Node curr = (*assertionsToPreprocess)[i]; + Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); + Node res = aiteu.reduceVariablesInItes(next); + Debug("arith::ite::red") << "@ " << i << " ... " << next << endl + << " ->" << res << endl; + Node more = aiteu.reduceConstantIteByGCD(res); + Debug("arith::ite::red") << " gcd->" << more << endl; + (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + } + } + } + } + } + return result; +} + +/* -------------------------------------------------------------------------- */ + +ITESimp::ITESimp(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ite-simp") +{ +} + +PreprocessingPassResult ITESimp::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + d_preprocContext->spendResource(options::preprocessStep()); + + size_t nasserts = assertionsToPreprocess->size(); + for (size_t i = 0; i < nasserts; ++i) + { + d_preprocContext->spendResource(options::preprocessStep()); + Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]); + assertionsToPreprocess->replace(i, simp); + if (simp.isConst() && !simp.getConst()) + { + return PreprocessingPassResult::CONFLICT; + } + } + bool done = doneSimpITE(assertionsToPreprocess); + if (nasserts < assertionsToPreprocess->size()) + { + compressBeforeRealAssertions(assertionsToPreprocess, nasserts); + } + return done ? PreprocessingPassResult::NO_CONFLICT + : PreprocessingPassResult::CONFLICT; +} + +/* -------------------------------------------------------------------------- */ + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h new file mode 100644 index 000000000..2296d663e --- /dev/null +++ b/src/preprocessing/passes/ite_simp.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file ite_simp.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief ITE simplification preprocessing pass. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class ITESimp : public PreprocessingPass +{ + public: + ITESimp(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + struct Statistics + { + IntStat d_arithSubstitutionsAdded; + Statistics(); + ~Statistics(); + }; + + bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss); + + /** A collection of ite preprocessing passes. */ + util::ITEUtilities d_iteUtilities; + + Statistics d_statistics; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index b50421e6c..a289752fa 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -2,7 +2,7 @@ /*! \file preprocessing_pass_context.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Aina Niemetz, Mathias Preiner + ** Justin Xu, Andres Noetzli, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -23,6 +23,7 @@ #include "context/context.h" #include "decision/decision_engine.h" +#include "preprocessing/util/ite_utilities.h" #include "smt/smt_engine.h" #include "smt/term_formula_removal.h" #include "theory/theory_engine.h" diff --git a/src/theory/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp similarity index 62% rename from src/theory/ite_utilities.cpp rename to src/preprocessing/util/ite_utilities.cpp index 40a58cf57..66d9151df 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -2,7 +2,7 @@ /*! \file ite_utilities.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andres Noetzli + ** 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. @@ -14,70 +14,74 @@ ** 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 + ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC + *'96 **/ -#include "theory/ite_utilities.h" +#include "preprocessing/util/ite_utilities.h" #include +#include "preprocessing/passes/rewrite.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" using namespace std; namespace CVC4 { -namespace theory { +namespace preprocessing { +namespace util { namespace ite { -inline static bool isTermITE(TNode e) { +inline static bool isTermITE(TNode e) +{ return (e.getKind() == kind::ITE && !e.getType().isBoolean()); } -inline static bool triviallyContainsNoTermITEs(TNode e) { +inline static bool triviallyContainsNoTermITEs(TNode e) +{ return e.isConst() || e.isVar(); } -static bool isTheoryAtom(TNode a){ +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; + 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 { +struct CTIVStackElement +{ TNode curr; unsigned pos; CTIVStackElement() : curr(), pos(0) {} CTIVStackElement(TNode c) : curr(c), pos(0) {} }; /* CTIVStackElement */ -} /* CVC4::theory::ite */ +} // namespace ite ITEUtilities::ITEUtilities() : d_containsVisitor(new ContainsTermITEVisitor()), @@ -88,57 +92,74 @@ ITEUtilities::ITEUtilities() Assert(d_containsVisitor != NULL); } -ITEUtilities::~ITEUtilities(){ - - if(d_simplifier != NULL){ +ITEUtilities::~ITEUtilities() +{ + if (d_simplifier != NULL) + { delete d_simplifier; } - if(d_compressor != NULL){ + if (d_compressor != NULL) + { delete d_compressor; } - if(d_careSimp != NULL){ + if (d_careSimp != NULL) + { delete d_careSimp; } } -Node ITEUtilities::simpITE(TNode assertion){ - if(d_simplifier == NULL){ +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){ +bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const +{ + if (d_simplifier == NULL) + { return false; - }else{ + } + else + { return d_simplifier->doneALotOfWorkHeuristic(); } } /* returns false if an assertion is discovered to be equal to false. */ -bool ITEUtilities::compress(std::vector& assertions){ - if(d_compressor == NULL){ +bool ITEUtilities::compress(std::vector& assertions) +{ + if (d_compressor == NULL) + { d_compressor = new ITECompressor(d_containsVisitor.get()); } return d_compressor->compress(assertions); } -Node ITEUtilities::simplifyWithCare(TNode e){ - if(d_careSimp == NULL){ - d_careSimp = new ITECareSimplifier(); +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){ +void ITEUtilities::clear() +{ + if (d_simplifier != NULL) + { d_simplifier->clearSimpITECaches(); } - if(d_compressor != NULL){ + if (d_compressor != NULL) + { d_compressor->garbageCollect(); } - if(d_careSimp != NULL){ + if (d_careSimp != NULL) + { d_careSimp->clear(); } d_containsVisitor->garbageCollect(); @@ -147,50 +168,67 @@ void ITEUtilities::clear(){ /********************* */ /* ContainsTermITEVisitor */ -ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {} -ContainsTermITEVisitor::~ContainsTermITEVisitor(){} -bool ContainsTermITEVisitor::containsTermITE(TNode e){ +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; } + 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){ + if (tmp_it != end) + { return (*tmp_it).second; } bool foundTermIte = false; std::vector stack; stack.push_back(ite::CTIVStackElement(e)); - while(!foundTermIte && !stack.empty()){ + while (!foundTermIte && !stack.empty()) + { ite::CTIVStackElement& top = stack.back(); TNode curr = top.curr; - if(top.pos >= curr.getNumChildren()){ + 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{ + } + 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)){ + if (ite::triviallyContainsNoTermITEs(child)) + { // skip - }else{ + } + else + { tmp_it = d_cache.find(child); - if(tmp_it != end){ + if (tmp_it != end) + { foundTermIte = (*tmp_it).second; - }else{ + } + else + { stack.push_back(ite::CTIVStackElement(child)); foundTermIte = ite::isTermITE(child); } } } } - if(foundTermIte){ - while(!stack.empty()){ + if (foundTermIte) + { + while (!stack.empty()) + { TNode curr = stack.back().curr; stack.pop_back(); d_cache[curr] = true; @@ -198,62 +236,62 @@ bool ContainsTermITEVisitor::containsTermITE(TNode e){ } return foundTermIte; } -void ContainsTermITEVisitor::garbageCollect() { - d_cache.clear(); -} +void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); } /********************* */ /* IncomingArcCounter */ IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants) - : d_reachCount() - , d_skipVariables(skipVars) - , d_skipConstants(skipConstants) -{} -IncomingArcCounter::~IncomingArcCounter(){} + : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants) +{ +} +IncomingArcCounter::~IncomingArcCounter() {} -void IncomingArcCounter::computeReachability(const std::vector& assertions){ +void IncomingArcCounter::computeReachability( + const std::vector& assertions) +{ std::vector tovisit(assertions.begin(), assertions.end()); - while(!tovisit.empty()){ + 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; + 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()){ + if (skip) + { + continue; + } + if (d_reachCount.find(back) != d_reachCount.end()) + { d_reachCount[back] = 1 + d_reachCount[back]; - }else{ + } + else + { d_reachCount[back] = 1; - for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){ + for (TNode::iterator cit = back.begin(), end = back.end(); cit != end; + ++cit) + { tovisit.push_back(*cit); } } } } -void IncomingArcCounter::clear() { - d_reachCount.clear(); -} +void IncomingArcCounter::clear() { d_reachCount.clear(); } /********************* */ /* ITECompressor */ ITECompressor::ITECompressor(ContainsTermITEVisitor* contains) - : d_contains(contains) - , d_assertions(NULL) - , d_incoming(true, true) + : d_contains(contains), d_assertions(NULL), d_incoming(true, true) { Assert(d_contains != NULL); @@ -261,53 +299,58 @@ ITECompressor::ITECompressor(ContainsTermITEVisitor* contains) d_false = NodeManager::currentNM()->mkConst(false); } -ITECompressor::~ITECompressor() { - reset(); -} +ITECompressor::~ITECompressor() { reset(); } -void ITECompressor::reset(){ +void ITECompressor::reset() +{ d_incoming.clear(); d_compressed.clear(); } -void ITECompressor::garbageCollect(){ - reset(); -} +void ITECompressor::garbageCollect() { reset(); } -ITECompressor::Statistics::Statistics(): - d_compressCalls("ite-simp::compressCalls", 0), - d_skolemsAdded("ite-simp::skolems", 0) +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(){ +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); +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()){ + 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()){ + } + 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())){ + } + 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{ + } + else + { NodeManager* nm = NodeManager::currentNM(); Node skolem = nm->mkSkolem("compress", nm->booleanType()); d_compressed[rewritten] = skolem; @@ -321,28 +364,37 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){ } } -bool ITECompressor::multipleParents(TNode c){ +bool ITECompressor::multipleParents(TNode c) +{ return d_incoming.lookupIncoming(c) >= 2; } -Node ITECompressor::compressBooleanITEs(Node toCompress){ +Node ITECompressor::compressBooleanITEs(Node toCompress) +{ Assert(toCompress.getKind() == kind::ITE); Assert(toCompress.getType().isBoolean()); - if(!(toCompress[1] == d_false || toCompress[2] == d_false)){ + if (!(toCompress[1] == d_false || toCompress[2] == d_false)) + { Node cmpCnd = compressBoolean(toCompress[0]); - if(cmpCnd.isConst()){ + if (cmpCnd.isConst()) + { Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2]; Node res = compressBoolean(branch); d_compressed[toCompress] = res; return res; - }else{ + } + else + { Node cmpThen = compressBoolean(toCompress[1]); Node cmpElse = compressBoolean(toCompress[2]); Node newIte = cmpCnd.iteNode(cmpThen, cmpElse); - if(multipleParents(toCompress)){ + if (multipleParents(toCompress)) + { return push_back_boolean(toCompress, newIte); - }else{ + } + else + { return newIte; } } @@ -350,19 +402,25 @@ Node ITECompressor::compressBooleanITEs(Node toCompress){ NodeBuilder<> nb(kind::AND); Node curr = toCompress; - while(curr.getKind() == kind::ITE && - (curr[1] == d_false || curr[2] == d_false) && - (!multipleParents(curr) || curr == toCompress)){ - + while (curr.getKind() == kind::ITE + && (curr[1] == d_false || curr[2] == d_false) + && (!multipleParents(curr) || curr == toCompress)) + { bool negateCnd = (curr[1] == d_false); Node compressCnd = compressBoolean(curr[0]); - if(compressCnd.isConst()){ - if(compressCnd.getConst() == negateCnd){ + if (compressCnd.isConst()) + { + if (compressCnd.getConst() == negateCnd) + { return push_back_boolean(toCompress, d_false); - }else{ + } + else + { // equivalent to true don't push back } - }else{ + } + else + { Node pb = negateCnd ? compressCnd.notNode() : compressCnd; nb << pb; } @@ -375,22 +433,29 @@ Node ITECompressor::compressBooleanITEs(Node toCompress){ return push_back_boolean(toCompress, res); } -Node ITECompressor::compressTerm(Node toCompress){ - if(toCompress.isConst() || toCompress.isVar()){ +Node ITECompressor::compressTerm(Node toCompress) +{ + if (toCompress.isConst() || toCompress.isVar()) + { return toCompress; } - if(d_compressed.find(toCompress) != d_compressed.end()){ + if (d_compressed.find(toCompress) != d_compressed.end()) + { return d_compressed[toCompress]; } - if(toCompress.getKind() == kind::ITE){ + if (toCompress.getKind() == kind::ITE) + { Node cmpCnd = compressBoolean(toCompress[0]); - if(cmpCnd.isConst()){ + if (cmpCnd.isConst()) + { Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2]; Node res = compressTerm(toCompress); d_compressed[toCompress] = res; return res; - }else{ + } + else + { Node cmpThen = compressTerm(toCompress[1]); Node cmpElse = compressTerm(toCompress[2]); Node newIte = cmpCnd.iteNode(cmpThen, cmpElse); @@ -401,51 +466,69 @@ Node ITECompressor::compressTerm(Node toCompress){ NodeBuilder<> nb(toCompress.getKind()); - if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) + { nb << (toCompress.getOperator()); } - for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){ + for (Node::iterator it = toCompress.begin(), end = toCompress.end(); + it != end; + ++it) + { nb << compressTerm(*it); } Node compressed = (Node)nb; - if(multipleParents(toCompress)){ + if (multipleParents(toCompress)) + { d_compressed[toCompress] = compressed; } return compressed; } -Node ITECompressor::compressBoolean(Node toCompress){ +Node ITECompressor::compressBoolean(Node toCompress) +{ static int instance = 0; ++instance; - if(toCompress.isConst() || toCompress.isVar()){ + if (toCompress.isConst() || toCompress.isVar()) + { return toCompress; } - if(d_compressed.find(toCompress) != d_compressed.end()){ + if (d_compressed.find(toCompress) != d_compressed.end()) + { return d_compressed[toCompress]; - }else if(toCompress.getKind() == kind::ITE){ + } + else if (toCompress.getKind() == kind::ITE) + { return compressBooleanITEs(toCompress); - }else{ + } + else + { bool ta = ite::isTheoryAtom(toCompress); NodeBuilder<> nb(toCompress.getKind()); - if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) + { nb << (toCompress.getOperator()); } - for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){ + 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)){ + if (ta || multipleParents(toCompress)) + { return push_back_boolean(toCompress, compressed); - }else{ + } + else + { return compressed; } } } - - -bool ITECompressor::compress(std::vector& assertions){ +bool ITECompressor::compress(std::vector& assertions) +{ reset(); d_assertions = &assertions; @@ -456,11 +539,12 @@ bool ITECompressor::compress(std::vector& assertions){ bool nofalses = true; size_t original_size = assertions.size(); - Chat () << "compressing " << original_size << endl; - for(size_t i = 0; i < original_size && nofalses; ++i){ + 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); + Node compressed = compressBoolean(assertion); + Node rewritten = theory::Rewriter::rewrite(compressed); assertions[i] = rewritten; Assert(!d_contains->containsTermITE(rewritten)); @@ -472,22 +556,20 @@ bool ITECompressor::compress(std::vector& assertions){ return nofalses; } -TermITEHeightCounter::TermITEHeightCounter() - :d_termITEHeight() -{} +TermITEHeightCounter::TermITEHeightCounter() : d_termITEHeight() {} -TermITEHeightCounter::~TermITEHeightCounter(){} +TermITEHeightCounter::~TermITEHeightCounter() {} -void TermITEHeightCounter::clear(){ - d_termITEHeight.clear(); -} +void TermITEHeightCounter::clear() { d_termITEHeight.clear(); } -size_t TermITEHeightCounter::cache_size() const{ +size_t TermITEHeightCounter::cache_size() const +{ return d_termITEHeight.size(); } namespace ite { -struct TITEHStackElement { +struct TITEHStackElement +{ TNode curr; unsigned pos; uint32_t maxChildHeight; @@ -496,34 +578,42 @@ struct TITEHStackElement { }; } /* namespace ite */ -uint32_t TermITEHeightCounter::termITEHeight(TNode e){ - - if(ite::triviallyContainsNoTermITEs(e)){ return 0; } +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){ + if (tmp_it != end) + { return (*tmp_it).second; } - uint32_t returnValue = 0; // This is initially 0 as the very first call this is included in the max, // but this has no effect. std::vector stack; stack.push_back(ite::TITEHStackElement(e)); - while(!stack.empty()){ + while (!stack.empty()) + { ite::TITEHStackElement& top = stack.back(); top.maxChildHeight = std::max(top.maxChildHeight, returnValue); TNode curr = top.curr; - if(top.pos >= curr.getNumChildren()){ + 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){ + } + else + { + if (top.pos == 0 && curr.getKind() == kind::ITE) + { ++top.pos; returnValue = 0; continue; @@ -531,13 +621,19 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){ // this is someone's child TNode child = curr[top.pos]; ++top.pos; - if(ite::triviallyContainsNoTermITEs(child)){ + if (ite::triviallyContainsNoTermITEs(child)) + { returnValue = 0; - }else{ + } + else + { tmp_it = d_termITEHeight.find(child); - if(tmp_it != end){ + if (tmp_it != end) + { returnValue = (*tmp_it).second; - }else{ + } + else + { stack.push_back(ite::TITEHStackElement(child)); } } @@ -546,40 +642,42 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){ 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() + : d_containsVisitor(contains), + d_termITEHeight(), + d_constantLeaves(), + d_allocatedConstantLeaves(), + d_citeEqConstApplications(0), + d_constantIteEqualsConstantCache(), + d_replaceOverCache(), + d_replaceOverTermIteCache(), + d_leavesConstCache(), + d_simpConstCache(), + d_simpContextCache(), + d_simpITECache() { Assert(d_containsVisitor != NULL); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } -ITESimplifier::~ITESimplifier() { +ITESimplifier::~ITESimplifier() +{ clearSimpITECaches(); Assert(d_constantLeaves.empty()); Assert(d_allocatedConstantLeaves.empty()); } -bool ITESimplifier::leavesAreConst(TNode e){ +bool ITESimplifier::leavesAreConst(TNode e) +{ return leavesAreConst(e, theory::Theory::theoryOf(e)); } -void ITESimplifier::clearSimpITECaches(){ +void ITESimplifier::clearSimpITECaches() +{ Chat() << "clear ite caches " << endl; - for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){ + for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i) + { NodeVec* curr = d_allocatedConstantLeaves[i]; delete curr; } @@ -597,21 +695,23 @@ void ITESimplifier::clearSimpITECaches(){ d_simpContextCache.clear(); } -bool ITESimplifier::doneALotOfWorkHeuristic() const { +bool ITESimplifier::doneALotOfWorkHeuristic() const +{ static const size_t SIZE_BOUND = 1000; - Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl; + 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") +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); @@ -623,7 +723,8 @@ ITESimplifier::Statistics::Statistics(): smtStatisticsRegistry()->registerStat(&d_inSmaller); } -ITESimplifier::Statistics::~Statistics(){ +ITESimplifier::Statistics::~Statistics() +{ smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded); smtStatisticsRegistry()->unregisterStat(&d_unexpected); smtStatisticsRegistry()->unregisterStat(&d_unsimplified); @@ -634,29 +735,38 @@ ITESimplifier::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_inSmaller); } -bool ITESimplifier::isConstantIte(TNode e){ - if(e.isConst()){ +bool ITESimplifier::isConstantIte(TNode e) +{ + if (e.isConst()) + { return true; - }else if(ite::isTermITE(e)){ + } + else if (ite::isTermITE(e)) + { NodeVec* constants = computeConstantLeaves(e); return constants != NULL; - }else{ + } + else + { return false; } } -ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ +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){ + if (it != end) + { return (*it).second; } TNode thenB = ite[1]; TNode elseB = ite[2]; // special case 2 constant children - if(thenB.isConst() && elseB.isConst()){ + if (thenB.isConst() && elseB.isConst()) + { NodeVec* pair = new NodeVec(2); d_allocatedConstantLeaves.push_back(pair); @@ -666,8 +776,9 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ return pair; } // At least 1 is an ITE - if(!(thenB.isConst() || thenB.getKind() == kind::ITE) || - !(elseB.isConst() || elseB.getKind() == kind::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; @@ -678,29 +789,36 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ TNode maybeITE = thenB.isConst() ? thenB : elseB; NodeVec* defChildren = computeConstantLeaves(definitelyITE); - if(defChildren == NULL){ + if (defChildren == NULL) + { d_constantLeaves[ite] = NULL; return NULL; } NodeVec scratch; NodeVec* maybeChildren = NULL; - if(maybeITE.getKind() == kind::ITE){ + if (maybeITE.getKind() == kind::ITE) + { maybeChildren = computeConstantLeaves(maybeITE); - }else{ + } + else + { scratch.push_back(maybeITE); maybeChildren = &scratch; } - if(maybeChildren == NULL){ + if (maybeChildren == NULL) + { d_constantLeaves[ite] = NULL; return NULL; } - NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size()); + 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(), + newEnd = std::set_union(defChildren->begin(), + defChildren->end(), + maybeChildren->begin(), + maybeChildren->end(), both->begin()); both->resize(newEnd - both->begin()); d_constantLeaves[ite] = both; @@ -708,7 +826,8 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ } // This is uncached! Better for protoyping or getting limited size examples -struct IteTreeSearchData{ +struct IteTreeSearchData +{ set visited; set constants; set nonConstants; @@ -717,60 +836,81 @@ struct IteTreeSearchData{ int maxDepth; bool failure; IteTreeSearchData() - : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false) - {} + : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false) + { + } }; -void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){ - if(search.maxDepth >= 0 && depth > search.maxDepth){ +void iteTreeSearch(Node e, int depth, IteTreeSearchData& search) +{ + if (search.maxDepth >= 0 && depth > search.maxDepth) + { search.failure = true; } - if(search.failure){ + if (search.failure) + { return; } - if(search.visited.find(e) != search.visited.end()){ + if (search.visited.find(e) != search.visited.end()) + { return; - }else{ + } + else + { search.visited.insert(e); } - if(e.isConst()){ + if (e.isConst()) + { search.constants.insert(e); - if(search.maxConstants >= 0 && - search.constants.size() > (unsigned)search.maxConstants){ + 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{ + } + 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){ + 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){ +Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar) +{ + if (n == simpVar) + { return replaceWith; - }else if(n.getNumChildren() == 0){ + } + else if (n.getNumChildren() == 0) + { return n; } Assert(n.getNumChildren() > 0); Assert(!n.isVar()); pair p = make_pair(n, replaceWith); - if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){ + if (d_replaceOverCache.find(p) != d_replaceOverCache.end()) + { return d_replaceOverCache[p]; } NodeBuilder<> builder(n.getKind()); - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { builder << n.getOperator(); } unsigned i = 0; - for (; i < n.getNumChildren(); ++ i) { + for (; i < n.getNumChildren(); ++i) + { Node newChild = replaceOver(n[i], replaceWith, simpVar); builder << newChild; } @@ -780,10 +920,13 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){ return result; } -Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){ - if(e.getKind() == kind::ITE){ +Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar) +{ + if (e.getKind() == kind::ITE) + { pair p = make_pair(e, simpAtom); - if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){ + if (d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()) + { return d_replaceOverTermIteCache[p]; } Assert(!e.getType().isBoolean()); @@ -793,61 +936,72 @@ Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){ Node newIte = cnd.iteNode(newThen, newElse); d_replaceOverTermIteCache[p] = newIte; return newIte; - }else{ + } + else + { return replaceOver(simpAtom, e, simpVar); } } -Node ITESimplifier::attemptLiftEquality(TNode atom){ - if(atom.getKind() == kind::EQUAL){ +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)){ - + 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 ite = left.getKind() == kind::ITE ? left : right; TNode notIte = left.getKind() == kind::ITE ? right : left; - if(notIte == ite[1]){ + if (notIte == ite[1]) + { ++(d_statistics.d_exactMatchFold); return ite[0].iteNode(d_true, notIte.eqNode(ite[2])); - }else if(notIte == 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())){ + 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])); + 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()){ - + 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)){ + 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 ite = leftIsIte ? left : right; Node notIte = leftIsIte ? right : left; - if(notIte.isConst()){ + 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; + 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 newLeft = leftIsIte ? simpVar : notIte; TNode newRight = leftIsIte ? notIte : simpVar; Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight); @@ -859,18 +1013,16 @@ Node ITESimplifier::attemptLiftEquality(TNode atom){ } // TODO "This is way too tailored. Must generalize!" - if(atom.getKind() == kind::EQUAL && - atom.getNumChildren() == 2 && - ite::isTermITE(atom[0]) && - atom[1].getKind() == kind::MULT && - atom[1].getNumChildren() == 2 && - atom[1][0].isConst() && - atom[1][0].getConst().isNegativeOne() && - ite::isTermITE(atom[1][1]) && - d_termITEHeight.termITEHeight(atom[0]) == 1 && - d_termITEHeight.termITEHeight(atom[1][1]) == 1 && - (atom[0][1].isConst() || atom[0][2].isConst()) && - (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){ + if (atom.getKind() == kind::EQUAL && atom.getNumChildren() == 2 + && ite::isTermITE(atom[0]) && atom[1].getKind() == kind::MULT + && atom[1].getNumChildren() == 2 && atom[1][0].isConst() + && atom[1][0].getConst().isNegativeOne() + && ite::isTermITE(atom[1][1]) + && d_termITEHeight.termITEHeight(atom[0]) == 1 + && d_termITEHeight.termITEHeight(atom[1][1]) == 1 + && (atom[0][1].isConst() || atom[0][2].isConst()) + && (atom[1][1][1].isConst() || atom[1][1][2].isConst())) + { // expand all 4 cases Node negOne = atom[1][0]; @@ -908,17 +1060,22 @@ Node ITESimplifier::attemptLiftEquality(TNode atom){ // 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()){ +Node ITESimplifier::transformAtom(TNode atom) +{ + if (!d_containsVisitor->containsTermITE(atom)) + { + if (atom.getKind() == kind::EQUAL && atom[0].isConst() && atom[1].isConst()) + { // constant equality return NodeManager::currentNM()->mkConst(atom[0] == atom[1]); } return Node::null(); - }else{ + } + else + { Node acr = attemptConstantRemoval(atom); - if(!acr.isNull()){ + if (!acr.isNull()) + { return acr; } // Node ale = attemptLiftEquality(atom); @@ -933,20 +1090,27 @@ static unsigned numBranches = 0; static unsigned numFalseBranches = 0; static unsigned itesMade = 0; -Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){ +Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant) +{ static int instance = 0; ++instance; - Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<" << res << endl; return res; } - std::pair pair = make_pair(cite, constant); + std::pair pair = make_pair(cite, constant); - NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair); - if(eq_pos != d_constantIteEqualsConstantCache.end()){ - Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl; + 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; } @@ -954,13 +1118,18 @@ Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){ NodeVec* leaves = computeConstantLeaves(cite); Assert(leaves != NULL); - if(std::binary_search(leaves->begin(), leaves->end(), constant)){ - if(leaves->size() == 1){ + 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; + Debug("ite::constantIteEqualsConstant") + << instance << "->" << d_true << endl; return d_true; - }else{ + } + else + { Assert(cite.getKind() == kind::ITE); TNode cnd = cite[0]; TNode tB = cite[1]; @@ -968,42 +1137,48 @@ Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){ Node tEqs = constantIteEqualsConstant(tB, constant); Node fEqs = constantIteEqualsConstant(fB, constant); Node boolIte = cnd.iteNode(tEqs, fEqs); - if(!(tEqs.isConst() || fEqs.isConst())){ + if (!(tEqs.isConst() || fEqs.isConst())) + { ++numBranches; } - if(!(tEqs == d_false || fEqs == d_false)){ + if (!(tEqs == d_false || fEqs == d_false)) + { ++numFalseBranches; } ++itesMade; d_constantIteEqualsConstantCache[pair] = boolIte; - //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl; + // Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte + // << endl; return boolIte; } - }else{ + } + else + { d_constantIteEqualsConstantCache[pair] = d_false; - Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl; + Debug("ite::constantIteEqualsConstant") + << instance << "->" << d_false << endl; return d_false; } } - -Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){ +Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite) +{ // intersect the constant ite trees lcite and rcite - if(lcite.isConst() || rcite.isConst()){ + if (lcite.isConst() || rcite.isConst()) + { bool lIsConst = lcite.isConst(); TNode constant = lIsConst ? lcite : rcite; TNode cite = lIsConst ? rcite : lcite; - (d_statistics.d_inSmaller)<< 1; + (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; + Debug("intersectConstantIte") << (numBranches - preNumBranches) << " " + << (numFalseBranches - preNumFalseBranches) + << " " << (itesMade - preItesMade) << endl; return bterm; } Assert(lcite.getKind() == kind::ITE); @@ -1014,19 +1189,25 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){ uint32_t smaller = std::min(leftValues->size(), rightValues->size()); - (d_statistics.d_inSmaller)<< smaller; + (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(), + newEnd = std::set_intersection(leftValues->begin(), + leftValues->end(), + rightValues->begin(), + rightValues->end(), intersection.begin()); intersection.resize(newEnd - intersection.begin()); - if(intersection.empty()){ + if (intersection.empty()) + { return d_false; - }else{ + } + else + { NodeBuilder<> nb(kind::OR); - NodeVec::const_iterator it = intersection.begin(), end=intersection.end(); - for(; it != end; ++it){ + 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); @@ -1038,33 +1219,40 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){ } } - -Node ITESimplifier::attemptEagerRemoval(TNode atom){ - if(atom.getKind() == kind::EQUAL){ +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))){ + if ((left.isConst() && right.getKind() == kind::ITE && isConstantIte(right)) + || (right.isConst() && left.getKind() == kind::ITE + && isConstantIte(left))) + { TNode constant = left.isConst() ? left : right; TNode cite = left.isConst() ? right : left; - std::pair pair = make_pair(cite, constant); - NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair); - if(eq_pos != d_constantIteEqualsConstantCache.end()){ + std::pair pair = make_pair(cite, constant); + NodePairMap::const_iterator eq_pos = + d_constantIteEqualsConstantCache.find(pair); + if (eq_pos != d_constantIteEqualsConstantCache.end()) + { Node ret = (*eq_pos).second; - if(ret.isConst()){ + if (ret.isConst()) + { return ret; - }else{ + } + else + { return Node::null(); } } NodeVec* leaves = computeConstantLeaves(cite); Assert(leaves != NULL); - if(!std::binary_search(leaves->begin(), leaves->end(), constant)){ - std::pair pair = make_pair(cite, constant); + if (!std::binary_search(leaves->begin(), leaves->end(), constant)) + { + std::pair pair = make_pair(cite, constant); d_constantIteEqualsConstantCache[pair] = d_false; return d_false; } @@ -1073,33 +1261,38 @@ Node ITESimplifier::attemptEagerRemoval(TNode atom){ return Node::null(); } -Node ITESimplifier::attemptConstantRemoval(TNode atom){ - if(atom.getKind() == kind::EQUAL){ +Node ITESimplifier::attemptConstantRemoval(TNode atom) +{ + if (atom.getKind() == kind::EQUAL) + { TNode left = atom[0]; TNode right = atom[1]; - if(isConstantIte(left) && isConstantIte(right)){ + if (isConstantIte(left) && isConstantIte(right)) + { return intersectConstantIte(left, right); } } return Node::null(); } - -bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) +bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid) { - Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) || - Theory::theoryOf(e) != THEORY_BOOL); - if (e.isConst()) { + Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) + || theory::Theory::theoryOf(e) != theory::THEORY_BOOL); + if (e.isConst()) + { return true; } unordered_map::iterator it; it = d_leavesConstCache.find(e); - if (it != d_leavesConstCache.end()) { + if (it != d_leavesConstCache.end()) + { return (*it).second; } - if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) { + if (!containsTermITE(e) && theory::Theory::isLeafOf(e, tid)) + { d_leavesConstCache[e] = false; return false; } @@ -1107,12 +1300,15 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) Assert(e.getNumChildren() > 0); size_t k = 0, sz = e.getNumChildren(); - if (e.getKind() == kind::ITE) { + if (e.getKind() == kind::ITE) + { k = 1; } - for (; k < sz; ++k) { - if (!leavesAreConst(e[k], tid)) { + for (; k < sz; ++k) + { + if (!leavesAreConst(e[k], tid)) + { d_leavesConstCache[e] = false; return false; } @@ -1121,35 +1317,42 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) return true; } - -Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar) +Node ITESimplifier::simpConstants(TNode simpContext, + TNode iteNode, + TNode simpVar) { NodePairMap::iterator it; - it = d_simpConstCache.find(pair(simpContext,iteNode)); - if (it != d_simpConstCache.end()) { + it = d_simpConstCache.find(pair(simpContext, iteNode)); + if (it != d_simpConstCache.end()) + { return (*it).second; } - if (iteNode.getKind() == kind::ITE) { + if (iteNode.getKind() == kind::ITE) + { NodeBuilder<> builder(kind::ITE); builder << iteNode[0]; unsigned i = 1; - for (; i < iteNode.getNumChildren(); ++ i) { + for (; i < iteNode.getNumChildren(); ++i) + { Node n = simpConstants(simpContext, iteNode[i], simpVar); - if (n.isNull()) { + if (n.isNull()) + { return n; } builder << n; } // Mark the substitution and continue Node result = builder; - result = Rewriter::rewrite(result); + result = theory::Rewriter::rewrite(result); d_simpConstCache[pair(simpContext, iteNode)] = result; return result; } - if (!containsTermITE(iteNode)) { - Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); + if (!containsTermITE(iteNode)) + { + Node n = + theory::Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); d_simpConstCache[pair(simpContext, iteNode)] = n; return n; } @@ -1158,11 +1361,13 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa Node simpVar2; d_simpContextCache.clear(); Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2); - if (!simpContext2.isNull()) { + if (!simpContext2.isNull()) + { Assert(!iteNode2.isNull()); simpContext2 = simpContext.substitute(simpVar, simpContext2); Node n = simpConstants(simpContext2, iteNode2, simpVar2); - if (n.isNull()) { + if (n.isNull()) + { return n; } d_simpConstCache[pair(simpContext, iteNode)] = n; @@ -1171,43 +1376,49 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa return Node(); } - Node ITESimplifier::getSimpVar(TypeNode t) { std::unordered_map::iterator it; it = d_simpVars.find(t); - if (it != d_simpVars.end()) { + if (it != d_simpVars.end()) + { return (*it).second; } - else { - Node var = NodeManager::currentNM()->mkSkolem("iteSimp", t, "is a variable resulting from ITE simplification"); + 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()) { + if (it != d_simpContextCache.end()) + { return (*it).second; } - if (!containsTermITE(c)) { + if (!containsTermITE(c)) + { d_simpContextCache[c] = c; return c; } - if (c.getKind() == kind::ITE && !c.getType().isBoolean()) { + 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()) { + if (!iteNode.isNull()) + { return Node(); } simpVar = getSimpVar(c.getType()); - if (simpVar.isNull()) { + if (simpVar.isNull()) + { return Node(); } d_simpContextCache[c] = simpVar; @@ -1216,13 +1427,16 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) } NodeBuilder<> builder(c.getKind()); - if (c.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (c.getMetaKind() == kind::metakind::PARAMETERIZED) + { builder << c.getOperator(); } unsigned i = 0; - for (; i < c.getNumChildren(); ++ i) { + for (; i < c.getNumChildren(); ++i) + { Node newChild = createSimpContext(c[i], iteNode, simpVar); - if (newChild.isNull()) { + if (newChild.isNull()) + { return newChild; } builder << newChild; @@ -1233,20 +1447,25 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) return result; } typedef std::unordered_set NodeSet; -void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){ - if(visited.find(x) != visited.end()){ +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){ + if (x.getKind() == k) + { ++reached; } - for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){ + for (unsigned i = 0, N = x.getNumChildren(); i < N; ++i) + { countReachable_(x[i], k, visited, reached); } } -uint32_t countReachable(TNode x, Kind k){ +uint32_t countReachable(TNode x, Kind k) +{ NodeSet visited; uint32_t reached = 0; countReachable_(x, k, visited, reached); @@ -1259,34 +1478,39 @@ Node ITESimplifier::simpITEAtom(TNode atom) 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); + 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; + << 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)) { + if (leavesAreConst(atom)) + { Node iteNode; Node simpVar; d_simpContextCache.clear(); Node simpContext = createSimpContext(atom, iteNode, simpVar); - if (!simpContext.isNull()) { - if (iteNode.isNull()) { + 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); + return theory::Rewriter::rewrite(simpContext); } Node n = simpConstants(simpContext, iteNode, simpVar); - if (!n.isNull()) { + if (!n.isNull()) + { ++(d_statistics.d_unexpected); Debug("ite::simpite") << instance << " " << "here?" << atom << endl; @@ -1296,8 +1520,10 @@ Node ITESimplifier::simpITEAtom(TNode atom) } } } - if(Debug.isOn("ite::simpite")){ - if(countReachable(atom, kind::ITE) > 0){ + if (Debug.isOn("ite::simpite")) + { + if (countReachable(atom, kind::ITE) > 0) + { Debug("ite::simpite") << instance << " " << "remaining " << atom << endl; } @@ -1306,14 +1532,12 @@ Node ITESimplifier::simpITEAtom(TNode atom) return atom; } - -struct preprocess_stack_element { +struct preprocess_stack_element +{ TNode node; bool children_added; - preprocess_stack_element(TNode node) - : node(node), children_added(false) {} -};/* struct preprocess_stack_element */ - + preprocess_stack_element(TNode node) : node(node), children_added(false) {} +}; /* struct preprocess_stack_element */ Node ITESimplifier::simpITE(TNode assertion) { @@ -1327,35 +1551,42 @@ Node ITESimplifier::simpITE(TNode assertion) while (!toVisit.empty()) { - iteration ++; - //cout << "call " << call << " : " << iteration << endl; + 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; + // 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()) { + if (find != d_simpITECache.end()) + { toVisit.pop_back(); continue; } // Not yet substituted, so process - if (stackHead.children_added) { + if (stackHead.children_added) + { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) + { builder << current.getOperator(); } - for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + 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]]; @@ -1365,8 +1596,9 @@ Node ITESimplifier::simpITE(TNode assertion) Node result = builder; // If this is an atom, we process it - if (Theory::theoryOf(result) != THEORY_BOOL && - result.getType().isBoolean()) { + if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL + && result.getType().isBoolean()) + { result = simpITEAtom(result); } @@ -1375,23 +1607,32 @@ Node ITESimplifier::simpITE(TNode assertion) // //cout << instance << " " << result << current << endl; // } - result = Rewriter::rewrite(result); + result = theory::Rewriter::rewrite(result); d_simpITECache[current] = result; ++(d_statistics.d_simpITEVisits); toVisit.pop_back(); - } else { + } + else + { // Mark that we have added the children if any - if (current.getNumChildren() > 0) { + 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) { + 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()) { + if (childFind == d_simpITECache.end()) + { toVisit.push_back(childNode); } } - } else { + } + else + { // No children, so we're done d_simpITECache[current] = current; ++(d_statistics.d_simpITEVisits); @@ -1402,31 +1643,33 @@ Node ITESimplifier::simpITE(TNode assertion) return d_simpITECache[assertion]; } -ITECareSimplifier::ITECareSimplifier() - : d_careSetsOutstanding(0) - , d_usedSets() +ITECareSimplifier::ITECareSimplifier() : d_careSetsOutstanding(0), d_usedSets() { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } -ITECareSimplifier::~ITECareSimplifier(){ +ITECareSimplifier::~ITECareSimplifier() +{ Assert(d_usedSets.empty()); Assert(d_careSetsOutstanding == 0); } -void ITECareSimplifier::clear(){ +void ITECareSimplifier::clear() +{ Assert(d_usedSets.empty()); Assert(d_careSetsOutstanding == 0); } ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet() { - if (d_usedSets.empty()) { + if (d_usedSets.empty()) + { d_careSetsOutstanding++; return ITECareSimplifier::CareSetPtr::mkNew(*this); } - else { + else + { ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back()); cs.getCareSet().clear(); @@ -1435,54 +1678,62 @@ ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet() } } - void ITECareSimplifier::updateQueue(CareMap& queue, TNode e, ITECareSimplifier::CareSetPtr& careSet) { CareMap::iterator it = queue.find(e), iend = queue.end(); - if (it != iend) { + if (it != iend) + { set& cs2 = (*it).second.getCareSet(); ITECareSimplifier::CareSetPtr csNew = getNewSet(); set_intersection(careSet.getCareSet().begin(), careSet.getCareSet().end(), - cs2.begin(), cs2.end(), + cs2.begin(), + cs2.end(), inserter(csNew.getCareSet(), csNew.getCareSet().begin())); (*it).second = csNew; } - else { + else + { queue[e] = careSet; } } - -Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache) +Node ITECareSimplifier::substitute(TNode e, + TNodeMap& substTable, + TNodeMap& cache) { TNodeMap::iterator it = cache.find(e), iend = cache.end(); - if (it != iend) { + if (it != iend) + { return it->second; } // do substitution? it = substTable.find(e); iend = substTable.end(); - if (it != iend) { + if (it != iend) + { Node result = substitute(it->second, substTable, cache); cache[e] = result; return result; } size_t sz = e.getNumChildren(); - if (sz == 0) { + if (sz == 0) + { cache[e] = e; return e; } NodeBuilder<> builder(e.getKind()); - if (e.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (e.getMetaKind() == kind::metakind::PARAMETERIZED) + { builder << e.getOperator(); } - for (unsigned i = 0; i < e.getNumChildren(); ++ i) { + for (unsigned i = 0; i < e.getNumChildren(); ++i) + { builder << substitute(e[i], substTable, cache); } @@ -1495,7 +1746,6 @@ Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cach return result; } - Node ITECareSimplifier::simplifyWithCare(TNode e) { TNodeMap substTable; @@ -1514,7 +1764,8 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) bool done; unsigned i; - while (!queue.empty()) { + while (!queue.empty()) + { it = queue.end(); --it; v = it->first; @@ -1525,19 +1776,24 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) done = false; set::iterator iCare, iCareEnd = css.end(); - switch (v.getKind()) { - case kind::ITE: { + switch (v.getKind()) + { + case kind::ITE: + { iCare = css.find(v[0]); - if (iCare != iCareEnd) { + if (iCare != iCareEnd) + { Assert(substTable.find(v) == substTable.end()); substTable[v] = v[1]; updateQueue(queue, v[1], cs); done = true; break; } - else { + else + { iCare = css.find(v[0].negate()); - if (iCare != iCareEnd) { + if (iCare != iCareEnd) + { Assert(substTable.find(v) == substTable.end()); substTable[v] = v[2]; updateQueue(queue, v[2], cs); @@ -1557,10 +1813,13 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) done = true; break; } - case kind::AND: { - for (i = 0; i < v.getNumChildren(); ++i) { + case kind::AND: + { + for (i = 0; i < v.getNumChildren(); ++i) + { iCare = css.find(v[i].negate()); - if (iCare != iCareEnd) { + if (iCare != iCareEnd) + { Assert(substTable.find(v) == substTable.end()); substTable[v] = d_false; done = true; @@ -1574,16 +1833,20 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) cs2 = getNewSet(); cs2.getCareSet() = css; cs2.getCareSet().insert(v[0]); - for (i = 1; i < v.getNumChildren(); ++i) { + 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) { + case kind::OR: + { + for (i = 0; i < v.getNumChildren(); ++i) + { iCare = css.find(v[i]); - if (iCare != iCareEnd) { + if (iCare != iCareEnd) + { Assert(substTable.find(v) == substTable.end()); substTable[v] = d_true; done = true; @@ -1597,27 +1860,30 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) cs2 = getNewSet(); cs2.getCareSet() = css; cs2.getCareSet().insert(v[0].negate()); - for (i = 1; i < v.getNumChildren(); ++i) { + for (i = 1; i < v.getNumChildren(); ++i) + { updateQueue(queue, v[i], cs2); } done = true; break; } - default: - break; + default: break; } - if (done) { + if (done) + { continue; } - for (unsigned i = 0; i < v.getNumChildren(); ++i) { + for (unsigned i = 0; i < v.getNumChildren(); ++i) + { updateQueue(queue, v[i], cs); } } } /* Perform garbage collection. */ - while (!d_usedSets.empty()) { + while (!d_usedSets.empty()) + { CareSetPtrVal* used = d_usedSets.back(); d_usedSets.pop_back(); Assert(used->safeToGarbageCollect()); @@ -1631,12 +1897,12 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) } ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew( - ITECareSimplifier& simp) { + ITECareSimplifier& simp) +{ CareSetPtrVal* val = new CareSetPtrVal(simp); return CareSetPtr(val); } - - -} /* namespace theory */ -} /* namespace CVC4 */ +} // namespace util +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/theory/ite_utilities.h b/src/preprocessing/util/ite_utilities.h similarity index 85% rename from src/theory/ite_utilities.h rename to src/preprocessing/util/ite_utilities.h index bfce390eb..e137749db 100644 --- a/src/theory/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -2,7 +2,7 @@ /*! \file ite_utilities.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Paul Meng, Andres Noetzli + ** 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. @@ -14,7 +14,8 @@ ** 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 + ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC + *'96 **/ #include "cvc4_private.h" @@ -30,7 +31,8 @@ #include "util/statistics_registry.h" namespace CVC4 { -namespace theory { +namespace preprocessing { +namespace util { class IncomingArcCounter; class TermITEHeightCounter; @@ -41,8 +43,9 @@ class ITECareSimplifier; /** * A caching visitor that computes whether a node contains a term ite. */ -class ContainsTermITEVisitor { -public: +class ContainsTermITEVisitor +{ + public: ContainsTermITEVisitor(); ~ContainsTermITEVisitor(); @@ -55,7 +58,7 @@ public: /** returns the size of the cache. */ size_t cache_size() const { return d_cache.size(); } -private: + private: typedef std::unordered_map NodeBoolMap; NodeBoolMap d_cache; }; @@ -94,22 +97,28 @@ class ITEUtilities ITECareSimplifier* d_careSimp; }; -class IncomingArcCounter { -public: +class IncomingArcCounter +{ + public: IncomingArcCounter(bool skipVars = false, bool skipConstants = false); ~IncomingArcCounter(); void computeReachability(const std::vector& assertions); - inline uint32_t lookupIncoming(Node n) const { + inline uint32_t lookupIncoming(Node n) const + { NodeCountMap::const_iterator it = d_reachCount.find(n); - if(it == d_reachCount.end()){ + if (it == d_reachCount.end()) + { return 0; - }else{ + } + else + { return (*it).second; } } void clear(); -private: + + private: typedef std::unordered_map NodeCountMap; NodeCountMap d_reachCount; @@ -117,8 +126,9 @@ private: bool d_skipConstants; }; -class TermITEHeightCounter { -public: +class TermITEHeightCounter +{ + public: TermITEHeightCounter(); ~TermITEHeightCounter(); @@ -130,7 +140,8 @@ public: * - 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)) + * - termITEHeight(e not term ite) = max_{c in children(e)) + * (termITEHeight(c)) */ uint32_t termITEHeight(TNode e); @@ -140,7 +151,7 @@ public: /** Size of the cache. */ size_t cache_size() const; -private: + private: typedef std::unordered_map NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -149,8 +160,9 @@ private: * A routine designed to undo the potentially large blow up * due to expansion caused by the ite simplifier. */ -class ITECompressor { -public: +class ITECompressor +{ + public: ITECompressor(ContainsTermITEVisitor* contains); ~ITECompressor(); @@ -160,9 +172,8 @@ public: /* garbage Collects the compressor. */ void garbageCollect(); -private: - - Node d_true; /* Copy of true. */ + private: + Node d_true; /* Copy of true. */ Node d_false; /* Copy of false. */ ContainsTermITEVisitor* d_contains; std::vector* d_assertions; @@ -179,8 +190,9 @@ private: Node compressTerm(Node toCompress); Node compressBoolean(Node toCompress); - class Statistics { - public: + class Statistics + { + public: IntStat d_compressCalls; IntStat d_skolemsAdded; Statistics(); @@ -189,8 +201,9 @@ private: Statistics d_statistics; }; /* class ITECompressor */ -class ITESimplifier { -public: +class ITESimplifier +{ + public: ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); ~ITESimplifier(); @@ -199,16 +212,18 @@ public: bool doneALotOfWorkHeuristic() const; void clearSimpITECaches(); -private: + private: Node d_true; Node d_false; ContainsTermITEVisitor* d_containsVisitor; - inline bool containsTermITE(TNode n) { + inline bool containsTermITE(TNode n) + { return d_containsVisitor->containsTermITE(n); } TermITEHeightCounter d_termITEHeight; - inline uint32_t termITEHeight(TNode e) { + inline uint32_t termITEHeight(TNode e) + { return d_termITEHeight.termITEHeight(e); } @@ -216,7 +231,8 @@ private: // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector NodeVec; - typedef std::unordered_map ConstantLeavesMap; + typedef std::unordered_map + ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -224,7 +240,8 @@ private: // 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 + // - 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), @@ -234,7 +251,6 @@ private: // Lists all of the vectors in d_constantLeaves for fast deletion. std::vector d_allocatedConstantLeaves; - /* transforms */ Node transformAtom(TNode atom); Node attemptConstantRemoval(TNode atom); @@ -276,10 +292,10 @@ private: NodeMap d_simpITECache; Node simpITEAtom(TNode atom); - -private: - class Statistics { - public: + private: + class Statistics + { + public: IntStat d_maxNonConstantsFolded; IntStat d_unexpected; IntStat d_unsimplified; @@ -297,16 +313,17 @@ private: Statistics d_statistics; }; -class ITECareSimplifier { -public: +class ITECareSimplifier +{ + public: ITECareSimplifier(); ~ITECareSimplifier(); Node simplifyWithCare(TNode e); void clear(); -private: + private: /** * This should always equal the number of care sets allocated by * this object - the number of these that have been deleted. This is @@ -321,46 +338,58 @@ private: typedef std::unordered_map TNodeMap; class CareSetPtr; - class CareSetPtrVal { + class CareSetPtrVal + { public: bool safeToGarbageCollect() const { return d_refCount == 0; } + private: friend class ITECareSimplifier::CareSetPtr; ITECareSimplifier& d_iteSimplifier; unsigned d_refCount; std::set d_careSet; CareSetPtrVal(ITECareSimplifier& simp) - : d_iteSimplifier(simp), d_refCount(1) {} + : d_iteSimplifier(simp), d_refCount(1) + { + } }; /* class ITECareSimplifier::CareSetPtrVal */ std::vector d_usedSets; - void careSetPtrGC(CareSetPtrVal* val) { - d_usedSets.push_back(val); - } + void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); } - class CareSetPtr { + class CareSetPtr + { CareSetPtrVal* d_val; CareSetPtr(CareSetPtrVal* val) : d_val(val) {} - public: + + public: CareSetPtr() : d_val(NULL) {} - CareSetPtr(const CareSetPtr& cs) { + CareSetPtr(const CareSetPtr& cs) + { d_val = cs.d_val; - if (d_val != NULL) { + if (d_val != NULL) + { ++(d_val->d_refCount); } } - ~CareSetPtr() { - if (d_val != NULL && (--(d_val->d_refCount) == 0)) { + ~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)) { + 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) { + if (d_val != NULL) + { ++(d_val->d_refCount); } } @@ -369,7 +398,8 @@ private: std::set& getCareSet() { return d_val->d_careSet; } static CareSetPtr mkNew(ITECareSimplifier& simp); - static CareSetPtr recycle(CareSetPtrVal* val) { + static CareSetPtr recycle(CareSetPtrVal* val) + { Assert(val != NULL && val->d_refCount == 0); val->d_refCount = 1; return CareSetPtr(val); @@ -383,7 +413,8 @@ private: Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); }; -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace util +} // namespace preprocessing +} // namespace CVC4 #endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e7d52676..7b45bcb3c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,6 +82,7 @@ #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" +#include "preprocessing/passes/ite_simp.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" @@ -202,8 +203,6 @@ struct SmtEngineStatistics { /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; /** time spent in simplifying ITEs */ - TimerStat d_simpITETime; - /** time spent in simplifying ITEs */ TimerStat d_unconstrainedSimpTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; @@ -237,7 +236,6 @@ struct SmtEngineStatistics { d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_simpITETime("smt::SmtEngine::simpITETime"), d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), @@ -257,7 +255,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_simpITETime); smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); @@ -279,7 +276,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_simpITETime); smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); @@ -590,18 +586,9 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify ITE structure - bool simpITE(); - // Simplify based on unconstrained values void unconstrainedSimp(); - /** - * Ensures the assertions asserted after before now effectively come before - * d_realAssertionsEnd. - */ - void compressBeforeRealAssertions(size_t before); - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. @@ -2663,6 +2650,8 @@ void SmtEnginePrivate::finishInit() new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr intToBV( new IntToBV(d_preprocessingPassContext.get())); + std::unique_ptr iteSimp( + new ITESimp(d_preprocessingPassContext.get())); std::unique_ptr quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr pbProc( @@ -2705,6 +2694,7 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("global-negate", std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); + d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", @@ -3320,60 +3310,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -bool SmtEnginePrivate::simpITE() { - TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); - - spendResource(options::preprocessStep()); - - Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; - - unsigned numAssertionOnEntry = d_assertions.size(); - for (unsigned i = 0; i < d_assertions.size(); ++i) { - spendResource(options::preprocessStep()); - Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]); - d_assertions.replace(i, result); - if(result.isConst() && !result.getConst()){ - return false; - } - } - bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref()); - if(numAssertionOnEntry < d_assertions.size()){ - compressBeforeRealAssertions(numAssertionOnEntry); - } - return result; -} - -void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ - size_t curr = d_assertions.size(); - if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0 - || d_assertions.getRealAssertionsEnd() >= curr) - { - return; - } - - // assertions - // original: [0 ... d_assertions.getRealAssertionsEnd()) - // can be modified - // ites skolems [d_assertions.getRealAssertionsEnd(), before) - // cannot be moved - // added [before, curr) - // can be modified - Assert(0 < d_assertions.getRealAssertionsEnd()); - Assert(d_assertions.getRealAssertionsEnd() <= before); - Assert(before < curr); - - std::vector intoConjunction; - for(size_t i = before; id_unconstrainedSimpTime); spendResource(options::preprocessStep()); @@ -3845,11 +3781,14 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertions : " << d_assertions.size() << endl; // ITE simplification - if(options::doITESimp() && - (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) { + if (options::doITESimp() + && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) + { Chat() << "...doing ITE simplification..." << endl; - bool noConflict = simpITE(); - if(!noConflict){ + PreprocessingPassResult res = + d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions); + if (res == PreprocessingPassResult::CONFLICT) + { Chat() << "...ITE simplification found unsat..." << endl; return false; } diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index a683d2bbb..5b51e162d 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Kshitij Bansal + ** Tim King, Aina Niemetz, Kshitij Bansal ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -21,9 +21,9 @@ #include "base/output.h" #include "options/smt_options.h" +#include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" -#include "theory/ite_utilities.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_model.h" @@ -140,18 +140,19 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ Unreachable(); } -ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* uc, - TheoryModel* model) - : d_contains(contains) - , d_subs(NULL) - , d_model(model) - , d_one(1) - , d_subcount(uc, 0) - , d_skolems(uc) - , d_implies() - , d_skolemsAdded() - , d_orBinEqs() +ArithIteUtils::ArithIteUtils( + preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* uc, + TheoryModel* model) + : d_contains(contains), + d_subs(NULL), + d_model(model), + d_one(1), + d_subcount(uc, 0), + d_skolems(uc), + d_implies(), + d_skolemsAdded(), + d_orBinEqs() { d_subs = new SubstitutionMap(uc); } diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 7950ef05f..2c6a30758 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -29,15 +29,21 @@ #include "context/cdinsert_hashmap.h" namespace CVC4 { -namespace theory { +namespace preprocessing { +namespace util { class ContainsTermITEVisitor; +} +} // namespace preprocessing + +namespace theory { + class SubstitutionMap; class TheoryModel; namespace arith { class ArithIteUtils { - ContainsTermITEVisitor& d_contains; + preprocessing::util::ContainsTermITEVisitor& d_contains; SubstitutionMap* d_subs; TheoryModel* d_model; @@ -68,24 +74,24 @@ class ArithIteUtils { std::vector d_orBinEqs; public: - ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* userContext, - TheoryModel* model); - ~ArithIteUtils(); + ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* userContext, + TheoryModel* model); + ~ArithIteUtils(); - //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) + //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) - /** removes common sums variables sums from term ites. */ - Node reduceVariablesInItes(Node n); + /** removes common sums variables sums from term ites. */ + Node reduceVariablesInItes(Node n); - Node reduceConstantIteByGCD(Node n); + Node reduceConstantIteByGCD(Node n); - void clear(); + void clear(); - Node applySubstitutions(TNode f); - unsigned getSubCount() const; + Node applySubstitutions(TNode f); + unsigned getSubCount() const; - void learnSubstitutions(const std::vector& assertions); + void learnSubstitutions(const std::vector& assertions); private: /* applies this to all children of n and constructs the result */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 968970049..89550295a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -36,6 +36,7 @@ #include "expr/node_builder.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() +#include "preprocessing/util/ite_utilities.h" #include "smt/logic_exception.h" #include "smt/logic_request.h" #include "smt/smt_statistics_registry.h" @@ -59,7 +60,6 @@ #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" -#include "theory/ite_utilities.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -5374,7 +5374,7 @@ bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational } // TODO Speed up - ContainsTermITEVisitor ctv; + preprocessing::util::ContainsTermITEVisitor ctv; if(ctv.containsTermITE(t)){ return false; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f5341b38b..c87a4be02 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -40,7 +40,6 @@ #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/care_graph.h" -#include "theory/ite_utilities.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -336,8 +335,6 @@ TheoryEngine::TheoryEngine(context::Context* context, ProofManager::currentPM()->initTheoryProofEngine(); #endif - d_iteUtilities = new ITEUtilities(); - smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } @@ -366,8 +363,6 @@ TheoryEngine::~TheoryEngine() { delete d_unconstrainedSimp; - delete d_iteUtilities; - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } @@ -2000,111 +1995,6 @@ void TheoryEngine::staticInitializeBVOptions( } } -Node TheoryEngine::ppSimpITE(TNode assertion) -{ - if (!d_iteUtilities->containsTermITE(assertion)) - { - return assertion; - } else { - Node result = d_iteUtilities->simpITE(assertion); - Node res_rewritten = Rewriter::rewrite(result); - - if(options::simplifyWithCareEnabled()){ - Chat() << "starting simplifyWithCare()" << endl; - Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten); - Chat() << "ending simplifyWithCare()" - << " post simplifyWithCare()" << postSimpWithCare.getId() << endl; - result = Rewriter::rewrite(postSimpWithCare); - } else { - result = res_rewritten; - } - return result; - } -} - -bool TheoryEngine::donePPSimpITE(std::vector& assertions){ - // This pass does not support dependency tracking yet - // (learns substitutions from all assertions so just - // adding addDependence is not enough) - if (options::unsatCores() || options::fewerPreprocessingHoles()) { - return true; - } - bool result = true; - bool simpDidALotOfWork = d_iteUtilities->simpIteDidALotOfWorkHeuristic(); - if(simpDidALotOfWork){ - if(options::compressItes()){ - result = d_iteUtilities->compress(assertions); - } - - if(result){ - // if false, don't bother to reclaim memory here. - NodeManager* nm = NodeManager::currentNM(); - if(nm->poolSize() >= options::zombieHuntThreshold()){ - Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; - Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; - d_iteUtilities->clear(); - Rewriter::clearCaches(); - nm->reclaimZombiesUntil(options::zombieHuntThreshold()); - Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; - } - } - } - - // Do theory specific preprocessing passes - if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH) - && !options::incrementalSolving() ){ - if(!simpDidALotOfWork){ - ContainsTermITEVisitor& contains = - *(d_iteUtilities->getContainsVisitor()); - arith::ArithIteUtils aiteu(contains, d_userContext, getModel()); - bool anyItes = false; - for(size_t i = 0; i < assertions.size(); ++i){ - Node curr = assertions[i]; - if(contains.containsTermITE(curr)){ - anyItes = true; - Node res = aiteu.reduceVariablesInItes(curr); - Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl << " ->" << res << endl; - if(curr != res){ - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - assertions[i] = Rewriter::rewrite(more); - } - } - } - if(!anyItes){ - unsigned prevSubCount = aiteu.getSubCount(); - aiteu.learnSubstitutions(assertions); - if(prevSubCount < aiteu.getSubCount()){ - d_arithSubstitutionsAdded += aiteu.getSubCount() - prevSubCount; - bool anySuccess = false; - for(size_t i = 0, N = assertions.size(); i < N; ++i){ - Node curr = assertions[i]; - Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); - Node res = aiteu.reduceVariablesInItes(next); - Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl; - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - if(more != next){ - anySuccess = true; - break; - } - } - for(size_t i = 0, N = assertions.size(); anySuccess && i < N; ++i){ - Node curr = assertions[i]; - Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr)); - Node res = aiteu.reduceVariablesInItes(next); - Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl; - Node more = aiteu.reduceConstantIteByGCD(res); - Debug("arith::ite::red") << " gcd->" << more << endl; - assertions[i] = Rewriter::rewrite(more); - } - } - } - } - } - return result; -} - void TheoryEngine::getExplanation(std::vector& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5763114ca..71a0234ed 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -84,7 +84,6 @@ struct NodeTheoryPairHashFunction { namespace theory { class TheoryModel; class TheoryEngineModelBuilder; - class ITEUtilities; namespace eq { class EqualityEngine; @@ -828,12 +827,6 @@ private: /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** - * A collection of ite preprocessing passes. - */ - theory::ITEUtilities* d_iteUtilities; - - /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier* d_unconstrainedSimp; -- 2.30.2