summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/Makefile.am4
-rw-r--r--src/smt/bad_option.h48
-rw-r--r--src/smt/noninteractive_exception.h49
-rw-r--r--src/smt/smt_engine.cpp92
-rw-r--r--src/smt/smt_engine.h147
5 files changed, 274 insertions, 66 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 90d58904a..192915152 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -7,4 +7,6 @@ noinst_LTLIBRARIES = libsmt.la
libsmt_la_SOURCES = \
smt_engine.cpp \
- smt_engine.h
+ smt_engine.h \
+ noninteractive_exception.h \
+ bad_option.h
diff --git a/src/smt/bad_option.h b/src/smt/bad_option.h
new file mode 100644
index 000000000..800d8e68a
--- /dev/null
+++ b/src/smt/bad_option.h
@@ -0,0 +1,48 @@
+/********************* */
+/*! \file bad_option.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an option setting is not
+ ** understood.
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__BAD_OPTION_H
+#define __CVC4__SMT__BAD_OPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC BadOption : public CVC4::Exception {
+public:
+ BadOption() :
+ Exception("Unrecognized informational or option key or setting") {
+ }
+
+ BadOption(const std::string& msg) :
+ Exception(msg) {
+ }
+
+ BadOption(const char* msg) :
+ Exception(msg) {
+ }
+};/* class BadOption */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__BAD_OPTION_H */
diff --git a/src/smt/noninteractive_exception.h b/src/smt/noninteractive_exception.h
new file mode 100644
index 000000000..4cf97ab3e
--- /dev/null
+++ b/src/smt/noninteractive_exception.h
@@ -0,0 +1,49 @@
+/********************* */
+/*! \file noninteractive_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an interactive-only
+ ** feature while CVC4 is being used in a non-interactive setting
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
+#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception {
+public:
+ NoninteractiveException() :
+ Exception("Interactive feature used while operating in "
+ "non-interactive mode") {
+ }
+
+ NoninteractiveException(const std::string& msg) :
+ Exception(msg) {
+ }
+
+ NoninteractiveException(const char* msg) :
+ Exception(msg) {
+ }
+};/* class NoninteractiveException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */
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();
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b5807852b..56e38af7a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -27,6 +27,9 @@
#include "expr/expr_manager.h"
#include "util/result.h"
#include "util/model.h"
+#include "util/sexpr.h"
+#include "smt/noninteractive_exception.h"
+#include "smt/bad_option.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
@@ -36,6 +39,7 @@ namespace CVC4 {
namespace context {
class Context;
+ template <class T> class CDList;
}/* CVC4::context namespace */
class Command;
@@ -63,6 +67,61 @@ namespace smt {
// The CNF conversion can go on in PropEngine.
class CVC4_PUBLIC SmtEngine {
+private:
+
+ /** Our Context */
+ context::Context* d_context;
+
+ /** Our expression manager */
+ ExprManager* d_exprManager;
+
+ /** Out internal expression/node manager */
+ NodeManager* d_nodeManager;
+
+ /** User-level options */
+ const Options* d_options;
+
+ /** The decision engine */
+ DecisionEngine* d_decisionEngine;
+
+ /** The decision engine */
+ TheoryEngine* d_theoryEngine;
+
+ /** The propositional engine */
+ prop::PropEngine* d_propEngine;
+
+ /**
+ * The assertion list, before any conversion, for supporting
+ * getAssertions(). Only maintained if in interactive mode.
+ */
+ context::CDList<Expr>* d_assertionList;
+
+ // preprocess() and addFormula() used to be housed here; they are
+ // now in an SmtEnginePrivate class. See the comment in
+ // smt_engine.cpp.
+
+ /**
+ * This is called by the destructor, just before destroying the
+ * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
+ * is important because there are destruction ordering issues
+ * between PropEngine and Theory.
+ */
+ void shutdown();
+
+ /**
+ * Full check of consistency in current context. Returns true iff
+ * consistent.
+ */
+ Result check();
+
+ /**
+ * Quick check of consistency in current context: calls
+ * processAssertionList() then look for inconsistency (based only on
+ * that).
+ */
+ Result quickCheck();
+
+ friend class ::CVC4::smt::SmtEnginePrivate;
public:
@@ -82,6 +141,37 @@ public:
void doCommand(Command*);
/**
+ * Set information about the script executing.
+ */
+ void setInfo(const std::string& key, const SExpr& value) throw(BadOption);
+
+ /**
+ * Query information about the SMT environment.
+ */
+ const SExpr& getInfo(const std::string& key) const throw(BadOption);
+
+ /**
+ * Set an aspect of the current SMT execution environment.
+ */
+ void setOption(const std::string& key, const SExpr& value) throw(BadOption);
+
+ /**
+ * Get an aspect of the current SMT execution environment.
+ */
+ const SExpr& getOption(const std::string& key) const throw(BadOption);
+
+ /**
+ * Add a formula to the current context: preprocess, do per-theory
+ * setup, use processAssertionList(), asserting to T-solver for
+ * literals and conjunction of literals. Returns false iff
+ * inconsistent.
+ */
+ void defineFunction(const std::string& name,
+ const std::vector<std::pair<std::string, Type> >& args,
+ Type type,
+ Expr formula);
+
+ /**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
* literals and conjunction of literals. Returns false iff
@@ -113,64 +203,25 @@ public:
Model getModel();
/**
- * Push a user-level context.
- */
- void push();
-
- /**
- * Pop a user-level context. Throws an exception if nothing to pop.
+ * Get the assigned value of a term (only if preceded by a SAT or
+ * INVALID query).
*/
- void pop();
-
-private:
-
- /** Our Context */
- CVC4::context::Context* d_ctxt;
-
- /** Our expression manager */
- ExprManager* d_exprManager;
-
- /** Out internal expression/node manager */
- NodeManager* d_nodeManager;
-
- /** User-level options */
- const Options* d_options;
-
- /** The decision engine */
- DecisionEngine* d_decisionEngine;
-
- /** The decision engine */
- TheoryEngine* d_theoryEngine;
-
- /** The propositional engine */
- prop::PropEngine* d_propEngine;
-
- // preprocess() and addFormula() used to be housed here; they are
- // now in an SmtEnginePrivate class. See the comment in
- // smt_engine.cpp.
+ Expr getValue(Expr term);
/**
- * This is called by the destructor, just before destroying the
- * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
- * is important because there are destruction ordering issues
- * between PropEngine and Theory.
+ * Get the current set of assertions.
*/
- void shutdown();
+ std::vector<Expr> getAssertions() throw(NoninteractiveException);
/**
- * Full check of consistency in current context. Returns true iff
- * consistent.
+ * Push a user-level context.
*/
- Result check();
+ void push();
/**
- * Quick check of consistency in current context: calls
- * processAssertionList() then look for inconsistency (based only on
- * that).
+ * Pop a user-level context. Throws an exception if nothing to pop.
*/
- Result quickCheck();
-
- friend class ::CVC4::smt::SmtEnginePrivate;
+ void pop();
};/* class SmtEngine */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback