diff options
35 files changed, 509 insertions, 194 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 98aea9707..f5ecf84c5 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -562,7 +562,8 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table, } /** - * 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) { @@ -575,7 +576,7 @@ 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(); diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index bd128267a..0c76ea845 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -136,7 +136,6 @@ Type DeclarationScope::lookupType(const std::string& name, return instantiation; } else { - Assert(p.second.isSort()); if(Debug.isOn("sort")) { Debug("sort") << "instantiating using a sort substitution" << endl; Debug("sort") << "have formals ["; diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 55b59d13c..5cf3373c2 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -34,9 +34,9 @@ using namespace CVC4::kind; 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() { @@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { 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); } } @@ -92,8 +92,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { child1.getNode(), child2.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -112,8 +111,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child2.getNode(), child3.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -133,8 +131,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child3.getNode(), child4.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -156,8 +153,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child4.getNode(), child5.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -181,8 +177,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { 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); } } @@ -207,7 +202,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { 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); } } @@ -309,16 +304,19 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio 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) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 92d039bd3..7946a734e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -74,12 +74,18 @@ private: /** 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 diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 5fb931a65..eb618a8c9 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -39,6 +39,7 @@ namespace expr { 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 */ @@ -47,8 +48,8 @@ std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) { } 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) @@ -61,6 +62,12 @@ TypeCheckingException::TypeCheckingException(const Expr& expr, std::string messa { } +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; } @@ -218,9 +225,10 @@ bool Expr::isConst() const { 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() { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 29164ffa5..2eac4ab62 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -26,6 +26,7 @@ #include <stdint.h> #include "util/exception.h" +#include "util/language.h" ${includes} @@ -33,7 +34,7 @@ ${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 { @@ -45,6 +46,8 @@ class Expr; class ExprManager; class SmtEngine; class Type; +class TypeCheckingException; +class TypeCheckingExceptionPrivate; namespace smt { class SmtEnginePrivate; @@ -53,6 +56,7 @@ namespace smt { namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; + class CVC4_PUBLIC ExprSetLanguage; }/* CVC4::expr namespace */ /** @@ -61,6 +65,7 @@ namespace expr { class CVC4_PUBLIC TypeCheckingException : public Exception { friend class SmtEngine; + friend class smt::SmtEnginePrivate; private: @@ -69,8 +74,10 @@ private: protected: - TypeCheckingException(): Exception() {} + TypeCheckingException() : Exception() {} TypeCheckingException(const Expr& expr, std::string message); + TypeCheckingException(ExprManager* em, + const TypeCheckingExceptionPrivate* exc); public: @@ -97,6 +104,14 @@ 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. */ @@ -281,7 +296,7 @@ public: * 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); @@ -296,7 +311,8 @@ public: * 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. @@ -367,6 +383,11 @@ public: 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(...) * @param out output stream to print to. @@ -402,15 +423,10 @@ protected: 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 @@ -551,7 +567,7 @@ public: static inline void setDepth(std::ostream& out, long depth) { out.iword(s_iosIndex) = depth; } -}; +};/* class ExprSetDepth */ /** * IOStream manipulator to print type ascriptions or not. @@ -598,11 +614,50 @@ public: } };/* 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 { @@ -634,6 +689,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { 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.. diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index aaecff800..c4968af26 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -198,7 +198,7 @@ function registerOperatorToKind { operatorKind=$1 applyKind=$2 metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind; -"; +"; } function register_metakind { diff --git a/src/expr/node.h b/src/expr/node.h index 871f1e0d7..1427bb9c2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -36,6 +36,8 @@ #include "util/Assert.h" #include "util/configuration.h" #include "util/output.h" +#include "util/exception.h" +#include "util/language.h" namespace CVC4 { @@ -58,7 +60,7 @@ private: protected: - TypeCheckingExceptionPrivate(): Exception() {} + TypeCheckingExceptionPrivate() : Exception() {} public: @@ -656,12 +658,12 @@ 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); } /** @@ -692,6 +694,11 @@ public: 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. * @param indent number of spaces to indent the formula by. @@ -720,7 +727,8 @@ public: 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; } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 2f10668c7..4c8bc578a 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -664,11 +664,11 @@ private: 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); } } } @@ -692,11 +692,11 @@ public: 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); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4653ee95f..5c24699b8 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -82,10 +82,11 @@ struct NVReclaim { }; -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) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0860365bc..6453a84d5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -118,6 +118,12 @@ class NodeManager { 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" * NodeValue. In particular, "non-inlined" constants are permitted @@ -233,9 +239,12 @@ class NodeManager { // 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. */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index a10b43c48..004f0c9a9 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/kind.h" #include "expr/metakind.h" +#include "util/language.h" #include <sstream> using namespace std; @@ -41,53 +42,67 @@ string NodeValue::toString() const { 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 { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index b91196559..bc592b4e5 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -29,6 +29,7 @@ #define __CVC4__EXPR__NODE_VALUE_H #include "expr/kind.h" +#include "util/language.h" #include <stdint.h> #include <string> @@ -260,7 +261,8 @@ public: } 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; diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 8cf555eb0..b8b2e4754 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -29,9 +29,9 @@ using namespace std; 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 { @@ -123,6 +123,13 @@ void Type::toStream(ostream& out) 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); diff --git a/src/expr/type.h b/src/expr/type.h index 19c3d27f3..435d640d0 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -56,6 +56,14 @@ struct CVC4_PUBLIC TypeHashStrategy { };/* 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. */ class CVC4_PUBLIC Type { @@ -65,6 +73,7 @@ class CVC4_PUBLIC Type { friend class ExprManager; friend class TypeNode; friend class TypeHashStrategy; + friend std::ostream& operator<<(std::ostream& out, const Type& t); protected: @@ -283,7 +292,12 @@ public: * @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. @@ -294,7 +308,7 @@ public: /** Construct from the base type */ BooleanType(const Type& type) throw(AssertionException); -}; +};/* class BooleanType */ /** * Singleton class encapsulating the integer type. @@ -305,7 +319,7 @@ public: /** Construct from the base type */ IntegerType(const Type& type) throw(AssertionException); -}; +};/* class IntegerType */ /** * Singleton class encapsulating the real type. @@ -316,8 +330,7 @@ public: /** Construct from the base type */ RealType(const Type& type) throw(AssertionException); -}; - +};/* class RealType */ /** * Class encapsulating a function type. @@ -334,7 +347,7 @@ public: /** Get the range type (i.e., the type of the result). */ Type getRangeType() const; -}; +};/* class FunctionType */ /** * Class encapsulating a tuple type. @@ -348,7 +361,7 @@ public: /** Get the constituent types */ std::vector<Type> getTypes() const; -}; +};/* class TupleType */ /** * Class encapsulating an array type. @@ -365,7 +378,7 @@ public: /** Get the constituent type */ Type getConstituentType() const; -}; +};/* class ArrayType */ /** * Class encapsulating a user-defined sort. @@ -379,7 +392,7 @@ public: /** Get the name of the sort */ std::string getName() const; -}; +};/* class SortType */ /** * Class encapsulating a user-defined sort constructor. @@ -399,7 +412,7 @@ public: /** 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). @@ -410,8 +423,7 @@ public: /** Construct from the base type */ KindType(const Type& type) throw(AssertionException); -}; - +};/* class KindType */ /** * Class encapsulating the bit-vector type. @@ -428,15 +440,7 @@ public: * @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 */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0e763128f..cc368e8c0 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -310,14 +310,14 @@ public: } /** - * 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); } /** diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 113b8a5f7..8faaefac4 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -30,7 +30,7 @@ #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" @@ -75,7 +75,8 @@ enum OptionValue { INTERACTIVE, NO_INTERACTIVE, PRODUCE_MODELS, - PRODUCE_ASSIGNMENTS + PRODUCE_ASSIGNMENTS, + NO_EARLY_TYPE_CHECKING };/* enum OptionValue */ /** @@ -127,6 +128,7 @@ static struct option cmdlineOptions[] = { { "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! */ @@ -183,16 +185,16 @@ throw(OptionException) { 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; } @@ -300,12 +302,16 @@ throw(OptionException) { 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()); diff --git a/src/main/main.cpp b/src/main/main.cpp index 4f261378d..7fd866112 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -120,7 +120,7 @@ int runCvc4(int argc, char* argv[]) { } // Create the expression manager - ExprManager exprMgr; + ExprManager exprMgr(options.earlyTypeChecking); // Create the SmtEngine SmtEngine smt(&exprMgr, &options); @@ -131,19 +131,19 @@ int runCvc4(int argc, char* argv[]) { 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; } } } @@ -167,11 +167,19 @@ int runCvc4(int argc, char* argv[]) { 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() ) diff --git a/src/main/usage.h b/src/main/usage.h index 15a30a426..ed35e76e8 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -51,7 +51,8 @@ CVC4 options:\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"; + --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 */ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index b919c3bd5..39c8e11b3 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -141,6 +141,8 @@ AntlrInputStream::newStringInputStream(const std::string& input, } AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) { + using namespace language::input; + AntlrInput* input; switch(lang) { diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 139795494..f53d7cc9c 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -58,7 +58,7 @@ public: 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), @@ -85,9 +85,9 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { 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); diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 2ae38622d..9a5b654a8 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -91,7 +91,7 @@ protected: std::string d_filename; unsigned long d_line; unsigned long d_column; -}; // end of class ParserException +};/* class ParserException */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_options.h b/src/parser/parser_options.h index b3fd203e2..b6c61786b 100644 --- a/src/parser/parser_options.h +++ b/src/parser/parser_options.h @@ -23,41 +23,12 @@ #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 */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a2792eaac..2c460c831 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -250,7 +250,7 @@ command returns [CVC4::Command* cmd] } | /* assertion */ ASSERT_TOK term[expr] - { cmd = new AssertCommand(expr); } + { cmd = new AssertCommand(expr); } | /* checksat */ CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); } 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: diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 78f91edc5..02315143d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -35,7 +35,8 @@ libutil_la_SOURCES = \ stats.h \ stats.cpp \ triple.h \ - dynamic_array.h + dynamic_array.h \ + language.h BUILT_SOURCES = \ rational.h \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index c1b7acd71..403f6f84b 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -12,7 +12,7 @@ ** 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. diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index e59eacf4d..d04efe0aa 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -85,7 +85,7 @@ namespace CVC4 { #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\ @@ -99,7 +99,8 @@ this CVC4 library cannot be used in proprietary applications. Please\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 */ diff --git a/src/util/language.h b/src/util/language.h new file mode 100644 index 000000000..5446357c4 --- /dev/null +++ b/src/util/language.h @@ -0,0 +1,157 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/options.h b/src/util/options.h index 08de590d8..af254dabf 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -21,10 +21,16 @@ #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 { @@ -45,7 +51,7 @@ struct CVC4_PUBLIC Options { int verbosity; /** The input language */ - parser::InputLanguage lang; + InputLanguage inputLanguage; /** Enumeration of UF implementation choices */ typedef enum { TIM, MORGAN } UfImplementation; @@ -83,13 +89,16 @@ struct CVC4_PUBLIC Options { /** 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), @@ -99,7 +108,8 @@ struct CVC4_PUBLIC Options { interactive(false), interactiveSetByUser(false), produceModels(false), - produceAssignments(false) { + produceAssignments(false), + earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { } };/* struct Options */ @@ -121,4 +131,6 @@ inline std::ostream& operator<<(std::ostream& out, }/* CVC4 namespace */ +#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT + #endif /* __CVC4__OPTIONS_H */ diff --git a/src/util/triple.h b/src/util/triple.h index 50bf30c4a..3a6f841c4 100644 --- a/src/util/triple.h +++ b/src/util/triple.h @@ -13,7 +13,8 @@ ** ** \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" diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2 index 08e99867a..6b38c6a70 100644 --- a/test/regress/regress0/simple-rdl-definefun.smt2 +++ b/test/regress/regress0/simple-rdl-definefun.smt2 @@ -1,14 +1,15 @@ (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) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 88a6eaf57..4f55edad5 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -32,6 +32,7 @@ using namespace CVC4; using namespace CVC4::parser; +using namespace CVC4::language::input; using namespace std; class ParserBlack { diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index b130501f5..c661f00d9 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -34,6 +34,7 @@ typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu; using namespace CVC4; using namespace CVC4::parser; +using namespace CVC4::language::input; using namespace std; class ParserBuilderBlack : public CxxTest::TestSuite { |