/*! \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
d_context->push();
}
-} // namespace CVC4
+size_t DeclarationScope::getLevel() const throw() {
+ return d_context->getLevel();
+}
+
+}/* CVC4 namespace */
/*! \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
*/
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;
/** Push a scope level. */
void pushScope() throw();
+ /** Get the current level of this declaration scope. */
+ size_t getLevel() const throw();
+
};/* class DeclarationScope */
}/* CVC4 namespace */
}
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)));
*/
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.
* 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.
** 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
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;
}
${getConst_instantiations}
-#line 682 "${template}"
+#line 758 "${template}"
namespace expr {
/*! \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
* The enumeration for the built-in atomic types.
*/
enum TypeConstant {
- ${type_constant_list}
+${type_constant_list}
LAST_TYPE
};/* enum TypeConstant */
inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
switch(typeConstant) {
- ${type_constant_descriptions}
+${type_constant_descriptions}
default:
out << "UNKNOWN_TYPE_CONSTANT";
break;
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;
}
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);
}
}
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;
"
}
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;
"
}
"
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;
"
}
}
/**
- * 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
/**
* 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
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);
}
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);
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());
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);
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 );
}
}
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;
}
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,
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>();
}
*/
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
/** 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 */
/*! \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
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();
}
*/
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.
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;
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;
}
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:
/** 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:
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;
}
OF_TOK = 'OF';
WITH_TOK = 'WITH';
+ SUBTYPE_TOK = 'SUBTYPE';
+
FORALL_TOK = 'FORALL';
EXISTS_TOK = 'EXISTS';
+ PATTERN_TOK = 'PATTERN';
+
+ LAMBDA = 'LAMBDA';
// Symbols
SEMICOLON = ';';
BAR = '|';
DOT = '.';
+ DOTDOT = '..';
SQHASH = '[#';
HASHSQ = '#]';
INTDIV_TOK = 'DIV';
FLOOR_TOK = 'FLOOR';
- //IS_INTEGER_TOK = 'IS_INTEGER';
-
// Bitvectors
BITVECTOR_TOK = 'BITVECTOR';
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';
// 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
;
;
/**
- * 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);
}
}
}
;
-/**
- * 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.
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); } )*
;
;
/**
- * 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
;
/**
}
;
-/**
- * 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 )+
;
/**
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]
--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]
@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]
;
@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); }
| 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]
;
@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) {
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");
}
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");
}
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]
;
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 {
@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); }
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);
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);
{ 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.
*/
{ f = MK_EXPR(CVC4::kind::ITE, args); }
;
-/**
- * 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
*/
@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()] )*
;
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;
}
*/
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.
*/
* Matches an allowed escaped character.
*/
fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
-
/** 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
/** 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.
#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"
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);
}
return expr;
}
-const std::vector<Expr>
+std::vector<Expr>
Parser::mkVars(const std::vector<std::string> names,
const Type& type) {
std::vector<Expr> vars;
defineType(name, params, type);
}
-Type
+SortType
Parser::mkSort(const std::string& name) {
Debug("parser") << "newSort(" << name << ")" << std::endl;
Type type = d_exprManager->mkSort(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;
}
}
}
+
+ // 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;
}
}
void Parser::checkDeclaration(const std::string& varName,
- DeclarationCheck check,
- SymbolType type)
- throw (ParserException) {
+ DeclarationCheck check,
+ SymbolType type)
+ throw(ParserException) {
if(!d_checksEnabled) {
return;
}
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;
}
}
-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;
}
}
-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) );
}
} 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() );
}
}
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";
}
}
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";
}
}
/** 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
* @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:
* @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.
* @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.
* <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
* @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.
/**
* 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. */
/**
* 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.
/** 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(); }
*
* In short, caveat emptor.
*/
- void useDeclarationsFrom(Parser* parser) {
+ inline void useDeclarationsFrom(Parser* parser) {
if(parser == NULL) {
d_declScope = &d_declScopeAllocated;
} else {
}
}
+ /**
+ * 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.
/*! \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
d_checksEnabled = true;
d_strictMode = false;
d_mmap = false;
+ d_parseOnly = false;
}
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 ) {
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) {
/*! \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
/** 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:
/** 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. */
: 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); }
;
: 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); }
;
: 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); }
;
** \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
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
** 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
Logic d_logic;
protected:
- Smt(ExprManager* exprManager, Input* input, bool strictMode = false);
+ Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
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:
/**
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
+ Command* parseCommand()
throw(ParserException, TypeCheckingException, AssertionException);
/**
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
+ Expr parseExpr()
throw(ParserException, TypeCheckingException, AssertionException);
private:
: 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); }
;
/*! \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
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);
/*! \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
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:
/**
/** 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:
/**
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;
if(toDepth != 0) {
n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
types, language::output::LANG_SMTLIB_V2);
- out << " ";
} else {
out << "(...)";
}
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:
break;
}
default:
- Unhandled();
+ Unhandled(assertion.getKind());
}
}
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());
}
};
/*! \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
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
~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));
}
/********************* */
-/*! \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
}
}
-};/* class BitVector */
-
-
+};/* class BooleanSimplification */
}/* CVC4 namespace */
-#endif /* __CVC4__BITVECTOR_H */
+#endif /* __CVC4__BOOLEAN_SIMPLIFICATION_H */
}
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++);
}
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, "
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 == "") {
}
}
} 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;
// 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));
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()) {
}
}
- 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);
* 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
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;
* 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()
--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 = "\
# 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
--- /dev/null
+% EXPECT: valid
+% EXIT: 20
+
+x : BITVECTOR(10);
+
+QUERY x /= ~x;
% 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;
% 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
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");
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() {
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() {
projects / cvc5.git / commitdiff