}
/**
- * Remove all attributes from the table calling the cleanup function if one is defined.
+ * Remove all attributes from the table calling the cleanup function
+ * if one is defined.
*/
template <class T>
inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
}
}
- if(anyRequireClearing){
+ if(anyRequireClearing) {
typename hash_t::iterator it = table.begin();
typename hash_t::iterator it_end = table.end();
return instantiation;
} else {
- Assert(p.second.isSort());
if(Debug.isOn("sort")) {
Debug("sort") << "instantiating using a sort substitution" << endl;
Debug("sort") << "have formals [";
namespace CVC4 {
-ExprManager::ExprManager() :
+ExprManager::ExprManager(bool earlyTypeChecking) :
d_ctxt(new Context),
- d_nodeManager(new NodeManager(d_ctxt)) {
+ d_nodeManager(new NodeManager(d_ctxt, earlyTypeChecking)) {
}
ExprManager::~ExprManager() {
try {
return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
child1.getNode(),
child2.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
- e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
child2.getNode(),
child3.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
- e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
child3.getNode(),
child4.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
- e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
child4.getNode(),
child5.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
- e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
try {
return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
- e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
try {
return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+ throw TypeCheckingException(this, &e);
}
}
NodeManagerScope nms(d_nodeManager);
Type t;
try {
- t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode(), check)));
+ t = Type(d_nodeManager,
+ new TypeNode(d_nodeManager->getType(e.getNode(), check)));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+ throw TypeCheckingException(this, &e);
}
return t;
}
Expr ExprManager::mkVar(const std::string& name, const Type& type) {
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
+ Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+ Debug("nm") << "set " << name << " on " << *n << std::endl;
+ return Expr(this, n);
}
Expr ExprManager::mkVar(const Type& type) {
/** ExprManagerScope reaches in to get the NodeManager */
friend class ExprManagerScope;
+ // undefined, private copy constructor (disallow copy)
+ ExprManager(const ExprManager&);
+
public:
/**
* Creates an expression manager.
+ * @param earlyTypeChecking whether to do type checking early (at Expr
+ * creation time); only used in debug builds---for other builds, type
+ * checking is never done early.
*/
- ExprManager();
+ explicit ExprManager(bool earlyTypeChecking = true);
/**
* Destroys the expression manager. No will be deallocated at this point, so
const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
+const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
}/* CVC4::expr namespace */
}
std::ostream& operator<<(std::ostream& out, const Expr& e) {
- e.toStream(out);
- return out;
+ ExprManagerScope ems(*e.getExprManager());
+ return out << e.getNode();
}
TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
{
}
+TypeCheckingException::TypeCheckingException(ExprManager* em,
+ const TypeCheckingExceptionPrivate* exc)
+: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode())))
+{
+}
+
TypeCheckingException::~TypeCheckingException() throw () {
delete d_expr;
}
return d_node->isConst();
}
-void Expr::toStream(std::ostream& out, int depth, bool types) const {
+void Expr::toStream(std::ostream& out, int depth, bool types,
+ OutputLanguage language) const {
ExprManagerScope ems(*this);
- d_node->toStream(out, depth, types);
+ d_node->toStream(out, depth, types, language);
}
Node Expr::getNode() const throw() {
#include <stdint.h>
#include "util/exception.h"
+#include "util/language.h"
${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
namespace CVC4 {
class ExprManager;
class SmtEngine;
class Type;
+class TypeCheckingException;
+class TypeCheckingExceptionPrivate;
namespace smt {
class SmtEnginePrivate;
namespace expr {
class CVC4_PUBLIC ExprSetDepth;
class CVC4_PUBLIC ExprPrintTypes;
+ class CVC4_PUBLIC ExprSetLanguage;
}/* CVC4::expr namespace */
/**
class CVC4_PUBLIC TypeCheckingException : public Exception {
friend class SmtEngine;
+ friend class smt::SmtEnginePrivate;
private:
protected:
- TypeCheckingException(): Exception() {}
+ TypeCheckingException() : Exception() {}
TypeCheckingException(const Expr& expr, std::string message);
+ TypeCheckingException(ExprManager* em,
+ const TypeCheckingExceptionPrivate* exc);
public:
std::ostream& operator<<(std::ostream& out,
const TypeCheckingException& e) CVC4_PUBLIC;
+/**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
/**
* Class encapsulating CVC4 expressions and methods for constructing new
* expressions.
* type checking is not requested, getType() will do the minimum
* amount of checking required to return a valid result.
*
- * @param check whether we should check the type as we compute it
+ * @param check whether we should check the type as we compute it
* (default: false)
*/
Type getType(bool check = false) const throw (TypeCheckingException);
* Outputs the string representation of the expression to the stream.
* @param out the output stream
*/
- void toStream(std::ostream& out, int depth = -1, bool types = false) const;
+ void toStream(std::ostream& out, int depth = -1, bool types = false,
+ OutputLanguage lang = language::output::LANG_AST) const;
/**
* Check if this is a null expression.
*/
typedef expr::ExprPrintTypes printtypes;
+ /**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+ typedef expr::ExprSetLanguage setlanguage;
+
/**
* Very basic pretty printer for Expr.
* This is equivalent to calling e.getNode().printAst(...)
friend class SmtEngine;
friend class smt::SmtEnginePrivate;
friend class ExprManager;
-};
+ friend class TypeCheckingException;
+ friend std::ostream& operator<<(std::ostream& out, const Expr& e);
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+};/* class Expr */
/**
* Extending the expression with the capability to construct Boolean
static inline void setDepth(std::ostream& out, long depth) {
out.iword(s_iosIndex) = depth;
}
-};
+};/* class ExprSetDepth */
/**
* IOStream manipulator to print type ascriptions or not.
}
};/* class ExprPrintTypes */
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC ExprSetLanguage {
+ /**
+ * The allocated index in ios_base for our depth setting.
+ */
+ static const int s_iosIndex;
+
+ /**
+ * The default language to use, for ostreams that haven't yet had a
+ * setlanguage() applied to them.
+ */
+ static const int s_defaultLanguage = language::output::LANG_AST;
+
+ /**
+ * When this manipulator is used, the setting is stored here.
+ */
+ OutputLanguage d_language;
+
+public:
+ /**
+ * Construct a ExprSetLanguage with the given setting.
+ */
+ ExprSetLanguage(OutputLanguage l) : d_language(l) {}
+
+ inline void applyLanguage(std::ostream& out) {
+ out.iword(s_iosIndex) = int(d_language);
+ }
+
+ static inline OutputLanguage getLanguage(std::ostream& out) {
+ return OutputLanguage(out.iword(s_iosIndex));
+ }
+
+ static inline void setLanguage(std::ostream& out, OutputLanguage l) {
+ out.iword(s_iosIndex) = int(l);
+ }
+};/* class ExprSetLanguage */
+
}/* CVC4::expr namespace */
${getConst_instantiations}
-#line 566 "${template}"
+#line 659 "${template}"
namespace expr {
return out;
}
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ * // let out be an ostream, e an Expr
+ * out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
+ l.applyLanguage(out);
+ return out;
+}
+
}/* CVC4::expr namespace */
// for hash_maps, hash_sets..
operatorKind=$1
applyKind=$2
metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind;
-";
+";
}
function register_metakind {
#include "util/Assert.h"
#include "util/configuration.h"
#include "util/output.h"
+#include "util/exception.h"
+#include "util/language.h"
namespace CVC4 {
protected:
- TypeCheckingExceptionPrivate(): Exception() {}
+ TypeCheckingExceptionPrivate() : Exception() {}
public:
/**
* Converst this node into a string representation and sends it to the
* given stream
- * @param out the sream to serialise this node to
+ * @param out the stream to serialize this node to
*/
- inline void toStream(std::ostream& out, int toDepth = -1,
- bool types = false) const {
+ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+ OutputLanguage language = language::output::LANG_AST) const {
assertTNodeNotExpired();
- d_nv->toStream(out, toDepth, types);
+ d_nv->toStream(out, toDepth, types, language);
}
/**
*/
typedef expr::ExprPrintTypes printtypes;
+ /**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+ typedef expr::ExprSetLanguage setlanguage;
+
/**
* Very basic pretty printer for Node.
* @param o output stream to print to.
inline std::ostream& operator<<(std::ostream& out, TNode n) {
n.toStream(out,
Node::setdepth::getDepth(out),
- Node::printtypes::getPrintTypes(out));
+ Node::printtypes::getPrintTypes(out),
+ Node::setlanguage::getLanguage(out));
return out;
}
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 ) {
+ if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) {
kind::MetaKind mk = n.getMetaKind();
if( mk != kind::metakind::VARIABLE
&& mk != kind::metakind::CONSTANT ) {
- d_nm->getType(n,true);
+ d_nm->getType(n, true);
}
}
}
operator Node();
operator Node() const;
- inline void toStream(std::ostream& out, int depth = -1,
- bool types = false) const {
+ inline void toStream(std::ostream& out, int depth = -1, bool types = false,
+ OutputLanguage language = language::output::LANG_AST) const {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
"attempt to access it after conversion");
- d_nv->toStream(out, depth, types);
+ d_nv->toStream(out, depth, types, language);
}
NodeBuilder<nchild_thresh>& operator&=(TNode);
};
-NodeManager::NodeManager(context::Context* ctxt) :
+NodeManager::NodeManager(context::Context* ctxt, bool earlyTypeChecking) :
d_attrManager(ctxt),
d_nodeUnderDeletion(NULL),
- d_inReclaimZombies(false) {
+ d_inReclaimZombies(false),
+ d_earlyTypeChecking(earlyTypeChecking) {
poolInsert( &expr::NodeValue::s_null );
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
*/
Node d_operators[kind::LAST_KIND];
+ /**
+ * Whether to do early type checking (only effective in debug
+ * builds; other builds never do early type checking.
+ */
+ const bool d_earlyTypeChecking;
+
/**
* Look up a NodeValue in the pool associated to this NodeManager.
* The NodeValue argument need not be a "completely-constructed"
// bool containsDecision(TNode); // is "atomic"
// bool properlyContainsDecision(TNode); // all children are atomic
+ // undefined private copy constructor (disallow copy)
+ NodeManager(const NodeManager&);
+
public:
- NodeManager(context::Context* ctxt);
+ explicit NodeManager(context::Context* ctxt, bool earlyTypeChecking = true);
~NodeManager();
/** The node manager in the current context. */
#include "expr/node.h"
#include "expr/kind.h"
#include "expr/metakind.h"
+#include "util/language.h"
#include <sstream>
using namespace std;
return ss.str();
}
-void NodeValue::toStream(std::ostream& out, int toDepth, bool types) const {
- using namespace CVC4::kind;
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
+ OutputLanguage language) const {
using namespace CVC4;
+ using namespace CVC4::kind;
+ using namespace CVC4::language::output;
- if(getKind() == kind::NULL_EXPR) {
- out << "null";
- } else if(getMetaKind() == kind::metakind::VARIABLE) {
- if(getKind() != kind::VARIABLE &&
- getKind() != kind::SORT_TYPE) {
- out << getKind() << ':';
- }
+ switch(language) {
+ case LANG_SMTLIB:
+ // FIXME support smt-lib output language
+ case LANG_SMTLIB_V2:
+ // FIXME support smt-lib v2 output language
+ case LANG_AST:
+ if(getKind() == kind::NULL_EXPR) {
+ out << "null";
+ } else if(getMetaKind() == kind::metakind::VARIABLE) {
+ if(getKind() != kind::VARIABLE &&
+ getKind() != kind::SORT_TYPE) {
+ out << getKind() << ':';
+ }
- string s;
- NodeManager* nm = NodeManager::currentNM();
+ string s;
+ NodeManager* nm = NodeManager::currentNM();
- // conceptually "this" is const, and hasAttribute() doesn't change
- // its argument, but it requires a non-const key arg (for now)
- if(nm->getAttribute(const_cast<NodeValue*>(this),
- VarNameAttr(), s)) {
- out << s;
- } else {
- out << "var_" << d_id;
- }
- if(types) {
- // print the whole type, but not *its* type
- out << ":";
- nm->getType(TNode(this)).toStream(out, -1, false);
- }
- } else {
- out << '(' << Kind(d_kind);
- if(getMetaKind() == kind::metakind::CONSTANT) {
- out << ' ';
- kind::metakind::NodeValueConstPrinter::toStream(out, this);
+ // conceptually "this" is const, and hasAttribute() doesn't change
+ // its argument, but it requires a non-const key arg (for now)
+ if(nm->getAttribute(const_cast<NodeValue*>(this),
+ VarNameAttr(), s)) {
+ out << s;
+ } else {
+ out << "var_" << d_id << "[" << this << "]";
+ }
+ if(types) {
+ // print the whole type, but not *its* type
+ out << ":";
+ nm->getType(TNode(this)).toStream(out, -1, false, language);
+ }
} else {
- for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
- if(i != nv_end()) {
- out << ' ';
- }
- if(toDepth != 0) {
- (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types);
- } else {
- out << "(...)";
+ out << '(' << Kind(d_kind);
+ if(getMetaKind() == kind::metakind::CONSTANT) {
+ out << ' ';
+ kind::metakind::NodeValueConstPrinter::toStream(out, this);
+ } else {
+ for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+ if(i != nv_end()) {
+ out << ' ';
+ }
+ if(toDepth != 0) {
+ (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+ types, language);
+ } else {
+ out << "(...)";
+ }
}
}
+ out << ')';
}
- out << ')';
- }
+ break;
+
+ default:
+ out << "[output language " << language << " unsupported]";
+ }// end switch(language)
}
void NodeValue::printAst(std::ostream& out, int ind) const {
#define __CVC4__EXPR__NODE_VALUE_H
#include "expr/kind.h"
+#include "util/language.h"
#include <stdint.h>
#include <string>
}
std::string toString() const;
- void toStream(std::ostream& out, int toDepth = -1, bool types = false) const;
+ void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+ OutputLanguage = language::output::LANG_AST) const;
static inline unsigned kindToDKind(Kind k) {
return ((unsigned) k) & kindMask;
namespace CVC4 {
-ostream& operator<<(ostream& out, const Type& e) {
- e.toStream(out);
- return out;
+ostream& operator<<(ostream& out, const Type& t) {
+ NodeManagerScope nms(t.d_nodeManager);
+ return out << *Type::getTypeNode(t);
}
Type Type::makeType(const TypeNode& typeNode) const {
return;
}
+string Type::toString() const {
+ NodeManagerScope nms(d_nodeManager);
+ stringstream ss;
+ ss << *d_typeNode;
+ return ss.str();
+}
+
/** Is this the Boolean type? */
bool Type::isBoolean() const {
NodeManagerScope nms(d_nodeManager);
static size_t hash(const CVC4::Type& t);
};/* struct TypeHashStrategy */
+/**
+ * Output operator for types
+ * @param out the stream to output to
+ * @param t the type to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+
/**
* Class encapsulating CVC4 expression types.
*/
friend class ExprManager;
friend class TypeNode;
friend class TypeHashStrategy;
+ friend std::ostream& operator<<(std::ostream& out, const Type& t);
protected:
* @param out the stream to output to
*/
void toStream(std::ostream& out) const;
-};
+
+ /**
+ * Constructs a string representation of this type.
+ */
+ std::string toString() const;
+};/* class Type */
/**
* Singleton class encapsulating the Boolean type.
/** Construct from the base type */
BooleanType(const Type& type) throw(AssertionException);
-};
+};/* class BooleanType */
/**
* Singleton class encapsulating the integer type.
/** Construct from the base type */
IntegerType(const Type& type) throw(AssertionException);
-};
+};/* class IntegerType */
/**
* Singleton class encapsulating the real type.
/** Construct from the base type */
RealType(const Type& type) throw(AssertionException);
-};
-
+};/* class RealType */
/**
* Class encapsulating a function type.
/** Get the range type (i.e., the type of the result). */
Type getRangeType() const;
-};
+};/* class FunctionType */
/**
* Class encapsulating a tuple type.
/** Get the constituent types */
std::vector<Type> getTypes() const;
-};
+};/* class TupleType */
/**
* Class encapsulating an array type.
/** Get the constituent type */
Type getConstituentType() const;
-};
+};/* class ArrayType */
/**
* Class encapsulating a user-defined sort.
/** Get the name of the sort */
std::string getName() const;
-};
+};/* class SortType */
/**
* Class encapsulating a user-defined sort constructor.
/** Instantiate a sort using this sort constructor */
SortType instantiate(const std::vector<Type>& params) const;
-};
+};/* class SortConstructorType */
/**
* Class encapsulating the kind type (the type of types).
/** Construct from the base type */
KindType(const Type& type) throw(AssertionException);
-};
-
+};/* class KindType */
/**
* Class encapsulating the bit-vector type.
* @return the width of the bit-vector type (> 0)
*/
unsigned getSize() const;
-};
-
-/**
- * Output operator for types
- * @param out the stream to output to
- * @param t the type to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
+};/* class BitVectorType */
}/* CVC4 namespace */
}
/**
- * Converst this node into a string representation and sends it to the
+ * Converts this node into a string representation and sends it to the
* given stream
*
- * @param out the sream to serialise this node to
+ * @param out the stream to serialize this node to
*/
- inline void toStream(std::ostream& out, int toDepth = -1,
- bool types = false) const {
- d_nv->toStream(out, toDepth, types);
+ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+ OutputLanguage language = language::output::LANG_AST) const {
+ d_nv->toStream(out, toDepth, types, language);
}
/**
#include "util/configuration.h"
#include "util/output.h"
#include "util/options.h"
-#include "parser/parser_options.h"
+#include "util/language.h"
#include "expr/expr.h"
#include "cvc4autoconfig.h"
INTERACTIVE,
NO_INTERACTIVE,
PRODUCE_MODELS,
- PRODUCE_ASSIGNMENTS
+ PRODUCE_ASSIGNMENTS,
+ NO_EARLY_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-early-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING},
{ NULL , no_argument , NULL, '\0' }
};/* if you add things to the above, please remember to update usage.h! */
case 'L':
if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
- opts->lang = parser::LANG_CVC4;
+ opts->inputLanguage = language::input::LANG_CVC4;
break;
} else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
- opts->lang = parser::LANG_SMTLIB;
+ opts->inputLanguage = language::input::LANG_SMTLIB;
break;
} else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
- opts->lang = parser::LANG_SMTLIB_V2;
+ opts->inputLanguage = language::input::LANG_SMTLIB_V2;
break;
} else if(!strcmp(optarg, "auto")) {
- opts->lang = parser::LANG_AUTO;
+ opts->inputLanguage = language::input::LANG_AUTO;
break;
}
opts->produceAssignments = true;
break;
+ case NO_EARLY_TYPE_CHECKING:
+ opts->earlyTypeChecking = false;
+ break;
+
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
- printf("version : %s\n", Configuration::getVersionString().c_str());
+ printf("version : %s\n", Configuration::getVersionString().c_str());
printf("\n");
- printf("library : %u.%u.%u\n",
+ printf("library : %u.%u.%u\n",
Configuration::getVersionMajor(),
Configuration::getVersionMinor(),
Configuration::getVersionRelease());
}
// Create the expression manager
- ExprManager exprMgr;
+ ExprManager exprMgr(options.earlyTypeChecking);
// Create the SmtEngine
SmtEngine smt(&exprMgr, &options);
ReferenceStat< const char* > s_statFilename("filename", filename);
StatisticsRegistry::registerStat(&s_statFilename);
- if(options.lang == parser::LANG_AUTO) {
+ if(options.inputLanguage == language::input::LANG_AUTO) {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- options.lang = parser::LANG_CVC4;
+ options.inputLanguage = language::input::LANG_CVC4;
} else {
unsigned len = strlen(filename);
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
- options.lang = parser::LANG_SMTLIB_V2;
+ options.inputLanguage = language::input::LANG_SMTLIB_V2;
} else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- options.lang = parser::LANG_SMTLIB;
+ options.inputLanguage = language::input::LANG_SMTLIB;
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- options.lang = parser::LANG_CVC4;
+ options.inputLanguage = language::input::LANG_CVC4;
}
}
}
Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
}
+
+ OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
+ Debug.getStream() << Expr::setlanguage(language);
+ Trace.getStream() << Expr::setlanguage(language);
+ Notice.getStream() << Expr::setlanguage(language);
+ Chat.getStream() << Expr::setlanguage(language);
+ Message.getStream() << Expr::setlanguage(language);
+ Warning.getStream() << Expr::setlanguage(language);
}
ParserBuilder parserBuilder =
ParserBuilder(exprMgr, filename)
- .withInputLanguage(options.lang)
+ .withInputLanguage(options.inputLanguage)
.withMmap(options.memoryMap)
.withChecks(options.semanticChecks &&
!Configuration::isMuzzledBuild() )
--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";
+ --lazy-definition-expansion expand define-fun lazily\n\
+ --no-early-type-checking don't typecheck at Expr creation [non-DEBUG builds never do]\n";
}/* CVC4::main namespace */
}/* CVC4 namespace */
}
AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) {
+ using namespace language::input;
+
AntlrInput* input;
switch(lang) {
ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) :
d_inputType(FILE_INPUT),
- d_lang(LANG_AUTO),
+ d_lang(language::input::LANG_AUTO),
d_filename(filename),
d_streamInput(NULL),
d_exprManager(exprManager),
Unreachable();
}
switch(d_lang) {
- case LANG_SMTLIB:
+ case language::input::LANG_SMTLIB:
return new Smt(&d_exprManager, input, d_strictMode);
- case LANG_SMTLIB_V2:
+ case language::input::LANG_SMTLIB_V2:
return new Smt2(&d_exprManager, input, d_strictMode);
default:
return new Parser(&d_exprManager, input, d_strictMode);
std::string d_filename;
unsigned long d_line;
unsigned long d_column;
-}; // end of class ParserException
+};/* class ParserException */
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#include <iostream>
+#include "util/language.h"
+
namespace CVC4 {
namespace parser {
-/** The input language option */
-enum InputLanguage {
- /** The SMTLIB input language */
- LANG_SMTLIB,
- /** The SMTLIB v2 input language */
- LANG_SMTLIB_V2,
- /** The CVC4 input language */
- LANG_CVC4,
- /** Auto-detect the language */
- LANG_AUTO
-};/* enum InputLanguage */
-
-inline std::ostream& operator<<(std::ostream& out, InputLanguage lang) {
- switch(lang) {
- case LANG_SMTLIB:
- out << "LANG_SMTLIB";
- break;
- case LANG_SMTLIB_V2:
- out << "LANG_SMTLIB_V2";
- break;
- case LANG_CVC4:
- out << "LANG_CVC4";
- break;
- case LANG_AUTO:
- out << "LANG_AUTO";
- break;
- default:
- out << "undefined_language";
- }
-
- return out;
-}
+// content moved to util/language.h
}/* CVC4::parser namespace */
}/* CVC4 namespace */
}
| /* assertion */
ASSERT_TOK term[expr]
- { cmd = new AssertCommand(expr); }
+ { cmd = new AssertCommand(expr); }
| /* checksat */
CHECKSAT_TOK
{ cmd = new CheckSatCommand(MK_CONST(true)); }
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();
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;
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;
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();
}
// assertions
NodeManagerScope nms(d_nodeManager);
+ Type type = term.getType(true);// ensure expr is type-checked at this point
+ SmtEnginePrivate::preprocess(*this, term.getNode());
Unimplemented();
}
*/
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:
stats.h \
stats.cpp \
triple.h \
- dynamic_array.h
+ dynamic_array.h \
+ language.h
BUILT_SOURCES = \
rational.h \
** information.\endverbatim
**
** \brief Implementation of Configuration class, which provides compile-time
- ** configuration information about the CVC4 library.
+ ** configuration information about the CVC4 library
**
** Implementation of Configuration class, which provides compile-time
** configuration information about the CVC4 library.
#endif /* TLS */
#define CVC4_ABOUT_STRING string("\
-This is a pre-release of CVC4.\n\
+This is CVC4 version " CVC4_RELEASE_STRING "\n\n\
Copyright (C) 2009, 2010\n\
The ACSys Group\n\
Courant Institute of Mathematical Sciences\n\
consult the CVC4 documentation for instructions about building a version\n\
of CVC4 that links against GMP, and can be used in such applications.\n" : \
"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n")
+CVC4 is open-source and is covered by the BSD license (modified).\n\n\
+THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n")
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file language.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 Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LANGUAGE_H
+#define __CVC4__LANGUAGE_H
+
+#include <sstream>
+#include <string>
+
+#include "util/exception.h"
+
+namespace CVC4 {
+namespace language {
+
+namespace input {
+
+enum Language {
+ // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
+
+ /** Auto-detect the language */
+ LANG_AUTO = -1,
+
+ // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+ // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
+ //
+ // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
+ // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
+ // INCLUDE IT HERE
+
+ /** The SMTLIB input language */
+ LANG_SMTLIB = 0,
+ /** The SMTLIB v2 input language */
+ LANG_SMTLIB_V2,
+ /** The CVC4 input language */
+ LANG_CVC4
+
+ // START INPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+ // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
+
+};/* enum Language */
+
+inline std::ostream& operator<<(std::ostream& out, Language lang) {
+ switch(lang) {
+ case LANG_SMTLIB:
+ out << "LANG_SMTLIB";
+ break;
+ case LANG_SMTLIB_V2:
+ out << "LANG_SMTLIB_V2";
+ break;
+ case LANG_CVC4:
+ out << "LANG_CVC4";
+ break;
+ case LANG_AUTO:
+ out << "LANG_AUTO";
+ break;
+ default:
+ out << "undefined_input_language";
+ }
+ return out;
+}
+
+}/* CVC4::language::input namespace */
+
+namespace output {
+
+enum Language {
+ // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
+
+ // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+ // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
+ //
+ // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
+ // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
+ // INCLUDE IT HERE
+
+ /** The SMTLIB output language */
+ LANG_SMTLIB = input::LANG_SMTLIB,
+ /** The SMTLIB v2 output language */
+ LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+ /** The CVC4 output language */
+ LANG_CVC4 = input::LANG_CVC4,
+
+ // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+ // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
+
+ /** The AST output language */
+ LANG_AST = 1000
+
+};/* enum Language */
+
+inline std::ostream& operator<<(std::ostream& out, Language lang) {
+ switch(lang) {
+ case LANG_SMTLIB:
+ out << "LANG_SMTLIB";
+ break;
+ case LANG_SMTLIB_V2:
+ out << "LANG_SMTLIB_V2";
+ break;
+ case LANG_CVC4:
+ out << "LANG_CVC4";
+ break;
+ case LANG_AST:
+ out << "LANG_AUTO";
+ break;
+ default:
+ out << "undefined_output_language";
+ }
+ return out;
+}
+
+}/* CVC4::language::output namespace */
+
+}/* CVC4::language namespace */
+
+typedef language::input::Language InputLanguage;
+typedef language::output::Language OutputLanguage;
+
+namespace language {
+
+inline OutputLanguage toOutputLanguage(InputLanguage language) {
+ switch(language) {
+ case input::LANG_SMTLIB:
+ case input::LANG_SMTLIB_V2:
+ case input::LANG_CVC4:
+ // these entries correspond
+ return OutputLanguage(int(language));
+
+ default: {
+ std::stringstream ss;
+ ss << "Cannot map input language `" << language
+ << "' to an output language.";
+ throw CVC4::Exception(ss.str());
+ }
+ }/* switch(language) */
+}/* toOutputLanguage() */
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LANGUAGE_H */
#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
+#ifdef CVC4_DEBUG
+# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
+#else /* CVC4_DEBUG */
+# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
+#endif /* CVC4_DEBUG */
+
#include <iostream>
#include <string>
-#include "parser/parser_options.h"
+#include "util/language.h"
namespace CVC4 {
int verbosity;
/** The input language */
- parser::InputLanguage lang;
+ InputLanguage inputLanguage;
/** Enumeration of UF implementation choices */
typedef enum { TIM, MORGAN } UfImplementation;
/** Whether we support SmtEngine::getAssignment() for this run. */
bool produceAssignments;
+ /** Whether we support SmtEngine::getAssignment() for this run. */
+ bool earlyTypeChecking;
+
Options() :
binary_name(),
statistics(false),
out(0),
err(0),
verbosity(0),
- lang(parser::LANG_AUTO),
+ inputLanguage(language::input::LANG_AUTO),
uf_implementation(MORGAN),
parseOnly(false),
semanticChecks(true),
interactive(false),
interactiveSetByUser(false),
produceModels(false),
- produceAssignments(false) {
+ produceAssignments(false),
+ earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
}
};/* struct Options */
}/* CVC4 namespace */
+#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+
#endif /* __CVC4__OPTIONS_H */
**
** \brief Similar to std::pair<>, for triples
**
- ** Similar to std::pair<>, for triples.
+ ** Similar to std::pair<>, for triples. Once we move to c++0x, this
+ ** can be removed in favor of (standard-provided) N-ary tuples.
**/
#include "cvc4_private.h"
(set-logic QF_RDL)
(set-info :status unsat)
+(set-info :notes | Simple test, based on simple-rdl.smt2, of define-sort and define-fun |)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-sort U 0)
-(declare-sort A 2)
-(define-sort F (x) (A Real Real))
+(define-sort A (x y) y)
+(define-sort F (x) (A x x))
(declare-fun x2 () (F Real))
-(define-fun minus ((x Real) (z Real)) Real (- x z))
+(define-fun minus ((x Real) (z Real)) (A (A U Bool) (A (F U) Real)) (- x z))
(define-fun less ((x Real) (z Real)) Bool (< x z))
-(define-fun foo ((x Real) (z Real)) Bool (less x z))
+(define-fun foo ((x (F Real)) (z (A U Real))) (F (F Bool)) (less x z))
(assert (not (=> (foo (minus x y) 0) (less x y))))
(check-sat)
(exit)
using namespace CVC4;
using namespace CVC4::parser;
+using namespace CVC4::language::input;
using namespace std;
class ParserBlack {
using namespace CVC4;
using namespace CVC4::parser;
+using namespace CVC4::language::input;
using namespace std;
class ParserBuilderBlack : public CxxTest::TestSuite {
projects / cvc5.git / commitdiff