4 files changed, 66 insertions, 28 deletions
diff --git a/src/smt/options b/src/smt/options
index 508c03a66..24c8b5e43 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -3,14 +3,6 @@
 # See src/options/base_options for a description of this file format
 #
 
-# FIXME: need to add support for SMT-LIBv2-required options:
-#
-#   expand-definitions
-#   regular-output-channel
-#   diagnostic-output-channel
-#   produce-unsat-cores
-#
-
 module SMT "smt/options.h" SMT layer
 
 common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
@@ -18,9 +10,6 @@ common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-inclu
 common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
  all dumping goes to FILE (instead of stdout)
 
-expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
- expand define-funs/LAMBDAs lazily
-
 option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
  choose simplification mode, see --simplification=help
 alias --no-simplification = --simplification=none
@@ -30,11 +19,18 @@ option doStaticLearning static-learning /--no-static-learning bool :default true
  use static learning (on by default)
 /turn off static learning (e.g. diamond-breaking)
 
-common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+option expandDefinitions expand-definitions bool :default false
+ always expand symbol definitions in output
+common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkModels check-models --check-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID, double-check that the generated model satisfies all user assertions
-common-option produceAssignments produce-assignments --produce-assignments bool
+common-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on proof generation
+# this is just a placeholder for later; it doesn't show up in command-line options listings
+common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation (NOT YET SUPPORTED)
+common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h"
  print format mode for models, see --model-format=help
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index fb6cd84d8..2c20e06bb 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -23,6 +23,8 @@
 
 #include "cvc4autoconfig.h"
 #include "util/dump.h"
+#include "smt/modal_exception.h"
+#include "smt/smt_engine.h"
 
 #include <cerrno>
 #include <cstring>
@@ -255,6 +257,32 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o
   }
 }
 
+// ensure we haven't started search yet
+inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
+  if(smt != NULL && smt->d_fullyInited) {
+    std::stringstream ss;
+    ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
+    throw ModalException(ss.str());
+  }
+}
+
+// ensure we are a proof-enabled build of CVC4
+inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
+#ifndef CVC4_PROOF
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_PROOF */
+}
+
+inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
+  if(value) {
+    throw OptionException("CVC4 does not yet have support for unsatisfiable cores");
+  }
+}
+
 // This macro is used for setting :regular-output-channel and :diagnostic-output-channel
 // to redirect a stream.  It maintains all attributes set on the stream.
 #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 256867d79..55ea09de4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1448,7 +1448,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  if(!options::lazyDefinitionExpansion()) {
+  {
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
@@ -1764,6 +1764,22 @@ Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) {
   return d_private->applySubstitutions(e).toExpr();
 }
 
+Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) {
+  Assert(e.getExprManager() == d_exprManager);
+  SmtScope smts(this);
+  finalOptionsAreSet();
+  doPendingPops();
+  if( options::typeChecking() ) {
+    e.getType(true);// ensure expr is type-checked at this point
+  }
+  Trace("smt") << "SMT expandDefinitions(" << e << ")" << endl;
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << ExpandDefinitionsCommand(e);
+  }
+  hash_map<Node, Node, NodeHashFunction> cache;
+  return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
+}
+
 Expr SmtEngine::getValue(const Expr& e)
   throw(ModalException, AssertionException) {
   Assert(e.getExprManager() == d_exprManager);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5b3229dea..9614c8ced 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -75,6 +75,8 @@ namespace smt {
 
   class SmtEnginePrivate;
   class SmtScope;
+
+  void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
 }/* CVC4::smt namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -261,6 +263,7 @@ class CVC4_PUBLIC SmtEngine {
 
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
+  friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
 
   StatisticsRegistry* d_statisticsRegistry;
 
@@ -370,8 +373,8 @@ public:
   /**
    * Simplify a formula without doing "much" work.  Does not involve
    * the SAT Engine in the simplification, but uses the current
-   * assertions and the current partial model, if one has been
-   * constructed.
+   * definitions, assertions, and the current partial model, if one
+   * has been constructed.  It also involves theory normalization.
    *
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
@@ -379,6 +382,12 @@ public:
   Expr simplify(const Expr& e) throw(TypeCheckingException);
 
   /**
+   * Expand the definitions in a term or formula.  No other
+   * simplification or normalization is done.
+   */
+  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException);
+
+  /**
    * Get the assigned value of an expr (only if immediately preceded
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
@@ -554,17 +563,6 @@ public:
   }
 
   /**
-   * Used as a predicate for options preprocessor.
-   */
-  static void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
-    if(smt != NULL && smt->d_fullyInited) {
-      std::stringstream ss;
-      ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
-      throw ModalException(ss.str());
-    }
-  }
-
-  /**
    * print model function (need this?)
    */
   void printModel( std::ostream& out, Model* m );