summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/options.h4
-rw-r--r--src/smt/smt_engine.cpp74
-rw-r--r--src/smt/smt_engine.h46
3 files changed, 90 insertions, 34 deletions
diff --git a/src/smt/options.h b/src/smt/options.h
index 7ddaf5d4d..73c38545f 100644
--- a/src/smt/options.h
+++ b/src/smt/options.h
@@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options {
/** 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;
@@ -109,6 +112,7 @@ struct CVC4_PUBLIC Options {
interactiveSetByUser(false),
produceModels(false),
produceAssignments(false),
+ typeChecking(true),
earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
}
};/* struct Options */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2f2fba848..d76a002e7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -111,21 +111,20 @@ public:
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);
@@ -133,15 +132,26 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
// 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() {
@@ -299,7 +309,7 @@ void SmtEngine::defineFunction(Expr func,
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;
@@ -388,7 +398,7 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n)
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;
@@ -416,7 +426,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
}
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;
@@ -468,7 +478,9 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
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();
}
@@ -476,14 +488,14 @@ Expr SmtEngine::simplify(const Expr& e) {
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);
@@ -510,13 +522,13 @@ Expr SmtEngine::getValue(const Expr& e)
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 "
@@ -530,7 +542,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
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) {
@@ -543,7 +555,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
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.";
@@ -576,7 +588,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
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) {
@@ -595,7 +607,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
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);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a3116dfa9..0831a0447 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -34,6 +34,7 @@
#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)
@@ -47,7 +48,6 @@ typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
class NodeHashFunction;
class Command;
-class Options;
class TheoryEngine;
class DecisionEngine;
@@ -99,7 +99,7 @@ class CVC4_PUBLIC SmtEngine {
/** 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 */
@@ -126,11 +126,39 @@ class CVC4_PUBLIC SmtEngine {
*/
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
@@ -163,9 +191,14 @@ class CVC4_PUBLIC SmtEngine {
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.
@@ -273,6 +306,13 @@ public:
*/
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback