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

5 files changed, 242 insertions, 66 deletions

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);