diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
commit | e63abd23b45a078a42cafb277a4817abb4d044a1 (patch) | |
tree | 43b8aaccc9b49887280e0c77471c5346eb1cf9c4 /src/smt | |
parent | fccdb4cbe2cde7c34e82f33e9de850a046fef888 (diff) |
* (define-fun...) now has proper type checking in non-debug builds
(resolves bug #212)
* also closed some other type checking loopholes in SmtEngine
* small fixes to define-sort (resolves bug #214)
* infrastructural support for printing expressions in languages
other than the internal representation language using an IO
manipulator, e.g.:
cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;
main() sets the output language for all streams to correspond to
the input language
* support delaying type checking in debug builds, so that one can debug
the type checker itself (before it was difficult, because debug builds did
all the type checking on Node creation!): new command-line flag
--no-early-type-checking (only makes sense for debug builds)
* disallowed copy-construction of ExprManager and NodeManager, and made other
constructors explicit; previously it was easy to unintentionally create
duplicate managers, with really weird results (i.e., disappearing
attributes!)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 29 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 |
2 files changed, 30 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fc2c8550e..de2fa4ebc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -199,11 +199,12 @@ void SmtEngine::defineFunction(Expr func, Type formulaType = formula.getType(true);// type check body if(formulaType != FunctionType(func.getType()).getRangeType()) { stringstream ss; - ss << "Defined function's declared type does not match type of body\n" - << "The function: " << func << "\n" - << "Its type : " << func.getType() << "\n" - << "The body : " << formula << "\n" - << "Body type : " << formulaType << "\n"; + ss << "Defined function's declared type does not match that of body\n" + << "The function : " << func << "\n" + << "Its range type: " + << FunctionType(func.getType()).getRangeType() << "\n" + << "The body : " << formula << "\n" + << "Body type : " << formulaType; throw TypeCheckingException(func, ss.str()); } TNode funcNode = func.getTNode(); @@ -305,9 +306,22 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } +void SmtEngine::ensureBoolean(const BoolExpr& e) { + Type type = e.getType(true); + Type boolType = d_exprManager->booleanType(); + if(type != boolType) { + stringstream ss; + ss << "Expected " << boolType << "\n" + << "The assertion : " << e << "\n" + << "Its type : " << type; + throw TypeCheckingException(e, ss.str()); + } +} + Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << endl; + ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; @@ -317,6 +331,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << endl; + ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; @@ -326,12 +341,14 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT assertFormula(" << e << ")" << endl; + ensureBoolean(e);// type check node SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { NodeManagerScope nms(d_nodeManager); + e.getType(true);// ensure expr is type-checked at this point Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } @@ -352,6 +369,8 @@ Expr SmtEngine::getValue(Expr term) // assertions NodeManagerScope nms(d_nodeManager); + Type type = term.getType(true);// ensure expr is type-checked at this point + SmtEnginePrivate::preprocess(*this, term.getNode()); Unimplemented(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index fd132a0c6..1fd68d2a5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -132,6 +132,12 @@ class CVC4_PUBLIC SmtEngine { */ Result quickCheck(); + /** + * Fully type-check the argument, and also type-check that it's + * actually Boolean. + */ + void ensureBoolean(const BoolExpr& e); + friend class ::CVC4::smt::SmtEnginePrivate; public: |