diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 218 |
1 files changed, 43 insertions, 175 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0d93c16bc..951b49603 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,8 +79,11 @@ #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#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/nl_ext_purify.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" @@ -116,7 +119,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" @@ -202,8 +204,6 @@ struct SmtEngineStatistics { IntStat d_numMiplibAssertionsRemoved; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent in simplifying ITEs */ - TimerStat d_simpITETime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; /** time spent converting to CNF */ @@ -236,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_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), @@ -255,7 +254,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_simpITETime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); @@ -276,7 +274,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_simpITETime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); @@ -567,14 +564,6 @@ class SmtEnginePrivate : public NodeManagerListener { bool nonClausalSimplify(); /** - * Performs static learning on the assertions. - */ - void staticLearning(); - - Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq); - Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false); - - /** * Helper function to fix up assertion list to restore invariants needed after * ite removal. */ @@ -586,15 +575,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify ITE structure - bool simpITE(); - - /** - * 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. @@ -740,10 +720,14 @@ class SmtEnginePrivate : public NodeManagerListener { } } - void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override + void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts, + uint32_t flags) override { - DatatypeDeclarationCommand c(dtts); - d_smt.addToModelCommandAndDump(c); + if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) + { + DatatypeDeclarationCommand c(dtts); + d_smt.addToModelCommandAndDump(c); + } } void nmNotifyNewVar(TNode n, uint32_t flags) override @@ -792,7 +776,7 @@ class SmtEnginePrivate : public NodeManagerListener { /** Process a user push. */ void notifyPush() { - + } /** @@ -874,13 +858,13 @@ class SmtEnginePrivate : public NodeManagerListener { std::ostream* getReplayLog() const { return d_managedReplayLog.getReplayLog(); } - + //------------------------------- expression names // implements setExpressionName, as described in smt_engine.h void setExpressionName(Expr e, std::string name) { d_exprNames[Node::fromExpr(e)] = name; } - + // implements getExpressionName, as described in smt_engine.h bool getExpressionName(Expr e, std::string& name) const { context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e); @@ -1192,6 +1176,8 @@ void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { return d_logic; } +void SmtEngine::setFilename(std::string filename) { d_filename = filename; } +std::string SmtEngine::getFilename() const { return d_filename; } void SmtEngine::setLogicInternal() { Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already" @@ -2026,7 +2012,6 @@ void SmtEngine::setDefaults() { } if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) { - options::cbqiAll.set( false ); if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } @@ -2301,15 +2286,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...) - if (key == "source" - || key == "category" - || key == "difficulty" - || key == "notes" - || key == "license") + if (key == "source" || key == "category" || key == "difficulty" + || key == "notes" || key == "name" || key == "license") { // ignore these return; - } else if(key == "name") { + } + else if (key == "filename") + { d_filename = value.getValue(); return; } @@ -2653,8 +2637,14 @@ void SmtEnginePrivate::finishInit() new BVToBool(d_preprocessingPassContext.get())); std::unique_ptr<ExtRewPre> extRewPre( new ExtRewPre(d_preprocessingPassContext.get())); + std::unique_ptr<GlobalNegate> globalNegate( + new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr<IntToBV> intToBV( new IntToBV(d_preprocessingPassContext.get())); + std::unique_ptr<ITESimp> iteSimp( + new ITESimp(d_preprocessingPassContext.get())); + std::unique_ptr<NlExtPurify> nlExtPurify( + new NlExtPurify(d_preprocessingPassContext.get())); std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess( new QuantifiersPreprocess(d_preprocessingPassContext.get())); std::unique_ptr<PseudoBooleanProcessor> pbProc( @@ -2696,7 +2686,12 @@ void SmtEnginePrivate::finishInit() std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); + 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("nl-ext-purify", + std::move(nlExtPurify)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", @@ -2709,7 +2704,7 @@ void SmtEnginePrivate::finishInit() std::move(sepSkolemEmp)); d_preprocessingPassRegistry.registerPass("sort-inference", std::move(sortInfer)); - d_preprocessingPassRegistry.registerPass("static-learning", + d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); d_preprocessingPassRegistry.registerPass("sygus-infer", std::move(sygusInfer)); @@ -2902,68 +2897,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node return result.top(); } -typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; - -Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) { - if( beneathMult ){ - NodeMap::iterator find = bcache.find(n); - if (find != bcache.end()) { - return (*find).second; - } - }else{ - NodeMap::iterator find = cache.find(n); - if (find != cache.end()) { - return (*find).second; - } - } - Node ret = n; - if( n.getNumChildren()>0 ){ - if (beneathMult - && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) - { - // don't do it if it rewrites to a constant - Node nr = Rewriter::rewrite(n); - if (nr.isConst()) - { - // return the rewritten constant - ret = nr; - } - else - { - // new variable - ret = NodeManager::currentNM()->mkSkolem( - "__purifyNl_var", - n.getType(), - "Variable introduced in purifyNl pass"); - Node np = purifyNlTerms(n, cache, bcache, var_eq, false); - var_eq.push_back(np.eqNode(ret)); - Trace("nl-ext-purify") - << "Purify : " << ret << " -> " << np << std::endl; - } - } - else - { - bool beneathMultNew = beneathMult || n.getKind()==kind::MULT; - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew ); - childChanged = childChanged || nc!=n[i]; - children.push_back( nc ); - } - if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - } - if( beneathMult ){ - bcache[n] = ret; - }else{ - cache[n] = ret; - } - return ret; -} - // do dumping (before/after any preprocessing pass) static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) { @@ -3314,60 +3247,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<bool>()){ - return false; - } - } - bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref()); - if(numAssertionOnEntry < d_assertions.size()){ - compressBeforeRealAssertions(numAssertionOnEntry); - } - return result; -} - -void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ - size_t curr = d_assertions.size(); - if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0 - || d_assertions.getRealAssertionsEnd() >= curr) - { - return; - } - - // assertions - // original: [0 ... d_assertions.getRealAssertionsEnd()) - // can be modified - // ites skolems [d_assertions.getRealAssertionsEnd(), before) - // cannot be moved - // added [before, curr) - // can be modified - Assert(0 < d_assertions.getRealAssertionsEnd()); - Assert(d_assertions.getRealAssertionsEnd() <= before); - Assert(before < curr); - - std::vector<Node> intoConjunction; - for(size_t i = before; i<curr; ++i){ - intoConjunction.push_back(d_assertions[i]); - } - d_assertions.resize(before); - size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1; - intoConjunction.push_back(d_assertions[lastBeforeItes]); - Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); - d_assertions.replace(lastBeforeItes, newLast); - Assert(d_assertions.size() == before); -} - void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) { const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) { @@ -3832,11 +3711,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; } @@ -4071,26 +3953,12 @@ void SmtEnginePrivate::processAssertions() { if (options::globalNegate()) { // global negation of the formula - quantifiers::GlobalNegate gn; - gn.simplify(d_assertions.ref()); + d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions); d_smt.d_globalNegation = !d_smt.d_globalNegation; } if( options::nlExtPurify() ){ - unordered_map<Node, Node, NodeHashFunction> cache; - unordered_map<Node, Node, NodeHashFunction> bcache; - std::vector< Node > var_eq; - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Node a = d_assertions[i]; - d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq)); - Trace("nl-ext-purify") - << "Purify : " << a << " -> " << d_assertions[i] << std::endl; - } - if( !var_eq.empty() ){ - unsigned lastIndex = d_assertions.size()-1; - var_eq.insert( var_eq.begin(), d_assertions[lastIndex] ); - d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); - } + d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions); } if( options::ceGuidedInst() ){ @@ -5564,7 +5432,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) Assert( inst_qs.size()<=1 ); Node ret_n; if( inst_qs.size()==1 ){ - Node top_q = inst_qs[0]; + Node top_q = inst_qs[0]; //Node top_q = Rewriter::rewrite( nn_e ).negate(); Assert( top_q.getKind()==kind::FORALL ); Trace("smt-qe") << "Get qe for " << top_q << std::endl; @@ -5987,7 +5855,7 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) { AlwaysAssert(!d_fullyInited, "Cannot set replay stream once fully initialized"); d_replayStream = replayStream; -} +} bool SmtEngine::getExpressionName(Expr e, std::string& name) const { return d_private->getExpressionName(e, name); |