Merge branch 'master' into overapproxMultiset

8 files changed, 226 insertions, 108 deletions

diff --git a/README b/README
deleted file mode 100644
index 0a8a37879..000000000
--- a/README
+++ /dev/null
@@ -1,102 +0,0 @@
-This is CVC4 release version 1.6.  For build and installation notes,
-please see the INSTALL file included with this distribution.
-
-The project leaders are Clark Barrett (Stanford University) and Cesare
-Tinelli (The University of Iowa).  For a full list of authors, please
-refer to the AUTHORS file in the source distribution.
-
-CVC4 is a tool for determining the satisfiability of a first order
-formula modulo a first order theory (or a combination of such
-theories).  It is the fourth in the Cooperating Validity Checker
-family of tools (CVC, CVC Lite, CVC3) but does not directly
-incorporate code from any previous version.
-
-CVC4 is intended to be an open and extensible SMT engine.  It can be
-used as a stand-alone tool or as a library.  It has been designed to
-increase the performance and reduce the memory overhead of its
-predecessors.  It is written entirely in C++ and is released under an
-open-source software license (see the file COPYING in the source
-distribution).
-
-*** Getting started with CVC4
-
-For help installing CVC4, see the INSTALL file that comes with this
-distribution.
-
-We recommend that you visit our CVC4 tutorials online at:
-
-  http://cvc4.cs.stanford.edu/wiki/Tutorials
-
-for help getting started using CVC4.
-
-*** Contributing to the CVC4 project
-
-We are always happy to hear feedback from our users:
-
-* if you need help with using CVC4, please refer to
-  http://cvc4.stanford.edu/#Technical_Support.
-
-* if you need to report a bug with CVC4, or make a feature request,
-  please visit our bugtracker at https://github.com/CVC4/CVC4/issues or
-  write to the cvc-bugs@cs.stanford.edu mailing list.  We are very
-  grateful for bug reports, as they help us improve CVC4, and patches
-  are generally reviewed and accepted quickly.
-
-* if you are using CVC4 in your work, or incorporating it into
-  software of your own, we'd like to invite you to leave a description
-  and link to your project/software on our "Third Party Applications"
-  page at
-  http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications
-
-* if you are interested in contributing code (for example, a new
-  decision procedure implementation) to the CVC4 project, please
-  contact one of the project leaders.  We'd be happy to point you to
-  some internals documentation to help you out.
-
-Thank you for using CVC4!
-
-*** The History of CVC4
-
-The Cooperating Validity Checker series has a long history.  The
-Stanford Validity Checker (SVC) came first in 1996, incorporating
-theories and its own SAT solver.  Its successor, the Cooperating
-Validity Checker (CVC), had a more optimized internal design, produced
-proofs, used the Chaff SAT solver, and featured a number of usability
-enhancements.  Its name comes from the cooperative nature of decision
-procedures in Nelson-Oppen theory combination, which share amongst
-each other equalities between shared terms.  CVC Lite, first made
-available in 2003, was a rewrite of CVC that attempted to make CVC
-more flexible (hence the "lite") while extending the feature set: CVC
-Lite supported quantifiers where its predecessors did not.  CVC3 was a
-major overhaul of portions of CVC Lite: it added better decision
-procedure implementations, added support for using MiniSat in the
-core, and had generally better performance.
-
-CVC4 is the new version, the fifth generation of this validity checker
-line that is now celebrating twenty-one years of heritage.  It
-represents a complete re-evaluation of the core architecture to be
-both performant and to serve as a cutting-edge research vehicle for
-the next several years.  Rather than taking CVC3 and redesigning
-problem parts, we've taken a clean-room approach, starting from
-scratch.  Before using any designs from CVC3, we have thoroughly
-scrutinized, vetted, and updated them.  Many parts of CVC4 bear only a
-superficial resemblance, if any, to their correspondent in CVC3.
-
-However, CVC4 is fundamentally similar to CVC3 and many other modern
-SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and
-a delegation path to different decision procedure implementations,
-each in charge of solving formulas in some background theory.
-
-The re-evaluation and ground-up rewrite was necessitated, we felt, by
-the performance characteristics of CVC3.  CVC3 has many useful
-features, but some core aspects of the design led to high memory use,
-and the use of heavyweight computation (where more nimble engineering
-approaches could suffice) makes CVC3 a much slower prover than other
-tools.  As these designs are central to CVC3, a new version was
-preferable to a selective re-engineering, which would have ballooned
-in short order.
-
-*** For more information
-
-More information about CVC4 is available at:
-http://cvc4.cs.stanford.edu/
diff --git a/README.md b/README.md
new file mode 100644
index 000000000..153118c6b
--- /dev/null
+++ b/README.md
@@ -0,0 +1,138 @@
+[![License: BSD](
+    https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](
+        https://opensource.org/licenses/BSD-3-Clause)
+[![Build Status](
+    https://travis-ci.org/CVC4/CVC4.svg?branch=master)](
+        https://travis-ci.org/CVC4/CVC4)
+
+CVC4
+===============================================================================
+
+CVC4 is a tool for determining the satisfiability of a first order formula
+modulo a first order theory (or a combination of such theories).  It is the
+fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite,
+CVC3) but does not directly incorporate code from any previous version.
+
+CVC4 is intended to be an open and extensible SMT engine.  It can be used as a
+stand-alone tool or as a library.  It has been designed to increase the
+performance and reduce the memory overhead of its predecessors.  It is written
+entirely in C++ and is released under an open-source software license (see file
+[COPYING](https://github.com/CVC4/CVC4/blob/master/COPYING)).
+
+
+Website
+-------------------------------------------------------------------------------
+
+More information about CVC4 is available at:
+http://cvc4.cs.stanford.edu/
+
+Download
+-------------------------------------------------------------------------------
+
+The latest version of CVC4 is available on GitHub:
+https://github.com/CVC4/CVC4
+
+Source tar balls and binaries for releases and latest stable builds of the
+[master branch](https://github.com/CVC4/CVC4) on GitHub can be
+found [here](http://cvc4.cs.stanford.edu/downloads).
+
+
+Build and Dependencies
+-------------------------------------------------------------------------------
+
+CVC4 can be built on Linux and macOS.  For Windows, CVC4 can be cross-compiled
+using Mingw-w64.
+
+For detailed build and installation instructions on these platforms,
+see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md).
+
+
+Getting Started
+-------------------------------------------------------------------------------
+
+We recommend that you visit our CVC4 tutorials online at:
+
+  http://cvc4.cs.stanford.edu/wiki/Tutorials
+
+for help getting started using CVC4.
+
+
+Contributing
+-------------------------------------------------------------------------------
+
+We are always happy to hear feedback from our users:
+
+* if you need help with using CVC4, please refer to
+  [http://cvc4.stanford.edu/#Technical_Support](http://cvc4.stanford.edu/#Technical_Support).
+
+* if you need to report a bug with CVC4, or make a feature request, please
+  visit our bugtracker at our
+  [GitHub issues](https://github.com/CVC4/CVC4/issues) page or write to the
+  cvc-bugs@cs.stanford.edu mailing list.  We are very grateful for bug reports,
+  as they help us improve CVC4, and patches are generally reviewed and accepted
+  quickly.
+
+* if you are using CVC4 in your work, or incorporating it into software of your
+  own, we'd like to invite you to leave a description and link to your
+  project/software on our [Third Party Applications](http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications).
+
+* if you are interested in contributing code (for example, a new
+  decision procedure implementation) to the CVC4 project, please
+  contact one of the [project leaders](#project_leaders).
+  We'd be happy to point you to some internal documentation to help you out.
+
+Thank you for using CVC4!
+
+
+Project Leaders
+-------------------------------------------------------------------------------
+
+* [Clark Barrett](http://theory.stanford.edu/~barrett/) (Stanford University)
+* [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/) (The University of Iowa)
+
+
+Authors
+-------------------------------------------------------------------------------
+
+For a full list of authors, please refer to the
+[AUTHORS](https://github.com/CVC4/CVC4/blob/master/AUTHORS) file.
+
+History
+-------------------------------------------------------------------------------
+
+The Cooperating Validity Checker series has a long history.  The Stanford
+Validity Checker (SVC) came first in 1996, incorporating theories and its own
+SAT solver.  Its successor, the Cooperating Validity Checker (CVC), had a more
+optimized internal design, produced proofs, used the Chaff SAT solver, and
+featured a number of usability enhancements.  Its name comes from the
+cooperative nature of decision procedures in Nelson-Oppen theory combination,
+which share amongst each other equalities between shared terms.
+
+CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to
+make CVC more flexible (hence the "lite") while extending the feature set: CVC
+Lite supported quantifiers where its predecessors did not.
+
+CVC3 was a major overhaul of portions of CVC Lite: it added better decision
+procedure implementations, added support for using MiniSat in the core, and had
+generally better performance.
+
+CVC4 is the fifth generation of this validity checker line.  It represents a
+complete re-evaluation of the core architecture to be both performant and to
+serve as a cutting-edge research vehicle for the next several years.  Rather
+than taking CVC3 and redesigning problem parts, we've taken a clean-room
+approach, starting from scratch.  Before using any designs from CVC3, we have
+thoroughly scrutinized, vetted, and updated them.  Many parts of CVC4 bear only
+a superficial resemblance, if any, to their correspondent in CVC3.
+
+However, CVC4 is fundamentally similar to CVC3 and many other modern SMT
+solvers: it is a DPLL(T) solver, with a SAT solver at its core and a delegation
+path to different decision procedure implementations, each in charge of solving
+formulas in some background theory.
+
+The re-evaluation and ground-up rewrite was necessitated, we felt, by the
+performance characteristics of CVC3.  CVC3 has many useful features, but some
+core aspects of the design led to high memory use, and the use of heavyweight
+computation (where more nimble engineering approaches could suffice) makes CVC3
+a much slower prover than other tools.  As these designs are central to CVC3, a
+new version was preferable to a selective re-engineering, which would have
+ballooned in short order.
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 32126cf4e..9401e772c 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -203,8 +203,31 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
       if (itc != tat->d_children.end()) {
         tat = &itc->second;
       } else {
-        // no functions match
-        return d_nullExpr;
+        Trace("parser-overloading")
+            << "Could not find overloaded function " << name << std::endl;
+        // it may be a parametric datatype
+        TypeNode tna = TypeNode::fromType(argTypes[i]);
+        if (tna.isParametricDatatype())
+        {
+          Trace("parser-overloading")
+              << "Parametric overloaded datatype selector " << name << " "
+              << tna << std::endl;
+          DatatypeType tnd = static_cast<DatatypeType>(argTypes[i]);
+          const Datatype& dt = tnd.getDatatype();
+          // tng is the "generalized" version of the instantiated parametric
+          // type tna
+          Type tng = dt.getDatatypeType();
+          itc = tat->d_children.find(tng);
+          if (itc != tat->d_children.end())
+          {
+            tat = &itc->second;
+          }
+        }
+        if (tat == nullptr)
+        {
+          // no functions match
+          return d_nullExpr;
+        }
       }
     }
     // we ensure that there is *only* one active symbol at this node
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e6ff02f10..36d2ddfb7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -407,12 +407,30 @@ void CvcPrinter::toStream(
     case kind::APPLY_SELECTOR_TOTAL: {
         TypeNode t = n[0].getType();
         Node opn = n.getOperator();
-        if( t.isTuple() ){
+        if (t.isTuple() || t.isRecord())
+        {
           toStream(out, n[0], depth, types, true);
+          out << '.';
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
-          int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
-          Assert( sindex>=0 );
-          out << '.' << sindex;
+          if (t.isTuple())
+          {
+            int sindex;
+            if (n.getKind() == kind::APPLY_SELECTOR)
+            {
+              sindex = Datatype::indexOf(opn.toExpr());
+            }
+            else
+            {
+              sindex = dt[0].getSelectorIndexInternal(opn.toExpr());
+            }
+            Assert(sindex >= 0);
+            out << sindex;
+          }
+          else
+          {
+            toStream(out, opn, depth, types, false);
+          }
+          return;
         }else{
           toStream(op, opn, depth, types, false);
         }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c8b052265..6f147db3c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -371,11 +371,13 @@ set(regress_0_tests
   regress0/datatypes/rec1.cvc
   regress0/datatypes/rec2.cvc
   regress0/datatypes/rec4.cvc
+  regress0/datatypes/repeated-selectors-2769.smt2
   regress0/datatypes/rewriter.cvc
   regress0/datatypes/sc-cdt1.smt2
   regress0/datatypes/some-boolean-tests.cvc
   regress0/datatypes/stream-singleton.smt2
   regress0/datatypes/tenum-bug.smt2
+  regress0/datatypes/tree-get-value.cvc
   regress0/datatypes/tuple-model.cvc
   regress0/datatypes/tuple-no-clash.cvc
   regress0/datatypes/tuple-record-bug.cvc
@@ -572,6 +574,7 @@ set(regress_0_tests
   regress0/print_lambda.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
+  regress0/printer/tuples_and_records.cvc
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
diff --git a/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2
new file mode 100644
index 000000000..827b17e36
--- /dev/null
+++ b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1))))))
+(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1))))))
+(define-fun s1 () (t1 Int) (mkt1 3))
+(define-fun s2 () (t2 Int) (mkt2 3))
+(define-fun s3 () Int (p1 s1))
+(define-fun s4 () Int (p1 s2))
+(assert (= s3 s4))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/tree-get-value.cvc b/test/regress/regress0/datatypes/tree-get-value.cvc
new file mode 100644
index 000000000..0a7da7f69
--- /dev/null
+++ b/test/regress/regress0/datatypes/tree-get-value.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+% EXPECT: ((left(x), leaf))
+OPTION "produce-models";
+DATATYPE
+  tree = node(left : tree, right : tree) | leaf
+END;
+x : tree;
+ASSERT is_leaf(left(x));
+CHECKSAT;
+GET_VALUE left(x);
diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc
new file mode 100644
index 000000000..267a316e8
--- /dev/null
+++ b/test/regress/regress0/printer/tuples_and_records.cvc
@@ -0,0 +1,18 @@
+% EXPECT: invalid
+% EXPECT: ((r.a, "active"))
+% EXPECT: ((y.1, 9))
+OPTION "produce-models";
+
+R : TYPE = [#
+   a : STRING,
+   b : STRING
+#];
+r : R;
+
+y: [REAL, INT, REAL];
+
+ASSERT r = (# a := "active", b := "who knows?" #);
+ASSERT y = ( 4/5, 9, 11/9 );
+QUERY r.a = "what?";
+GET_VALUE r.a;
+GET_VALUE y.1;