summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/declaration_scope.cpp4
-rw-r--r--src/expr/declaration_scope.h6
-rw-r--r--src/parser/cvc/Cvc.g211
-rw-r--r--src/parser/parser.cpp15
-rw-r--r--src/parser/parser.h14
-rw-r--r--src/printer/cvc/cvc_printer.cpp27
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h11
-rw-r--r--src/theory/uf/theory_uf_type_rules.h10
-rw-r--r--test/system/ouroborous.cpp1
-rw-r--r--test/unit/parser/parser_black.h2
10 files changed, 190 insertions, 111 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index cfcc62335..8dd329b83 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -72,6 +72,10 @@ bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const thr
return found != d_exprMap->end() && d_functions->contains((*found).second);
}
+bool DeclarationScope::isBoundDefinedFunction(Expr func) const throw() {
+ return d_functions->contains(func);
+}
+
Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) {
return (*d_exprMap->find(name)).second;
}
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 6d89f5f4e..699dca6fa 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -134,6 +134,12 @@ public:
bool isBoundDefinedFunction(const std::string& name) const throw();
/**
+ * Check whether an Expr was bound to a function (i.e., was the
+ * second arg to bindDefinedFunction()).
+ */
+ bool isBoundDefinedFunction(Expr func) const throw();
+
+ /**
* Check whether a name is bound to a type (or type constructor).
*
* @param name the identifier to check.
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 794f0a670..543538f32 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -88,6 +88,7 @@ tokens {
BAR = '|';
DOT = '.';
DOTDOT = '..';
+ UNDERSCORE = '_';
SQHASH = '[#';
HASHSQ = '#]';
@@ -349,6 +350,14 @@ Expr createPrecedenceTree(ExprManager* em,
return e;
}
+/** Add n NOTs to the front of e and return the result. */
+Expr addNots(ExprManager* em, size_t n, Expr e) {
+ while(n-- > 0) {
+ e = em->mkExpr(kind::NOT, e);
+ }
+ return e;
+}
+
}/* @parser::members */
@header {
@@ -480,6 +489,7 @@ command returns [CVC4::Command* cmd = 0]
{ PARSER_STATE->popScope();
cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
| toplevelDeclaration[cmd]
+ | SEMICOLON c=command { $cmd = c; }
| EOF
;
@@ -710,7 +720,6 @@ type[CVC4::Type& t,
} else {
args.push_back(t);
}
- Debug("parser") << "type: " << t << std::endl;
}
( ARROW_TOK type[t2,check] { args.push_back(t2); } )?
{ if(t2.isNull()) {
@@ -783,9 +792,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
t = Type(); }
/* subrange types */
- | LBRACKET bound DOTDOT bound RBRACKET
+/* parsing not working -- some kind of conflict betw [0..1] and 0.0
+ | bounds
{ PARSER_STATE->unimplementedFeature("subranges not supported yet");
t = Type(); }
+*/
/* tuple types / old-style function types */
| LBRACKET type[t,check] { types.push_back(t); }
@@ -828,12 +839,6 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
}
;
-bound
- : '_'
- | numeral
- | MINUS_TOK numeral
- ;
-
/**
* Matches a type identifier. Returns the identifier. If the type is
* declared, returns the Type in the 't' parameter; otherwise a null
@@ -873,6 +878,52 @@ typeLetDecl[CVC4::parser::DeclarationCheck check]
formula[CVC4::Expr& f]
@init {
Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ Expr f2;
+ std::vector<CVC4::Expr> expressions;
+ std::vector<unsigned> operators;
+ unsigned op;
+}
+ : n=nots
+ ( prefixFormula[f]
+ { f = addNots(EXPR_MANAGER, n, f); }
+ | comparison[f]
+ { f = addNots(EXPR_MANAGER, n, f);
+ expressions.push_back(f);
+ }
+ i=morecomparisons[expressions,operators]?
+ { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+ )
+ ;
+
+morecomparisons[std::vector<CVC4::Expr>& expressions,
+ std::vector<unsigned>& operators] returns [size_t i]
+@init {
+ unsigned op;
+ Expr f;
+ $i = expressions.size();
+}
+ : booleanBinop[op] { operators.push_back(op); }
+ n=nots
+ ( prefixFormula[f]
+ { expressions.push_back(addNots(EXPR_MANAGER, n, f)); }
+ | comparison[f]
+ { f = addNots(EXPR_MANAGER, n, f);
+ expressions.push_back(f);
+ }
+ inner=morecomparisons[expressions,operators]?
+ )
+ ;
+
+/** Matches 0 or more NOTs. */
+nots returns [size_t n]
+@init {
+ $n = 0;
+}
+ : ( NOT_TOK { ++$n; } )*
+ ;
+
+prefixFormula[CVC4::Expr& f]
+@init {
std::vector<std::string> ids;
std::vector<Expr> terms;
std::vector<Type> types;
@@ -894,20 +945,20 @@ formula[CVC4::Expr& f]
f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
}
- /* lets: letDecl defines the variables and functionss, we just
+ /* 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 */
| 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);
+ Expr func = PARSER_STATE->mkAnonymousFunction("lambda", t);
Command* cmd = new DefineFunctionCommand(func, terms, f);
PARSER_STATE->preemptCommand(cmd);
f = func;
@@ -920,9 +971,6 @@ formula[CVC4::Expr& f]
PARSER_STATE->unimplementedFeature("array literals not supported yet");
f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()));
}
-
- /* everything else */
- | booleanFormula[f]
;
instantiationPatterns
@@ -949,36 +997,6 @@ letDecl
}
;
-booleanFormula[CVC4::Expr& f]
-@init {
- std::vector<CVC4::Expr> expressions;
- std::vector<unsigned> operators;
- unsigned op;
- unsigned notCount = 0;
-}
- : ( NOT_TOK { ++notCount; } )* comparison[f]
- { while(notCount > 0) {
- --notCount;
- f = EXPR_MANAGER->mkExpr(kind::NOT, f);
- }
- expressions.push_back(f);
- Assert(notCount == 0);
- }
- ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f]
- { 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);
- }
- )*
- { Assert(notCount == 0);
- f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
- ;
-
booleanBinop[unsigned& op]
@init {
op = LT(1)->getType(LT(1));
@@ -1089,17 +1107,19 @@ bvNegTerm[CVC4::Expr& f]
;
/**
- * Parses an array select / bitvector extract / bitvector shift.
- * These are all parsed the same way because they are all effectively
- * post-fix operators and can continue piling onto an expression.
- * Array selects and bitvector extracts even share similar syntax with
- * their use of [ square brackets ], so we left-factor as much out as
- * possible to make ANTLR happy.
+ * Parses an array select / bitvector extract / bitvector shift /
+ * function or constructor application. These are all parsed the same
+ * way because they are all effectively post-fix operators and can
+ * continue piling onto an expression. Array selects and bitvector
+ * extracts even share similar syntax with their use of [ square
+ * brackets ], so we left-factor as much out as possible to make ANTLR
+ * happy.
*/
selectExtractShift[CVC4::Expr& f]
@init {
Expr f2;
bool extract, left;
+ std::vector<Expr> args;
}
: bvTerm[f]
( /* array select / bitvector extract */
@@ -1115,6 +1135,8 @@ selectExtractShift[CVC4::Expr& f]
f = MK_EXPR(CVC4::kind::SELECT, f, f2);
}
}
+
+ /* left- or right-shift */
| ( LEFTSHIFT_TOK { left = true; }
| RIGHTSHIFT_TOK { left = false; } ) k=numeral
{ // Defined in:
@@ -1127,6 +1149,29 @@ selectExtractShift[CVC4::Expr& f]
MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
}
}
+
+ /* function/constructor application */
+ | LPAREN { args.push_back(f); }
+ formula[f] { args.push_back(f); }
+ ( COMMA formula[f] { args.push_back(f); } )* RPAREN
+ // TODO: check arity
+ { Type t = args.front().getType();
+ Debug("parser") << "type is " << t << std::endl;
+ Debug("parser") << "expr is " << args.front() << std::endl;
+ if(PARSER_STATE->isDefinedFunction(args.front())) {
+ f = MK_EXPR(CVC4::kind::APPLY, args);
+ } else if(t.isFunction()) {
+ f = MK_EXPR(CVC4::kind::APPLY_UF, args);
+ } else if(t.isConstructor()) {
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ } else if(t.isSelector()) {
+ f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
+ } else if(t.isTester()) {
+ f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
+ } else {
+ Unhandled(t);
+ }
+ }
)*
;
@@ -1135,15 +1180,15 @@ bvTerm[CVC4::Expr& f]
Expr f2;
}
/* BV xor */
- : BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
- | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
- | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
- | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
- | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
/* BV unary minus */
@@ -1159,7 +1204,7 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV subtraction */
@@ -1172,12 +1217,12 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV multiplication */
| BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
- { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
+ { f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
if(k == 0) {
PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
}
@@ -1185,7 +1230,7 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV unsigned division */
@@ -1271,44 +1316,8 @@ simpleTerm[CVC4::Expr& f]
std::vector<Expr> args;
Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- /* 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 = 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()) {
- Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl;
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
- } 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()) {
- 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]
+ : iteTerm[f]
/* parenthesized sub-formula / tuple literals */
| LPAREN formula[f] { args.push_back(f); }
@@ -1345,9 +1354,11 @@ simpleTerm[CVC4::Expr& f]
| identifier[name,CHECK_DECLARED,SYM_VARIABLE]
{ f = PARSER_STATE->getVariable(name);
// datatypes: zero-ary constructors
- if(PARSER_STATE->getType(name).isConstructor()) {
- args.push_back(f);
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ Type t = PARSER_STATE->getType(name);
+ if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
+ // don't require parentheses, immediately turn it into an
+ // apply
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
}
}
;
@@ -1475,7 +1486,7 @@ numeral returns [unsigned k]
/**
* Matches a decimal literal.
*/
-DECIMAL_LITERAL: DIGIT+ '.' DIGIT+;
+DECIMAL_LITERAL: DIGIT+ DOT DIGIT+;
/**
* Matches a hexadecimal constant.
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 19d1bbcb8..29ade43c1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -45,6 +45,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
d_input(input),
d_declScopeAllocated(),
d_declScope(&d_declScopeAllocated),
+ d_anonymousFunctionCount(0),
d_done(false),
d_checksEnabled(true),
d_strictMode(strictMode),
@@ -117,6 +118,13 @@ bool Parser::isDefinedFunction(const std::string& name) {
return d_declScope->isBoundDefinedFunction(name);
}
+/* Returns true if the Expr is a defined function. */
+bool Parser::isDefinedFunction(Expr func) {
+ // more permissive in type than isFunction(), because defined
+ // functions can be zero-ary and declared functions cannot.
+ return d_declScope->isBoundDefinedFunction(func);
+}
+
/* Returns true if name is bound to a function returning boolean. */
bool Parser::isPredicate(const std::string& name) {
return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
@@ -138,6 +146,13 @@ Parser::mkFunction(const std::string& name, const Type& type) {
return expr;
}
+Expr
+Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
+ stringstream name;
+ name << prefix << ':' << ++d_anonymousFunctionCount;
+ return mkFunction(name.str(), type);
+}
+
std::vector<Expr>
Parser::mkVars(const std::vector<std::string> names,
const Type& type) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 25fb30be6..033abb42a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -125,8 +125,8 @@ class CVC4_PUBLIC Parser {
*/
DeclarationScope* d_declScope;
- /** The name of the input file. */
-// std::string d_filename;
+ /** How many anonymous functions we've created. */
+ size_t d_anonymousFunctionCount;
/** Are we done */
bool d_done;
@@ -322,6 +322,13 @@ public:
/** Create a new CVC4 function expression of the given type. */
Expr mkFunction(const std::string& name, const Type& type);
+ /**
+ * Create a new CVC4 function expression of the given type,
+ * appending a unique index to its name. (That's the ONLY
+ * difference between mkAnonymousFunction() and mkFunction()).
+ */
+ Expr mkAnonymousFunction(const std::string& prefix, const Type& type);
+
/** Create a new variable definition (e.g., from a let binding). */
void defineVar(const std::string& name, const Expr& val);
@@ -394,6 +401,9 @@ public:
/** Is the symbol bound to a defined function? */
bool isDefinedFunction(const std::string& name);
+ /** Is the Expr a defined function? */
+ bool isDefinedFunction(Expr func);
+
/** Is the symbol bound to a predicate? */
bool isPredicate(const std::string& name);
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e23d7c88b..b83fd42dc 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -198,12 +198,23 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
case kind::FUNCTION_TYPE:
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
- case kind::TESTER_TYPE:
- if(n.getNumChildren() > 0) {
- copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " -> "));
- out << n[n.getNumChildren() - 1];
+ if(n.getNumChildren() > 2) {
+ out << '(';
+ for(unsigned i = 0; i < n.getNumChildren() - 2; ++i) {
+ out << n[i] << ", ";
+ }
+ out << n[n.getNumChildren() - 2]
+ << ") -> " << n[n.getNumChildren() - 1];
+ } else if(n.getNumChildren() == 2) {
+ out << n[0] << " -> " << n[1];
+ } else {
+ Assert(n.getNumChildren() == 1);
+ out << n[0];
}
break;
+ case kind::TESTER_TYPE:
+ out << n[0] << " -> BOOLEAN";
+ break;
case kind::ARRAY_TYPE:
out << "ARRAY " << n[0] << " OF " << n[1];
@@ -265,6 +276,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')';
break;
+ // N-ary infix
+ case kind::BITVECTOR_CONCAT:
+ out << '(';
+ for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
+ cout << n[i] << ' ' << n.getOperator();
+ }
+ out << n[n.getNumChildren() - 1] << ')';
+
default:
if(k == kind::NOT && n[0].getKind() == kind::EQUAL) {
// collapse NOT-over-EQUAL
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index ec98e61d2..0d313594c 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -48,9 +48,15 @@ class ApplyTypeRule {
TNode::iterator argument_it = n.begin();
TNode::iterator argument_it_end = n.end();
TypeNode::iterator argument_type_it = fType.begin();
- for(; argument_it != argument_it_end; ++argument_it) {
+ for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
if((*argument_it).getType() != *argument_type_it) {
- throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+ std::stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
+ ss << "argument types do not match the function type:\n"
+ << "argument: " << *argument_it << "\n"
+ << "has type: " << (*argument_it).getType() << "\n"
+ << "not equal: " << *argument_type_it;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
} else {
@@ -75,6 +81,7 @@ class EqualityTypeRule {
if ( lhsType != rhsType ) {
std::stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
ss << "Types do not match in equation ";
ss << "[" << lhsType << "<>" << rhsType << "]";
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 748ac3f9d..7a4bf721f 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -41,9 +41,15 @@ public:
TNode::iterator argument_it = n.begin();
TNode::iterator argument_it_end = n.end();
TypeNode::iterator argument_type_it = fType.begin();
- for(; argument_it != argument_it_end; ++argument_it) {
+ for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
if((*argument_it).getType() != *argument_type_it) {
- throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+ std::stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+ << "argument types do not match the function type:\n"
+ << "argument: " << *argument_it << "\n"
+ << "has type: " << (*argument_it).getType() << "\n"
+ << "not equal: " << *argument_type_it;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
}
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index abce24751..ac864d16b 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -127,6 +127,7 @@ int runTest() {
runTestString("(= (f (f y)) x)");
runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
+ runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4);
runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
delete psr;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index f288f6b1a..632db2b91 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -200,6 +200,7 @@ public:
void testGoodCvc4Inputs() {
tryGoodInput(""); // empty string is OK
+ tryGoodInput(";"); // no command is OK
tryGoodInput("ASSERT TRUE;");
tryGoodInput("QUERY TRUE;");
tryGoodInput("CHECKSAT FALSE;");
@@ -219,7 +220,6 @@ public:
}
void testBadCvc4Inputs() {
- tryBadInput(";"); // no command
tryBadInput("ASSERT;"); // no args
tryBadInput("QUERY");
tryBadInput("CHECKSAT");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback