* Option --no-type-checking now disables type checks in SmtEngine

* Adding options --lazy-type-checking and --eager-type-checking
  to control type checking in NodeBuilder, which can now be enabled
  in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options

3 files changed, 11 insertions, 11 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d7b1e6d99..f503efae2 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -57,15 +57,15 @@ public:
   }
 };
 
-PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
-                       TheoryEngine* te, Context* context) :
+PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, 
+                       Context* context, const Options& opts) :
   d_inCheckSat(false),
-  d_options(opts),
+  // d_options(opts),
   d_decisionEngine(de),
   d_theoryEngine(te),
   d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
-  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
+  d_satSolver = new SatSolver(this, d_theoryEngine, d_context, opts);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
   d_satSolver->setCnfStream(d_cnfStream);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1dada2e69..1c7c506ee 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -26,11 +26,11 @@
 #include "expr/node.h"
 #include "util/result.h"
 #include "util/decision_engine.h"
+#include "smt/options.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
-class Options;
 
 namespace prop {
 
@@ -50,7 +50,7 @@ class PropEngine {
   bool d_inCheckSat;
 
   /** The global options */
-  const Options *d_options;
+  //const Options d_options;
 
   /** The decision engine we will be using */
   DecisionEngine *d_decisionEngine;
@@ -76,7 +76,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*);
+  PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&);
 
   /**
    * Destructor.
diff --git a/src/prop/sat.h b/src/prop/sat.h
index a335b733b..17bf447f8 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -125,7 +125,7 @@ class SatSolver : public SatInputInterface {
   context::Context* d_context;
 
   /** Remember the options */
-  Options* d_options;
+  // Options* d_options;
 
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
@@ -203,7 +203,7 @@ public:
   SatSolver(PropEngine* propEngine,
                    TheoryEngine* theoryEngine,
                    context::Context* context,
-                   const Options* options);
+                   const Options& options);
 
   ~SatSolver();
 
@@ -233,7 +233,7 @@ public:
 #ifdef __CVC4_USE_MINISAT
 
 inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
-                     context::Context* context, const Options* options) :
+                     context::Context* context, const Options& options) :
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),
@@ -243,7 +243,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   // Create the solver
   d_minisat = new Minisat::SimpSolver(this, d_context);
   // Setup the verbosity
-  d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
+  d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
 
   // No random choices
   if(Debug.isOn("no_rnd_decisions")){