summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp154
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback