minor interface improvements, compliance fixes

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

1 files changed, 11 insertions, 13 deletions

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