parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

32 files changed, 1162 insertions, 458 deletions

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 7e382697c..02418d3df 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__CONTEXT__CDLIST_H
 #define __CVC4__CONTEXT__CDLIST_H
 
+#include <iterator>
+
 #include "context/context.h"
 #include "util/Assert.h"
 
@@ -224,6 +226,12 @@ public:
 
   public:
 
+    typedef std::input_iterator_tag iterator_category;
+    typedef T value_type;
+    typedef ptrdiff_t difference_type;
+    typedef const T* pointer;
+    typedef const T& reference;
+
     const_iterator() : d_it(NULL) {}
 
     inline bool operator==(const const_iterator& i) const {
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 6c466a74c..a1486fcab 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -16,13 +16,24 @@
  ** Implementation of command objects.
  **/
 
+#include <iostream>
+#include <vector>
+#include <utility>
+#include <iterator>
+
 #include "expr/command.h"
 #include "smt/smt_engine.h"
+#include "util/output.h"
 
 using namespace std;
 
 namespace CVC4 {
 
+std::ostream& operator<<(std::ostream& out, const Command& c) {
+  c.toStream(out);
+  return out;
+}
+
 ostream& operator<<(ostream& out, const Command* command) {
   if(command == NULL) {
     out << "null";
@@ -32,12 +43,136 @@ ostream& operator<<(ostream& out, const Command* command) {
   return out;
 }
 
+/* class Command */
+
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
+  invoke(smtEngine);
+  printResult(out);
+}
+
+std::string Command::toString() const {
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+void Command::printResult(std::ostream& out) const {
+}
+
+/* class EmptyCommand */
+
+EmptyCommand::EmptyCommand(std::string name) :
+  d_name(name) {
+}
+
+void EmptyCommand::invoke(SmtEngine* smtEngine) {
+  /* empty commands have no implementation */
+}
+
+void EmptyCommand::toStream(std::ostream& out) const {
+  out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+AssertCommand::AssertCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+void AssertCommand::invoke(SmtEngine* smtEngine) {
+  smtEngine->assertFormula(d_expr);
+}
+
+void AssertCommand::toStream(std::ostream& out) const {
+  out << "Assert(" << d_expr << ")";
+}
+
+/* class PushCommand */
+
+void PushCommand::invoke(SmtEngine* smtEngine) {
+  smtEngine->push();
+}
+
+void PushCommand::toStream(std::ostream& out) const {
+  out << "Push()";
+}
+
+/* class PopCommand */
+
+void PopCommand::invoke(SmtEngine* smtEngine) {
+  smtEngine->pop();
+}
+
+void PopCommand::toStream(std::ostream& out) const {
+  out << "Pop()";
+}
+
+/* class CheckSatCommand */
+
+CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
+  d_expr(expr) {
+}
+
+void CheckSatCommand::invoke(SmtEngine* smtEngine) {
+  d_result = smtEngine->checkSat(d_expr);
+}
+
+void CheckSatCommand::toStream(std::ostream& out) const {
+  if(d_expr.isNull()) {
+    out << "CheckSat()";
+  } else {
+    out << "CheckSat(" << d_expr << ")";
+  }
+}
+
+Result CheckSatCommand::getResult() const {
+  return d_result;
+}
+
+void CheckSatCommand::printResult(std::ostream& out) const {
+  out << d_result << endl;
+}
+
+/* class QueryCommand */
+
+QueryCommand::QueryCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+void QueryCommand::invoke(SmtEngine* smtEngine) {
+  d_result = smtEngine->query(d_expr);
+}
+
+Result QueryCommand::getResult() const {
+  return d_result;
+}
+
+void QueryCommand::printResult(std::ostream& out) const {
+  out << d_result << endl;
+}
+
+void QueryCommand::toStream(std::ostream& out) const {
+  out << "Query(";
+  d_expr.printAst(out, 0);
+  out << ")";
+}
+
+/* class CommandSequence */
+
+CommandSequence::CommandSequence() :
+  d_index(0) {
+}
+
 CommandSequence::~CommandSequence() {
   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
     delete d_commandSequence[i];
   }
 }
 
+void CommandSequence::addCommand(Command* cmd) {
+  d_commandSequence.push_back(cmd);
+}
+
 void CommandSequence::invoke(SmtEngine* smtEngine) {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine);
@@ -45,11 +180,10 @@ void CommandSequence::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void CheckSatCommand::toStream(std::ostream& out) const {
-  if(d_expr.isNull()) {
-    out << "CheckSat()";
-  } else {
-    out << "CheckSat(" << d_expr << ")";
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
+  for(; d_index < d_commandSequence.size(); ++d_index) {
+    d_commandSequence[d_index]->invoke(smtEngine, out);
+    delete d_commandSequence[d_index];
   }
 }
 
@@ -61,33 +195,257 @@ void CommandSequence::toStream(std::ostream& out) const {
   out << "]";
 }
 
+/* class DeclarationCommand */
+
+DeclarationCommand::DeclarationCommand(const std::string& id, Type t) :
+  d_type(t) {
+  d_declaredSymbols.push_back(id);
+}
+
+DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type t) :
+  d_declaredSymbols(ids),
+  d_type(t) {
+}
+
 void DeclarationCommand::toStream(std::ostream& out) const {
-  out << "Declare(";
-  bool first = true;
-  for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
-    if(!first) {
-      out << ", ";
-    }
-    out << d_declaredSymbols[i];
-    first = false;
+  out << "Declare([";
+  copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1,
+        ostream_iterator<string>(out, ", ") );
+  out << d_declaredSymbols.back();
+  out << "])";
+}
+
+/* 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),
+  d_formula(formula) {
+}
+
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
+  smtEngine->defineFunction(d_name, d_args, d_type, 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 << " >> )";
+}
+
+/* class GetValueCommand */
+
+GetValueCommand::GetValueCommand(Expr term) :
+  d_term(term) {
+}
+
+void GetValueCommand::invoke(SmtEngine* smtEngine) {
+  d_result = smtEngine->getValue(d_term);
+}
+
+Expr GetValueCommand::getResult() const {
+  return d_result;
+}
+
+void GetValueCommand::printResult(std::ostream& out) const {
+  out << d_result << endl;
+}
+
+void GetValueCommand::toStream(std::ostream& out) const {
+  out << "GetValue( << " << d_term << " >> )";
+}
+
+/* class GetAssertionsCommand */
+
+GetAssertionsCommand::GetAssertionsCommand() {
+}
+
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
+  stringstream ss;
+  const vector<Expr> v = smtEngine->getAssertions();
+  copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+  d_result = ss.str();
+}
+
+std::string GetAssertionsCommand::getResult() const {
+  return d_result;
+}
+
+void GetAssertionsCommand::printResult(std::ostream& out) const {
+  out << d_result;
+}
+
+void GetAssertionsCommand::toStream(std::ostream& out) const {
+  out << "GetAssertions()";
+}
+
+/* class SetBenchmarkStatusCommand */
+
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+  d_status(status) {
+}
+
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
+  // FIXME: TODO: something to be done with the status
+}
+
+void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
+  d_logic(logic) {
+}
+
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
+  // FIXME: TODO: something to be done with the logic
+}
+
+void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* class SetInfoCommand */
+
+SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
+  d_flag(flag),
+  d_sexpr(sexpr) {
+}
+
+void SetInfoCommand::invoke(SmtEngine* smtEngine) {
+  try {
+    smtEngine->setInfo(d_flag, d_sexpr);
+    //d_result = "success";
+  } catch(BadOption& bo) {
+    d_result = "unsupported";
   }
-  out << ")";
 }
 
-void PushCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->push();
+std::string SetInfoCommand::getResult() const {
+  return d_result;
 }
 
-void PushCommand::toStream(std::ostream& out) const {
-  out << "Push()";
+void SetInfoCommand::printResult(std::ostream& out) const {
+  if(d_result != "") {
+    out << d_result << endl;
+  }
 }
 
-void PopCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->pop();
+void SetInfoCommand::toStream(std::ostream& out) const {
+  out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
 }
 
-void PopCommand::toStream(std::ostream& out) const {
-  out << "Pop()";
+/* class GetInfoCommand */
+
+GetInfoCommand::GetInfoCommand(std::string flag) :
+  d_flag(flag) {
+}
+
+void GetInfoCommand::invoke(SmtEngine* smtEngine) {
+  try {
+    d_result = smtEngine->getInfo(d_flag).getValue();
+  } catch(BadOption& bo) {
+    d_result = "unsupported";
+  }
+}
+
+std::string GetInfoCommand::getResult() const {
+  return d_result;
+}
+
+void GetInfoCommand::printResult(std::ostream& out) const {
+  if(d_result != "") {
+    out << d_result << endl;
+  }
+}
+
+void GetInfoCommand::toStream(std::ostream& out) const {
+  out << "GetInfo(" << d_flag << ")";
+}
+
+/* class SetOptionCommand */
+
+SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
+  d_flag(flag),
+  d_sexpr(sexpr) {
+}
+
+void SetOptionCommand::invoke(SmtEngine* smtEngine) {
+  try {
+    smtEngine->setOption(d_flag, d_sexpr);
+    //d_result = "success";
+  } catch(BadOption& bo) {
+    d_result = "unsupported";
+  }
+}
+
+std::string SetOptionCommand::getResult() const {
+  return d_result;
+}
+
+void SetOptionCommand::printResult(std::ostream& out) const {
+  if(d_result != "") {
+    out << d_result << endl;
+  }
+}
+
+void SetOptionCommand::toStream(std::ostream& out) const {
+  out << "SetOption(" << d_flag << ", " << d_sexpr << ")";
+}
+
+/* class GetOptionCommand */
+
+GetOptionCommand::GetOptionCommand(std::string flag) :
+  d_flag(flag) {
+}
+
+void GetOptionCommand::invoke(SmtEngine* smtEngine) {
+  try {
+    d_result = smtEngine->getOption(d_flag).getValue();
+  } catch(BadOption& bo) {
+    d_result = "unsupported";
+  }
+}
+
+std::string GetOptionCommand::getResult() const {
+  return d_result;
+}
+
+void GetOptionCommand::printResult(std::ostream& out) const {
+  if(d_result != "") {
+    out << d_result << endl;
+  }
+}
+
+void GetOptionCommand::toStream(std::ostream& out) const {
+  out << "GetOption(" << d_flag << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+std::ostream& operator<<(std::ostream& out,
+                         BenchmarkStatus status) {
+  switch(status) {
+
+  case SMT_SATISFIABLE:
+    return out << "sat";
+
+  case SMT_UNSATISFIABLE:
+    return out << "unsat";
+
+  case SMT_UNKNOWN:
+    return out << "unknown";
+
+  default:
+    return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+  }
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/command.h b/src/expr/command.h
index 388ad62e6..0c78dd1c6 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -39,7 +39,7 @@ namespace CVC4 {
 class SmtEngine;
 class Command;
 
-inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
 
 /** The status an SMT benchmark can have */
@@ -52,115 +52,203 @@ enum BenchmarkStatus {
   SMT_UNKNOWN
 };
 
-inline std::ostream& operator<<(std::ostream& out,
-                                BenchmarkStatus status)
-  CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+                         BenchmarkStatus status) CVC4_PUBLIC;
 
 class CVC4_PUBLIC Command {
 public:
-  virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+  virtual void invoke(SmtEngine* smtEngine) = 0;
+  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
   virtual ~Command() {};
   virtual void toStream(std::ostream&) const = 0;
   std::string toString() const;
+  virtual void printResult(std::ostream& out) const;
 };/* class Command */
 
+/**
+ * EmptyCommands (and its subclasses) are the residue of a command
+ * after the parser handles them (and there's nothing left to do).
+ */
 class CVC4_PUBLIC EmptyCommand : public Command {
+protected:
+  std::string d_name;
 public:
   EmptyCommand(std::string name = "");
-  void invoke(CVC4::SmtEngine* smtEngine);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
-private:
-  std::string d_name;
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
+protected:
+  BoolExpr d_expr;
 public:
   AssertCommand(const BoolExpr& e);
-  void invoke(CVC4::SmtEngine* smtEngine);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
-protected:
-  BoolExpr d_expr;
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
-  void invoke(CVC4::SmtEngine* smtEngine);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
-  void invoke(CVC4::SmtEngine* smtEngine);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
 };/* class PopCommand */
 
-
 class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
-public:
-  DeclarationCommand(const std::string& id, const Type& t);
-  DeclarationCommand(const std::vector<std::string>& ids, const Type& t);
-  void toStream(std::ostream& out) const;
 protected:
   std::vector<std::string> d_declaredSymbols;
   Type d_type;
-};
+public:
+  DeclarationCommand(const std::string& id, Type t);
+  DeclarationCommand(const std::vector<std::string>& ids, Type t);
+  void toStream(std::ostream& out) const;
+};/* class DeclarationCommand */
 
-class CVC4_PUBLIC CheckSatCommand : public Command {
+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_formula;
 public:
-  CheckSatCommand(const BoolExpr& expr);
-  void invoke(SmtEngine* smt);
-  Result getResult();
+  DefineFunctionCommand(const std::string& name,
+                        const std::vector<std::pair<std::string, Type> >& args,
+                        Type type, Expr formula);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
+};/* class DefineFunctionCommand */
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
 protected:
   BoolExpr d_expr;
   Result d_result;
+public:
+  CheckSatCommand(const BoolExpr& expr);
+  void invoke(SmtEngine* smtEngine);
+  Result getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
-public:
-  QueryCommand(const BoolExpr& e);
-  void invoke(SmtEngine* smt);
-  Result getResult();
-  void toStream(std::ostream& out) const;
 protected:
   BoolExpr d_expr;
   Result d_result;
+public:
+  QueryCommand(const BoolExpr& e);
+  void invoke(SmtEngine* smtEngine);
+  Result getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
 };/* class QueryCommand */
 
-class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+class CVC4_PUBLIC GetValueCommand : public Command {
+protected:
+  Expr d_term;
+  Expr d_result;
 public:
-  SetBenchmarkStatusCommand(BenchmarkStatus status);
-  void invoke(SmtEngine* smt);
+  GetValueCommand(Expr term);
+  void invoke(SmtEngine* smtEngine);
+  Expr getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
+};/* class GetValueCommand */
+
+class CVC4_PUBLIC GetAssertionsCommand : public Command {
+protected:
+  std::string d_result;
+public:
+  GetAssertionsCommand();
+  void invoke(SmtEngine* smtEngine);
+  std::string getResult() const;
+  void printResult(std::ostream& out) const;
   void toStream(std::ostream& out) const;
+};/* class GetAssertionsCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 protected:
   BenchmarkStatus d_status;
+public:
+  SetBenchmarkStatusCommand(BenchmarkStatus status);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
 };/* class SetBenchmarkStatusCommand */
 
-
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+protected:
+  std::string d_logic;
 public:
   SetBenchmarkLogicCommand(std::string logic);
-  void invoke(SmtEngine* smt);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
-protected:
-  std::string d_logic;
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
+protected:
+  std::string d_flag;
+  SExpr d_sexpr;
+  std::string d_result;
 public:
   SetInfoCommand(std::string flag, SExpr& sexpr);
-  void invoke(SmtEngine* smt);
+  void invoke(SmtEngine* smtEngine);
   void toStream(std::ostream& out) const;
+  std::string getResult() const;
+  void printResult(std::ostream& out) const;
+};/* class SetInfoCommand */
+
+class CVC4_PUBLIC GetInfoCommand : public Command {
+protected:
+  std::string d_flag;
+  std::string d_result;
+public:
+  GetInfoCommand(std::string flag);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+  std::string getResult() const;
+  void printResult(std::ostream& out) const;
+};/* class GetInfoCommand */
+
+class CVC4_PUBLIC SetOptionCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-};/* class SetInfoCommand */
+  std::string d_result;
+public:
+  SetOptionCommand(std::string flag, SExpr& sexpr);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+  std::string getResult() const;
+  void printResult(std::ostream& out) const;
+};/* class SetOptionCommand */
+
+class CVC4_PUBLIC GetOptionCommand : public Command {
+protected:
+  std::string d_flag;
+  std::string d_result;
+public:
+  GetOptionCommand(std::string flag);
+  void invoke(SmtEngine* smtEngine);
+  void toStream(std::ostream& out) const;
+  std::string getResult() const;
+  void printResult(std::ostream& out) const;
+};/* class GetOptionCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
+private:
+  /** All the commands to be executed (in sequence) */
+  std::vector<Command*> d_commandSequence;
+  /** Next command to be executed */
+  unsigned int d_index;
 public:
   CommandSequence();
   ~CommandSequence();
-  void invoke(SmtEngine* smt);
+  void invoke(SmtEngine* smtEngine);
+  void invoke(SmtEngine* smtEngine, std::ostream& out);
   void addCommand(Command* cmd);
   void toStream(std::ostream& out) const;
 
@@ -172,178 +260,8 @@ public:
 
   iterator begin() { return d_commandSequence.begin(); }
   iterator end() { return d_commandSequence.end(); }
-
-private:
-  /** All the commands to be executed (in sequence) */
-  std::vector<Command*> d_commandSequence;
-  /** Next command to be executed */
-  unsigned int d_index;
 };/* class CommandSequence */
 
 }/* CVC4 namespace */
 
-/* =========== inline function definitions =========== */
-
-#include "smt/smt_engine.h"
-
-namespace CVC4 {
-
-inline std::ostream& operator<<(std::ostream& out, const Command& c) {
-  c.toStream(out);
-  return out;
-}
-
-/* class Command */
-
-inline std::string Command::toString() const {
-  std::stringstream ss;
-  toStream(ss);
-  return ss.str();
-}
-
-/* class EmptyCommand */
-
-inline EmptyCommand::EmptyCommand(std::string name) :
-  d_name(name) {
-}
-
-inline void EmptyCommand::invoke(SmtEngine* smtEngine) {
-}
-
-inline void EmptyCommand::toStream(std::ostream& out) const {
-  out << "EmptyCommand(" << d_name << ")";
-}
-
-/* class AssertCommand */
-
-inline AssertCommand::AssertCommand(const BoolExpr& e) :
-  d_expr(e) {
-}
-
-inline void AssertCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->assertFormula(d_expr);
-}
-
-inline void AssertCommand::toStream(std::ostream& out) const {
-  out << "Assert(" << d_expr << ")";
-}
-
-/* class CheckSatCommand */
-
-inline CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
-  d_expr(expr) {
-}
-
-inline void CheckSatCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->checkSat(d_expr);
-}
-
-inline Result CheckSatCommand::getResult() {
-  return d_result;
-}
-
-/* class QueryCommand */
-
-inline QueryCommand::QueryCommand(const BoolExpr& e) :
-  d_expr(e) {
-}
-
-inline void QueryCommand::invoke(CVC4::SmtEngine* smtEngine) {
-  d_result = smtEngine->query(d_expr);
-}
-
-inline Result QueryCommand::getResult() {
-  return d_result;
-}
-
-inline void QueryCommand::toStream(std::ostream& out) const {
-  out << "Query(";
-  d_expr.printAst(out, 0);
-  out << ")";
-}
-
-/* class CommandSequence */
-
-inline CommandSequence::CommandSequence() :
-  d_index(0) {
-}
-
-inline void CommandSequence::addCommand(Command* cmd) {
-  d_commandSequence.push_back(cmd);
-}
-
-/* class DeclarationCommand */
-
-inline DeclarationCommand::DeclarationCommand(const std::string& id, const Type& t) :
-  d_type(t)
-{
-  d_declaredSymbols.push_back(id);
-}
-
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) :
-  d_declaredSymbols(ids),
-  d_type(t)
-{
-}
-
-/* class SetBenchmarkStatusCommand */
-
-inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
-  d_status(status) {
-}
-
-inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
-  // FIXME: TODO: something to be done with the status
-}
-
-inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkStatus(" << d_status << ")";
-}
-
-/* class SetBenchmarkLogicCommand */
-
-inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
-  d_logic(logic) {
-}
-
-inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
-  // FIXME: TODO: something to be done with the logic
-}
-
-inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
-inline SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
-  d_flag(flag),
-  d_sexpr(sexpr) {
-}
-
-inline void SetInfoCommand::invoke(SmtEngine* smt) { }
-
-inline void SetInfoCommand::toStream(std::ostream& out) const {
-  out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
-}
-
-/* output stream insertion operator for benchmark statuses */
-inline std::ostream& operator<<(std::ostream& out,
-                                BenchmarkStatus status) {
-  switch(status) {
-
-  case SMT_SATISFIABLE:
-    return out << "sat";
-
-  case SMT_UNSATISFIABLE:
-    return out << "unsat";
-
-  case SMT_UNKNOWN:
-    return out << "unknown";
-
-  default:
-    return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
-  }
-}
-
-}/* CVC4 namespace */
-
 #endif /* __CVC4__COMMAND_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index da209c581..56b89c125 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -268,9 +268,9 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
 }
 
-SortType ExprManager::mkSort(const std::string& name) const {
+SortType ExprManager::mkSort(const std::string& name, size_t arity) const {
   NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, arity)));
 }
 
 /**
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8e02c8ca4..316a9b7b1 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -224,11 +224,11 @@ public:
   /** Make the type of arrays with the given parameterization */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
-  /** Make a new sort with the given name. */
-  SortType mkSort(const std::string& name) const;
+  /** Make a new sort with the given name and arity. */
+  SortType mkSort(const std::string& name, size_t arity = 0) const;
 
   /** Get the type of an expression */
-  Type getType(const Expr& e, bool check = false) 
+  Type getType(const Expr& e, bool check = false)
     throw (TypeCheckingException);
 
   // variables are special, because duplicates are permitted
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 54e20667f..83d5dc47f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -42,6 +42,10 @@ const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
+std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
+  return out << e.getMessage() << ": " << e.getExpression();
+}
+
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
   e.toStream(out);
   return out;
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 349795156..fee8e70db 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -83,7 +83,10 @@ public:
   std::string toString() const;
 
   friend class ExprManager;
-};
+};/* class TypeCheckingException */
+
+std::ostream& operator<<(std::ostream& out,
+                         const TypeCheckingException& e) CVC4_PUBLIC;
 
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index ad698975f..a336662c3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -98,7 +98,7 @@ struct NodeValueConstPrinter {
  * "metakind" is an ugly name but it's not used by client code, just
  * by the expr package, and the intent here is to keep it from
  * polluting the kind namespace.  For more documentation on what these
- * mean, see src/expr/builtin_kinds.
+ * mean, see src/theory/builtin/kinds.
  */
 enum MetaKind_t {
   INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 77f00ab33..ca93473db 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -395,7 +395,7 @@ public:
    * <code>AttrKind::value_type</code> if not.
    */
   template <class AttrKind>
-  inline typename AttrKind::value_type 
+  inline typename AttrKind::value_type
   getAttribute(TNode n, const AttrKind& attr) const;
 
   /**
@@ -504,11 +504,11 @@ public:
   /** Make the type of arrays with the given parameterization */
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
-  /** Make a new sort. */
+  /** Make a new (anonymous) sort of arity 0. */
   inline TypeNode mkSort();
 
-  /** Make a new sort with the given name. */
-  inline TypeNode mkSort(const std::string& name);
+  /** Make a new sort with the given name and arity. */
+  inline TypeNode mkSort(const std::string& name, size_t arity = 0);
 
   /**
    * Get the type for the given node and optionally do type checking.
@@ -532,7 +532,7 @@ public:
    * amount of checking required to return a valid result.
    *
    * @param n the Node for which we want a type
-   * @param check whether we should check the type as we compute it 
+   * @param check whether we should check the type as we compute it
    * (default: false)
    */
   TypeNode getType(TNode n, bool check = false)
@@ -765,7 +765,8 @@ inline TypeNode NodeManager::mkSort() {
   return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
 }
 
-inline TypeNode NodeManager::mkSort(const std::string& name) {
+inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) {
+  Assert(arity == 0, "parameterized sorts not yet supported.");
   TypeNode type = mkSort();
   type.setAttribute(expr::VarNameAttr(), name);
   return type;
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 08bcbaa7c..4af882aa1 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -70,7 +70,9 @@ enum OptionValue {
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
   PRINT_EXPR_TYPES,
-  UF_THEORY
+  UF_THEORY,
+  INTERACTIVE,
+  NO_INTERACTIVE
 };/* enum OptionValue */
 
 /**
@@ -117,6 +119,8 @@ 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 },
+  { "interactive", no_argument      , NULL, INTERACTIVE },
+  { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -268,6 +272,16 @@ throw(OptionException) {
       }
       break;
 
+    case INTERACTIVE:
+      opts->interactive = true;
+      opts->interactiveSetByUser = true;
+      break;
+
+    case NO_INTERACTIVE:
+      opts->interactive = false;
+      opts->interactiveSetByUser = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/main.cpp b/src/main/main.cpp
index f0c04e5f6..4f261378d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -110,20 +110,25 @@ int runCvc4(int argc, char* argv[]) {
     throw Exception("Too many input files specified.");
   }
 
+  // If no file supplied we will read from standard input
+  const bool inputFromStdin =
+    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+
+  // if we're reading from stdin, default to interactive mode
+  if(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin;
+  }
+
   // Create the expression manager
   ExprManager exprMgr;
 
   // Create the SmtEngine
   SmtEngine smt(&exprMgr, &options);
 
-  // If no file supplied we read from standard input
-  bool inputFromStdin =
-    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
-
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
-  ReferenceStat< const char* > s_statFilename("filename",filename);
+  ReferenceStat< const char* > s_statFilename("filename", filename);
   StatisticsRegistry::registerStat(&s_statFilename);
 
   if(options.lang == parser::LANG_AUTO) {
@@ -180,6 +185,9 @@ int runCvc4(int argc, char* argv[]) {
 
   // Parse and execute commands until we are done
   Command* cmd;
+  if( options.interactive ) {
+    // cout << "CVC4> " << flush;
+  }
   while((cmd = parser->nextCommand())) {
     if( !options.parseOnly ) {
       doCommand(smt, cmd);
@@ -238,21 +246,19 @@ void doCommand(SmtEngine& smt, Command* cmd) {
       cout << "Invoking: " << *cmd << endl;
     }
 
-    cmd->invoke(&smt);
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, cout);
+    } else {
+      cmd->invoke(&smt);
+    }
 
     QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd);
     if(qc != NULL) {
       lastResult = qc->getResult();
-      if(options.verbosity >= 0) {
-        cout << lastResult << endl;
-      }
     } else {
       CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd);
       if(csc != NULL) {
         lastResult = csc->getResult();
-        if(options.verbosity >= 0) {
-          cout << lastResult << endl;
-        }
       }
     }
   }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f73e268a3..39f61c16d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -18,6 +18,7 @@
 
 #include <iostream>
 #include <fstream>
+#include <iterator>
 #include <stdint.h>
 
 #include "input.h"
@@ -79,6 +80,14 @@ Type Parser::getSort(const std::string& name) {
   return t;
 }
 
+Type Parser::getSort(const std::string& name,
+                     const std::vector<Type>& params) {
+  Assert( isDeclared(name, SYM_SORT) );
+  Type t = d_declScope.lookupType(name);
+  Warning() << "FIXME use params to realize parameterized sort\n";
+  return t;
+}
+
 /* Returns true if name is bound to a boolean variable. */
 bool Parser::isBoolean(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
@@ -94,7 +103,7 @@ bool Parser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 }
 
-Expr 
+Expr
 Parser::mkVar(const std::string& name, const Type& type) {
   Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
@@ -124,10 +133,25 @@ Parser::defineType(const std::string& name, const Type& type) {
   Assert( isDeclared(name, SYM_SORT) ) ;
 }
 
+void
+Parser::defineParameterizedType(const std::string& name,
+                                const std::vector<Type>& params,
+                                const Type& type) {
+  if(Debug.isOn("parser")) {
+    Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
+    copy(params.begin(), params.end() - 1,
+         ostream_iterator<Type>(Debug("parser"), ", ") );
+    Debug("parser") << params.back();
+    Debug("parser") << "], " << type << ")" << std::endl;
+  }
+  Warning("defineSort unimplemented\n");
+  defineType(name,type);
+}
+
 Type
-Parser::mkSort(const std::string& name) {
-  Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Type type = d_exprManager->mkSort(name);
+Parser::mkSort(const std::string& name, size_t arity) {
+  Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl;
+  Type type = d_exprManager->mkSort(name, arity);
   defineType(name,type);
   return type;
 }
@@ -234,10 +258,10 @@ Command* Parser::nextCommand() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
-    } catch(TypeCheckingException& e) {
+    } catch(Exception& e) {
       setDone();
       stringstream ss;
-      ss << e.getMessage() << ": " << e.getExpression();
+      ss << e;
       parseError( ss.str() );
     }
   }
@@ -257,10 +281,10 @@ Expr Parser::nextExpression() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
-    } catch(TypeCheckingException& e) {
+    } catch(Exception& e) {
       setDone();
       stringstream ss;
-      ss << e.getMessage() << ": " << e.getExpression();
+      ss << e;
       parseError( ss.str() );
     }
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1c02aa482..0faf9bebf 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -208,11 +208,17 @@ public:
   Expr getVariable(const std::string& var_name);
 
   /**
-   * Returns a sort, given a name
+   * Returns a sort, given a name.
    */
   Type getSort(const std::string& sort_name);
 
   /**
+   * Returns a sort, given a name and args.
+   */
+  Type getSort(const std::string& sort_name,
+               const std::vector<Type>& params);
+
+  /**
    * Checks if a symbol has been declared.
    * @param name the symbol name
    * @param type the symbol type
@@ -267,8 +273,10 @@ public:
   /** Create a new CVC4 variable expression of the given type. */
   Expr mkVar(const std::string& name, const Type& type);
 
-  /** Create a set of new CVC4 variable expressions of the given
-   type. */
+  /**
+   * Create a set of new CVC4 variable expressions of the given
+   * type.
+   */
   const std::vector<Expr>
   mkVars(const std::vector<std::string> names, const Type& type);
 
@@ -278,13 +286,18 @@ public:
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
+  /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
+  void defineParameterizedType(const std::string& name,
+                               const std::vector<Type>& params,
+                               const Type& type);
+
   /**
-   * Creates a new sort with the given name.
+   * Creates a new sort with the given name and arity.
    */
-  Type mkSort(const std::string& name);
+  Type mkSort(const std::string& name, size_t arity = 0);
 
   /**
-   * Creates a new sorts with the given names.
+   * Creates new sorts with the given names (all of arity 0).
    */
   const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 23881c8b9..ffc113574 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -87,11 +87,9 @@ public:
    * @param parser the CVC4 Parser object
    * @param theory the theory to open (e.g., Core, Ints)
    */
-  void
-  addTheory(Theory theory);
+  void addTheory(Theory theory);
 
-  bool
-  logicIsSet();
+  bool logicIsSet();
 
   /**
    * Sets the logic for the current benchmark. Declares any logic and theory symbols.
@@ -99,8 +97,7 @@ public:
    * @param parser the CVC4 Parser object
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    */
-  void
-  setLogic(const std::string& name);
+  void setLogic(const std::string& name);
 
   static Logic toLogic(const std::string& name);
 
@@ -109,7 +106,8 @@ private:
   void addArithmeticOperators();
   void addUf();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
-};
+};/* class Smt */
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6919c86c4..4c742adfc 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -61,7 +61,7 @@ options {
 using namespace CVC4;
 using namespace CVC4::parser;
 
-#undef PARSER_STATE 
+#undef PARSER_STATE
 #define PARSER_STATE ((Smt2*)LEXER->super)
 }
 
@@ -91,7 +91,7 @@ using namespace CVC4::parser;
 
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef PARSER_STATE 
+#undef PARSER_STATE
 #define PARSER_STATE ((Smt2*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
@@ -112,7 +112,7 @@ parseExpr returns [CVC4::Expr expr]
   ;
 
 /**
- * Parses a command 
+ * Parses a command
  * @return the parsed command, or NULL if we've reached the end of the input
  */
 parseCommand returns [CVC4::Command* cmd]
@@ -126,15 +126,18 @@ parseCommand returns [CVC4::Command* cmd]
 command returns [CVC4::Command* cmd]
 @declarations {
   std::string name;
+  std::vector<std::string> names;
   Expr expr;
   Type t;
+  std::vector<Expr> terms;
   std::vector<Type> sorts;
+  std::vector<std::pair<std::string, Type> > sortedVars;
   SExpr sexpr;
 }
   : /* set the logic */
     SET_LOGIC_TOK SYMBOL
     { name = AntlrInput::tokenText($SYMBOL);
-      Debug("parser") << "set logic: '" << name << "' " << std::endl;
+      Debug("parser") << "set logic: '" << name << "'" << std::endl;
       if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) {
         PARSER_STATE->parseError("Only one set-logic is allowed.");
       }
@@ -142,35 +145,113 @@ command returns [CVC4::Command* cmd]
       $cmd = new SetBenchmarkLogicCommand(name); }
   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      PARSER_STATE->setInfo(name,sexpr);    
+      PARSER_STATE->setInfo(name,sexpr);
       cmd = new SetInfoCommand(name,sexpr); }
+  | /* get-info */
+    GET_INFO_TOK KEYWORD
+    { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
+  | /* set-option */
+    SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
+    { name = AntlrInput::tokenText($KEYWORD);
+      PARSER_STATE->setOption(name,sexpr);
+      cmd = new SetOptionCommand(name,sexpr); }
+  | /* get-option */
+    GET_OPTION_TOK KEYWORD
+    { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
   | /* sort declaration */
     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
-    { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl;
-      if( AntlrInput::tokenToInteger(n) > 0 ) {
-        Unimplemented("Parameterized user sorts.");
-      }
-      PARSER_STATE->mkSort(name); 
+    { Debug("parser") << "declare sort: '" << name
+                      << "' arity=" << n << std::endl;
+      PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n));
       $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); }
+  | /* sort definition */
+    DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
+    LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
+    {
+      PARSER_STATE->pushScope();
+      for(std::vector<std::string>::const_iterator i = names.begin(),
+            iend = names.end();
+          i != iend;
+          ++i) {
+        sorts.push_back(PARSER_STATE->mkSort(*i));
+      }
+    }
+    sortSymbol[t]
+    { PARSER_STATE->popScope();
+      // Do NOT call mkSort, since that creates a new sort!
+      // This name is not its own distinct sort, it's an alias.
+      PARSER_STATE->defineParameterizedType(name, sorts, t);
+      $cmd = new EmptyCommand;
+    }
   | /* function declaration */
-    DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] 
-    LPAREN_TOK sortList[sorts] RPAREN_TOK 
+    DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    LPAREN_TOK sortList[sorts] RPAREN_TOK
     sortSymbol[t]
-    { Debug("parser") << "declare fun: '" << name << "' " << std::endl;
+    { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
       if( sorts.size() > 0 ) {
         t = EXPR_MANAGER->mkFunctionType(sorts,t);
       }
-      PARSER_STATE->mkVar(name, t); 
-      $cmd = new DeclarationCommand(name,t); } 
+      PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclarationCommand(name,t); }
+  | /* function definition */
+    DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK
+    sortSymbol[t]
+    { /* add variables to parser state before parsing term */
+      Debug("parser") << "define fun: '" << name << "'" << std::endl;
+      if( sortedVars.size() > 0 ) {
+        std::vector<CVC4::Type> sorts;
+        sorts.reserve(sortedVars.size());
+        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+              sortedVars.begin(), iend = sortedVars.end();
+            i != iend;
+            ++i) {
+          sorts.push_back((*i).second);
+        }
+        t = EXPR_MANAGER->mkFunctionType(sorts,t);
+      }
+      PARSER_STATE->pushScope();
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVars.begin(), iend = sortedVars.end();
+          i != iend;
+          ++i) {
+        PARSER_STATE->mkVar((*i).first, (*i).second);
+      }
+    }
+    term[expr]
+    { PARSER_STATE->popScope();
+      // declare the name down here (while parsing term, signature
+      // must not be extended with the name itself; no recursion
+      // permitted)
+      PARSER_STATE->mkVar(name, t);
+      $cmd = new DefineFunctionCommand(name,sortedVars,t,expr);
+    }
+  | /* value query */
+    GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
+    { if(terms.size() == 1) {
+        $cmd = new GetValueCommand(terms[0]);
+      } else {
+        CommandSequence* seq = new CommandSequence();
+        for(std::vector<Expr>::const_iterator i = terms.begin(),
+              iend = terms.end();
+            i != iend;
+            ++i) {
+          seq->addCommand(new GetValueCommand(*i));
+        }
+        $cmd = seq;
+      }
+    }
   | /* assertion */
     ASSERT_TOK term[expr]
     { cmd = new AssertCommand(expr);   }
   | /* checksat */
-    CHECKSAT_TOK 
+    CHECKSAT_TOK
     { cmd = new CheckSatCommand(MK_CONST(true)); }
+  | /* get-assertions */
+    GET_ASSERTIONS_TOK
+    { cmd = new GetAssertionsCommand; }
   | EXIT_TOK
-    { // TODO: Explicitly represent exit as command?
-      cmd = 0; }
+    { cmd = NULL; }
   ;
 
 symbolicExpr[CVC4::SExpr& sexpr]
@@ -187,12 +268,12 @@ symbolicExpr[CVC4::SExpr& sexpr]
     { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
   | KEYWORD
     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
-  | LPAREN_TOK 
-    (symbolicExpr[sexpr] { children.push_back(sexpr); } )* 
+  | LPAREN_TOK
+    (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
   	RPAREN_TOK
     { sexpr = SExpr(children); }
   ;
-  
+
 /**
  * Matches a term.
  * @return the expression representing the formula
@@ -202,11 +283,11 @@ term[CVC4::Expr& expr]
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind;
   std::string name;
-  std::vector<Expr> args; 
-} 
+  std::vector<Expr> args;
+}
   : /* a built-in operator application */
-    LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK 
-    { 
+    LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
+    {
       if( kind == CVC4::kind::EQUAL &&
           args.size() > 0 &&
           args[0].getType() == EXPR_MANAGER->booleanType() ) {
@@ -214,13 +295,13 @@ term[CVC4::Expr& expr]
         kind = CVC4::kind::IFF;
       }
 
-      if( !PARSER_STATE->strictModeEnabled() && 
-          (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && 
+      if( !PARSER_STATE->strictModeEnabled() &&
+          (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
           args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
-      } else if( CVC4::kind::isAssociative(kind) && 
+      } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
@@ -233,7 +314,7 @@ term[CVC4::Expr& expr]
     }
 
   | /* A non-built-in function application */
-    LPAREN_TOK 
+    LPAREN_TOK
     functionSymbol[expr]
     { args.push_back(expr); }
     termList[args,expr] RPAREN_TOK
@@ -241,18 +322,18 @@ term[CVC4::Expr& expr]
     { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
 
   // | /* An ite expression */
-  //   LPAREN_TOK ITE_TOK 
+  //   LPAREN_TOK ITE_TOK
   //   term[expr]
-  //   { args.push_back(expr); } 
+  //   { args.push_back(expr); }
   //   term[expr]
-  //   { args.push_back(expr); } 
+  //   { args.push_back(expr); }
   //   term[expr]
-  //   { args.push_back(expr); } 
+  //   { args.push_back(expr); }
   //   RPAREN_TOK
   //   { expr = MK_EXPR(CVC4::kind::ITE, args); }
 
   | /* a let binding */
-    LPAREN_TOK LET_TOK LPAREN_TOK 
+    LPAREN_TOK LET_TOK LPAREN_TOK
     { PARSER_STATE->pushScope(); }
     ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK
       { PARSER_STATE->defineVar(name,expr); } )+
@@ -270,7 +351,8 @@ term[CVC4::Expr& expr]
     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
 
   | DECIMAL_LITERAL
-    { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
+    { // FIXME: This doesn't work because an SMT rational is not a
+      // valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 
   | HEX_LITERAL
@@ -290,8 +372,8 @@ term[CVC4::Expr& expr]
  * vector.
  * @param formulas the vector to fill with terms
  * @param expr an Expr reference for the elements of the sequence
- */   
-/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every 
+ */
+/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
  * time through this rule. */
 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
   : ( term[expr] { formulas.push_back(expr); } )+
@@ -334,7 +416,7 @@ builtinOp[CVC4::Kind& kind]
  * @param check what kind of check to do with the symbol
  */
 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
-  :  symbol[name,check,SYM_VARIABLE] 
+  : symbol[name,check,SYM_VARIABLE]
   ;
 
 /**
@@ -348,23 +430,38 @@ functionSymbol[CVC4::Expr& fun]
     { PARSER_STATE->checkFunction(name);
       fun = PARSER_STATE->getVariable(name); }
   ;
-  
+
 /**
- * Matches a sequence of sort symbols and fills them into the given vector.
+ * Matches a sequence of sort symbols and fills them into the given
+ * vector.
  */
 sortList[std::vector<CVC4::Type>& sorts]
 @declarations {
   Type t;
 }
-  : ( sortSymbol[t] { sorts.push_back(t); })* 
+  : ( sortSymbol[t] { sorts.push_back(t); } )*
+  ;
+
+/**
+ * Matches a sequence of (variable,sort) symbol pairs and fills them
+ * into the given vector.
+ */
+sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
+@declarations {
+  std::string name;
+  Type t;
+}
+  : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK
+      { sortedVars.push_back(make_pair(name, t)); }
+    )*
   ;
 
 /**
  * Matches the sort symbol, which can be an arbitrary symbol.
  * @param check the check to perform on the name
  */
-sortName[std::string& name, CVC4::parser::DeclarationCheck check] 
-  : symbol[name,check,SYM_SORT] 
+sortName[std::string& name, CVC4::parser::DeclarationCheck check]
+  : symbol[name,check,SYM_SORT]
   ;
 
 sortSymbol[CVC4::Type& t]
@@ -372,15 +469,15 @@ sortSymbol[CVC4::Type& t]
   std::string name;
   std::vector<CVC4::Type> args;
 }
-  : sortName[name,CHECK_NONE] 
+  : sortName[name,CHECK_NONE]
   	{ t = PARSER_STATE->getSort(name); }
   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
-    { 
+    {
       if( name == "Array" ) {
         if( args.size() != 2 ) {
           PARSER_STATE->parseError("Illegal array type.");
         }
-        t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); 
+        t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
       } else {
         PARSER_STATE->parseError("Unhandled parameterized type.");
       }
@@ -388,14 +485,27 @@ sortSymbol[CVC4::Type& t]
   ;
 
 /**
+ * Matches a list of symbols, with check and type arguments as for the
+ * symbol[] rule below.
+ */
+symbolList[std::vector<std::string>& names,
+           CVC4::parser::DeclarationCheck check,
+           CVC4::parser::SymbolType type]
+@declarations {
+  std::string id;
+}
+  : ( symbol[id,check,type] { names.push_back(id); } )*
+  ;
+
+/**
  * Matches an symbol and sets the string reference parameter id.
  * @param id string to hold the symbol
  * @param check what kinds of check to do on the symbol
  * @param type the intended namespace for the symbol
  */
 symbol[std::string& id,
-		   CVC4::parser::DeclarationCheck check, 
-           CVC4::parser::SymbolType type] 
+       CVC4::parser::DeclarationCheck check,
+       CVC4::parser::SymbolType type]
   : SYMBOL
     { id = AntlrInput::tokenText($SYMBOL);
       Debug("parser") << "symbol: " << id
@@ -411,6 +521,10 @@ CHECKSAT_TOK : 'check-sat';
 //DIFFICULTY_TOK : ':difficulty';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
+DEFINE_FUN_TOK : 'define-fun';
+DEFINE_SORT_TOK : 'define-sort';
+GET_VALUE_TOK : 'get-value';
+GET_ASSERTIONS_TOK : 'get-assertions';
 EXIT_TOK : 'exit';
 //FALSE_TOK : 'false';
 ITE_TOK : 'ite';
@@ -421,6 +535,8 @@ RPAREN_TOK : ')';
 //SAT_TOK : 'sat';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
+SET_OPTION_TOK : 'set-option';
+GET_OPTION_TOK : 'get-option';
 //SMT_VERSION_TOK : ':smt-lib-version';
 //SOURCE_TOK : ':source';
 //STATUS_TOK : ':status';
@@ -456,8 +572,8 @@ TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
 /**
- * Matches a symbol from the input. A symbol is a "simple" symbol or a 
- * sequence of printable ASCII characters that starts and ends with | and 
+ * Matches a symbol from the input. A symbol is a "simple" symbol or a
+ * sequence of printable ASCII characters that starts and ends with | and
  * does not otherwise contain |.
  */
 SYMBOL
@@ -473,11 +589,11 @@ KEYWORD
   : ':' SIMPLE_SYMBOL
   ;
 
-/** Matches a "simple" symbol: a non-empty sequence of letters, digits and 
- * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a 
- * digit. 
+/** Matches a "simple" symbol: a non-empty sequence of letters, digits and
+ * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
+ * digit.
  */
-fragment SIMPLE_SYMBOL 
+fragment SIMPLE_SYMBOL
   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)*
   ;
 
@@ -485,7 +601,7 @@ fragment SIMPLE_SYMBOL
  * Matches and skips whitespace in the input.
  */
 WHITESPACE
-  :  (' ' | '\t' | '\f' | '\r' | '\n')+             { $channel = HIDDEN;; }
+  : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN; }
   ;
 
 /**
@@ -503,19 +619,19 @@ fragment NUMERAL
   char *start = (char*) GETCHARINDEX();
 }
   : DIGIT+
-    { Debug("parser-extra") << "NUMERAL: " 
-       << (uintptr_t)start << ".." << GETCHARINDEX() 
+    { Debug("parser-extra") << "NUMERAL: "
+       << (uintptr_t)start << ".." << GETCHARINDEX()
        << " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
        << " ^0? " << (bool)(*start == '0')
        << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
        << std::endl; }
-    { !PARSER_STATE->strictModeEnabled() || 
+    { !PARSER_STATE->strictModeEnabled() ||
       *start != '0' ||
       start == (char*)(GETCHARINDEX() - 1) }?
   ;
-  
+
 /**
-  * Matches a decimal constant from the input. 
+  * Matches a decimal constant from the input.
   */
 DECIMAL_LITERAL
   : NUMERAL '.' DIGIT+
@@ -537,18 +653,18 @@ DECIMAL_LITERAL
 
 
 /**
- * Matches a double quoted string literal. Escaping is supported, and escape
- * character '\' has to be escaped.
+ * Matches a double quoted string literal. Escaping is supported, and
+ * escape character '\' has to be escaped.
  */
-STRING_LITERAL 
-  :  '"' (ESCAPE | ~('"'|'\\'))* '"'
+STRING_LITERAL
+  : '"' (ESCAPE | ~('"'|'\\'))* '"'
   ;
 
 /**
  * Matches the comments and ignores them
  */
-COMMENT 
-  : ';' (~('\n' | '\r'))*                    { $channel = HIDDEN;; }
+COMMENT
+  : ';' (~('\n' | '\r'))* { $channel = HIDDEN; }
   ;
 
 
@@ -556,9 +672,9 @@ COMMENT
  * Matches any letter ('a'-'z' and 'A'-'Z').
  */
 fragment
-ALPHA 
-  :  'a'..'z'
-  |  'A'..'Z'
+ALPHA
+  : 'a'..'z'
+  | 'A'..'Z'
   ;
 
 /**
@@ -568,10 +684,10 @@ fragment DIGIT : '0'..'9';
 
 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 
-/** Matches the characters that may appear in a "symbol" (i.e., an identifier) 
+/** Matches the characters that may appear in a "symbol" (i.e., an identifier)
  */
-fragment SYMBOL_CHAR 
-  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' 
+fragment SYMBOL_CHAR
+  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
   | '&' | '^' | '<' | '>' | '@'
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e704d027d..308f45ed0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -98,7 +98,8 @@ bool Smt2::logicIsSet() {
 }
 
 /**
- * Sets the logic for the current benchmark. Declares any logic and theory symbols.
+ * Sets the logic for the current benchmark. Declares any logic and
+ * theory symbols.
  *
  * @param parser the CVC4 Parser object
  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
@@ -124,7 +125,7 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::QF_NIA:
     addTheory(THEORY_INTS);
     break;
-    
+
   case Smt::QF_LRA:
   case Smt::QF_RDL:
     addTheory(THEORY_REALS);
@@ -162,5 +163,9 @@ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
 }
 
+void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
+  // TODO: ???
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index fe152a7f6..6398fa735 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -57,28 +57,28 @@ public:
    * @param parser the CVC4 Parser object
    * @param theory the theory to open (e.g., Core, Ints)
    */
-  void
-  addTheory(Theory theory);
+  void addTheory(Theory theory);
 
-  bool
-  logicIsSet();
+  bool logicIsSet();
 
   /**
-   * Sets the logic for the current benchmark. Declares any logic and theory symbols.
+   * Sets the logic for the current benchmark. Declares any logic and
+   * theory symbols.
    *
    * @param parser the CVC4 Parser object
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    */
-  void
-  setLogic(const std::string& name);
+  void setLogic(const std::string& name);
 
-  void
-  setInfo(const std::string& flag, const SExpr& sexpr);
+  void setInfo(const std::string& flag, const SExpr& sexpr);
+
+  void setOption(const std::string& flag, const SExpr& sexpr);
 
 private:
 
   void addArithmeticOperators();
-};
+};/* class Smt2 */
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 320f5ab75..02a480971 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -64,7 +64,8 @@ public:
   /**
    * Create a string input.
    *
-   * @param exprManager the manager to use when building expressions from the input
+   * @param exprManager the manager to use when building expressions
+   * from the input
    * @param input the string to read
    * @param name the "filename" to use when reporting errors
    */
@@ -81,7 +82,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() 
+  Command* parseCommand()
     throw(ParserException, TypeCheckingException, AssertionException);
 
   /**
@@ -90,7 +91,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() 
+  Expr parseExpr()
     throw(ParserException, TypeCheckingException, AssertionException);
 
 };/* class Smt2Input */
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 */
 
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 07d48b1f6..5cd4719b1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::arith::TheoryArith "theory_arith.h"
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 68daa8cb5..4ad9c7463 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 43c37f4b7..ac6b05881 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 54f861b76..cc6fe0c20 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
index 616d3da74..d8a54b1e4 100644
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -11,9 +11,19 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief The theory output channel interface.
+ ** \brief An exception signaling that a Theory should immediately
+ ** stop performing processing
  **
- ** The theory output channel interface.
+ ** An exception signaling that a Theory should immediately stop
+ ** performing processing and relinquish control to its caller (e.g.,
+ ** in a parallel environment).  A Theory might be interrupted if it
+ ** calls into its CVC4::theory::OutputChannel, and it should only
+ ** catch this exception to perform emergency repair of any invariants
+ ** it must re-establish.  Further, if this exception is caught by a
+ ** Theory, the Theory should rethrow the same exception (via "throw;"
+ ** in the exception block) rather than return, as the Interrupted
+ ** instance might contain additional information needed for the
+ ** proper management of CVC4 components.
  **/
 
 #include "cvc4_private.h"
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index fb2fde589..cdc1e1cc2 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief The theory output channel interface.
+ ** \brief The theory output channel interface
  **
  ** The theory output channel interface.
  **/
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 4bfba382c..13cd5e91b 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
diff --git a/src/util/options.h b/src/util/options.h
index c79bc93b1..c504177bf 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -65,21 +65,34 @@ struct CVC4_PUBLIC Options {
   /** Should we strictly enforce the language standard while parsing? */
   bool strictParsing;
 
-  Options() : binary_name(),
-              statistics(false),
-              out(0),
-              err(0),
-              verbosity(0),
-              lang(parser::LANG_AUTO),
-              uf_implementation(MORGAN),
-              parseOnly(false),
-              semanticChecks(true),
-              memoryMap(false),
-              strictParsing(false)
-  {}
+  /** Whether we're in interactive mode or not */
+  bool interactive;
+
+  /**
+   * Whether we're in interactive mode (or not) due to explicit user
+   * setting (if false, we inferred the proper default setting).
+   */
+  bool interactiveSetByUser;
+
+  Options() :
+    binary_name(),
+    statistics(false),
+    out(0),
+    err(0),
+    verbosity(0),
+    lang(parser::LANG_AUTO),
+    uf_implementation(MORGAN),
+    parseOnly(false),
+    semanticChecks(true),
+    memoryMap(false),
+    strictParsing(false),
+    interactive(false),
+    interactiveSetByUser(false) {
+  }
 };/* struct Options */
 
-inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) {
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::UfImplementation uf) {
   switch(uf) {
   case Options::TIM:
     out << "TIM";
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index d3681f471..9821664bd 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -29,8 +29,8 @@
 namespace CVC4 {
 
 /**
- * A simple S-expression. An S-expression is either an atom with a string value, or a
- * list of other S-expressions.
+ * A simple S-expression. An S-expression is either an atom with a
+ * string value, or a list of other S-expressions.
  */
 class CVC4_PUBLIC SExpr {
 
@@ -61,13 +61,15 @@ public:
   /** Is this S-expression an atom? */
   bool isAtom() const;
 
-  /** Get the string value of this S-expression. This will cause an error if this S-expression
-   * is not an atom.
+  /**
+   * Get the string value of this S-expression. This will cause an
+   * error if this S-expression is not an atom.
    */
   const std::string getValue() const;
 
-  /** Get the children of this S-expression. This will cause an error if this S-expression
-   * is not a list.
+  /**
+   * Get the children of this S-expression. This will cause an error
+   * if this S-expression is not a list.
    */
   const std::vector<SExpr> getChildren() const;
 };
@@ -93,7 +95,9 @@ inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
     std::vector<SExpr> children = sexpr.getChildren();
     out << "(";
     bool first = true;
-    for( std::vector<SExpr>::iterator it = children.begin(); it != children.end(); ++it ) {
+    for( std::vector<SExpr>::iterator it = children.begin();
+         it != children.end();
+         ++it ) {
       if( first ) {
         first = false;
       } else {