diff options
author | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 13:21:40 -0700 |
---|---|---|
committer | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 15:52:45 -0700 |
commit | 1880e0ecd5ffeab77f0a1dcdea1c78b8c5eabcd4 (patch) | |
tree | bb5b801b71a5a752ba40421a20bffad95f5b84df /src/smt | |
parent | e79fa19f8eacdeab55089cdfec717574b9b7af34 (diff) |
ContrainSubtypes and ExpandingDefinitions classes
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 42 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 13 |
2 files changed, 35 insertions, 20 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d61639ad0..f43e6533e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -144,7 +144,8 @@ public: * support getValue() over defined functions, to support user output * in terms of defined functions, etc. */ -class DefinedFunction { + +/*class DefinedFunction { Node d_func; vector<Node> d_formals; Node d_formula; @@ -158,7 +159,8 @@ public: Node getFunction() const { return d_func; } vector<Node> getFormals() const { return d_formals; } Node getFormula() const { return d_formula; } -};/* class DefinedFunction */ +};*/ +/* class DefinedFunction */ /*class AssertionPipeline { vector<Node> d_nodes; @@ -1014,7 +1016,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_userContext->push(); d_context->push(); - d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); + d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext); d_modelCommands = new(true) smt::CommandList(d_userContext); } @@ -3498,16 +3500,10 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", d_assertions); { -/* preproc::ExpandingDefinitionsPass pass(d_resourceManager, d_smt.d_stats->d_definitionExpansionTime); - pass.apply(&d_assertions);*/ - Chat() << "expanding definitions..." << endl; - Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); - unordered_map<Node, Node, NodeHashFunction> cache; - for(unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); - } - } + preproc::ExpandingDefinitionsPass pass(d_resourceManager, &d_smt, d_smt.d_stats->d_definitionExpansionTime); + pass.apply(&d_assertions); + } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); @@ -3567,6 +3563,18 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; +<<<<<<< e79fa19f8eacdeab55089cdfec717574b9b7af34 +======= + dumpAssertions("pre-constrain-subtypes", d_assertions); + { + preproc::ConstrainSubtypesPass pass(d_resourceManager, &d_smt); + pass.apply(&d_assertions); + } + dumpAssertions("post-constrain-subtypes", d_assertions); + + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + +>>>>>>> ContrainSubtypes and ExpandingDefinitions classes bool noConflict = true; // Unconstrained simplification @@ -3690,12 +3698,12 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-repeat-simplify", d_assertions); if(options::repeatSimp()) { - preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth); +/* preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth, &d_smt, d_propagatorNeedsFinish, d_propagator, d_substitutionsIndex, d_nonClausalLearnedLiterals, d_true, d_smt.d_stats->d_nonclausalSimplificationTime); noConflict &= pass.apply(&d_assertions).d_noConflict; preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); - pass1.apply(&d_assertions); -/* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; + pass1.apply(&d_assertions);*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); @@ -3761,7 +3769,7 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; } dumpAssertions("post-repeat-simplify", d_assertions); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1202b4ff6..dd4906aad 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -81,7 +81,7 @@ namespace smt { * support getValue() over defined functions, to support user output * in terms of defined functions, etc. */ - class DefinedFunction; +// class DefinedFunction; struct SmtEngineStatistics; class SmtEnginePrivate; @@ -99,8 +99,12 @@ namespace theory { }/* CVC4::theory namespace */ namespace preproc{ + class DefinedFunction; class DoStaticLearningPass; class QuantifiedPass; + class SimplifyAssertionsPass; + class ExpandingDefinitionsPass; + class ConstrainSubtypesPass; }/* CVC4::preproc namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -116,7 +120,7 @@ namespace preproc{ class CVC4_PUBLIC SmtEngine { /** The type of our internal map of defined functions */ - typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> + typedef context::CDHashMap<Node, preproc::DefinedFunction, NodeHashFunction> DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList<Expr> AssertionList; @@ -345,9 +349,12 @@ class CVC4_PUBLIC SmtEngine { * be called when d_logic is updated. */ void setLogicInternal() throw(); - + friend class ::CVC4::preproc::DefinedFunction; friend class ::CVC4::preproc::DoStaticLearningPass; friend class ::CVC4::preproc::QuantifiedPass; + friend class ::CVC4::preproc::SimplifyAssertionsPass; + friend class ::CVC4::preproc::ExpandingDefinitionsPass; + friend class ::CVC4::preproc::ConstrainSubtypesPass; friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; |