minor interface improvements, compliance fixes

(this commit was certified error- and warning-free by the test-and-commit script.)

10 files changed, 181 insertions, 37 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 1e4a266a5..53ca266f4 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -26,6 +26,8 @@
 #include "expr/command.h"
 #include "smt/smt_engine.h"
 #include "options/options.h"
+#include "smt/options.h"
+#include "smt/smt_engine_scope.h"
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/sexpr.h"
@@ -691,7 +693,7 @@ Command* SetUserAttributeCommand::clone() const{
   return new SetUserAttributeCommand( d_attr, d_expr );
 }
 
-/* class Simplify */
+/* class SimplifyCommand */
 
 SimplifyCommand::SimplifyCommand(Expr term) throw() :
   d_term(term) {
@@ -730,6 +732,45 @@ Command* SimplifyCommand::clone() const {
   return c;
 }
 
+/* class ExpandDefinitionsCommand */
+
+ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
+  d_term(term) {
+}
+
+Expr ExpandDefinitionsCommand::getTerm() const throw() {
+  return d_term;
+}
+
+void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
+  d_result = smtEngine->expandDefinitions(d_term);
+  d_commandStatus = CommandSuccess::instance();
+}
+
+Expr ExpandDefinitionsCommand::getResult() const throw() {
+  return d_result;
+}
+
+void ExpandDefinitionsCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
+}
+
+Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  return c;
+}
+
+Command* ExpandDefinitionsCommand::clone() const {
+  ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -752,7 +793,10 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
     NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager());
     for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
       Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
-      result.push_back(nm->mkNode(kind::TUPLE, Node::fromExpr(*i), Node::fromExpr(smtEngine->getValue(*i))));
+      smt::SmtScope scope(smtEngine);
+      Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
+      Node value = Node::fromExpr(smtEngine->getValue(*i));
+      result.push_back(nm->mkNode(kind::TUPLE, request, value));
     }
     Node n = nm->mkNode(kind::TUPLE, result);
     d_result = nm->toExpr(n);
@@ -908,6 +952,44 @@ Command* GetProofCommand::clone() const {
   return c;
 }
 
+/* class GetUnsatCoreCommand */
+
+GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
+}
+
+void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
+  /*
+  try {
+    d_result = smtEngine->getUnsatCore();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+  */
+  d_commandStatus = new CommandFailure("unsat cores not supported yet");
+}
+
+void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    //do nothing -- unsat cores not yet supported
+    // d_result->toStream(out);
+  }
+}
+
+Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
+  //c->d_result = d_result;
+  return c;
+}
+
+Command* GetUnsatCoreCommand::clone() const {
+  GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
+  //c->d_result = d_result;
+  return c;
+}
+
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 70e71a111..5786f4e71 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -475,6 +475,21 @@ public:
   Command* clone() const;
 };/* class SimplifyCommand */
 
+class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
+protected:
+  Expr d_term;
+  Expr d_result;
+public:
+  ExpandDefinitionsCommand(Expr term) throw();
+  ~ExpandDefinitionsCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+};/* class ExpandDefinitionsCommand */
+
 class CVC4_PUBLIC GetValueCommand : public Command {
 protected:
   std::vector<Expr> d_terms;
@@ -531,6 +546,18 @@ public:
   Command* clone() const;
 };/* class GetProofCommand */
 
+class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
+protected:
+  //UnsatCore* d_result;
+public:
+  GetUnsatCoreCommand() throw();
+  ~GetUnsatCoreCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+};/* class GetUnsatCoreCommand */
+
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 73a2b94a3..500f5373f 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -518,7 +518,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
       preemptGetopt(extra_argc, extra_argv, \"$link\");"
     done
   fi
-  if [ "$type" = bool -a -n "$cases" -o -n "$cases_alternate" ]; then
+  if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
     run_handlers=
     if [ -n "$handlers" ]; then
       echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
@@ -713,7 +713,7 @@ template <> void Options::assignBool(options::${internal}__option_t, std::string
 #line $lineno \"$kf\"
   Trace(\"options\") << \"user assigned option $internal\" << std::endl;
 }"
-  elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o "$cases_alternate" -o "$smtname" ]; then
+  elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
     all_custom_handlers="${all_custom_handlers}
 #line $lineno \"$kf\"
 template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 867250c0f..5950f568f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -302,7 +302,7 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetProofCommand; }
   | /* get-unsat-core */
     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { UNSUPPORTED("unsat cores not yet supported"); }
+    { cmd = new GetUnsatCoreCommand; }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
diff --git a/src/proof/options b/src/proof/options
index f00c8fc75..af4ffeb93 100644
--- a/src/proof/options
+++ b/src/proof/options
@@ -5,7 +5,4 @@
 
 module PROOF "proof/options.h" Proof
 
-option proof produce-proofs --proof bool
- turn on proof generation
-
 endmodule
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 4b76d70ae..4ce621e43 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__PROOF__PROOF_H
 #define __CVC4__PROOF__PROOF_H
 
-#include "proof/options.h"
+#include "smt/options.h"
 
 #ifdef CVC4_PROOF
 #  define PROOF(x) if(options::proof()) { x; }
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 );