SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time

18 files changed, 476 insertions, 127 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index a1486fcab..8c90f337e 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -23,6 +23,7 @@
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
+#include "smt/bad_option_exception.h"
 #include "util/output.h"
 
 using namespace std;
@@ -217,26 +218,26 @@ void DeclarationCommand::toStream(std::ostream& out) const {
 
 /* class DefineFunctionCommand */
 
-DefineFunctionCommand::DefineFunctionCommand(const std::string& name,
-                                                    const std::vector<std::pair<std::string, Type> >& args,
-                                                    Type type,
-                                                    Expr formula) :
-  d_name(name),
-  d_args(args),
-  d_type(type),
+DefineFunctionCommand::DefineFunctionCommand(Expr func,
+                                             const std::vector<Expr>& formals,
+                                             Expr formula) :
+  d_func(func),
+  d_formals(formals),
   d_formula(formula) {
 }
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->defineFunction(d_name, d_args, d_type, d_formula);
+  smtEngine->defineFunction(d_func, d_formals, d_formula);
 }
 
 void DefineFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineFunction( \"" << d_name << "\", [";
-  copy( d_args.begin(), d_args.end() - 1,
-        ostream_iterator<std::pair<std::string, Type> >(out, ", ") );
-  out << d_args.back();
-  out << "], << " << d_type << " >>, << " << d_formula << " >> )";
+  out << "DefineFunction( \"" << d_func << "\", [";
+  if(d_formals.size() > 0) {
+    copy( d_formals.begin(), d_formals.end() - 1,
+          ostream_iterator<Expr>(out, ", ") );
+    out << d_formals.back();
+  }
+  out << "], << " << d_formula << " >> )";
 }
 
 /* class GetValueCommand */
@@ -324,7 +325,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -352,7 +353,7 @@ GetInfoCommand::GetInfoCommand(std::string flag) :
 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getInfo(d_flag).getValue();
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -382,7 +383,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     //d_result = "success";
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
@@ -410,7 +411,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) :
 void GetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
-  } catch(BadOption& bo) {
+  } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
 }
diff --git a/src/expr/command.h b/src/expr/command.h
index 0c78dd1c6..4c74cfd6c 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -111,14 +111,13 @@ public:
 
 class CVC4_PUBLIC DefineFunctionCommand : public Command {
 protected:
-  std::string d_name;
-  std::vector<std::pair<std::string, Type> > d_args;
-  Type d_type;
+  Expr d_func;
+  std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(const std::string& name,
-                        const std::vector<std::pair<std::string, Type> >& args,
-                        Type type, Expr formula);
+  DefineFunctionCommand(Expr func,
+                        const std::vector<Expr>& formals,
+                        Expr formula);
   void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
 };/* class DefineFunctionCommand */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 803808b0f..5fb931a65 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -223,7 +223,11 @@ void Expr::toStream(std::ostream& out, int depth, bool types) const {
   d_node->toStream(out, depth, types);
 }
 
-Node Expr::getNode() const {
+Node Expr::getNode() const throw() {
+  return *d_node;
+}
+
+TNode Expr::getTNode() const throw() {
   return *d_node;
 }
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 8fab13b37..bb227f92f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -43,8 +43,13 @@ class NodeTemplate;
 
 class Expr;
 class ExprManager;
+class SmtEngine;
 class Type;
 
+namespace smt {
+  class SmtEnginePrivate;
+}/* CVC4::smt namespace */
+
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
@@ -383,10 +388,17 @@ protected:
    * Returns the actual internal node.
    * @return the internal node
    */
-  NodeTemplate<true> getNode() const;
+  NodeTemplate<true> getNode() const throw();
+
+  /**
+   * Returns the actual internal node as a TNode.
+   * @return the internal node
+   */
+  NodeTemplate<false> getTNode() const throw();
 
   // Friend to access the actual internal expr information and private methods
   friend class SmtEngine;
+  friend class smt::SmtEnginePrivate;
   friend class ExprManager;
 };
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 67d46a977..bd6b53522 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -380,6 +380,20 @@ public:
     throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException);
 
   /**
+   * Substitution of Nodes.
+   */
+  Node substitute(TNode node, TNode replacement) const;
+
+  /**
+   * Simultaneous substitution of Nodes.
+   */
+  template <class Iterator1, class Iterator2>
+  Node substitute(Iterator1 nodesBegin,
+                  Iterator1 nodesEnd,
+                  Iterator2 replacementsBegin,
+                  Iterator2 replacementsEnd) const;
+
+  /**
    * Returns the kind of this node.
    * @return the kind
    */
@@ -1035,6 +1049,59 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
   return NodeManager::currentNM()->getType(*this, check);
 }
 
+template <bool ref_count>
+Node NodeTemplate<ref_count>::substitute(TNode node,
+                                         TNode replacement) const {
+  NodeBuilder<> nb(getKind());
+  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+    // push the operator
+    nb << getOperator();
+  }
+  for(TNode::const_iterator i = begin(),
+        iend = end();
+      i != iend;
+      ++i) {
+    if(*i == node) {
+      nb << replacement;
+    } else {
+      (*i).substitute(node, replacement);
+    }
+  }
+  Node n = nb;
+  return n;
+}
+
+template <bool ref_count>
+template <class Iterator1, class Iterator2>
+Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
+                                         Iterator1 nodesEnd,
+                                         Iterator2 replacementsBegin,
+                                         Iterator2 replacementsEnd) const {
+  Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
+          "Substitution iterator ranges must be equal size" );
+  Iterator1 j = find(nodesBegin, nodesEnd, *this);
+  if(j != nodesEnd) {
+    return *(replacementsBegin + (j - nodesBegin));
+  } else if(getNumChildren() == 0) {
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << getOperator();
+    }
+    for(TNode::const_iterator i = begin(),
+          iend = end();
+        i != iend;
+        ++i) {
+      nb << (*i).substitute(nodesBegin, nodesEnd,
+                            replacementsBegin, replacementsEnd);
+    }
+    Node n = nb;
+    return n;
+  }
+}
+
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index e4fc479b7..658cb1e2d 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -171,8 +171,48 @@ private:
       return iterator(d_i++);
     }
 
-    typedef std::input_iterator_tag iterator_category;
-  };
+    iterator& operator--() {
+      --d_i;
+      return *this;
+    }
+
+    iterator operator--(int) {
+      return iterator(d_i--);
+    }
+
+    iterator& operator+=(difference_type p) {
+      d_i += p;
+      return *this;
+    }
+
+    iterator& operator-=(difference_type p) {
+      d_i -= p;
+      return *this;
+    }
+
+    iterator operator+(difference_type p) {
+      return iterator(d_i + p);
+    }
+
+    iterator operator-(difference_type p) {
+      return iterator(d_i - p);
+    }
+
+    difference_type operator-(iterator i) {
+      return d_i - i.d_i;
+    }
+
+    typedef std::random_access_iterator_tag iterator_category;
+  };/* class NodeValue::iterator<T> */
+
+  // operator+ (as a function) cannot be a template, so we have to
+  // define two versions
+  friend NodeValue::iterator<NodeTemplate<true> >
+  operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+            NodeValue::iterator<NodeTemplate<true> > i);
+  friend NodeValue::iterator<NodeTemplate<false> >
+  operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+            NodeValue::iterator<NodeTemplate<false> > i);
 
   /** Decrement ref counts of children */
   inline void decrRefCounts();
@@ -259,6 +299,26 @@ private:
 };/* class NodeValue */
 
 /**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<true> >
+operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+          NodeValue::iterator<NodeTemplate<true> > i) {
+  return i + p;
+}
+
+/**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<false> >
+operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+          NodeValue::iterator<NodeTemplate<false> > i) {
+  return i + p;
+}
+
+/**
  * For hash_maps, hash_sets, etc.. but this is for expr package
  * internal use only at present!  This is likely to be POORLY
  * PERFORMING for other uses!  NodeValue::poolHash() will lead to
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 05b69f6f4..8cf555eb0 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -111,7 +111,10 @@ Type Type::substitute(const vector<Type>& types,
     replacementsNodes.push_back(*(*i).d_typeNode);
   }
 
-  return makeType(d_typeNode->substitute(typesNodes, replacementsNodes));
+  return makeType(d_typeNode->substitute(typesNodes.begin(),
+                                         typesNodes.end(),
+                                         replacementsNodes.begin(),
+                                         replacementsNodes.end()));
 }
 
 void Type::toStream(ostream& out) const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 57ec3bf5c..19c3d27f3 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -60,6 +60,8 @@ struct CVC4_PUBLIC TypeHashStrategy {
  */
 class CVC4_PUBLIC Type {
 
+  friend class SmtEngine;
+  friend class SmtEnginePrivate;
   friend class ExprManager;
   friend class TypeNode;
   friend class TypeHashStrategy;
@@ -87,7 +89,7 @@ protected:
   Type(NodeManager* em, TypeNode* typeNode);
 
   /** Accessor for derived classes */
-  static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+  static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
 
 public:
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a55c05c5a..badc3b72f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -33,7 +33,10 @@ TypeNode TypeNode::substitute(const TypeNode& type,
     // push the operator
     nb << TypeNode(d_nv->d_children[0]);
   }
-  for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+  for(TypeNode::const_iterator i = begin(),
+        iend = end();
+      i != iend;
+      ++i) {
     if(*i == type) {
       nb << replacement;
     } else {
@@ -43,26 +46,6 @@ TypeNode TypeNode::substitute(const TypeNode& type,
   return nb.constructTypeNode();
 }
 
-TypeNode TypeNode::substitute(const vector<TypeNode>& types,
-                              const vector<TypeNode>& replacements) const {
-  vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this);
-  if(j != types.end()) {
-    return replacements[j - types.begin()];
-  } else if(getNumChildren() == 0) {
-    return *this;
-  } else {
-    NodeBuilder<> nb(getKind());
-    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
-      // push the operator
-      nb << TypeNode(d_nv->d_children[0]);
-    }
-    for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
-      nb << (*i).substitute(types, replacements);
-    }
-    return nb.constructTypeNode();
-  }
-}
-
 bool TypeNode::isBoolean() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == BOOLEAN_TYPE;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 6780b08f7..0e763128f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -118,8 +118,11 @@ public:
   /**
    * Simultaneous substitution of TypeNodes.
    */
-  TypeNode substitute(const std::vector<TypeNode>& types,
-                      const std::vector<TypeNode>& replacements) const;
+  template <class Iterator1, class Iterator2>
+  TypeNode substitute(Iterator1 typesBegin,
+                      Iterator1 typesEnd,
+                      Iterator2 replacementsBegin,
+                      Iterator2 replacementsEnd) const;
 
   /**
    * Structural comparison operator for expressions.
@@ -436,6 +439,35 @@ struct TypeNodeHashStrategy {
 
 namespace CVC4 {
 
+template <class Iterator1, class Iterator2>
+TypeNode TypeNode::substitute(Iterator1 typesBegin,
+                              Iterator1 typesEnd,
+                              Iterator2 replacementsBegin,
+                              Iterator2 replacementsEnd) const {
+  Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin,
+          "Substitution iterator ranges must be equal size" );
+  Iterator1 j = find(typesBegin, typesEnd, *this);
+  if(j != typesEnd) {
+    return *(replacementsBegin + (j - typesBegin));
+  } else if(getNumChildren() == 0) {
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << TypeNode(d_nv->d_children[0]);
+    }
+    for(TypeNode::const_iterator i = begin(),
+          iend = end();
+        i != iend;
+        ++i) {
+      nb << (*i).substitute(typesBegin, typesEnd,
+                            replacementsBegin, replacementsEnd);
+    }
+    return nb.constructTypeNode();
+  }
+}
+
 inline size_t TypeNode::getNumChildren() const {
   return d_nv->getNumChildren();
 }
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 4af882aa1..82214bed3 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -71,6 +71,7 @@ enum OptionValue {
   DEFAULT_EXPR_DEPTH,
   PRINT_EXPR_TYPES,
   UF_THEORY,
+  LAZY_DEFINITION_EXPANSION,
   INTERACTIVE,
   NO_INTERACTIVE
 };/* enum OptionValue */
@@ -119,6 +120,7 @@ static struct option cmdlineOptions[] = {
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
   { "uf"         , required_argument, NULL, UF_THEORY },
+  { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { NULL         , no_argument      , NULL, '\0'        }
@@ -272,6 +274,10 @@ throw(OptionException) {
       }
       break;
 
+    case LAZY_DEFINITION_EXPANSION:
+      opts->lazyDefinitionExpansion = true;
+      break;
+
     case INTERACTIVE:
       opts->interactive = true;
       opts->interactiveSetByUser = true;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9ad8c3177..a2792eaac 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -131,7 +131,7 @@ command returns [CVC4::Command* cmd]
   Type t;
   std::vector<Expr> terms;
   std::vector<Type> sorts;
-  std::vector<std::pair<std::string, Type> > sortedVars;
+  std::vector<std::pair<std::string, Type> > sortedVarNames;
   SExpr sexpr;
 }
   : /* set the logic */
@@ -202,15 +202,15 @@ command returns [CVC4::Command* cmd]
       $cmd = new DeclarationCommand(name,t); }
   | /* function definition */
     DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-    LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK
+    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     sortSymbol[t]
     { /* add variables to parser state before parsing term */
       Debug("parser") << "define fun: '" << name << "'" << std::endl;
-      if( sortedVars.size() > 0 ) {
+      if( sortedVarNames.size() > 0 ) {
         std::vector<CVC4::Type> sorts;
-        sorts.reserve(sortedVars.size());
+        sorts.reserve(sortedVarNames.size());
         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
-              sortedVars.begin(), iend = sortedVars.end();
+              sortedVarNames.begin(), iend = sortedVarNames.end();
             i != iend;
             ++i) {
           sorts.push_back((*i).second);
@@ -219,10 +219,10 @@ command returns [CVC4::Command* cmd]
       }
       PARSER_STATE->pushScope();
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
-            sortedVars.begin(), iend = sortedVars.end();
+            sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        PARSER_STATE->mkVar((*i).first, (*i).second);
+        terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
       }
     }
     term[expr]
@@ -230,8 +230,8 @@ command returns [CVC4::Command* cmd]
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
-      PARSER_STATE->mkFunction(name, t);
-      $cmd = new DefineFunctionCommand(name, sortedVars, t, expr);
+      Expr func = PARSER_STATE->mkFunction(name, t);
+      $cmd = new DefineFunctionCommand(func, terms, expr);
     }
   | /* value query */
     GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 192915152..319b25576 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -9,4 +9,5 @@ libsmt_la_SOURCES = \
 	smt_engine.cpp \
 	smt_engine.h \
 	noninteractive_exception.h \
-	bad_option.h
+	bad_option_exception.h \
+	no_such_function_exception.h
diff --git a/src/smt/bad_option.h b/src/smt/bad_option_exception.h
index 800d8e68a..13e5d96d0 100644
--- a/src/smt/bad_option.h
+++ b/src/smt/bad_option_exception.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file bad_option.h
+/*! \file bad_option_exception.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -21,28 +21,28 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SMT__BAD_OPTION_H
-#define __CVC4__SMT__BAD_OPTION_H
+#ifndef __CVC4__SMT__BAD_OPTION_EXCEPTION_H
+#define __CVC4__SMT__BAD_OPTION_EXCEPTION_H
 
 #include "util/exception.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC BadOption : public CVC4::Exception {
+class CVC4_PUBLIC BadOptionException : public CVC4::Exception {
 public:
-  BadOption() :
+  BadOptionException() :
     Exception("Unrecognized informational or option key or setting") {
   }
 
-  BadOption(const std::string& msg) :
+  BadOptionException(const std::string& msg) :
     Exception(msg) {
   }
 
-  BadOption(const char* msg) :
+  BadOptionException(const char* msg) :
     Exception(msg) {
   }
-};/* class BadOption */
+};/* class BadOptionException */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SMT__BAD_OPTION_H */
+#endif /* __CVC4__SMT__BAD_OPTION_EXCEPTION_H */
diff --git a/src/smt/no_such_function_exception.h b/src/smt/no_such_function_exception.h
new file mode 100644
index 000000000..0a5f2889c
--- /dev/null
+++ b/src/smt/no_such_function_exception.h
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file no_such_function_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 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__NO_SUCH_FUNCTION_EXCEPTION_H
+#define __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC NoSuchFunctionException : public CVC4::Exception {
+public:
+  NoSuchFunctionException(Expr name) :
+    Exception(std::string("Undefined function: `") + name.toString() + "': ") {
+  }
+
+  NoSuchFunctionException(Expr name, const std::string& msg) :
+    Exception(std::string("Undefined function: `") + name.toString() + "': " + msg) {
+  }
+};/* class NoSuchFunctionException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index be4abb8ab..c41737028 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -16,10 +16,16 @@
  ** The main entry point into the CVC4 library's SMT interface.
  **/
 
+#include <vector>
+#include <string>
+
 #include "smt/smt_engine.h"
 #include "smt/noninteractive_exception.h"
+#include "smt/bad_option_exception.h"
+#include "smt/no_such_function_exception.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "expr/expr.h"
 #include "expr/command.h"
 #include "expr/node_builder.h"
 #include "util/output.h"
@@ -28,6 +34,7 @@
 #include "prop/prop_engine.h"
 #include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
 using namespace CVC4::prop;
@@ -38,6 +45,28 @@ namespace CVC4 {
 namespace smt {
 
 /**
+ * Representation of a defined function.  We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction {
+  Node d_func;
+  std::vector<Node> d_formals;
+  Node d_formula;
+public:
+  DefinedFunction() {}
+  DefinedFunction(Node func, vector<Node> formals, Node formula) :
+    d_func(func),
+    d_formals(formals),
+    d_formula(formula) {
+  }
+  Node getFunction() const { return d_func; }
+  vector<Node> getFormals() const { return d_formals; }
+  Node getFormula() const { return d_formula; }
+};/* class DefinedFunction */
+
+/**
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
  * the SmtEngine class, so that smt_engine.h doesn't
@@ -60,19 +89,27 @@ public:
    * passes over the Node.  TODO: may need to specify a LEVEL of
    * preprocessing (certain contexts need more/less ?).
    */
-  static Node preprocess(SmtEngine& smt, TNode n);
+  static Node preprocess(SmtEngine& smt, TNode n)
+    throw(NoSuchFunctionException, AssertionException);
 
   /**
    * Adds a formula to the current context.
    */
-  static void addFormula(SmtEngine& smt, TNode n);
+  static void addFormula(SmtEngine& smt, TNode n)
+    throw(NoSuchFunctionException, AssertionException);
+
+  /**
+   * Expand definitions in n.
+   */
+  static Node expandDefinitions(SmtEngine& smt, TNode n)
+    throw(NoSuchFunctionException, AssertionException);
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
 
-using ::CVC4::smt::SmtEnginePrivate;
+using namespace CVC4::smt;
 
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_context(em->getContext()),
   d_exprManager(em),
   d_nodeManager(em->getNodeManager()),
@@ -94,7 +131,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
                                 d_theoryEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
 
-  d_functions = new(true) FunctionMap(d_context);
+  d_definedFunctions = new(true) DefinedFunctionMap(d_context);
 
   if(d_options->interactive) {
     d_assertionList = new(true) AssertionList(d_context);
@@ -116,46 +153,125 @@ SmtEngine::~SmtEngine() {
     d_assertionList->deleteSelf();
   }
 
-  d_functions->deleteSelf();
+  d_definedFunctions->deleteSelf();
 
   delete d_theoryEngine;
   delete d_propEngine;
   delete d_decisionEngine;
 }
 
-void SmtEngine::doCommand(Command* c) {
-  NodeManagerScope nms(d_nodeManager);
-  c->invoke(this);
-}
-
-void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) {
+void SmtEngine::setInfo(const string& key, const SExpr& value)
+  throw(BadOptionException) {
+  if(key == ":status") {
+    return;
+  }
   // FIXME implement me
+  throw BadOptionException();
 }
 
-const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) {
+const SExpr& SmtEngine::getInfo(const string& key) const
+  throw(BadOptionException) {
   // FIXME implement me
-  throw BadOption();
+  throw BadOptionException();
 }
 
-void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) {
+void SmtEngine::setOption(const string& key, const SExpr& value)
+  throw(BadOptionException) {
   // FIXME implement me
+  throw BadOptionException();
 }
 
-const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) {
+const SExpr& SmtEngine::getOption(const string& key) const
+  throw(BadOptionException) {
   // FIXME implement me
-  throw BadOption();
+  throw BadOptionException();
 }
 
-void SmtEngine::defineFunction(const string& name,
-                               const vector<pair<string, Type> >& args,
-                               Type type,
+void SmtEngine::defineFunction(Expr func,
+                               const vector<Expr>& formals,
                                Expr formula) {
   NodeManagerScope nms(d_nodeManager);
-  d_functions->insert(name, make_pair(make_pair(args, type), formula));
+  TNode funcNode = func.getTNode();
+  vector<Node> formalsNodes;
+  for(vector<Expr>::const_iterator i = formals.begin(),
+        iend = formals.end();
+      i != iend;
+      ++i) {
+    formalsNodes.push_back((*i).getNode());
+  }
+  TNode formulaNode = formula.getTNode();
+  DefinedFunction def(funcNode, formalsNodes, formulaNode);
+  d_definedFunctions->insert(funcNode, def);
 }
 
-Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) {
-  return smt.d_theoryEngine->preprocess(n);
+Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n)
+  throw(NoSuchFunctionException, AssertionException) {
+  if(n.getKind() == kind::APPLY) {
+    TNode func = n.getOperator();
+    SmtEngine::DefinedFunctionMap::const_iterator i =
+      smt.d_definedFunctions->find(func);
+    DefinedFunction def = (*i).second;
+    vector<Node> formals = def.getFormals();
+
+    if(Debug.isOn("expand")) {
+      Debug("expand") << "found: " << n << endl;
+      Debug("expand") << " func: " << func << endl;
+      string name = func.getAttribute(expr::VarNameAttr());
+      Debug("expand") << "     : \"" << name << "\"" << endl;
+      if(i == smt.d_definedFunctions->end()) {
+        throw NoSuchFunctionException(Expr(smt.d_exprManager, new Node(func)));
+      }
+      Debug("expand") << " defn: " << def.getFunction() << endl
+                      << "       [";
+      if(formals.size() > 0) {
+        copy( formals.begin(), formals.end() - 1,
+              ostream_iterator<Node>(Debug("expand"), ", ") );
+        Debug("expand") << formals.back();
+      }
+      Debug("expand") << "]" << endl
+                      << "       " << def.getFunction().getType() << endl
+                      << "       " << def.getFormula() << endl;
+    }
+
+    TNode fm = def.getFormula();
+    Node instance = fm.substitute(formals.begin(), formals.end(),
+                                  n.begin(), n.end());
+    Debug("expand") << "made : " << instance << endl;
+
+    Node expanded = expandDefinitions(smt, instance);
+    return expanded;
+  } else if(n.getNumChildren() == 0) {
+    return n;
+  } else {
+    Debug("expand") << "cons : " << n << endl;
+    NodeBuilder<> nb(n.getKind());
+    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      Debug("expand") << "op   : " << n.getOperator() << endl;
+      nb << n.getOperator();
+    }
+    for(TNode::iterator i = n.begin(),
+          iend = n.end();
+        i != iend;
+        ++i) {
+      Node expanded = expandDefinitions(smt, *i);
+      Debug("expand") << "exchld: " << expanded << endl;
+      nb << expanded;
+    }
+    Node node = nb;
+    return node;
+  }
+}
+
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n)
+  throw(NoSuchFunctionException, AssertionException) {
+  if(!smt.d_options->lazyDefinitionExpansion) {
+    Node node = expandDefinitions(smt, n);
+    Debug("expand") << "have: " << n << endl
+                    << "made: " << node << endl;
+    return smt.d_theoryEngine->preprocess(node);
+  } else {
+    return smt.d_theoryEngine->preprocess(n);
+  }
 }
 
 Result SmtEngine::check() {
@@ -168,7 +284,8 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
-void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) {
+void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
+  throw(NoSuchFunctionException, AssertionException) {
   Debug("smt") << "push_back assertion " << n << endl;
   smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
 }
@@ -209,8 +326,16 @@ Model SmtEngine::getModel() {
   Unimplemented();
 }
 
-Expr SmtEngine::getValue(Expr term) {
+Expr SmtEngine::getValue(Expr term)
+  throw(NoninteractiveException, AssertionException) {
+  if(!d_options->interactive) {
+    const char* msg =
+      "Cannot query the current assertion list when not in interactive mode.";
+    throw NoninteractiveException(msg);
+  }
+
   NodeManagerScope nms(d_nodeManager);
+
   Unimplemented();
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 97772273d..c9bf321b9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -31,7 +31,8 @@
 #include "util/sexpr.h"
 #include "util/hash.h"
 #include "smt/noninteractive_exception.h"
-#include "smt/bad_option.h"
+#include "smt/no_such_function_exception.h"
+#include "smt/bad_option_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -39,21 +40,33 @@
 
 namespace CVC4 {
 
-namespace context {
-  class Context;
-  template <class T> class CDList;
-}/* CVC4::context namespace */
-
+template <bool ref_count> class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> TNode;
+class NodeHashFunction;
 class Command;
 class Options;
 class TheoryEngine;
 class DecisionEngine;
 
+namespace context {
+  class Context;
+  template <class T> class CDList;
+}/* CVC4::context namespace */
+
 namespace prop {
   class PropEngine;
 }/* CVC4::prop namespace */
 
 namespace smt {
+  /**
+   * Representation of a defined function.  We keep these around in
+   * SmtEngine to permit expanding definitions late (and lazily), to
+   * support getValue() over defined functions, to support user output
+   * in terms of defined functions, etc.
+   */
+  class DefinedFunction;
+
   class SmtEnginePrivate;
 }/* CVC4::smt namespace */
 
@@ -69,17 +82,10 @@ namespace smt {
 // The CNF conversion can go on in PropEngine.
 
 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;
-
+  typedef context::CDMap<Node, smt::DefinedFunction, NodeHashFunction>
+    DefinedFunctionMap;
   /** The type of our internal assertion list */
   typedef context::CDList<Expr> AssertionList;
 
@@ -98,7 +104,7 @@ private:
   /** The propositional engine */
   prop::PropEngine* d_propEngine;
   /** An index of our defined functions */
-  FunctionMap* d_functions;
+  DefinedFunctionMap* d_definedFunctions;
   /**
    * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in interactive mode.
@@ -141,29 +147,28 @@ public:
   ~SmtEngine();
 
   /**
-   * Execute a command.
-   */
-  void doCommand(Command*);
-
-  /**
    * Set information about the script executing.
    */
-  void setInfo(const std::string& key, const SExpr& value) throw(BadOption);
+  void setInfo(const std::string& key, const SExpr& value)
+    throw(BadOptionException);
 
   /**
    * Query information about the SMT environment.
    */
-  const SExpr& getInfo(const std::string& key) const throw(BadOption);
+  const SExpr& getInfo(const std::string& key) const
+    throw(BadOptionException);
 
   /**
    * Set an aspect of the current SMT execution environment.
    */
-  void setOption(const std::string& key, const SExpr& value) throw(BadOption);
+  void setOption(const std::string& key, const SExpr& value)
+    throw(BadOptionException);
 
   /**
    * Get an aspect of the current SMT execution environment.
    */
-  const SExpr& getOption(const std::string& key) const throw(BadOption);
+  const SExpr& getOption(const std::string& key) const
+    throw(BadOptionException);
 
   /**
    * Add a formula to the current context: preprocess, do per-theory
@@ -171,9 +176,8 @@ public:
    * 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,
+  void defineFunction(Expr func,
+                      const std::vector<Expr>& formals,
                       Expr formula);
 
   /**
@@ -209,12 +213,14 @@ public:
 
   /**
    * Get the assigned value of a term (only if preceded by a SAT or
-   * INVALID query).
+   * INVALID query).  Only permitted if the SmtEngine is set to
+   * operate interactively.
    */
-  Expr getValue(Expr term);
+  Expr getValue(Expr term) throw(NoninteractiveException, AssertionException);
 
   /**
-   * Get the current set of assertions.
+   * Get the current set of assertions.  Only permitted if the
+   * SmtEngine is set to operate interactively.
    */
   std::vector<Expr> getAssertions() throw(NoninteractiveException);
 
diff --git a/src/util/options.h b/src/util/options.h
index c504177bf..9bb0b0a38 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -65,6 +65,9 @@ struct CVC4_PUBLIC Options {
   /** Should we strictly enforce the language standard while parsing? */
   bool strictParsing;
 
+  /** Should we expand function definitions lazily? */
+  bool lazyDefinitionExpansion;
+
   /** Whether we're in interactive mode or not */
   bool interactive;
 
@@ -86,6 +89,7 @@ struct CVC4_PUBLIC Options {
     semanticChecks(true),
     memoryMap(false),
     strictParsing(false),
+    lazyDefinitionExpansion(false),
     interactive(false),
     interactiveSetByUser(false) {
   }