diff options
47 files changed, 1208 insertions, 426 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 09aa3ed9f..cfcc62335 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -2,10 +2,10 @@ /*! \file declaration_scope.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -174,4 +174,8 @@ void DeclarationScope::pushScope() throw() { d_context->push(); } -} // namespace CVC4 +size_t DeclarationScope::getLevel() const throw() { + return d_context->getLevel(); +} + +}/* CVC4 namespace */ diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 17140c850..6d89f5f4e 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -2,10 +2,10 @@ /*! \file declaration_scope.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -49,7 +49,7 @@ class CVC4_PUBLIC ScopeException : public Exception { */ class CVC4_PUBLIC DeclarationScope { /** The context manager for the scope maps. */ - context::Context *d_context; + context::Context* d_context; /** A map for expressions. */ context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap; @@ -180,6 +180,9 @@ public: /** Push a scope level. */ void pushScope() throw(); + /** Get the current level of this declaration scope. */ + size_t getLevel() const throw(); + };/* class DeclarationScope */ }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 870c77383..b116a4671 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -475,47 +475,137 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { } DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { - NodeManagerScope nms(d_nodeManager); - TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype)); - Type type(d_nodeManager, typeNode); - DatatypeType dtt(type); - const Datatype& dt = typeNode->getConst<Datatype>(); - if(!dt.isResolved()) { - std::map<std::string, DatatypeType> resolutions; - resolutions.insert(std::make_pair(datatype.getName(), dtt)); - const_cast<Datatype&>(dt).resolve(this, resolutions); - } - return dtt; + // Not worth a special implementation; this doesn't need to be fast + // code anyway.. + vector<Datatype> datatypes; + datatypes.push_back(datatype); + vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes); + Assert(result.size() == 1); + return result.front(); } -std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { +std::vector<DatatypeType> +ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + return mkMutualDatatypeTypes(datatypes, set<SortType>()); +} + +std::vector<DatatypeType> +ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, + const std::set<SortType>& unresolvedTypes) { NodeManagerScope nms(d_nodeManager); - std::map<std::string, DatatypeType> resolutions; + std::map<std::string, DatatypeType> nameResolutions; std::vector<DatatypeType> dtts; - for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); + + // First do some sanity checks, set up the final Type to be used for + // each datatype, and set up the "named resolutions" used to handle + // simple self- and mutual-recursion, for example in the definition + // "nat = succ(pred:nat) | zero", a named resolution can handle the + // pred selector. + for(std::vector<Datatype>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); i != i_end; ++i) { TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); Type type(d_nodeManager, typeNode); DatatypeType dtt(type); - CheckArgument(resolutions.find((*i).getName()) == resolutions.end(), + CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(), datatypes, - "cannot construct two datatypes at the same time with the same name `%s'", + "cannot construct two datatypes at the same time " + "with the same name `%s'", (*i).getName().c_str()); - resolutions.insert(std::make_pair((*i).getName(), dtt)); + nameResolutions.insert(std::make_pair((*i).getName(), dtt)); dtts.push_back(dtt); } - for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); + + // Second, set up the type substitution map for complex type + // resolution (e.g. if "list" is the type we're defining, and it has + // a selector of type "ARRAY INT OF list", this can't be taken care + // of using the named resolutions that we set up above. A + // preliminary array type was set up, and now needs to have "list" + // substituted in it for the correct type. + // + // @TODO get rid of named resolutions altogether and handle + // everything with these resolutions? + std::vector<Type> placeholders;// to hold the "unresolved placeholders" + std::vector<Type> replacements;// to hold our final, resolved types + for(std::set<SortType>::const_iterator i = unresolvedTypes.begin(), + i_end = unresolvedTypes.end(); + i != i_end; + ++i) { + std::string name = (*i).getName(); + std::map<std::string, DatatypeType>::const_iterator resolver = + nameResolutions.find(name); + CheckArgument(resolver != nameResolutions.end(), + unresolvedTypes, + "cannot resolve type `%s'; it's not among " + "the datatypes being defined", name.c_str()); + // We will instruct the Datatype to substitute "*i" (the + // unresolved SortType used as a placeholder in complex types) + // with "(*resolver).second" (the DatatypeType we created in the + // first step, above). + placeholders.push_back(*i); + replacements.push_back((*resolver).second); + } + + // Lastly, perform the final resolutions and checks. + for(std::vector<DatatypeType>::iterator i = dtts.begin(), + i_end = dtts.end(); i != i_end; ++i) { const Datatype& dt = (*i).getDatatype(); if(!dt.isResolved()) { - const_cast<Datatype&>(dt).resolve(this, resolutions); + const_cast<Datatype&>(dt).resolve(this, nameResolutions, + placeholders, replacements); } + + // Now run some checks, including a check to make sure that no + // selector is function-valued. + checkResolvedDatatype(*i); } + return dtts; } +void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { + const Datatype& dt = dtt.getDatatype(); + + AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved"); + + // for all constructors... + for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); + i != i_end; + ++i) { + const Datatype::Constructor& c = *i; + Type testerType CVC4_UNUSED = c.getTester().getType(); + Assert(c.isResolved() && + testerType.isTester() && + TesterType(testerType).getDomain() == dtt && + TesterType(testerType).getRangeType() == booleanType(), + "malformed tester in datatype post-resolution"); + Type ctorType CVC4_UNUSED = c.getConstructor().getType(); + Assert(ctorType.isConstructor() && + ConstructorType(ctorType).getArity() == c.getNumArgs() && + ConstructorType(ctorType).getReturnType() == dtt, + "malformed constructor in datatype post-resolution"); + // for all selectors... + for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end(); + j != j_end; + ++j) { + const Datatype::Constructor::Arg& a = *j; + Type selectorType = a.getSelector().getType(); + Assert(a.isResolved() && + selectorType.isSelector() && + SelectorType(selectorType).getDomain() == dtt, + "malformed selector in datatype post-resolution"); + // This next one's a "hard" check, performed in non-debug builds + // as well; the other ones should all be guaranteed by the + // CVC4::Datatype class, but this actually needs to be checked. + AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(), + "cannot put function-like things in datatypes"); + } + } +} + ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const { NodeManagerScope nms(d_nodeManager); return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31ce7855a..b7f376811 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -72,6 +72,11 @@ private: context::Context* getContext() const; /** + * Check some things about a newly-created DatatypeType. + */ + void checkResolvedDatatype(DatatypeType dtt) const; + + /** * SmtEngine will use all the internals, so it will grab the * NodeManager. */ @@ -319,7 +324,41 @@ public: * Make a set of types representing the given datatypes, which may be * mutually recursive. */ - std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + std::vector<DatatypeType> + mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + + /** + * Make a set of types representing the given datatypes, which may + * be mutually recursive. unresolvedTypes is a set of SortTypes + * that were used as placeholders in the Datatypes for the Datatypes + * of the same name. This is just a more complicated version of the + * above mkMutualDatatypeTypes() function, but is required to handle + * complex types. + * + * For example, unresolvedTypes might contain the single sort "list" + * (with that name reported from SortType::getName()). The + * datatypes list might have the single datatype + * + * DATATYPE + * list = cons(car:ARRAY INT OF list, cdr:list) | nil; + * END; + * + * To represent the Type of the array, the user had to create a + * placeholder type (an uninterpreted sort) to stand for "list" in + * the type of "car". It is this placeholder sort that should be + * passed in unresolvedTypes. If the datatype was of the simpler + * form: + * + * DATATYPE + * list = cons(car:list, cdr:list) | nil; + * END; + * + * then no complicated Type needs to be created, and the above, + * simpler form of mkMutualDatatypeTypes() is enough. + */ + std::vector<DatatypeType> + mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, + const std::set<SortType>& unresolvedTypes); /** * Make a type representing a constructor with the given parameterization. diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f6d346630..51a734757 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -117,10 +117,24 @@ Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); - ExprManagerScope ems(*this); - *d_node = *e.d_node; - d_exprManager = e.d_exprManager; + if(this != &e) { + if(d_exprManager == e.d_exprManager) { + ExprManagerScope ems(*this); + *d_node = *e.d_node; + } else { + // This happens more than you think---every time you set to or + // from the null Expr. It's tricky because each node manager + // must be in play at the right time. + + ExprManagerScope ems1(*this); + *d_node = Node::null(); + ExprManagerScope ems2(e); + *d_node = *e.d_node; + + d_exprManager = e.d_exprManager; + } + } return *this; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 489564d5f..c45cc9b99 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -754,7 +754,7 @@ public: ${getConst_instantiations} -#line 682 "${template}" +#line 758 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 932ec31c8..6b9787f6c 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -2,10 +2,10 @@ /*! \file kind_template.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -95,7 +95,7 @@ struct KindHashStrategy { * The enumeration for the built-in atomic types. */ enum TypeConstant { - ${type_constant_list} +${type_constant_list} LAST_TYPE };/* enum TypeConstant */ @@ -110,7 +110,7 @@ struct TypeConstantHashStrategy { inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { - ${type_constant_descriptions} +${type_constant_descriptions} default: out << "UNKNOWN_TYPE_CONSTANT"; break; @@ -121,13 +121,13 @@ inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { namespace theory { enum TheoryId { - ${theory_enum} +${theory_enum} THEORY_LAST }; inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { - ${theory_descriptions} +${theory_descriptions} default: out << "UNKNOWN_THEORY"; break; @@ -136,18 +136,18 @@ inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { } inline TheoryId kindToTheoryId(::CVC4::Kind k) { - switch (k) { - ${kind_to_theory_id} + switch(k) { +${kind_to_theory_id} default: - Unreachable(); + Unhandled(k); } } inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { - switch (typeConstant) { - ${type_constant_to_theory_id} + switch(typeConstant) { +${type_constant_to_theory_id} default: - Unreachable(); + Unhandled(typeConstant); } } diff --git a/src/expr/mkkind b/src/expr/mkkind index f7f6ba836..fa80894b2 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -73,9 +73,9 @@ function theory { fi theory_id="$1" - theory_enum="$1, - ${theory_enum}" - theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; + theory_enum="${theory_enum} $1, +" + theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " } @@ -144,11 +144,11 @@ function register_sort { id=$1 comment=$2 - type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ + type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " - type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; + type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; " - type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; " } @@ -161,7 +161,7 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " - kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; " } diff --git a/src/expr/node.h b/src/expr/node.h index d3775cb3f..6fe1e7d0e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -720,7 +720,7 @@ 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 stream to serialize this node to @@ -790,6 +790,7 @@ public: /** * Serializes a given node to the given stream. + * * @param out the output stream to use * @param n the node to output to the stream * @return the stream diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 9449594e3..716e2a3b3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -519,18 +519,26 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } -TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) { +TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, + TypeNode range) { std::vector<TypeNode> sorts; Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl; for(Datatype::Constructor::const_iterator i = constructor.begin(); i != constructor.end(); ++i) { - Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl; - TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1]; + TypeNode selectorType = *(*i).getSelector().getType().d_typeNode; + Debug("datatypes") << selectorType << std::endl; + TypeNode sort = selectorType[1]; + + // should be guaranteed here already, but just in case + Assert(!sort.isFunctionLike()); + Debug("datatypes") << "ctor sort: " << sort << std::endl; sorts.push_back(sort); } Debug("datatypes") << "ctor range: " << range << std::endl; + CheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); sorts.push_back(range); return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 94b7e5c40..9974df6ca 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -799,6 +799,8 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 2); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); sortNodes.push_back(sorts[i]); } return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); @@ -809,6 +811,8 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 1); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); sortNodes.push_back(sorts[i]); } sortNodes.push_back(booleanType()); @@ -819,6 +823,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { Assert(types.size() >= 2); std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { + /* FIXME when congruence closure no longer abuses tuples + CheckArgument(!types[i].isFunctionLike(), types, + "cannot put function-like types in tuples"); + */ typeNodes.push_back(types[i]); } return mkTypeNode(kind::TUPLE_TYPE, typeNodes); @@ -830,14 +838,24 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { + CheckArgument(!indexType.isFunctionLike(), domain, + "cannot index arrays by a function-like type"); + CheckArgument(!constituentType.isFunctionLike(), domain, + "cannot store function-like types in arrays"); return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); + CheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); return mkTypeNode(kind::SELECTOR_TYPE, domain, range); } inline TypeNode NodeManager::mkTesterType(TypeNode domain) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); return mkTypeNode(kind::TESTER_TYPE, domain ); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 6dd9c5cec..4ea425aa7 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -69,10 +69,26 @@ bool Type::isNull() const { } Type& Type::operator=(const Type& t) { - NodeManagerScope nms(t.d_nodeManager); + Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!"); + Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!"); + if(this != &t) { - *d_typeNode = *t.d_typeNode; - d_nodeManager = t.d_nodeManager; + if(d_nodeManager == t.d_nodeManager) { + NodeManagerScope nms(d_nodeManager); + *d_typeNode = *t.d_typeNode; + } else { + // This happens more than you think---every time you set to or + // from the null Type. It's tricky because each node manager + // must be in play at the right time. + + NodeManagerScope nms1(d_nodeManager); + *d_typeNode = TypeNode::null(); + + NodeManagerScope nms2(t.d_nodeManager); + *d_typeNode = *t.d_typeNode; + + d_nodeManager = t.d_nodeManager; + } } return *this; } @@ -85,6 +101,10 @@ bool Type::operator!=(const Type& t) const { return *d_typeNode != *t.d_typeNode; } +bool Type::operator<(const Type& t) const { + return *d_typeNode < *t.d_typeNode; +} + Type Type::substitute(const Type& type, const Type& replacement) const { NodeManagerScope nms(d_nodeManager); return makeType(d_typeNode->substitute(*type.d_typeNode, @@ -468,6 +488,22 @@ Type ConstructorType::getReturnType() const { return makeType(d_typeNode->getConstructorReturnType()); } +size_t ConstructorType::getArity() const { + return d_typeNode->getNumChildren() - 1; +} + +std::vector<Type> ConstructorType::getArgTypes() const { + NodeManagerScope nms(d_nodeManager); + vector<Type> args; + vector<TypeNode> argNodes = d_typeNode->getArgTypes(); + vector<TypeNode>::iterator it = argNodes.begin(); + vector<TypeNode>::iterator it_end = argNodes.end(); + for(; it != it_end; ++ it) { + args.push_back(makeType(*it)); + } + return args; +} + const Datatype& DatatypeType::getDatatype() const { return d_typeNode->getConst<Datatype>(); } diff --git a/src/expr/type.h b/src/expr/type.h index 3b476ddf5..290bb360a 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -174,6 +174,11 @@ public: bool operator!=(const Type& t) const; /** + * An ordering on Types so they can be stored in maps, etc. + */ + bool operator<(const Type& t) const; + + /** * Is this the Boolean type? * @return true if the type is a Boolean type */ @@ -533,6 +538,12 @@ public: /** Get the return type */ Type getReturnType() const; + /** Get the argument types */ + std::vector<Type> getArgTypes() const; + + /** Get the number of constructor arguments */ + size_t getArity() const; + };/* class ConstructorType */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7549af895..0b22fdf0f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -2,8 +2,8 @@ /*! \file type_node.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -85,6 +85,14 @@ bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; } +bool TypeNode::isFunctionLike() const { + return + getKind() == kind::FUNCTION_TYPE || + getKind() == kind::CONSTRUCTOR_TYPE || + getKind() == kind::SELECTOR_TYPE || + getKind() == kind::TESTER_TYPE; +} + bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 049173867..c04bef0c7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -371,6 +371,19 @@ public: bool isFunction() const; /** + * Is this a function-LIKE type? Function-like things + * (e.g. datatype selectors) that aren't actually functions ARE + * considered functions, here. The main point is that this is used + * to avoid anything higher-order: anything function-like cannot be + * the argument or return value for anything else function-like. + * + * Arrays are explicitly *not* function-like for the purposes of + * this test. However, functions still cannot contain anything + * function-like. + */ + bool isFunctionLike() const; + + /** * Get the argument types of a function, datatype constructor, * datatype selector, or datatype tester. */ @@ -383,9 +396,9 @@ public: TypeNode getRangeType() const; /** - * Is this a predicate type? - * NOTE: all predicate types are also function types (so datatype - * testers are not considered "predicates" for the purpose of this function). + * Is this a predicate type? NOTE: all predicate types are also + * function types (so datatype testers are NOT considered + * "predicates" for the purpose of this function). */ bool isPredicate() const; @@ -451,7 +464,8 @@ private: inline std::ostream& operator<<(std::ostream& out, const TypeNode& 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/parser/antlr_input.h b/src/parser/antlr_input.h index c48185f58..4ae063266 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -54,10 +54,10 @@ class AntlrInputStream : public InputStream { bool fileIsTemporary = false); /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream(const AntlrInputStream& inputStream); + AntlrInputStream(const AntlrInputStream& inputStream) CVC4_UNUSED; /* This is private and unimplemented, because you should never use it. */ - AntlrInputStream& operator=(const AntlrInputStream& inputStream); + AntlrInputStream& operator=(const AntlrInputStream& inputStream) CVC4_UNUSED; public: @@ -178,6 +178,7 @@ public: /** Get a bitvector constant from the text of the number and the size token */ static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size); + /** Retrieve the remaining text in this input. */ std::string getUnparsedText(); protected: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 30866eddb..792f53605 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -19,8 +19,13 @@ grammar Cvc; options { - language = 'C'; // C output for antlr -// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + // C output for antlr + language = 'C'; + + // Skip the default error handling, just break with exceptions + // defaultErrorHandler = false; + + // Only lookahead of <= k requested (disable for LL* parsing) k = 2; } @@ -61,8 +66,13 @@ tokens { OF_TOK = 'OF'; WITH_TOK = 'WITH'; + SUBTYPE_TOK = 'SUBTYPE'; + FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; + PATTERN_TOK = 'PATTERN'; + + LAMBDA = 'LAMBDA'; // Symbols @@ -77,6 +87,7 @@ tokens { SEMICOLON = ';'; BAR = '|'; DOT = '.'; + DOTDOT = '..'; SQHASH = '[#'; HASHSQ = '#]'; @@ -104,8 +115,6 @@ tokens { INTDIV_TOK = 'DIV'; FLOOR_TOK = 'FLOOR'; - //IS_INTEGER_TOK = 'IS_INTEGER'; - // Bitvectors BITVECTOR_TOK = 'BITVECTOR'; @@ -131,9 +140,10 @@ tokens { BVCOMP_TOK = 'BVCOMP'; BVXNOR_TOK = 'BVXNOR'; CONCAT_TOK = '@'; - BVTOINT_TOK = 'BVTOINT'; - INTTOBV_TOK = 'INTTOBV'; - BOOLEXTRACT_TOK = 'BOOLEXTRACT'; + //BVTOINT_TOK = 'BVTOINT'; + //INTTOBV_TOK = 'INTTOBV'; + //BOOLEXTRACT_TOK = 'BOOLEXTRACT'; + //IS_INTEGER_TOK = 'IS_INTEGER'; BVLT_TOK = 'BVLT'; BVGT_TOK = 'BVGT'; BVLE_TOK = 'BVLE'; @@ -461,11 +471,15 @@ command returns [CVC4::Command* cmd = 0] // Datatypes can be mututally-recursive if they're in the same // definition block, separated by a comma. So we parse everything // and then ask the ExprManager to resolve everything in one go. - | DATATYPE_TOK datatypeDef[dts] + | DATATYPE_TOK + { /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(); } + datatypeDef[dts] ( COMMA datatypeDef[dts] )* END_TOK SEMICOLON - { cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } - | declaration[cmd] + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + | toplevelDeclaration[cmd] | EOF ; @@ -486,46 +500,154 @@ symbolicExpr[CVC4::SExpr& sexpr] ; /** - * Match a declaration + * Match a top-level declaration. */ -declaration[CVC4::Command*& cmd] +toplevelDeclaration[CVC4::Command*& cmd] @init { std::vector<std::string> ids; Type t; Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : // FIXME: These could be type or function declarations, if that matters. - identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t, ids] SEMICOLON - { cmd = new DeclarationCommand(ids, t); } + : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON + ( declareVariables[t,ids,true] { cmd = new DeclarationCommand(ids, t); } + | declareTypes[ids] { cmd = new DeclarationCommand(ids, EXPR_MANAGER->kindType()); } ) SEMICOLON + ; + +/** + * A bound variable declaration. + */ +boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t] + : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[t,ids,false] ; -/** Match the right-hand side of a declaration. Returns the type. */ -declType[CVC4::Type& t, std::vector<std::string>& idList] +/** + * A series of bound variable declarations. + */ +boundVarDecls @init { - Expr f; - Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector<std::string> ids; + Type t; } - : /* A sort declaration (e.g., "T : TYPE") */ - TYPE_TOK - { PARSER_STATE->mkSorts(idList); - t = EXPR_MANAGER->kindType(); } - | /* A type alias */ - TYPE_TOK EQUAL_TOK type[t] + : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )* + ; + +boundVarDeclsReturn[std::vector<CVC4::Expr>& terms, + std::vector<CVC4::Type>& types] +@init { + std::vector<std::string> ids; + Type t; + terms.clear(); + types.clear(); +} + : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )* + ; + +boundVarDeclReturn[std::vector<CVC4::Expr>& terms, + std::vector<CVC4::Type>& types] +@init { + std::vector<std::string> ids; + Type t; + // NOTE: do not clear the vectors here! +} + : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] + { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t); + terms.insert(terms.end(), vars.begin(), vars.end()); + for(unsigned i = 0; i < vars.size(); ++i) { + types.push_back(t); + } + } + ; + +/** + * Match the right-hand-side of a type declaration. Unlike + * declareVariables[] below, don't need to return the Type, since it's + * always the KindType (the type of types). Also don't need toplevel + * because type declarations are always top-level, except for + * type-lets, which don't use this rule. + */ +declareTypes[const std::vector<std::string>& idList] +@init { + Type t; +} + /* A sort declaration (e.g., "T : TYPE") */ + : TYPE_TOK + { for(std::vector<std::string>::const_iterator i = idList.begin(); + i != idList.end(); + ++i) { + // Don't allow a type variable to clash with a previously + // declared type variable, however a type variable and a + // non-type variable can clash unambiguously. Break from CVC3 + // behavior here. + PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); + } + PARSER_STATE->mkSorts(idList); + } + + /* A type alias "T : TYPE = foo..." */ + | TYPE_TOK EQUAL_TOK type[t,CHECK_DECLARED] { for(std::vector<std::string>::const_iterator i = idList.begin(); i != idList.end(); ++i) { + PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); PARSER_STATE->defineType(*i, t); } - t = EXPR_MANAGER->kindType(); } - | /* A variable declaration */ - type[t] ( EQUAL_TOK formula[f] )? + } + ; + +/** + * Match the right-hand side of a variable declaration. Returns the + * type. Some IDs might have been declared previously, and are not + * re-declared if topLevel is true (CVC allows re-declaration if the + * types are compatible---if they aren't compatible, an error is + * thrown). Also if topLevel is true, variable definitions are + * permitted. + */ +declareVariables[CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel] +@init { + Expr f; + Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + /* A variable declaration (or definition) */ + : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? { if(f.isNull()) { - PARSER_STATE->mkVars(idList, t); + Debug("parser") << "working on " << idList.front() << " : " << t << std::endl; + // CVC language allows redeclaration of variables if types are the same + for(std::vector<std::string>::const_iterator i = idList.begin(), + i_end = idList.end(); + i != i_end; + ++i) { + if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) { + Type oldType = PARSER_STATE->getType(*i); + Debug("parser") << " " << *i << " was declared previously " + << "with type " << oldType << std::endl; + if(oldType != t) { + std::stringstream ss; + ss << Expr::setlanguage(language::output::LANG_CVC4) + << "incompatible type for `" << *i << "':" << std::endl + << " old type: " << oldType << std::endl + << " new type: " << t << std::endl; + PARSER_STATE->parseError(ss.str()); + } else { + Debug("parser") << " types " << t << " and " << oldType + << " are compatible" << std::endl; + } + } else { + Debug("parser") << " " << *i << " not declared" << std::endl; + PARSER_STATE->mkVar(*i, t); + } + } } else { + if(!topLevel) { + // must be top-level; doesn't make sense to write something + // like e.g. FORALL(x:INT = 4): [...] + PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET"); + } + Debug("parser") << "made " << idList.front() << " = " << f << std::endl; for(std::vector<std::string>::const_iterator i = idList.begin(), i_end = idList.end(); i != i_end; ++i) { + PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); PARSER_STATE->defineFunction(*i, f); } } @@ -533,29 +655,6 @@ declType[CVC4::Type& t, std::vector<std::string>& idList] ; /** - * Match the type in a declaration and do the declaration binding. - * TODO: Actually parse sorts into Type objects. - */ -type[CVC4::Type& t] -@init { - Type t2; - std::vector<Type> typeList; - Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : /* Simple type */ - bitvectorType[t] - | /* Single-parameter function type */ - baseType[t] ARROW_TOK baseType[t2] - { t = EXPR_MANAGER->mkFunctionType(t, t2); } - | /* Multi-parameter function type */ - LPAREN baseType[t] - { typeList.push_back(t); } - ( COMMA baseType[t] { typeList.push_back(t); } )* - RPAREN ARROW_TOK baseType[t] - { t = EXPR_MANAGER->mkFunctionType(typeList, t); } - ; - -/** * Matches a list of identifiers separated by a comma and puts them in the * given list. * @param idList the list to fill with identifiers. @@ -566,9 +665,10 @@ identifierList[std::vector<std::string>& idList, CVC4::parser::SymbolType type] @init { std::string id; + idList.clear(); } : identifier[id,check,type] { idList.push_back(id); } - (COMMA identifier[id,check,type] { idList.push_back(id); })* + ( COMMA identifier[id,check,type] { idList.push_back(id); } )* ; @@ -584,53 +684,145 @@ identifier[std::string& id, ; /** - * Matches a bitvector type. + * Match the type in a declaration and do the declaration binding. */ -bitvectorType[CVC4::Type& t] - : arrayType[t] - | BITVECTOR_TOK LPAREN INTEGER_LITERAL RPAREN - { t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); } - ; - -arrayType[CVC4::Type& t] +type[CVC4::Type& t, + CVC4::parser::DeclarationCheck check] @init { Type t2; + bool lhs; + std::vector<Type> args; } - : baseType[t] - | ARRAY_TOK bitvectorType[t] OF_TOK bitvectorType[t2] - { t = EXPR_MANAGER->mkArrayType(t, t2); } + /* a type, possibly a function */ + : restrictedTypePossiblyFunctionLHS[t,check,lhs] + { if(lhs) { + Assert(t.isTuple()); + args = TupleType(t).getTypes(); + } else { + args.push_back(t); + } + Debug("parser") << "type: " << t << std::endl; + } + ( ARROW_TOK type[t2,check] { args.push_back(t2); } )? + { if(t2.isNull()) { + if(lhs) { + PARSER_STATE->parseError("improperly-placed type list; expected `->' after to define a function; or else maybe these parentheses were meant to be square brackets, to define a tuple type?"); + } + } else { + t = EXPR_MANAGER->mkFunctionType(args); + } + } + + /* type-lets: typeLetDecl defines the types, we just manage the + * scopes here. NOTE that LET in the CVC language is always + * sequential! */ + | LET_TOK { PARSER_STATE->pushScope(); } + typeLetDecl[check] ( COMMA typeLetDecl[check] )* IN_TOK type[t,check] + { PARSER_STATE->popScope(); } ; -/** - * Matches a type (which MUST be already declared). - * - * @return the type identifier - */ -baseType[CVC4::Type& t] - : maybeUndefinedBaseType[t,CHECK_DECLARED] +// A restrictedType is one that is not a "bare" function type (it can +// be enclosed in parentheses) and is not a type list. To support the +// syntax +// +// f : (nat, nat) -> nat; +// +// we have to permit restrictedTypes to be type lists (as on the LHS +// there). The "type" rule above uses restictedTypePossiblyFunctionLHS +// directly in order to implement that; this rule allows a type list to +// parse but then issues an error. +restrictedType[CVC4::Type& t, + CVC4::parser::DeclarationCheck check] +@init { + bool lhs; +} + : restrictedTypePossiblyFunctionLHS[t,check,lhs] + { if(lhs) { PARSER_STATE->parseError("improperly-placed type list; maybe these parentheses were meant to be square brackets, to define a tuple type?"); } } ; /** - * Matches a type (which may not be declared yet). Returns the - * identifier. If the type is declared, returns the Type in the 't' - * parameter; otherwise a null Type is returned in 't'. If 'check' is - * CHECK_DECLARED and the type is not declared, an exception is - * thrown. - * - * @return the type identifier in 't', and the id (where applicable) in 'id' + * lhs is set to "true" on output if we have a list of types, so an + * ARROW must follow. An ARROW can always follow; lhs means it MUST. */ -maybeUndefinedBaseType[CVC4::Type& t, - CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] +restrictedTypePossiblyFunctionLHS[CVC4::Type& t, + CVC4::parser::DeclarationCheck check, + bool& lhs] @init { - Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; - AssertArgument(check == CHECK_DECLARED || check == CHECK_NONE, - check, "CVC parser: can't use CHECK_UNDECLARED with maybeUndefinedBaseType[]"); + Type t2; + Expr f; + std::string id; + std::vector<Type> types; + lhs = false; } - : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); id = AntlrInput::tokenText($BOOLEAN_TOK); } - | INT_TOK { t = EXPR_MANAGER->integerType(); id = AntlrInput::tokenText($INT_TOK); } - | REAL_TOK { t = EXPR_MANAGER->realType(); id = AntlrInput::tokenText($REAL_TOK); } - | typeSymbol[t,check] - { id = $typeSymbol.id; } + /* named types */ + : identifier[id,check,SYM_SORT] + { if(check == CHECK_DECLARED || + PARSER_STATE->isDeclared(id, SYM_SORT)) { + t = PARSER_STATE->getSort(id); + } else { + t = PARSER_STATE->mkUnresolvedType(id); + } + } + + /* array types */ + | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check] + { t = EXPR_MANAGER->mkArrayType(t, t2); } + + /* subtypes */ + | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN + { PARSER_STATE->unimplementedFeature("subtypes not supported yet"); + t = Type(); } + + /* subrange types */ + | LBRACKET bound DOTDOT bound RBRACKET + { PARSER_STATE->unimplementedFeature("subranges not supported yet"); + t = Type(); } + + /* tuple types / old-style function types */ + | LBRACKET type[t,check] { types.push_back(t); } + ( COMMA type[t,check] { types.push_back(t); } )* RBRACKET + { if(types.size() == 1) { + if(types.front().isFunction()) { + // old style function syntax [ T -> U ] + PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax"); + } else { + PARSER_STATE->parseError("I'm not sure what you're trying to do here; tuples must have > 1 type"); + } + } else { + // tuple type [ T, U, V... ] + t = EXPR_MANAGER->mkTupleType(types); + } + } + + /* record types */ + | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] + ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ + { PARSER_STATE->unimplementedFeature("records not supported yet"); + t = Type(); } + + /* bitvector types */ + | BITVECTOR_TOK LPAREN k=numeral RPAREN + { t = EXPR_MANAGER->mkBitVectorType(k); } + + /* basic types */ + | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } + | REAL_TOK { t = EXPR_MANAGER->realType(); } + | INT_TOK { t = EXPR_MANAGER->integerType(); } + + /* Parenthesized general type, or the lhs of an ARROW (a list of + * types). These two things are combined to avoid conflicts in + * parsing. */ + | LPAREN type[t,check] { types.push_back(t); } + ( COMMA type[t,check] { lhs = true; types.push_back(t); } )* RPAREN + { if(lhs) { t = EXPR_MANAGER->mkTupleType(types); } + // if !lhs, t is already set up correctly, nothing to do.. + } + ; + +bound + : '_' + | numeral + | MINUS_TOK numeral ; /** @@ -653,51 +845,82 @@ typeSymbol[CVC4::Type& t, } ; -/** - * Matches a CVC4 formula. - * - * @return the expression representing the formula - */ -formula[CVC4::Expr& formula] +typeLetDecl[CVC4::parser::DeclarationCheck check] @init { - Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Type t; + std::string id; } - : letBinding[formula] + : identifier[id,CHECK_NONE,SYM_SORT] (COLON TYPE_TOK)? EQUAL_TOK restrictedType[t,check] + { PARSER_STATE->defineType(id, t); } ; /** - * Matches a comma-separated list of formulas + * Matches a CVC4 expression. Formulas and terms are not really + * distinguished during parsing; please ignore the naming of the + * grammar rules. + * + * @return the expression representing the formula/term */ -formulaList[std::vector<CVC4::Expr>& formulas] +formula[CVC4::Expr& f] @init { - Expr f; + Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector<std::string> ids; + std::vector<Expr> terms; + std::vector<Type> types; + Type t; } - : formula[f] { formulas.push_back(f); } - ( COMMA formula[f] - { formulas.push_back(f); } - )* - ; + /* quantifiers */ + : FORALL_TOK { PARSER_STATE->pushScope(); } LPAREN + boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN + COLON instantiationPatterns? formula[f] + { PARSER_STATE->popScope(); + PARSER_STATE->unimplementedFeature("quantifiers not supported yet"); + f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + } + | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN + boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN + COLON instantiationPatterns? formula[f] + { PARSER_STATE->popScope(); + PARSER_STATE->unimplementedFeature("quantifiers not supported yet"); + f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + } -/** - * Matches a LET binding - */ -letBinding[CVC4::Expr& f] -@init { -} - : LET_TOK - { PARSER_STATE->pushScope(); } - letDecls - IN_TOK letBinding[f] - { PARSER_STATE->popScope(); } + /* lets: letDecl defines the variables and functionss, we just + * manage the scopes here. NOTE that LET in the CVC language is + * always sequential! */ + | LET_TOK { PARSER_STATE->pushScope(); } + letDecl ( COMMA letDecl )* + IN_TOK formula[f] { PARSER_STATE->popScope(); } + + /* lambda */ + | LAMBDA { PARSER_STATE->pushScope(); } LPAREN + boundVarDeclsReturn[terms,types] + RPAREN COLON formula[f] + { PARSER_STATE->popScope(); + Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); + Expr func = PARSER_STATE->mkFunction("anonymous", t); + Command* cmd = new DefineFunctionCommand(func, terms, f); + PARSER_STATE->preemptCommand(cmd); + f = func; + } + + /* array literals */ + | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN + boundVarDecl[ids,t] RPAREN COLON formula[f] + { PARSER_STATE->popScope(); + PARSER_STATE->unimplementedFeature("array literals not supported yet"); + f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType())); + } + + /* everything else */ | booleanFormula[f] ; -/** - * Matches (and defines) LET declarations in order. Note this implements - * sequential-let (think "let*") rather than simultaneous-let. - */ -letDecls - : letDecl (COMMA letDecl)* +instantiationPatterns +@init { + Expr f; +} + : ( PATTERN_TOK LPAREN formula[f] (COMMA formula[f])* RPAREN COLON )+ ; /** @@ -709,7 +932,12 @@ letDecl std::string name; } : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e] - { PARSER_STATE->defineVar(name, e); } + { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl; + PARSER_STATE->defineVar(name, e); + Debug("parser") << "LET[" << PARSER_STATE->getDeclarationLevel() << "]: " + << name << std::endl + << " ==>" << " " << e << std::endl; + } ; booleanFormula[CVC4::Expr& f] @@ -724,17 +952,22 @@ booleanFormula[CVC4::Expr& f] --notCount; f = EXPR_MANAGER->mkExpr(kind::NOT, f); } - expressions.push_back(f); } + expressions.push_back(f); + Assert(notCount == 0); + } ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f] - { operators.push_back(op); - while(notCount > 0) { + { while(notCount > 0) { --notCount; f = EXPR_MANAGER->mkExpr(kind::NOT, f); } + operators.push_back(op); +# warning cannot do NOT FORALL or TRUE AND FORALL, or.. expressions.push_back(f); + Assert(notCount == 0); } )* - { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + { Assert(notCount == 0); + f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; booleanBinop[unsigned& op] @@ -812,9 +1045,8 @@ uminusTerm[CVC4::Expr& f] @init { unsigned minusCount = 0; } - : /* Unary minus */ -// (MINUS_TOK { ++minusCount; })* concatBitwiseTerm[f] - (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f] + /* Unary minus */ + : (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f] { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } } | concatBitwiseTerm[f] ; @@ -844,8 +1076,8 @@ bitwiseXorTerm[CVC4::Expr& f] @init { Expr f2; } - : /* BV xor */ - BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + /* BV xor */ + : BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); } | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); } @@ -858,8 +1090,8 @@ bitwiseXorTerm[CVC4::Expr& f] | bvNegTerm[f] ; bvNegTerm[CVC4::Expr& f] - : /* BV neg */ - BVNEG_TOK bvNegTerm[f] + /* BV neg */ + : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } | bvUminusTerm[f] ; @@ -867,14 +1099,15 @@ bvUminusTerm[CVC4::Expr& f] @init { Expr f2; } - : /* BV unary minus */ - BVUMINUS_TOK LPAREN formula[f] RPAREN + /* BV unary minus */ + : BVUMINUS_TOK LPAREN formula[f] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); } - | BVPLUS_TOK LPAREN INTEGER_LITERAL COMMA formula[f] + /* BV addition */ + | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN { unsigned size = BitVectorType(f.getType()).getSize(); - unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); if(k == 0) { +# warning cannot do BVPLUS(...)[i:j] PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0"); } if(k > size) { @@ -883,9 +1116,9 @@ bvUminusTerm[CVC4::Expr& f] f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); } } - | BVSUB_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + /* BV subtraction */ + | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2); - unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); if(k == 0) { PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0"); } @@ -896,9 +1129,9 @@ bvUminusTerm[CVC4::Expr& f] f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); } } - | BVMULT_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + /* BV multiplication */ + | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2); - unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); if(k == 0) { PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0"); } @@ -909,41 +1142,56 @@ bvUminusTerm[CVC4::Expr& f] f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); } } + /* BV unsigned division */ | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); } + /* BV signed division */ | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); } + /* BV unsigned remainder */ | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); } + /* BV signed remainder */ | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); } + /* BV signed modulo */ | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); } + /* BV left shift */ | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); } + /* BV arithmetic right shift */ | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); } + /* BV logical left shift */ | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); } - | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - unsigned n = BitVectorType(f.getType()).getSize(); - // sign extension in TheoryBitVector is defined as in SMT-LIBv2 + /* BV sign extension */ + | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN + { unsigned n = BitVectorType(f.getType()).getSize(); + // Sign extension in TheoryBitVector is defined as in SMT-LIBv2 + // which is different than in the CVC language + // SX(BITVECTOR(k), n) in CVC language extends to n bits + // In SMT-LIBv2, such a thing expands to k + n bits f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); } - | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - unsigned n = BitVectorType(f.getType()).getSize(); - // also zero extension - f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - n)), f); } - | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } - | BVROTR_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } - | BVROTL_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + /* BV zero extension */ + | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN + { unsigned n = BitVectorType(f.getType()).getSize(); + // Zero extension in TheoryBitVector is defined as in SMT-LIBv2 + // which is the same as in CVC3, but different than SX! + // SX(BITVECTOR(k), n) in CVC language extends to n bits + // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); } + /* BV repeat operation */ + | BVREPEAT_TOK LPAREN formula[f] COMMA k=numeral RPAREN + { f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } + /* BV rotate right */ + | BVROTR_TOK LPAREN formula[f] COMMA k=numeral RPAREN + { f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + /* BV rotate left */ + | BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN + { f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + /* left and right shifting with << and >>, or something else */ | bvShiftTerm[f] ; @@ -952,8 +1200,9 @@ bvShiftTerm[CVC4::Expr& f] bool left = false; } : bvComparison[f] - ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) INTEGER_LITERAL - { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) k=numeral + { // Defined in: + // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit if(left) { f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k))); } else { @@ -969,8 +1218,8 @@ bvComparison[CVC4::Expr& f] @init { Expr f2; } - : /* BV comparison */ - BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + /* BV comparisons */ + : BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); } | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); } @@ -999,16 +1248,15 @@ selectExtractTerm[CVC4::Expr& f] Expr f2; bool extract; } - : /* array select / bitvector extract */ - simpleTerm[f] + /* array select / bitvector extract */ + : simpleTerm[f] ( { extract = false; } - LBRACKET formula[f2] ( COLON INTEGER_LITERAL { extract = true; } )? RBRACKET + LBRACKET formula[f2] ( COLON k2=numeral { extract = true; } )? RBRACKET { if(extract) { if(f2.getKind() != kind::CONST_INTEGER) { - PARSER_STATE->parseError("bitvector extraction requires [INTEGER_LITERAL:INTEGER_LITERAL] range"); + PARSER_STATE->parseError("bitvector extraction requires [numeral:numeral] range"); } unsigned k1 = f2.getConst<Integer>().getLong(); - unsigned k2 = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f); } else { f = MK_EXPR(CVC4::kind::SELECT, f, f2); @@ -1025,37 +1273,63 @@ simpleTerm[CVC4::Expr& f] std::vector<Expr> args; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : /* function/constructor application */ - functionSymbol[f] - { args.push_back( f ); } - LPAREN formulaList[args] RPAREN + /* function/constructor application */ + : identifier[name,CHECK_DECLARED,SYM_VARIABLE] + { Debug("parser") << " at level " << PARSER_STATE->getDeclarationLevel() << std::endl; + Debug("parser") << " isFunction " << PARSER_STATE->isFunctionLike(name) << std::endl; + Debug("parser") << " isDefinedFunction " << PARSER_STATE->isDefinedFunction(name) << std::endl; + Debug("parser") << " name " << name << std::endl; + Debug("parser") << " isDeclared " << PARSER_STATE->isDeclared(name) << std::endl; + Debug("parser") << " getType " << PARSER_STATE->getType(name) << std::endl; + PARSER_STATE->checkFunctionLike(name); + f = PARSER_STATE->getVariable(name); + args.push_back(f); + } + LPAREN formula[f] { args.push_back(f); } + ( COMMA formula[f] { args.push_back(f); } )* RPAREN // TODO: check arity - { Type t = f.getType(); - if( t.isFunction() ) { + { Type t = args.front().getType(); + Debug("parser") << "type is " << t << std::endl; + Debug("parser") << "expr is " << args.front() << std::endl; + if(PARSER_STATE->isDefinedFunction(name)) { + f = MK_EXPR(CVC4::kind::APPLY, args); + } else if(t.isFunction()) { f = MK_EXPR(CVC4::kind::APPLY_UF, args); - } else if( t.isConstructor() ) { + } else if(t.isConstructor()) { Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl; f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); - } else if( t.isSelector() ) { + } else if(t.isSelector()) { Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl; f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args); - } else if( t.isTester() ) { + } else if(t.isTester()) { Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl; f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); + } else { + Unhandled(t); } } - | /* if-then-else */ - iteTerm[f] - - | /* parenthesized sub-formula */ - LPAREN formula[f] RPAREN + /* if-then-else */ + | iteTerm[f] + + /* parenthesized sub-formula / tuple literals */ + | LPAREN formula[f] { args.push_back(f); } + ( COMMA formula[f] { args.push_back(f); } )* RPAREN + { if(args.size() > 1) { + /* If args has elements, we must be a tuple literal. + * Otherwise, f is already the sub-formula, and + * there's nothing to do */ + f = EXPR_MANAGER->mkExpr(kind::TUPLE, args); + } + } - /* constants */ + /* boolean literals */ | TRUE_TOK { f = MK_CONST(true); } | FALSE_TOK { f = MK_CONST(false); } + /* arithmetic literals */ | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + /* bitvector literals */ | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); @@ -1064,19 +1338,34 @@ simpleTerm[CVC4::Expr& f] { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } + /* record literals */ + | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN + { PARSER_STATE->unimplementedFeature("records not implemented yet"); + f = Expr(); } - | /* variable */ - identifier[name,CHECK_DECLARED,SYM_VARIABLE] + /* variable / zero-ary constructor application */ + | identifier[name,CHECK_DECLARED,SYM_VARIABLE] { f = PARSER_STATE->getVariable(name); - // datatypes: 0-ary constructors - if( PARSER_STATE->getType(name).isConstructor() ){ - args.push_back( f ); + // datatypes: zero-ary constructors + if(PARSER_STATE->getType(name).isConstructor()) { + args.push_back(f); f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); } } ; /** + * Matches an entry in a record literal. + */ +recordEntry +@init { + std::string id; + Expr f; +} + : identifier[id,CHECK_DECLARED,SYM_VARIABLE] ASSIGN_TOK formula[f] + ; + +/** * Parses an ITE term. */ iteTerm[CVC4::Expr& f] @@ -1107,29 +1396,19 @@ iteElseTerm[CVC4::Expr& f] ; /** - * Parses a function symbol (an identifier). - * @param what kind of check to perform on the id - * @return the predicate symol - */ -functionSymbol[CVC4::Expr& f] -@init { - Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; - std::string name; -} - : identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { PARSER_STATE->checkFunctionLike(name); - f = PARSER_STATE->getVariable(name); } - ; - -/** * Parses a datatype definition */ datatypeDef[std::vector<CVC4::Datatype>& datatypes] @init { std::string id; } - : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { datatypes.push_back(Datatype(id)); } + : identifier[id,CHECK_NONE,SYM_SORT] + { datatypes.push_back(Datatype(id)); + if(!PARSER_STATE->isUnresolvedType(id)) { + // if not unresolved, must be undeclared + PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); + } + } EQUAL_TOK constructorDef[datatypes.back()] ( BAR constructorDef[datatypes.back()] )* ; @@ -1165,19 +1444,15 @@ constructorDef[CVC4::Datatype& type] selector[CVC4::Datatype::Constructor& ctor] @init { std::string id; - Type type; + Type t; } - : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON - maybeUndefinedBaseType[type,CHECK_NONE] - // TODO: this doesn't permit datatype fields of ARRAY or BITVECTOR - // type. This will be problematic, since, after all, you could - // have something nasty like this: - // - // DATATYPE list = cons(car:ARRAY list OF list, cdr:list) | nil END; - { if(type.isNull()) { - ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id)); + : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE] + { if(t.isNull()) { +# warning FIXME datatypes + //std::pair<Type, std::string> unresolved = PARSER_STATE->newUnresolvedType(); + //ctor.addArg(id, Datatype::UnresolvedType(unresolved.second); } else { - ctor.addArg(id, type); + ctor.addArg(id, t); } Debug("parser-idt") << "selector: " << id.c_str() << std::endl; } @@ -1195,6 +1470,17 @@ IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*; INTEGER_LITERAL: DIGIT+; /** + * Same as an integer literal converted to an unsigned int, but + * slightly more convenient AND works around a strange ANTLR bug (?) + * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was + * returning a reference to the wrong token?! + */ +numeral returns [unsigned k] + : INTEGER_LITERAL + { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); } + ; + +/** * Matches a decimal literal. */ DECIMAL_LITERAL: DIGIT+ '.' DIGIT+; @@ -1245,4 +1531,3 @@ COMMENT : '%' (~('\n' | '\r'))* { SKIP();; }; * Matches an allowed escaped character. */ fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r'); - diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index a3de3a61f..45a0edf95 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -53,6 +53,11 @@ public: /** Destructor. Frees the lexer and the parser. */ ~CvcInput(); + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_CVC4; + } + protected: /** Parse a command from the input. Returns <code>NULL</code> if there is diff --git a/src/parser/input.h b/src/parser/input.h index 71b2faeae..25023e1a8 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -142,6 +142,9 @@ public: /** Retrieve the remaining text in this input. */ virtual std::string getUnparsedText() = 0; + /** Get the language that this Input is reading. */ + virtual InputLanguage getLanguage() const throw() = 0; + protected: /** Create an input. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c8a9876d5..19d1bbcb8 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -29,6 +29,7 @@ #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" +#include "util/options.h" #include "util/Assert.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" @@ -39,14 +40,15 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) : +Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), d_input(input), d_declScopeAllocated(), d_declScope(&d_declScopeAllocated), d_done(false), d_checksEnabled(true), - d_strictMode(strictMode) { + d_strictMode(strictMode), + d_parseOnly(parseOnly) { d_input->setParser(*this); } @@ -136,7 +138,7 @@ Parser::mkFunction(const std::string& name, const Type& type) { return expr; } -const std::vector<Expr> +std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, const Type& type) { std::vector<Expr> vars; @@ -188,7 +190,7 @@ Parser::defineParameterizedType(const std::string& name, defineType(name, params, type); } -Type +SortType Parser::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Type type = d_exprManager->mkSort(name); @@ -196,34 +198,54 @@ Parser::mkSort(const std::string& name) { return type; } -Type +SortConstructorType Parser::mkSortConstructor(const std::string& name, size_t arity) { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - Type type = d_exprManager->mkSortConstructor(name, arity); + SortConstructorType type = d_exprManager->mkSortConstructor(name, arity); defineType(name, vector<Type>(arity), type); return type; } -std::vector<Type> +std::vector<SortType> Parser::mkSorts(const std::vector<std::string>& names) { - std::vector<Type> types; + std::vector<SortType> types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(mkSort(names[i])); } return types; } +SortType Parser::mkUnresolvedType(const std::string& name) { + SortType unresolved = mkSort(name); + d_unresolved.insert(unresolved); + return unresolved; +} + +bool Parser::isUnresolvedType(const std::string& name) { + if(!isDeclared(name, SYM_SORT)) { + return false; + } + return d_unresolved.find(getSort(name)) != d_unresolved.end(); +} + std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + std::vector<DatatypeType> types = - d_exprManager->mkMutualDatatypeTypes(datatypes); + d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); + Assert(datatypes.size() == types.size()); + for(unsigned i = 0; i < datatypes.size(); ++i) { DatatypeType t = types[i]; const Datatype& dt = t.getDatatype(); - Debug("parser-idt") << "define " << dt.getName() << " as " << t << std::endl; - defineType(dt.getName(), t); + const std::string& name = dt.getName(); + Debug("parser-idt") << "define " << name << " as " << t << std::endl; + if(isDeclared(name, SYM_SORT)) { + throw ParserException(name + " already declared"); + } + defineType(name, t); for(Datatype::const_iterator j = dt.begin(), j_end = dt.end(); j != j_end; @@ -258,6 +280,12 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { } } } + + // These are no longer used, and the ExprManager would have + // complained of a bad substitution if anything is left unresolved. + // Clear out the set. + d_unresolved.clear(); + return types; } @@ -273,9 +301,9 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { } void Parser::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type) - throw (ParserException) { + DeclarationCheck check, + SymbolType type) + throw(ParserException) { if(!d_checksEnabled) { return; } @@ -283,13 +311,13 @@ void Parser::checkDeclaration(const std::string& varName, switch(check) { case CHECK_DECLARED: if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared"); + parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); } break; case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared"); + parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); } break; @@ -301,21 +329,20 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunctionLike(const std::string& name) - throw (ParserException) { - if( d_checksEnabled && !isFunctionLike(name) ) { +void Parser::checkFunctionLike(const std::string& name) throw(ParserException) { + if(d_checksEnabled && !isFunctionLike(name)) { parseError("Expecting function-like symbol, found '" + name + "'"); } } -void Parser::checkArity(Kind kind, unsigned int numArgs) - throw (ParserException) { +void Parser::checkArity(Kind kind, unsigned numArgs) + throw(ParserException) { if(!d_checksEnabled) { return; } - unsigned int min = d_exprManager->minArity(kind); - unsigned int max = d_exprManager->maxArity(kind); + unsigned min = d_exprManager->minArity(kind); + unsigned max = d_exprManager->maxArity(kind); if( numArgs < min || numArgs > max ) { stringstream ss; @@ -331,7 +358,7 @@ void Parser::checkArity(Kind kind, unsigned int numArgs) } } -void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) { +void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) { if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); } @@ -371,7 +398,11 @@ Command* Parser::nextCommand() throw(ParserException) { } catch(Exception& e) { setDone(); stringstream ss; - ss << e; + // set the language of the stream, otherwise if it contains + // Exprs or Types it prints in the AST language + OutputLanguage outlang = + language::toOutputLanguage(d_input->getLanguage()); + ss << Expr::setlanguage(outlang) << e; parseError( ss.str() ); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 718b862ab..25fb30be6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -55,18 +55,20 @@ enum DeclarationCheck { CHECK_NONE }; -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(DeclarationCheck check) { +/** + * Returns a string representation of the given object (for + * debugging). + */ +inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { switch(check) { case CHECK_NONE: - return "CHECK_NONE"; + return out << "CHECK_NONE"; case CHECK_DECLARED: - return "CHECK_DECLARED"; + return out << "CHECK_DECLARED"; case CHECK_UNDECLARED: - return "CHECK_UNDECLARED"; + return out << "CHECK_UNDECLARED"; default: - Unreachable(); + return out << "DeclarationCheck!UNKNOWN"; } } @@ -80,16 +82,18 @@ enum SymbolType { SYM_SORT }; -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(SymbolType type) { +/** + * Returns a string representation of the given object (for + * debugging). + */ +inline std::ostream& operator<<(std::ostream& out, SymbolType type) { switch(type) { case SYM_VARIABLE: - return "SYM_VARIABLE"; + return out << "SYM_VARIABLE"; case SYM_SORT: - return "SYM_SORT"; + return out << "SYM_SORT"; default: - Unreachable(); + return out << "SymbolType!UNKNOWN"; } } @@ -133,10 +137,22 @@ class CVC4_PUBLIC Parser { /** Are we parsing in strict mode? */ bool d_strictMode; + /** Are we only parsing? */ + bool d_parseOnly; + /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; /** + * The current set of unresolved types. We can get by with this NOT + * being on the scope, because we can only have one DATATYPE + * definition going on at one time. This is a bit hackish; we + * depend on mkMutualDatatypeTypes() to check everything and clear + * this out. + */ + std::set<SortType> d_unresolved; + + /** * "Preemption commands": extra commands implied by subterms that * should be issued before the currently-being-parsed command is * issued. Used to support SMT-LIBv2 ":named" attribute on terms. @@ -155,7 +171,7 @@ protected: * @param input the parser input * @param strictMode whether to incorporate strict(er) compliance checks */ - Parser(ExprManager* exprManager, Input* input, bool strictMode = false); + Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: @@ -255,7 +271,7 @@ public: * @throws ParserException if checks are enabled and the check fails */ void checkDeclaration(const std::string& name, DeclarationCheck check, - SymbolType type = SYM_VARIABLE) throw (ParserException); + SymbolType type = SYM_VARIABLE) throw(ParserException); /** * Checks whether the given name is bound to a function. @@ -263,7 +279,7 @@ public: * @throws ParserException if checks are enabled and name is not * bound to a function */ - void checkFunctionLike(const std::string& name) throw (ParserException); + void checkFunctionLike(const std::string& name) throw(ParserException); /** * Check that <code>kind</code> can accept <code>numArgs</code> arguments. @@ -273,7 +289,7 @@ public: * <code>kind</code> cannot be applied to <code>numArgs</code> * arguments. */ - void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); + void checkArity(Kind kind, unsigned numArgs) throw(ParserException); /** * Check that <code>kind</code> is a legal operator in the current @@ -284,7 +300,7 @@ public: * @throws ParserException if the parser mode is strict and the * operator <code>kind</code> has not been enabled */ - void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); + void checkOperator(Kind kind, unsigned numArgs) throw(ParserException); /** * Returns the type for the variable with the given name. @@ -300,7 +316,7 @@ public: /** * Create a set of new CVC4 variable expressions of the given type. */ - const std::vector<Expr> + std::vector<Expr> mkVars(const std::vector<std::string> names, const Type& type); /** Create a new CVC4 function expression of the given type. */ @@ -327,17 +343,27 @@ public: /** * Creates a new sort with the given name. */ - Type mkSort(const std::string& name); + SortType mkSort(const std::string& name); /** * Creates a new sort constructor with the given name and arity. */ - Type mkSortConstructor(const std::string& name, size_t arity); + SortConstructorType mkSortConstructor(const std::string& name, size_t arity); /** * Creates new sorts with the given names (all of arity 0). */ - std::vector<Type> mkSorts(const std::vector<std::string>& names); + std::vector<SortType> mkSorts(const std::vector<std::string>& names); + + /** + * Creates a new "unresolved type," used only during parsing. + */ + SortType mkUnresolvedType(const std::string& name); + + /** + * Returns true IFF name is an unresolved type. + */ + bool isUnresolvedType(const std::string& name); /** * Create sorts of mutually-recursive datatypes. @@ -371,13 +397,37 @@ public: /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); + /** Parse and return the next command. */ Command* nextCommand() throw(ParserException); + + /** Parse and return the next expression. */ Expr nextExpression() throw(ParserException); - inline void parseError(const std::string& msg) throw (ParserException) { + /** Raise a parse error with the given message. */ + inline void parseError(const std::string& msg) throw(ParserException) { d_input->parseError(msg); } + /** + * If we are parsing only, don't raise an exception; if we are not, + * raise a parse error with the given message. There is no actual + * parse error, everything is as expected, but we cannot create the + * Expr, Type, or other requested thing yet due to internal + * limitations. Even though it's not a parse error, we throw a + * parse error so that the input line and column information is + * available. + * + * Think quantifiers. We don't have a TheoryQuantifiers yet, so we + * have no kind::FORALL or kind::EXISTS. But we might want to + * support parsing quantifiers (just not doing anything with them). + * So this mechanism gives you a way to do it with --parse-only. + */ + inline void unimplementedFeature(const std::string& msg) throw(ParserException) { + if(!d_parseOnly) { + parseError(msg); + } + } + inline void pushScope() { d_declScope->pushScope(); } inline void popScope() { d_declScope->popScope(); } @@ -405,7 +455,7 @@ public: * * In short, caveat emptor. */ - void useDeclarationsFrom(Parser* parser) { + inline void useDeclarationsFrom(Parser* parser) { if(parser == NULL) { d_declScope = &d_declScopeAllocated; } else { @@ -414,6 +464,13 @@ public: } /** + * Gets the current declaration level. + */ + inline size_t getDeclarationLevel() const throw() { + return d_declScope->getLevel(); + } + + /** * An expression stream interface for a parser. This stream simply * pulls expressions from the given Parser object. * diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 38f41f47a..9773445ed 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -2,10 +2,10 @@ /*! \file parser_builder.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -57,6 +57,7 @@ void ParserBuilder::init(ExprManager* exprManager, d_checksEnabled = true; d_strictMode = false; d_mmap = false; + d_parseOnly = false; } Parser *ParserBuilder::build() @@ -81,13 +82,13 @@ Parser *ParserBuilder::build() Parser *parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: - parser = new Smt(d_exprManager, input, d_strictMode); + parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_SMTLIB_V2: - parser = new Smt2(d_exprManager, input, d_strictMode); + parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; default: - parser = new Parser(d_exprManager, input, d_strictMode); + parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); } if( d_checksEnabled ) { @@ -124,18 +125,23 @@ ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { return *this; } - ParserBuilder& ParserBuilder::withMmap(bool flag) { d_mmap = flag; return *this; } +ParserBuilder& ParserBuilder::withParseOnly(bool flag) { + d_parseOnly = flag; + return *this; +} + ParserBuilder& ParserBuilder::withOptions(const Options& options) { return withInputLanguage(options.inputLanguage) .withMmap(options.memoryMap) .withChecks(options.semanticChecks) - .withStrictMode(options.strictParsing); + .withStrictMode(options.strictParsing) + .withParseOnly(options.parseOnly); } ParserBuilder& ParserBuilder::withStrictMode(bool flag) { diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 0d01104eb..6f4f051ec 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -2,10 +2,10 @@ /*! \file parser_builder.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -75,6 +75,10 @@ class CVC4_PUBLIC ParserBuilder { /** Should we memory-map a file input? */ bool d_mmap; + /** Are we parsing only? */ + bool d_parseOnly; + + /** Initialize this parser builder */ void init(ExprManager* exprManager, const std::string& filename); public: @@ -97,24 +101,50 @@ public: /** Set the parser to read a file for its input. (Default) */ ParserBuilder& withFileInput(); - /** Set the filename for use by the parser. If file input is used, + /** + * Set the filename for use by the parser. If file input is used, * this file will be opened and read by the parser. Otherwise, the * filename string (possibly a non-existent path) will only be used - * in error messages. */ + * in error messages. + */ ParserBuilder& withFilename(const std::string& filename); - /** Set the input language to be used by the parser. (Default: - LANG_AUTO). */ + /** + * Set the input language to be used by the parser. + * + * (Default: LANG_AUTO) + */ ParserBuilder& withInputLanguage(InputLanguage lang); - /** Should the parser memory-map its input? This is only relevant if - * the parser will have a file input. (Default: no) */ + /** + * Should the parser memory-map its input? This is only relevant if + * the parser will have a file input. + * + * (Default: no) + */ ParserBuilder& withMmap(bool flag = true); + /** + * Are we only parsing, or doing something with the resulting + * commands and expressions? This setting affects whether the + * parser will raise certain errors about unimplemented features, + * even if there isn't a parsing error, because the result of the + * parse would otherwise be an incorrect parse tree and the error + * would go undetected. This is specifically for circumstances + * where the parser is ahead of the functionality present elsewhere + * in CVC4 (such as quantifiers, subtypes, records, etc. in the CVC + * language parser). + */ + ParserBuilder& withParseOnly(bool flag = true); + /** Derive settings from the given options. */ ParserBuilder& withOptions(const Options& options); - /** Should the parser use strict mode? (Default: no) */ + /** + * Should the parser use strict mode? + * + * (Default: no) + */ ParserBuilder& withStrictMode(bool flag = true); /** Set the parser to use the given stream for its input. */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 96ac46bf1..86682f9a9 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -474,8 +474,8 @@ identifier[std::string& id, : IDENTIFIER { id = AntlrInput::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id - << " check? " << toString(check) - << " type? " << toString(type) << std::endl; + << " check? " << check + << " type? " << type << std::endl; PARSER_STATE->checkDeclaration(id, check, type); } ; @@ -489,7 +489,7 @@ let_identifier[std::string& id, : LET_IDENTIFIER { id = AntlrInput::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id - << " check? " << toString(check) << std::endl; + << " check? " << check << std::endl; PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } ; @@ -503,7 +503,7 @@ flet_identifier[std::string& id, : FLET_IDENTIFIER { id = AntlrInput::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id - << " check? " << toString(check) << std::endl; + << " check? " << check << std::endl; PARSER_STATE->checkDeclaration(id, check); } ; diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index bfac4f300..a8dabeffe 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -47,8 +47,8 @@ Smt::Logic Smt::toLogic(const std::string& name) { return logicMap[name]; } -Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode) : - Parser(exprManager,input,strictMode), +Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : + Parser(exprManager,input,strictMode,parseOnly), d_logicSet(false) { // Boolean symbols are always defined diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 388b4cd6d..98ebf6410 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -78,7 +78,7 @@ private: Logic d_logic; protected: - Smt(ExprManager* exprManager, Input* input, bool strictMode = false); + Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: /** diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index c5b147b71..0ab382c73 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -55,6 +55,11 @@ public: /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_SMTLIB; + } + protected: /** @@ -63,7 +68,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() + Command* parseCommand() throw(ParserException, TypeCheckingException, AssertionException); /** @@ -72,7 +77,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() + Expr parseExpr() throw(ParserException, TypeCheckingException, AssertionException); private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d27abc735..4f141891b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -673,8 +673,8 @@ symbol[std::string& id, : SYMBOL { id = AntlrInput::tokenText($SYMBOL); Debug("parser") << "symbol: " << id - << " check? " << toString(check) - << " type? " << toString(type) << std::endl; + << " check? " << check + << " type? " << type << std::endl; PARSER_STATE->checkDeclaration(id, check, type); } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 03b901164..4bc90ec8f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -2,10 +2,10 @@ /*! \file smt2.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -24,8 +24,8 @@ namespace CVC4 { namespace parser { -Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) : - Parser(exprManager,input,strictMode), +Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : + Parser(exprManager,input,strictMode,parseOnly), d_logicSet(false) { if( !strictModeEnabled() ) { addTheory(Smt2::THEORY_CORE); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ef5f5e729..e9363b970 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -2,10 +2,10 @@ /*! \file smt2.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -48,7 +48,7 @@ private: Smt::Logic d_logic; protected: - Smt2(ExprManager* exprManager, Input* input, bool strictMode = false); + Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: /** diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 836472107..04fe48fe1 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -64,6 +64,11 @@ public: /** Destructor. Frees the lexer and the parser. */ virtual ~Smt2Input(); + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_SMTLIB_V2; + } + protected: /** diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 97f434e9b..409518fcf 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -85,6 +85,24 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; break; } + case kind::TYPE_CONSTANT: + switch(TypeConstant tc = n.getConst<TypeConstant>()) { + case REAL_TYPE: + out << "REAL"; + break; + case INTEGER_TYPE: + out << "INT"; + break; + case BOOLEAN_TYPE: + out << "BOOLEAN"; + break; + case KIND_TYPE: + out << "TYPE"; + break; + default: + Unhandled(tc); + } + break; case kind::BUILTIN: switch(Kind k = n.getConst<Kind>()) { case kind::EQUAL: out << '='; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9bad4c7b5..3f7eb58c0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -178,7 +178,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(toDepth != 0) { n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types, language::output::LANG_SMTLIB_V2); - out << " "; } else { out << "(...)"; } @@ -207,7 +206,7 @@ void printBvParameterizedOp(std::ostream& out, TNode n) { switch(n.getKind()) { case kind::BITVECTOR_EXTRACT: { BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>(); - out << "extract " << p.high << " " << p.low; + out << "extract " << p.high << ' ' << p.low; break; } case kind::BITVECTOR_REPEAT: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bcf6339ac..314e6b714 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -102,7 +102,7 @@ void TheoryBV::check(Effort e) { break; } default: - Unhandled(); + Unhandled(assertion.getKind()); } } diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 49b210501..a27fd351c 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -185,8 +185,7 @@ public: unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ? (unsigned) n.getOperator().getConst<BitVectorSignExtend>() : (unsigned) n.getOperator().getConst<BitVectorZeroExtend>(); - - return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); + return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } }; diff --git a/src/theory/theory.h b/src/theory/theory.h index b5122d3c5..ac40c55d1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -2,10 +2,10 @@ /*! \file theory.h ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, taking, barrett + ** Major contributors: dejan + ** Minor contributors (to current version): taking, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -59,10 +59,10 @@ private: friend class ::CVC4::TheoryEngine; - /** - * Disallow default construction. - */ - Theory(); + // Disallow default construction, copy, assignment. + Theory() CVC4_UNUSED; + Theory(const Theory&) CVC4_UNUSED; + Theory& operator=(const Theory&) CVC4_UNUSED; /** * A unique integer identifying the theory diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6973a7cad..85f26f012 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -172,11 +172,13 @@ public: ~TheoryEngine(); /** - * Adds a theory. Only one theory per theoryId can be present, so if there is another theory it will be deleted. + * Adds a theory. Only one theory per theoryId can be present, so if + * there is another theory it will be deleted. */ template <class TheoryClass> void addTheory() { - TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); + TheoryClass* theory = + new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); d_theoryTable[theory->getId()] = theory; d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); } diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index 062bf11b6..95d5fb435 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bitvector.h +/*! \file boolean_simplification.h ** \verbatim - ** Original author: dejan - ** Major contributors: cconway - ** Minor contributors (to current version): mdeters + ** Original author: taking + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -107,10 +107,8 @@ public: } } -};/* class BitVector */ - - +};/* class BooleanSimplification */ }/* CVC4 namespace */ -#endif /* __CVC4__BITVECTOR_H */ +#endif /* __CVC4__BOOLEAN_SIMPLIFICATION_H */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index c795eaba6..afd5af703 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -62,18 +62,23 @@ size_t Datatype::indexOf(Expr item) { } void Datatype::resolve(ExprManager* em, - const std::map<std::string, DatatypeType>& resolutions) + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements) throw(AssertionException, DatatypeResolutionException) { - CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!d_resolved, "cannot resolve a Datatype twice"); - CheckArgument(resolutions.find(d_name) != resolutions.end(), "Datatype::resolve(): resolutions doesn't contain me!"); + AssertArgument(resolutions.find(d_name) != resolutions.end(), + "Datatype::resolve(): resolutions doesn't contain me!"); + AssertArgument(placeholders.size() == replacements.size(), placeholders, + "placeholders and replacements must be the same size"); DatatypeType self = (*resolutions.find(d_name)).second; - CheckArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); + AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; size_t index = 0; for(iterator i = begin(), i_end = end(); i != i_end; ++i) { - (*i).resolve(em, self, resolutions); + (*i).resolve(em, self, resolutions, placeholders, replacements); Assert((*i).isResolved()); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); @@ -167,9 +172,11 @@ const Datatype::Constructor& Datatype::operator[](size_t index) const { } void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, - const std::map<std::string, DatatypeType>& resolutions) + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements) throw(AssertionException, DatatypeResolutionException) { - CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); CheckArgument(!isResolved(), "cannot resolve a Datatype constructor twice; " "perhaps the same constructor was added twice, " @@ -177,6 +184,7 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, size_t index = 0; for(iterator i = begin(), i_end = end(); i != i_end; ++i) { if((*i).d_selector.isNull()) { + // the unresolved type wasn't created here; do name resolution string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1); (*i).d_name.resize((*i).d_name.find('\0')); if(typeName == "") { @@ -194,7 +202,13 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, } } } else { - (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*i).d_selector.getType())); + // the type for the selector already exists; may need + // complex-type substitution + Type range = (*i).d_selector.getType(); + if(!placeholders.empty()) { + range = range.substitute(placeholders, replacements); + } + (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, range)); } Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); (*i).d_resolved = true; @@ -204,7 +218,9 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, // Set constructor/tester last, since Constructor::isResolved() // returns true when d_tester is not the null Expr. If something - // fails above, we want Constuctor::isResolved() to remain "false" + // fails above, we want Constuctor::isResolved() to remain "false". + // Further, mkConstructorType() iterates over the selectors, so + // should get the results of any resolutions we did above. d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self)); d_name.resize(d_name.find('\0')); d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self)); @@ -302,6 +318,8 @@ bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() { return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } +static const int s_printDatatypeNamesOnly = std::ios_base::xalloc(); + std::string Datatype::Constructor::Arg::getSelectorTypeName() const { Type t; if(isResolved()) { @@ -315,10 +333,35 @@ std::string Datatype::Constructor::Arg::getSelectorTypeName() const { } } - return t.isDatatype() ? DatatypeType(t).getDatatype().getName() : t.toString(); + // Unfortunately, in the case of complex selector types, we can + // enter nontrivial recursion here. Make sure that doesn't happen. + stringstream ss; + ss << Expr::setlanguage(language::output::LANG_CVC4); + ss.iword(s_printDatatypeNamesOnly) = 1; + t.toStream(ss); + return ss.str(); } std::ostream& operator<<(std::ostream& os, const Datatype& dt) { + // These datatype things are recursive! Be very careful not to + // print an infinite chain of them. + long& printNameOnly = os.iword(s_printDatatypeNamesOnly); + Debug("datatypes") << "printNameOnly is " << printNameOnly << std::endl; + if(printNameOnly) { + return os << dt.getName(); + } + + class Scope { + long& d_ref; + long d_oldValue; + public: + Scope(long& ref, long value) : d_ref(ref), d_oldValue(ref) { d_ref = value; } + ~Scope() { d_ref = d_oldValue; } + } scope(printNameOnly, 1); + // when scope is destructed, the value pops back + + Debug("datatypes") << "printNameOnly is now " << printNameOnly << std::endl; + // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); diff --git a/src/util/datatype.h b/src/util/datatype.h index e3e7d669c..26e58264a 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -155,6 +155,7 @@ public: * only permitted after resolution. */ Expr getSelector() const; + /** * Get the name of the type of this constructor argument * (Datatype field). Can be used for not-yet-resolved Datatypes @@ -183,7 +184,9 @@ public: std::vector<Arg> d_args; void resolve(ExprManager* em, DatatypeType self, - const std::map<std::string, DatatypeType>& resolutions) + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements) throw(AssertionException, DatatypeResolutionException); friend class Datatype; @@ -277,7 +280,9 @@ private: * will fail after a call to resolve(). */ void resolve(ExprManager* em, - const std::map<std::string, DatatypeType>& resolutions) + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements) throw(AssertionException, DatatypeResolutionException); friend class ExprManager;// for access to resolve() diff --git a/src/util/options.cpp b/src/util/options.cpp index 6018ce611..1329a443a 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -121,7 +121,7 @@ static const string optionsDescription = "\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\ - --enable-arithmetic-propagation turns on arithmetic propagation\n \ + --enable-arithmetic-propagation turns on arithmetic propagation\n\ --incremental enable incremental solving\n"; static const string languageDescription = "\ diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 92db8d453..edda090ba 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -8,19 +8,19 @@ MAKEFLAGS = -k # put it below in "TESTS +=" # Regression tests for SMT inputs -SMT_TESTS = +SMT_TESTS = # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = # Regression tests for PL inputs CVC_TESTS = bvsimple.cvc # Regression tests derived from bug reports -BUG_TESTS = +BUG_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ - test00.smt - + test00.smt \ + bvcomp.smt diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc new file mode 100644 index 000000000..c3397dfd7 --- /dev/null +++ b/test/regress/regress0/bv/bvcomp.cvc @@ -0,0 +1,6 @@ +% EXPECT: valid +% EXIT: 20 + +x : BITVECTOR(10); + +QUERY x /= ~x; diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index f1cb8ff01..59fe57386 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -4,18 +4,47 @@ % Some tests from the CVC3 user manual. % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html +x : BITVECTOR(5); +y : BITVECTOR(4); +yy : BITVECTOR(3); + +bv : BITVECTOR(10); +a : BOOLEAN; + +xx : BITVECTOR(8); +zz : BITVECTOR(12); + +x4, y4 : BITVECTOR(4); + QUERY +( 0bin0000111101010000 = 0hex0f50 ) AND ( 0bin01@0bin0 = 0bin010 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND ( 0bin0011 << 3 = 0bin0011000 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND -TRUE - % these not working yet.. -%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND +% +%( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND %( SX(0bin100, 5) = 0bin11100 ) AND % -%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND -%( SX(0bin100, 3) = 0bin100 ) -; +%( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND +%( SX(0bin100, 3) = 0bin100 ) AND +% +%( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND +% +%( x4 = 0hex5 AND y4 = 0bin0101 ) => +%( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND +% ( NOT(BVLT(x4,y4)) ) AND +% ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND +% ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND + + +( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND +( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND + +( xx = 0hexff AND zz = 0hexff0 => + ( zz = xx << 4 ) AND + ( (zz >> 4)[7:0] = xx ) ) AND + +TRUE; diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index 982731b34..6d1641092 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,4 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared +% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol BOOL not declared as a type p : BOOL; % EXIT: 1 diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index 497f11c08..821b43a2f 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -88,11 +88,15 @@ int runTest() { AlwaysAssert(parser->done(), "parser should be done"); string instr = "(= (f (f y)) x)"; + cout << "starting with: " << instr << endl; string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2); + cout << "in SMT2 : " << smt2 << endl; string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB); - //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4); - //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); - string out = smt1; + cout << "in SMT1 : " << smt1 << endl; + string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4); + cout << "in CVC : " << cvc << endl; + string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); + cout << "back to SMT2 : " << out << endl; AlwaysAssert(out == smt2, "differences in output"); diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index dbc8e2281..f288f6b1a 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -214,6 +214,8 @@ public: tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); tryGoodInput("%% nothing but a comment"); tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); + tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible + tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible } void testBadCvc4Inputs() { @@ -225,8 +227,11 @@ public: tryBadInput("0x : INT;"); // 0x isn't an identifier tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal - tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function + tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible + tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared + tryBadInput("a : INT; a: INT = 5;"); // can't define after decl + tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type } void testGoodCvc4Exprs() { |