diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 92 |
1 files changed, 75 insertions, 17 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb97d7f4c..c4eceeb24 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -17,6 +17,9 @@ **/ #include "smt/smt_engine.h" +#include "smt/noninteractive_exception.h" +#include "context/context.h" +#include "context/cdlist.h" #include "expr/command.h" #include "expr/node_builder.h" #include "util/output.h" @@ -25,9 +28,10 @@ #include "prop/prop_engine.h" #include "theory/theory_engine.h" - +using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::prop; -using CVC4::context::Context; +using namespace CVC4::context; namespace CVC4 { @@ -69,19 +73,30 @@ public: using ::CVC4::smt::SmtEnginePrivate; SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : - d_ctxt(em->getContext()), + d_context(em->getContext()), d_exprManager(em), d_nodeManager(em->getNodeManager()), - d_options(opts) { + d_options(opts), + /* These next few are initialized below, after we have a NodeManager + * in scope. */ + d_decisionEngine(NULL), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_assertionList(NULL) { NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_ctxt, opts); - d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); + d_theoryEngine = new TheoryEngine(d_context, opts); + d_propEngine = new PropEngine(opts, d_decisionEngine, + d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + + if(d_options->interactive) { + d_assertionList = new(true) CDList<Expr>(d_context); + } } void SmtEngine::shutdown() { @@ -95,6 +110,8 @@ SmtEngine::~SmtEngine() { shutdown(); + ::delete d_assertionList; + delete d_theoryEngine; delete d_propEngine; delete d_decisionEngine; @@ -105,53 +122,79 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } +void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::defineFunction(const string& name, + const vector<pair<string, Type> >& args, + Type type, + Expr formula) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { return smt.d_theoryEngine->preprocess(n); } Result SmtEngine::check() { - Debug("smt") << "SMT check()" << std::endl; + Debug("smt") << "SMT check()" << endl; return d_propEngine->checkSat(); } Result SmtEngine::quickCheck() { - Debug("smt") << "SMT quickCheck()" << std::endl; + Debug("smt") << "SMT quickCheck()" << endl; return Result(Result::VALIDITY_UNKNOWN); } void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) { - Debug("smt") << "push_back assertion " << n << std::endl; + Debug("smt") << "push_back assertion " << n << endl; smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; + Debug("smt") << "SMT checkSat(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); - Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT query(" << e << ")" << std::endl; + Debug("smt") << "SMT query(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); - Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; + Debug("smt") << "SMT assertFormula(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT simplify(" << e << ")" << std::endl; + Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } @@ -160,15 +203,30 @@ Model SmtEngine::getModel() { Unimplemented(); } +Expr SmtEngine::getValue(Expr term) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + +vector<Expr> SmtEngine::getAssertions() throw(NoninteractiveException) { + if(!d_options->interactive) { + const char* msg = + "Cannot query the current assertion list when not in interactive mode."; + throw NoninteractiveException(msg); + } + Assert(d_assertionList != NULL); + return vector<Expr>(d_assertionList->begin(), d_assertionList->end()); +} + void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT push()" << std::endl; + Debug("smt") << "SMT push()" << endl; Unimplemented(); } void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT pop()" << std::endl; + Debug("smt") << "SMT pop()" << endl; Unimplemented(); } |