declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

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