From b63e4a11733051728397f7d4ecb3b205fbd81dab Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 7 Oct 2010 22:54:43 +0000 Subject: [PATCH] type checking for define-fun in production builds; related to (and might resolve) bug 212 --- configure.ac | 4 +- src/expr/expr_template.h | 2 + src/expr/node.h | 2 +- src/expr/node_manager.h | 14 +++--- src/main/getopt.cpp | 14 +++++- src/main/usage.h | 8 +++- ...eractive_exception.h => modal_exception.h} | 22 +++++----- src/smt/smt_engine.cpp | 44 +++++++++++++++---- src/smt/smt_engine.h | 14 +++--- src/util/options.h | 10 ++++- .../regress0/simple-rdl-definefun.smt2 | 2 +- 11 files changed, 93 insertions(+), 43 deletions(-) rename src/smt/{noninteractive_exception.h => modal_exception.h} (65%) diff --git a/configure.ac b/configure.ac index d2033ac1f..ced90d56f 100644 --- a/configure.ac +++ b/configure.ac @@ -228,10 +228,10 @@ if test $cvc4_use_cln = 1; then [cvc4_use_cln=1], [if test $cvc4_use_cln = 0; then # fall back to GMP - AC_MSG_NOTICE([CLN not installed (or too old), will use gmp]) + AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp]) else # fail - AC_MSG_ERROR([CLN not installed (or too old)]) + AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing]) fi ] ) diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index bb227f92f..29164ffa5 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -60,6 +60,8 @@ namespace expr { */ class CVC4_PUBLIC TypeCheckingException : public Exception { + friend class SmtEngine; + private: /** The expression responsible for the error */ diff --git a/src/expr/node.h b/src/expr/node.h index bd6b53522..871f1e0d7 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -53,7 +53,7 @@ class TypeCheckingExceptionPrivate : public Exception { private: - /** The node repsonsible for the failure */ + /** The node responsible for the failure */ NodeTemplate* d_node; protected: diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c0f489d7a..0860365bc 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -789,15 +789,11 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, constructor.getNumChildren() == 0, "expected a sort constructor"); Assert(children.size() > 0, "expected non-zero # of children"); - uint64_t arity; - std::string name; - bool hasArityAttribute = - getAttribute(constructor.d_nv, expr::SortArityAttr(), arity); - Assert(hasArityAttribute, "expected a sort constructor"); - bool hasNameAttribute = - getAttribute(constructor.d_nv, expr::VarNameAttr(), name); - Assert(hasNameAttribute, "expected a sort constructor"); - Assert(arity == children.size(), + Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) && + hasAttribute(constructor.d_nv, expr::VarNameAttr()), + "expected a sort constructor" ); + std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); + Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(), "arity mismatch in application of sort constructor"); NodeBuilder<> nb(this, kind::SORT_TYPE); Node sortTag = Node(constructor.d_nv->d_children[0]); diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 82214bed3..113b8a5f7 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -73,7 +73,9 @@ enum OptionValue { UF_THEORY, LAZY_DEFINITION_EXPANSION, INTERACTIVE, - NO_INTERACTIVE + NO_INTERACTIVE, + PRODUCE_MODELS, + PRODUCE_ASSIGNMENTS };/* enum OptionValue */ /** @@ -123,6 +125,8 @@ static struct option cmdlineOptions[] = { { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, + { "produce-models", no_argument , NULL, PRODUCE_MODELS}, + { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS}, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -288,6 +292,14 @@ throw(OptionException) { opts->interactiveSetByUser = true; break; + case PRODUCE_MODELS: + opts->produceModels = true; + break; + + case PRODUCE_ASSIGNMENTS: + opts->produceAssignments = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/main/usage.h b/src/main/usage.h index 2be5f092e..15a30a426 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -46,8 +46,12 @@ CVC4 options:\n\ --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ - --uf=morgan|tim select uninterpreted function theory implementation\n" -; + --uf=morgan|tim select uninterpreted function theory implementation\n\ + --interactive run interactively\n\ + --no-interactive do not run interactively\n\ + --produce-models support the get-value command\n\ + --produce-assignments support the get-assignment command\n\ + --lazy-definition-expansion expand define-fun lazily\n"; }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/smt/noninteractive_exception.h b/src/smt/modal_exception.h similarity index 65% rename from src/smt/noninteractive_exception.h rename to src/smt/modal_exception.h index 4cf97ab3e..c5c0f6ab2 100644 --- a/src/smt/noninteractive_exception.h +++ b/src/smt/modal_exception.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file noninteractive_exception.h +/*! \file modal_exception.h ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -21,29 +21,29 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H -#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H +#ifndef __CVC4__SMT__MODAL_EXCEPTION_H +#define __CVC4__SMT__MODAL_EXCEPTION_H #include "util/exception.h" namespace CVC4 { -class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception { +class CVC4_PUBLIC ModalException : public CVC4::Exception { public: - NoninteractiveException() : - Exception("Interactive feature used while operating in " - "non-interactive mode") { + ModalException() : + Exception("Feature used while operating in " + "incorrect state") { } - NoninteractiveException(const std::string& msg) : + ModalException(const std::string& msg) : Exception(msg) { } - NoninteractiveException(const char* msg) : + ModalException(const char* msg) : Exception(msg) { } -};/* class NoninteractiveException */ +};/* class ModalException */ }/* CVC4 namespace */ -#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */ +#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c41737028..5bf5ebd69 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -20,7 +20,7 @@ #include #include "smt/smt_engine.h" -#include "smt/noninteractive_exception.h" +#include "smt/modal_exception.h" #include "smt/bad_option_exception.h" #include "smt/no_such_function_exception.h" #include "context/context.h" @@ -191,6 +191,16 @@ void SmtEngine::defineFunction(Expr func, const vector& formals, Expr formula) { NodeManagerScope nms(d_nodeManager); + 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"; + throw TypeCheckingException(func, ss.str()); + } TNode funcNode = func.getTNode(); vector formalsNodes; for(vector::const_iterator i = formals.begin(), @@ -321,29 +331,45 @@ Expr SmtEngine::simplify(const Expr& e) { Unimplemented(); } -Model SmtEngine::getModel() { +Expr SmtEngine::getValue(Expr term) + throw(ModalException, AssertionException) { + if(!d_options->interactive) { + const char* msg = + "Cannot get value when not in interactive mode."; + throw ModalException(msg); + } + if(!d_options->produceModels) { + const char* msg = + "Cannot get value when produce-models options is off."; + throw ModalException(msg); + } + // TODO also check that the last query was sat/unknown, without intervening + // assertions + NodeManagerScope nms(d_nodeManager); + Unimplemented(); } -Expr SmtEngine::getValue(Expr term) - throw(NoninteractiveException, AssertionException) { - if(!d_options->interactive) { +SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { + if(!d_options->produceAssignments) { const char* msg = - "Cannot query the current assertion list when not in interactive mode."; - throw NoninteractiveException(msg); + "Cannot get the current assignment when produce-assignments option is off."; + throw ModalException(msg); } + // TODO also check that the last query was sat/unknown, without intervening + // assertions NodeManagerScope nms(d_nodeManager); Unimplemented(); } -vector SmtEngine::getAssertions() throw(NoninteractiveException) { +vector SmtEngine::getAssertions() throw(ModalException, AssertionException) { if(!d_options->interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; - throw NoninteractiveException(msg); + throw ModalException(msg); } Assert(d_assertionList != NULL); return vector(d_assertionList->begin(), d_assertionList->end()); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c9bf321b9..fd132a0c6 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -30,7 +30,7 @@ #include "util/model.h" #include "util/sexpr.h" #include "util/hash.h" -#include "smt/noninteractive_exception.h" +#include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" #include "smt/bad_option_exception.h" @@ -207,22 +207,24 @@ public: Expr simplify(const Expr& e); /** - * Get a (counter)model (only if preceded by a SAT or INVALID query). + * Get the assigned value of a term (only if preceded by a SAT or + * INVALID query). Only permitted if the SmtEngine is set to + * operate interactively and produce-models is on. */ - Model getModel(); + Expr getValue(Expr term) throw(ModalException, AssertionException); /** * Get the assigned value of a term (only if preceded by a SAT or * INVALID query). Only permitted if the SmtEngine is set to - * operate interactively. + * operate interactively and produce-assignments is on. */ - Expr getValue(Expr term) throw(NoninteractiveException, AssertionException); + SExpr getAssignment() throw(ModalException, AssertionException); /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ - std::vector getAssertions() throw(NoninteractiveException); + std::vector getAssertions() throw(ModalException, AssertionException); /** * Push a user-level context. diff --git a/src/util/options.h b/src/util/options.h index 9bb0b0a38..08de590d8 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -77,6 +77,12 @@ struct CVC4_PUBLIC Options { */ bool interactiveSetByUser; + /** Whether we support SmtEngine::getValue() for this run. */ + bool produceModels; + + /** Whether we support SmtEngine::getAssignment() for this run. */ + bool produceAssignments; + Options() : binary_name(), statistics(false), @@ -91,7 +97,9 @@ struct CVC4_PUBLIC Options { strictParsing(false), lazyDefinitionExpansion(false), interactive(false), - interactiveSetByUser(false) { + interactiveSetByUser(false), + produceModels(false), + produceAssignments(false) { } };/* struct Options */ diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2 index 08e99867a..c04a1ed64 100644 --- a/test/regress/regress0/simple-rdl-definefun.smt2 +++ b/test/regress/regress0/simple-rdl-definefun.smt2 @@ -7,7 +7,7 @@ (define-sort F (x) (A Real Real)) (declare-fun x2 () (F Real)) (define-fun minus ((x Real) (z Real)) Real (- x z)) -(define-fun less ((x Real) (z Real)) Bool (< x z)) +(define-fun less ((x Real) (z Real)) Real (< x z)) (define-fun foo ((x Real) (z Real)) Bool (less x z)) (assert (not (=> (foo (minus x y) 0) (less x y)))) (check-sat) -- 2.30.2