summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/exception.h2
-rw-r--r--src/expr/node_manager.h36
-rw-r--r--src/parser/smt2/Smt2.g21
3 files changed, 40 insertions, 19 deletions
diff --git a/src/base/exception.h b/src/base/exception.h
index 704ca928e..0d1abd9e0 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -128,7 +128,7 @@ template <class T> inline void CheckArgument(bool cond, const T& arg,
template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED,
const char* tail CVC4_UNUSED) {
if(__builtin_expect( ( !cond ), false )) { \
- throw ::CVC4::IllegalArgumentException("", "", ""); \
+ throw ::CVC4::IllegalArgumentException("", "", tail); \
} \
}
template <class T> inline void CheckArgument(bool cond, const T& arg)
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8daaa04e6..f47795c15 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1095,8 +1095,10 @@ 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].isFirstClass(), sorts,
- "cannot create function types for argument types that are not first-class");
+ CheckArgument(sorts[i].isFirstClass(),
+ sorts,
+ "cannot create function types for argument types that are "
+ "not first-class. Try option --uf-ho.");
sortNodes.push_back(sorts[i]);
}
CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1],
@@ -1109,8 +1111,10 @@ 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].isFirstClass(), sorts,
- "cannot create predicate types for argument types that are not first-class");
+ CheckArgument(sorts[i].isFirstClass(),
+ sorts,
+ "cannot create predicate types for argument types that are "
+ "not first-class. Try option --uf-ho.");
sortNodes.push_back(sorts[i]);
}
sortNodes.push_back(booleanType());
@@ -1143,10 +1147,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
"unexpected NULL index type");
CheckArgument(!constituentType.isNull(), constituentType,
"unexpected NULL constituent type");
- CheckArgument(indexType.isFirstClass(), indexType,
- "cannot index arrays by types that are not first-class");
- CheckArgument(constituentType.isFirstClass(), constituentType,
- "cannot store types that are not first-class in arrays");
+ CheckArgument(indexType.isFirstClass(),
+ indexType,
+ "cannot index arrays by types that are not first-class. Try "
+ "option --uf-ho.");
+ CheckArgument(constituentType.isFirstClass(),
+ constituentType,
+ "cannot store types that are not first-class in arrays. Try "
+ "option --uf-ho.");
Debug("arrays") << "making array type " << indexType << " "
<< constituentType << std::endl;
return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
@@ -1155,8 +1163,10 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
CheckArgument(!elementType.isNull(), elementType,
"unexpected NULL element type");
- CheckArgument(elementType.isFirstClass(), elementType,
- "cannot store types that are not first-class in sets");
+ CheckArgument(elementType.isFirstClass(),
+ elementType,
+ "cannot store types that are not first-class in sets. Try "
+ "option --uf-ho.");
Debug("sets") << "making sets type " << elementType << std::endl;
return mkTypeNode(kind::SET_TYPE, elementType);
}
@@ -1164,8 +1174,10 @@ inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
CheckArgument(domain.isDatatype(), domain,
"cannot create non-datatype selector type");
- CheckArgument(range.isFirstClass(), range,
- "cannot have selector fields that are not first-class types");
+ CheckArgument(range.isFirstClass(),
+ range,
+ "cannot have selector fields that are not first-class types. "
+ "Try option --uf-ho.");
return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
}
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9110b9660..c1a9df887 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -305,8 +305,11 @@ command [std::unique_ptr<CVC4::Command>* cmd]
t = PARSER_STATE->mkFlatFunctionType(sorts, t);
}
if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
- PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
- "be declared in logic ");
+ PARSER_STATE->parseError(
+ "Functions (of non-zero arity) cannot "
+ "be declared in logic "
+ + PARSER_STATE->getLogic().getLogicString()
+ + " unless option --uf-ho is used.");
}
// we allow overloading for function declarations
if (PARSER_STATE->sygus_v1())
@@ -1283,8 +1286,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{ Type t;
if(sorts.size() > 1) {
if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
- PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
- "cannot be declared in logic ");
+ PARSER_STATE->parseError(
+ "Functions (of non-zero arity) cannot "
+ "be declared in logic "
+ + PARSER_STATE->getLogic().getLogicString()
+ + " unless option --uf-ho is used");
}
// must flatten
Type range = sorts.back();
@@ -1310,8 +1316,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{ Type t = EXPR_MANAGER->booleanType();
if(sorts.size() > 0) {
if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
- PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) "
- "cannot be declared in logic ");
+ PARSER_STATE->parseError(
+ "Functions (of non-zero arity) cannot "
+ "be declared in logic "
+ + PARSER_STATE->getLogic().getLogicString()
+ + " unless option --uf-ho is used");
}
t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback