diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/smt | |
parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 31 |
2 files changed, 27 insertions, 16 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c4eceeb24..be4abb8ab 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -94,8 +94,10 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + d_functions = new(true) FunctionMap(d_context); + if(d_options->interactive) { - d_assertionList = new(true) CDList<Expr>(d_context); + d_assertionList = new(true) AssertionList(d_context); } } @@ -110,7 +112,11 @@ SmtEngine::~SmtEngine() { shutdown(); - ::delete d_assertionList; + if(d_assertionList != NULL) { + d_assertionList->deleteSelf(); + } + + d_functions->deleteSelf(); delete d_theoryEngine; delete d_propEngine; @@ -145,7 +151,7 @@ void SmtEngine::defineFunction(const string& name, Type type, Expr formula) { NodeManagerScope nms(d_nodeManager); - Unimplemented(); + d_functions->insert(name, make_pair(make_pair(args, type), formula)); } Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 56e38af7a..97772273d 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -25,9 +25,11 @@ #include "expr/expr.h" #include "expr/expr_manager.h" +#include "context/cdmap_forward.h" #include "util/result.h" #include "util/model.h" #include "util/sexpr.h" +#include "util/hash.h" #include "smt/noninteractive_exception.h" #include "smt/bad_option.h" @@ -69,36 +71,39 @@ namespace smt { class CVC4_PUBLIC SmtEngine { private: + /** A name/type pair, used for signatures */ + typedef std::pair<std::string, Type> TypedArg; + /** A vector of typed formals, and a return type */ + typedef std::pair<std::vector<TypedArg>, Type> FunctionSignature; + /** The type of our internal map of defined functions */ + typedef context::CDMap<std::string, std::pair<FunctionSignature, Expr>, + StringHashFunction> + FunctionMap; + + /** The type of our internal assertion list */ + typedef context::CDList<Expr> AssertionList; + /** 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; - + /** An index of our defined functions */ + FunctionMap* d_functions; /** - * The assertion list, before any conversion, for supporting + * 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. + AssertionList* d_assertionList; /** * This is called by the destructor, just before destroying the |