diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 154 |
1 files changed, 29 insertions, 125 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c4492d3a1..02e9892e2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,7 +83,10 @@ #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/quantifier_macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" @@ -94,6 +97,7 @@ #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" +#include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -117,7 +121,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" @@ -202,8 +205,6 @@ struct SmtEngineStatistics { IntStat d_numMiplibAssertionsRemoved; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent in simplifying ITEs */ - TimerStat d_unconstrainedSimpTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; /** time spent converting to CNF */ @@ -236,7 +237,6 @@ struct SmtEngineStatistics { d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), @@ -255,7 +255,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->registerStat(&d_numConstantProps); - smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); smtStatisticsRegistry()->registerStat(&d_numAssertionsPre); @@ -276,7 +275,6 @@ struct SmtEngineStatistics { smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); smtStatisticsRegistry()->unregisterStat(&d_numConstantProps); - smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime); smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime); smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre); @@ -567,14 +565,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,9 +576,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); - // Simplify based on unconstrained values - void unconstrainedSimp(); - /** * Trace nodes back to their assertions using CircuitPropagator's * BackEdgesMap. @@ -790,7 +777,7 @@ class SmtEnginePrivate : public NodeManagerListener { /** Process a user push. */ void notifyPush() { - + } /** @@ -872,13 +859,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); @@ -2026,7 +2013,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 ); } @@ -2658,6 +2644,8 @@ void SmtEnginePrivate::finishInit() 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( @@ -2681,6 +2669,8 @@ void SmtEnginePrivate::finishInit() new SynthRewRulesPass(d_preprocessingPassContext.get())); std::unique_ptr<SepSkolemEmp> sepSkolemEmp( new SepSkolemEmp(d_preprocessingPassContext.get())); + std::unique_ptr<UnconstrainedSimplifier> unconstrainedSimplifier( + new UnconstrainedSimplifier(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("apply-substs", std::move(applySubsts)); d_preprocessingPassRegistry.registerPass("apply-to-const", @@ -2692,6 +2682,8 @@ void SmtEnginePrivate::finishInit() std::move(bvAckermann)); d_preprocessingPassRegistry.registerPass("bv-eager-atoms", std::move(bvEagerAtoms)); + std::unique_ptr<QuantifierMacros> quantifierMacros( + new QuantifierMacros(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); @@ -2701,6 +2693,8 @@ void SmtEnginePrivate::finishInit() 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", @@ -2713,12 +2707,16 @@ 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)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); + d_preprocessingPassRegistry.registerPass("quantifier-macros", + std::move(quantifierMacros)); + d_preprocessingPassRegistry.registerPass("unconstrained-simplifier", + std::move(unconstrainedSimplifier)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) @@ -2904,68 +2902,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) { @@ -3316,13 +3252,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::unconstrainedSimp() { - TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); - spendResource(options::preprocessStep()); - Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; - d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); -} - 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) { @@ -3806,14 +3735,10 @@ bool SmtEnginePrivate::simplifyAssertions() // Unconstrained simplification if(options::unconstrainedSimp()) { - Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } - dumpAssertions("post-unconstrained", d_assertions); - Trace("smt") << "POST unconstrainedSimp" << endl; - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -4038,20 +3963,7 @@ void SmtEnginePrivate::processAssertions() { } 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() ){ @@ -4101,12 +4013,9 @@ void SmtEnginePrivate::processAssertions() { // Unconstrained simplification if(options::unconstrainedSimp()) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; - dumpAssertions("pre-unconstrained-simp", d_assertions); d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); - unconstrainedSimp(); - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; - dumpAssertions("post-unconstrained-simp", d_assertions); + d_preprocessingPassRegistry.getPass("unconstrained-simplifier") + ->apply(&d_assertions); } if(options::bvIntroducePow2()) @@ -4157,13 +4066,8 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); - bool success; - do{ - success = qm.simplify( d_assertions.ref(), true ); - }while( success ); - //finalize the definitions - qm.finalizeDefinitions(); + d_preprocessingPassRegistry.getPass("quantifier-macros") + ->apply(&d_assertions); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF @@ -5528,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; @@ -5951,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); |