inline void debugCheckType(const TNode n) const {
// force an immediate type check, if we are in debug mode
// and the current node isn't a variable or constant
- if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) {
+ if( d_nm->d_earlyTypeChecking ) {
kind::MetaKind mk = n.getMetaKind();
if( mk != kind::metakind::VARIABLE
&& mk != kind::metakind::CONSTANT ) {
NO_INTERACTIVE,
PRODUCE_MODELS,
PRODUCE_ASSIGNMENTS,
- NO_EARLY_TYPE_CHECKING
+ NO_TYPE_CHECKING,
+ LAZY_TYPE_CHECKING,
+ EAGER_TYPE_CHECKING,
};/* enum OptionValue */
/**
{ "no-interactive", no_argument , NULL, NO_INTERACTIVE },
{ "produce-models", no_argument , NULL, PRODUCE_MODELS},
{ "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
- { "no-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
+ { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
+ { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
+ { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
{ NULL , no_argument , NULL, '\0' }
};/* if you add things to the above, please remember to update usage.h! */
case NO_CHECKING:
opts->semanticChecks = false;
+ opts->typeChecking = false;
+ opts->earlyTypeChecking = false;
break;
case USE_MMAP:
opts->produceAssignments = true;
break;
- case NO_EARLY_TYPE_CHECKING:
+ case NO_TYPE_CHECKING:
+ opts->typeChecking = false;
+ opts->earlyTypeChecking = false;
+ break;
+
+ case LAZY_TYPE_CHECKING:
opts->earlyTypeChecking = false;
break;
+ case EAGER_TYPE_CHECKING:
+ opts->typeChecking = true;
+ opts->earlyTypeChecking = true;
+ break;
+
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
options.interactive = inputFromStdin && isatty(fileno(stdin));
}
- /* Early type checking can be turned off by --no-type-checking OR
- --no-checking. We're assuming that earlyTypeChecking is not
- explicitly set by the user. */
- if(options.earlyTypeChecking) {
- options.earlyTypeChecking = options.semanticChecks;
- }
-
// Create the expression manager
ExprManager exprMgr(options.earlyTypeChecking);
// Create the SmtEngine
- SmtEngine smt(&exprMgr, &options);
+ SmtEngine smt(&exprMgr, options);
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
--mmap memory map file input\n\
--show-config show CVC4 static configuration\n\
--segv-nospin don't spin on segfault waiting for gdb\n\
- --no-checking disable semantic checks in the parser\n\
- --no-type-checking disable type checking [default in non-debug builds]\n\
+ --lazy-type-checking type check expressions only when necessary (default)\n\
+ --eager-type-checking type check expressions immediately on creation\n\
+ --no-type-checking never type check expressions\n\
+ --no-checking disable ALL semantic checks, including type checks \n\
--strict-parsing fail on non-conformant inputs (SMT2 only)\n\
--verbose | -v increase verbosity (repeatable)\n\
--quiet | -q decrease verbosity (repeatable)\n\
}
};
-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);
}
#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 {
bool d_inCheckSat;
/** The global options */
- const Options *d_options;
+ //const Options d_options;
/** The decision engine we will be using */
DecisionEngine *d_decisionEngine;
/**
* 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.
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
SatSolver(PropEngine* propEngine,
TheoryEngine* theoryEngine,
context::Context* context,
- const Options* options);
+ const Options& options);
~SatSolver();
#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),
// 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")){
/** Whether we support SmtEngine::getAssignment() for this run. */
bool produceAssignments;
+ /** Whether we do typechecking at all. */
+ bool typeChecking;
+
/** Whether we do typechecking at Expr creation time. */
bool earlyTypeChecking;
interactiveSetByUser(false),
produceModels(false),
produceAssignments(false),
+ typeChecking(true),
earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
}
};/* struct Options */
using namespace CVC4::smt;
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
- d_context(em->getContext()),
- d_exprManager(em),
- d_nodeManager(em->getNodeManager()),
- d_options(opts),
- /* These next few are initialized below, after we have a NodeManager
- * in scope. */
- d_decisionEngine(NULL),
- d_theoryEngine(NULL),
- d_propEngine(NULL),
- d_definedFunctions(NULL),
- d_assertionList(NULL),
- d_assignments(NULL),
- d_haveAdditions(false),
- d_status() {
+SmtEngine::SmtEngine(ExprManager* em) throw() :
+ d_exprManager(em) {
+ Options opts;
+ init(opts);
+}
+
+SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() :
+ d_exprManager(em){
+ init(opts);
+}
+
+void SmtEngine::init(const Options& opts) throw() {
+ d_context = d_exprManager->getContext();
+ d_nodeManager = d_exprManager->getNodeManager();
NodeManagerScope nms(d_nodeManager);
// We have mutual dependancy here, so we add the prop engine to the theory
// engine later (it is non-essential there)
d_theoryEngine = new TheoryEngine(d_context, opts);
- d_propEngine = new PropEngine(opts, d_decisionEngine,
- d_theoryEngine, d_context);
+ d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine,
+ d_context, opts);
d_theoryEngine->setPropEngine(d_propEngine);
d_definedFunctions = new(true) DefinedFunctionMap(d_context);
- if(d_options->interactive) {
+ d_assertionList = NULL;
+ d_interactive = opts.interactive;
+ if(d_interactive) {
d_assertionList = new(true) AssertionList(d_context);
}
+
+ d_assignments = NULL;
+ d_haveAdditions = false;
+
+ d_typeChecking = opts.typeChecking;
+ d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion;
+ d_produceModels = opts.produceModels;
+ d_produceAssignments = opts.produceAssignments;
+
}
void SmtEngine::shutdown() {
Expr formula) {
Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
NodeManagerScope nms(d_nodeManager);
- Type formulaType = formula.getType(true);// type check body
+ Type formulaType = formula.getType(d_typeChecking);// type check body
Type funcType = func.getType();
Type rangeType = funcType.isFunction() ?
FunctionType(funcType).getRangeType() : funcType;
Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n)
throw(NoSuchFunctionException, AssertionException) {
- if(!smt.d_options->lazyDefinitionExpansion) {
+ if(!smt.d_lazyDefinitionExpansion) {
Node node = expandDefinitions(smt, n);
Debug("expand") << "have: " << n << endl
<< "made: " << node << endl;
}
void SmtEngine::ensureBoolean(const BoolExpr& e) {
- Type type = e.getType(true);
+ Type type = e.getType(d_typeChecking);
Type boolType = d_exprManager->booleanType();
if(type != boolType) {
stringstream ss;
Expr SmtEngine::simplify(const Expr& e) {
Assert(e.getExprManager() == d_exprManager);
NodeManagerScope nms(d_nodeManager);
- e.getType(true);// ensure expr is type-checked at this point
+ if( d_typeChecking ) {
+ e.getType(true);// ensure expr is type-checked at this point
+ }
Debug("smt") << "SMT simplify(" << e << ")" << endl;
Unimplemented();
}
Expr SmtEngine::getValue(const Expr& e)
throw(ModalException, AssertionException) {
Assert(e.getExprManager() == d_exprManager);
- Type type = e.getType(true);// ensure expr is type-checked at this point
+ Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point
Debug("smt") << "SMT getValue(" << e << ")" << endl;
- if(!d_options->interactive) {
+ if(!d_interactive) {
const char* msg =
"Cannot get value when not in interactive mode.";
throw ModalException(msg);
}
- if(!d_options->produceModels) {
+ if(!d_produceModels) {
const char* msg =
"Cannot get value when produce-models options is off.";
throw ModalException(msg);
Node resultNode = d_theoryEngine->getValue(n);
// type-check the result we got
- Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType());
+ Assert(resultNode.isNull() || resultNode.getType() == eNode.getType());
return Expr(d_exprManager, new Node(resultNode));
}
bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Type type = e.getType(true);
+ Type type = e.getType(d_typeChecking);
// must be Boolean
CheckArgument( type.isBoolean(), e,
"expected Boolean-typed variable or function application "
n.getMetaKind() == kind::metakind::VARIABLE ), e,
"expected variable or defined-function application "
"in addToAssignment(),\ngot %s", e.toString().c_str() );
- if(!d_options->produceAssignments) {
+ if(!d_produceAssignments) {
return false;
}
if(d_assignments == NULL) {
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Debug("smt") << "SMT getAssignment()" << endl;
- if(!d_options->produceAssignments) {
+ if(!d_produceAssignments) {
const char* msg =
"Cannot get the current assignment when "
"produce-assignments option is off.";
Node resultNode = d_theoryEngine->getValue(n);
// type-check the result we got
- Assert(resultNode.isNull() || resultNode.getType(true) == boolType);
+ Assert(resultNode.isNull() || resultNode.getType() == boolType);
vector<SExpr> v;
if((*i).getKind() == kind::APPLY) {
vector<Expr> SmtEngine::getAssertions()
throw(ModalException, AssertionException) {
Debug("smt") << "SMT getAssertions()" << endl;
- if(!d_options->interactive) {
+ if(!d_interactive) {
const char* msg =
"Cannot query the current assertion list when not in interactive mode.";
throw ModalException(msg);
#include "util/hash.h"
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
+#include "smt/options.h"
#include "smt/bad_option_exception.h"
// In terms of abstraction, this is below (and provides services to)
typedef NodeTemplate<false> TNode;
class NodeHashFunction;
class Command;
-class Options;
class TheoryEngine;
class DecisionEngine;
/** Out internal expression/node manager */
NodeManager* d_nodeManager;
/** User-level options */
- const Options* d_options;
+ //const Options d_options;
/** The decision engine */
DecisionEngine* d_decisionEngine;
/** The decision engine */
*/
bool d_haveAdditions;
+ /**
+ * Whether or not to type check input expressions.
+ */
+ bool d_typeChecking;
+
+ /**
+ * Whether we're being used in an interactive setting.
+ */
+ bool d_interactive;
+
+ /**
+ * Whether we expand function definitions lazily.
+ */
+ bool d_lazyDefinitionExpansion;
+
+ /**
+ * Whether getValue() is enabled.
+ */
+ bool d_produceModels;
+
+ /**
+ * Whether getAssignment() is enabled.
+ */
+ bool d_produceAssignments;
+
/**
* Most recent result of last checkSat/query or (set-info :status).
*/
Result d_status;
+ /** Called by the constructors to setup fields. */
+ void init(const Options& opts) throw();
+
/**
* This is called by the destructor, just before destroying the
* PropEngine, TheoryEngine, and DecisionEngine (in that order). It
public:
+ /**
+ * Construct an SmtEngine with the given expression manager.
+ */
+ SmtEngine(ExprManager* em) throw();
+
/**
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager* em, const Options* opts) throw();
+ SmtEngine(ExprManager* em, const Options& opts) throw();
/**
* Destruct the SMT engine.
*/
void pop();
+ /** Enable type checking. Forces a type check on any Expr parameter
+ to an SmtEngine method. */
+ void enableTypeChecking() { d_typeChecking = true; }
+
+ /** Disable type checking. */
+ void disableTypeChecking() { d_typeChecking = false; }
+
};/* class SmtEngine */
}/* CVC4 namespace */
}
}
-TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
+TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
d_propEngine(NULL),
d_theoryOut(this, ctxt),
d_hasShutDown(false),
d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
- switch(opts->uf_implementation) {
+ switch(opts.uf_implementation) {
case Options::TIM:
d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
break;
d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
break;
default:
- Unhandled(opts->uf_implementation);
+ Unhandled(opts.uf_implementation);
}
d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
#define __CVC4__THEORY_ENGINE_H
#include "expr/node.h"
-#include "theory/theory.h"
-#include "theory/theoryof_table.h"
#include "prop/prop_engine.h"
+#include "smt/options.h"
#include "theory/shared_term_manager.h"
+#include "theory/theory.h"
+#include "theory/theoryof_table.h"
#include "util/stats.h"
namespace CVC4 {
/**
* Construct a theory engine.
*/
- TheoryEngine(context::Context* ctxt, const Options* opts);
+ TheoryEngine(context::Context* ctxt, const Options& opts);
/**
* Destroy a theory engine.
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
- d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
+ d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
}
void tearDown() {
d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
// create the TheoryEngine
- d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
+ d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
// insert our fake versions into the TheoryEngine's theoryOf table
d_theoryEngine->d_theoryOfTable.
projects / cvc5.git / commitdiff