[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
]
)
*/
class CVC4_PUBLIC TypeCheckingException : public Exception {
+ friend class SmtEngine;
+
private:
/** The expression responsible for the error */
private:
- /** The node repsonsible for the failure */
+ /** The node responsible for the failure */
NodeTemplate<true>* d_node;
protected:
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]);
UF_THEORY,
LAZY_DEFINITION_EXPANSION,
INTERACTIVE,
- NO_INTERACTIVE
+ NO_INTERACTIVE,
+ PRODUCE_MODELS,
+ PRODUCE_ASSIGNMENTS
};/* enum OptionValue */
/**
{ "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! */
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");
--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 */
--- /dev/null
+/********************* */
+/*! \file modal_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an interactive-only
+ ** feature while CVC4 is being used in a non-interactive setting
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__MODAL_EXCEPTION_H
+#define __CVC4__SMT__MODAL_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC ModalException : public CVC4::Exception {
+public:
+ ModalException() :
+ Exception("Feature used while operating in "
+ "incorrect state") {
+ }
+
+ ModalException(const std::string& msg) :
+ Exception(msg) {
+ }
+
+ ModalException(const char* msg) :
+ Exception(msg) {
+ }
+};/* class ModalException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */
+++ /dev/null
-/********************* */
-/*! \file noninteractive_exception.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an interactive-only
- ** feature while CVC4 is being used in a non-interactive setting
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
-#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception {
-public:
- NoninteractiveException() :
- Exception("Interactive feature used while operating in "
- "non-interactive mode") {
- }
-
- NoninteractiveException(const std::string& msg) :
- Exception(msg) {
- }
-
- NoninteractiveException(const char* msg) :
- Exception(msg) {
- }
-};/* class NoninteractiveException */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */
#include <string>
#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"
const vector<Expr>& 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<Node> formalsNodes;
for(vector<Expr>::const_iterator i = formals.begin(),
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<Expr> SmtEngine::getAssertions() throw(NoninteractiveException) {
+vector<Expr> 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<Expr>(d_assertionList->begin(), d_assertionList->end());
#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"
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<Expr> getAssertions() throw(NoninteractiveException);
+ std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
/**
* Push a user-level context.
*/
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),
strictParsing(false),
lazyDefinitionExpansion(false),
interactive(false),
- interactiveSetByUser(false) {
+ interactiveSetByUser(false),
+ produceModels(false),
+ produceAssignments(false) {
}
};/* struct Options */
(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)
projects / cvc5.git / commitdiff