merge

41 files changed, 140 insertions, 99 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index a2885d1b6..3e7e86446 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -2,9 +2,9 @@
 /*! \file antlr_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Kshitij Bansal, Tim King
+ **   Christopher L. Conway, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 576b693e8..17e21e21f 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 91ced0f41..39b109232 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Francois Bobot, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index 356663559..052bd5f7f 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andres Noetzli, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
index c33566e22..3a1843ee5 100644
--- a/src/parser/antlr_line_buffered_input.h
+++ b/src/parser/antlr_line_buffered_input.h
@@ -2,9 +2,9 @@
 /*! \file antlr_line_buffered_input.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, Tim King
+ **   Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index 017c72fb4..77d16aedb 100644
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -2,9 +2,9 @@
 /*! \file antlr_tracing.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index fc2b0dea9..5746793e3 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index b1567f346..3258441b8 100644
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp
index 472a7125c..fb6208d0c 100644
--- a/src/parser/bounded_token_factory.cpp
+++ b/src/parser/bounded_token_factory.cpp
@@ -2,9 +2,9 @@
 /*! \file bounded_token_factory.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters
+ **   Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h
index 8371c7e17..f44218786 100644
--- a/src/parser/bounded_token_factory.h
+++ b/src/parser/bounded_token_factory.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 29bc84510..6de746ad7 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2,9 +2,9 @@
 /*! \file Cvc.g
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
+ **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -1552,9 +1552,6 @@ booleanBinop[unsigned& op]
   | OR_TOK
   | XOR_TOK
   | AND_TOK
-  | JOIN_TOK
-  | PRODUCT_TOK
-  | JOIN_IMAGE_TOK  
   ;
 
 comparison[CVC4::Expr& f]
@@ -1705,9 +1702,8 @@ uminusTerm[CVC4::Expr& f]
   unsigned minusCount = 0;
 }
     /* Unary minus */
-  : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f]
+  : (MINUS_TOK { ++minusCount; })* bvBinaryOpTerm[f]
     { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
-  | bvBinaryOpTerm[f]
   ;
 
 /** Parses bitvectors.  Starts with binary operators @, &, and |. */
@@ -1734,28 +1730,27 @@ bvNegTerm[CVC4::Expr& f]
     /* BV neg */
   : BVNEG_TOK bvNegTerm[f]
     { f = f.getType().isSet() ? MK_EXPR(CVC4::kind::COMPLEMENT, f) : MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
-  | relationTerm[f]
+  | relationBinopTerm[f]
   ;
 
-relationTerm[CVC4::Expr& f]
-    /* relation terms */
-  : TRANSPOSE_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
-  | TRANSCLOSURE_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
-  | TUPLE_TOK LPAREN relationTerm[f] RPAREN
-    { std::vector<Type> types;
-      std::vector<Expr> args;
-      args.push_back(f);
-	    types.push_back(f.getType());
-      DatatypeType t = EXPR_MANAGER->mkTupleType(types);
-      const Datatype& dt = t.getDatatype();
-      args.insert( args.begin(), dt[0].getConstructor() );
-      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
-    }
-  | IDEN_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::IDEN, f); }                 
-  | postfixTerm[f]
+relationBinop[unsigned& op]
+@init {
+  op = LT(1)->getType(LT(1));
+}
+  : JOIN_TOK
+  | PRODUCT_TOK
+  | JOIN_IMAGE_TOK
+  ;
+
+relationBinopTerm[CVC4::Expr& f]
+@init {
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+}
+  : postfixTerm[f] { expressions.push_back(f); }
+    ( relationBinop[op] postfixTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
   ;
 
 /**
@@ -1775,7 +1770,7 @@ postfixTerm[CVC4::Expr& f]
   std::string id;
   Type t;
 }
-  : ( bvTerm[f]
+  : ( relationTerm[f]
     ( /* array select / bitvector extract */
       LBRACKET
         ( formula[f2] { extract = false; }
@@ -1883,7 +1878,28 @@ postfixTerm[CVC4::Expr& f]
       }
     )?
   ;
-
+  
+relationTerm[CVC4::Expr& f]
+    /* relation terms */
+  : TRANSPOSE_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
+  | TRANSCLOSURE_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
+  | TUPLE_TOK LPAREN formula[f] RPAREN
+    { std::vector<Type> types;
+      std::vector<Expr> args;
+      args.push_back(f);
+      types.push_back(f.getType());
+      DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+      const Datatype& dt = t.getDatatype();
+      args.insert( args.begin(), dt[0].getConstructor() );
+      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
+    }
+  | IDEN_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::IDEN, f); }                 
+  | bvTerm[f]
+  ;
+  
 bvTerm[CVC4::Expr& f]
 @init {
   Expr f2;
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 17a670f40..1de624f49 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -2,9 +2,9 @@
 /*! \file cvc_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Christopher L. Conway, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index d9a065fd5..944a125c2 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index cfc4796bf..78e9b474d 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -2,9 +2,9 @@
 /*! \file input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Christopher L. Conway, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/input.h b/src/parser/input.h
index 02d92749d..c8d6bbb0e 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp
index 71b913227..35263f3ac 100644
--- a/src/parser/line_buffer.cpp
+++ b/src/parser/line_buffer.cpp
@@ -2,9 +2,9 @@
 /*! \file line_buffer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/line_buffer.h b/src/parser/line_buffer.h
index 2b447a0e9..d493ed7ae 100644
--- a/src/parser/line_buffer.h
+++ b/src/parser/line_buffer.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index b2bc04de9..2fa0bd7b9 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h
index c99329d79..efa739912 100644
--- a/src/parser/memory_mapped_input_buffer.h
+++ b/src/parser/memory_mapped_input_buffer.h
@@ -2,9 +2,9 @@
 /*! \file memory_mapped_input_buffer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters
+ **   Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 71d226c98..bc88166d3 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8c18055a7..8bdc28d15 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 95a3a7840..57b63cc0f 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 3e14d715a..3f48b0bdb 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -2,9 +2,9 @@
 /*! \file parser_builder.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Aina Niemetz
+ **   Morgan Deters, Christopher L. Conway, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 9054b88ac..5e7e2500e 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -2,9 +2,9 @@
 /*! \file parser_exception.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Christopher L. Conway
+ **   Tim King, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 455da3b42..ca67ec592 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 544c6e85c..979880f8b 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index fe177d21e..f8a018806 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Christopher L. Conway, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
index 0a8118711..b8f476687 100644
--- a/src/parser/smt1/smt1_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -2,9 +2,9 @@
 /*! \file smt1_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index 6e7a8f8c4..511ddfd53 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -2,9 +2,9 @@
 /*! \file smt1_input.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Morgan Deters, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c72a4f99b..00f2e944d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -407,6 +407,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
                                            ExprManager::VAR_FLAG_DEFINED, true);
       cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
     }
+  | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
+  | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -1211,9 +1213,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
      * --smtlib2 compliance mode. */
   : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd]
   | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
-  | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
-  | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | rewriterulesCommand[cmd]
 
@@ -1886,7 +1886,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       Kind lassocKind = CVC4::kind::UNDEFINED_KIND;
       if (args.size() >= 2)
       {
-        if (kind == CVC4::kind::INTS_DIVISION)
+        if (kind == CVC4::kind::INTS_DIVISION
+            || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6()))
         {
           // Builtin operators that are not tokenized, are left associative,
           // but not internally variadic must set this.
@@ -2306,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
-        api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type));
-        api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2));
+        api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
+        api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
       }
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d52dd948b..47da10f42 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 7a3dbb9db..7a3c3b0c3 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -319,15 +319,25 @@ private:
     // that CVC4 permits as N-ary but the standard requires is binary
     if(strictModeEnabled()) {
       switch(kind) {
-      case kind::BITVECTOR_CONCAT:
       case kind::BITVECTOR_AND:
-      case kind::BITVECTOR_OR:
-      case kind::BITVECTOR_XOR:
       case kind::BITVECTOR_MULT:
+      case kind::BITVECTOR_OR:
       case kind::BITVECTOR_PLUS:
+      case kind::BITVECTOR_XOR:
+        if (numArgs != 2 && !v2_6())
+        {
+          parseError(
+              "Operator requires exactly 2 arguments in strict SMT-LIB "
+              "compliance mode (for versions <2.6): "
+              + kindToString(kind));
+        }
+        break;
+      case kind::BITVECTOR_CONCAT:
         if(numArgs != 2) {
-          parseError("Operator requires exact 2 arguments in strict SMT-LIB "
-                     "compliance mode: " + kindToString(kind));
+          parseError(
+              "Operator requires exactly 2 arguments in strict SMT-LIB "
+              "compliance mode: "
+              + kindToString(kind));
         }
         break;
       default:
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index e8b52ee34..87739789b 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Tim King, Morgan Deters
+ **   Christopher L. Conway, Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 47b420068..a456a33f8 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -2,9 +2,9 @@
 /*! \file smt2_input.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Tim King, Andres Noetzli
+ **   Christopher L. Conway, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index 00760bffc..ff1a409ae 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index 826c81670..23227e96c 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 54e9b0b4a..758198e0d 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Francois Bobot, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -352,10 +352,24 @@ definedPred[CVC4::Expr& expr]
   | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); }
   | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); }
   | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); }
-  | '$is_rat' // all "real" are actually "rat" in CVC4
+  | '$is_rat'
+    // a real n is a rational if there exists q,r integers such that
+    //   to_real(q) = n*to_real(r),
+    // where r is non-zero.
     { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
-      n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
-      expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true)));
+      Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
+      Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q);
+      Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
+      Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r);
+      Expr body =
+          MK_EXPR(CVC4::kind::AND,
+                  MK_EXPR(CVC4::kind::NOT,
+                          MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))),
+                  MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr)));
+      Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r);
+      body = MK_EXPR(CVC4::kind::EXISTS, bvl, body);
+      Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body);
     }
   | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
   | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ee313a202..fd593c68b 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -2,9 +2,9 @@
 /*! \file tptp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Francois Bobot, Tim King, Andrew Reynolds
+ **   Francois Bobot, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index eb5532247..db08311f0 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Francois Bobot, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 126b28735..e17e6608e 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -2,9 +2,9 @@
 /*! \file tptp_input.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Francois Bobot, Tim King, Morgan Deters
+ **   Francois Bobot, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index e7c681804..dab98b91b 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Francois Bobot, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim