numerous bugfixes

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index cfcc62335f5f9bd2d8de2f831c432df5ba37a3ed..8dd329b8390fb1523c77944f1ad81c5807eb3903 100644 (file)
--- 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 6d89f5f4e6500690d355e23dfa33dba5be493ea0..699dca6fa6f4ed2f06e5f4b16716a9baf994c165 100644 (file)
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -133,6 +133,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).
    *

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 794f0a670f5038571b94dd49c43cf55060bf91d8..543538f3227b0d47d1e0699efbc5cc8bc176783b 100644 (file)
--- 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 19d1bbcb8d1b2744256534a3aafae3d8d856a41f..29ade43c1b63059a81864f6baec626f94c408671 100644 (file)
--- 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 25fb30be6dd33c36dd0074bbca3c46b6c082969a..033abb42a9e5304260258e9e0f23c3bb6c858845 100644 (file)
--- 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 e23d7c88bd0965ffc057cb250d608a5053eb771a..b83fd42dc3d61a11a5db99a2760654d43c3e4ffa 100644 (file)
--- 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 ec98e61d2a04ca3c6e0a7f47d1f48daf8db35557..0d313594c99a0930e56bfb19b2a93a10ca35500d 100644 (file)
--- 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 748ac3f9d0542bc52a280a6d97f37a793ac936e5..7a4bf721f098c92eea6fc301b0ba460a621fe836 100644 (file)
--- 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 abce24751dfe91b335fc525a020d59d5c3977e68..ac864d16b7ffb689fb51099b3d5ce8f1ef112015 100644 (file)
--- 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 f288f6b1a56ea38012c37c3517b3110e9d26f328..632db2b91a1f4504ddd70b7e1180466e862b7363 100644 (file)
--- 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");