diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
commit | 7742c4211f765c2ba2637a211265c20789b861ee (patch) | |
tree | 05622a9df5dc2c900608b8e2ac5611d70e3208c6 /src/smt | |
parent | ccd77233892ace44fd4852999e66534d1c2283ea (diff) |
A dummy decision engine. Expected performance impact: none.
Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.
Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 21 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
2 files changed, 20 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 97407a425..a41def821 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): cconway, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -27,6 +27,7 @@ #include "context/cdlist.h" #include "context/cdhashset.h" #include "context/context.h" +#include "decision/decision_engine.h" #include "expr/command.h" #include "expr/expr.h" #include "expr/kind.h" @@ -223,6 +224,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_userContext(new UserContext()), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), + d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), d_definedFunctions(NULL), @@ -262,8 +264,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY); CVC4_FOR_EACH_THEORY; - d_propEngine = new PropEngine(d_theoryEngine, d_context); + d_decisionEngine = new DecisionEngine(); + d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + // d_decisionEngine->setPropEngine(d_propEngine); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); @@ -309,6 +313,7 @@ void SmtEngine::shutdown() { d_propEngine->shutdown(); d_theoryEngine->shutdown(); + d_decisionEngine->shutdown(); } SmtEngine::~SmtEngine() throw() { @@ -917,9 +922,6 @@ void SmtEnginePrivate::simplifyAssertions() staticLearning(); } - // Remove ITEs - removeITEs(); - } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -1004,6 +1006,15 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); + if(d_smt.d_decisionEngine->needSimplifiedPreITEAssertions()) { + d_smt.d_decisionEngine->informSimplifiedPreITEAssertions(d_assertionsToCheck); + } + + // Remove ITEs + removeITEs(); // This may need to be in a try-catch + // block. make regress is passing, so + // skipping for now --K + Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5149ed2e9..abd07538b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): cconway, kshitij ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -50,6 +50,7 @@ typedef NodeTemplate<true> Node; typedef NodeTemplate<false> TNode; class NodeHashFunction; +class DecisionEngine; class TheoryEngine; class StatisticsRegistry; @@ -109,6 +110,8 @@ class CVC4_PUBLIC SmtEngine { /** Our internal expression/node manager */ NodeManager* d_nodeManager; /** The decision engine */ + DecisionEngine* d_decisionEngine; + /** The theory engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ prop::PropEngine* d_propEngine; |