Merge branch 'overapproxMultiset' into cav2019strings

13 files changed, 581 insertions, 277 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/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 2a47c2315..3b44bfddf 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -564,14 +564,6 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
   return true;
 }
 
-void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp)
-{
-  THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver);
-               prop::SatVariable t = d_satSolver->trueVar();
-               prop::SatVariable f = d_satSolver->falseVar();
-               bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f));
-}
-
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0);
   d_assertedAtoms->deleteSelf();
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 9af74d8db..8dbf7807d 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -77,7 +77,6 @@ class TLazyBitblaster : public TBitblaster<Node>
    * constants to equivalence classes that don't already have them
    */
   bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog(proof::BitVectorProof* bvp);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index ae3afb65c..f6854b1b4 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -385,91 +385,77 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
   // ------- homogeneous constants
   for (unsigned i = 0; i < 2; i++)
   {
-    if (node[i].isConst())
-    {
-      bool isHomogeneous = true;
-      unsigned hchar = 0;
-      String lhss = node[i].getConst<String>();
-      std::vector<unsigned> vec = lhss.getVec();
-      if (vec.size() >= 1)
-      {
-        hchar = vec[0];
-        for (unsigned j = 1, size = vec.size(); j < size; j++)
+    Node cn = checkEntailHomogeneousString(node[i]);
+    if (!cn.isNull() && cn.getConst<String>().size() > 0)
+    {
+      Assert(cn.isConst());
+      Assert(cn.getConst<String>().size() == 1);
+      unsigned hchar = cn.getConst<String>().front();
+
+      // The operands of the concat on each side of the equality without
+      // constant strings
+      std::vector<Node> trimmed[2];
+      // Counts the number of `hchar`s on each side
+      size_t numHChars[2] = {0, 0};
+      for (size_t j = 0; j < 2; j++)
+      {
+        // Sort the operands of the concats on both sides of the equality
+        // (since both sides may only contain one char, the order does not
+        // matter)
+        std::sort(c[j].begin(), c[j].end());
+        for (const Node& cc : c[j])
         {
-          if (vec[j] != hchar)
+          if (cc.getKind() == CONST_STRING)
           {
-            isHomogeneous = false;
-            break;
-          }
-        }
-      }
-      if (isHomogeneous)
-      {
-        std::sort(c[1 - i].begin(), c[1 - i].end());
-        std::vector<Node> trimmed;
-        unsigned rmChar = 0;
-        for (unsigned j = 0, size = c[1 - i].size(); j < size; j++)
-        {
-          if (c[1 - i][j].isConst())
-          {
-            // process the constant : either we have a conflict, or we
-            // drop an equal number of constants on the LHS
-            std::vector<unsigned> vecj =
-                c[1 - i][j].getConst<String>().getVec();
-            for (unsigned k = 0, sizev = vecj.size(); k < sizev; k++)
+            // Count the number of `hchar`s in the string constant and make
+            // sure that all chars are `hchar`s
+            std::vector<unsigned> veccc = cc.getConst<String>().getVec();
+            for (size_t k = 0, size = veccc.size(); k < size; k++)
             {
-              bool conflict = false;
-              if (vec.empty())
-              {
-                // e.g. "" = x ++ "A" ---> false
-                conflict = true;
-              }
-              else if (vecj[k] != hchar)
-              {
-                // e.g. "AA" = x ++ "B" ---> false
-                conflict = true;
-              }
-              else
+              if (veccc[k] != hchar)
               {
-                rmChar++;
-                if (rmChar > lhss.size())
-                {
-                  // e.g. "AA" = x ++ "AAA" ---> false
-                  conflict = true;
-                }
-              }
-              if (conflict)
-              {
-                // The three conflict cases should mostly should be taken
-                // care of by multiset reasoning in the strings rewriter,
-                // but we recognize this conflict just in case.
+                // This conflict case should mostly should be taken care of by
+                // multiset reasoning in the strings rewriter, but we recognize
+                // this conflict just in case.
                 new_ret = nm->mkConst(false);
-                return returnRewrite(node, new_ret, "string-eq-const-conflict");
+                return returnRewrite(
+                    node, new_ret, "string-eq-const-conflict-non-homog");
               }
+              numHChars[j]++;
             }
           }
           else
           {
-            trimmed.push_back(c[1 - i][j]);
+            trimmed[j].push_back(cc);
           }
         }
-        Node lhs = node[i];
-        if (rmChar > 0)
-        {
-          Assert(lhss.size() >= rmChar);
-          // we trimmed
-          lhs = nm->mkConst(lhss.substr(0, lhss.size() - rmChar));
-        }
-        Node ss = mkConcat(STRING_CONCAT, trimmed);
-        if (lhs != node[i] || ss != node[1 - i])
+      }
+
+      // We have to remove the same number of `hchar`s from both sides, so the
+      // side with less `hchar`s determines how many we can remove
+      size_t trimmedConst = std::min(numHChars[0], numHChars[1]);
+      for (size_t j = 0; j < 2; j++)
+      {
+        size_t diff = numHChars[j] - trimmedConst;
+        if (diff != 0)
         {
-          // e.g.
-          //  "AA" = y ++ x ---> "AA" = x ++ y if x < y
-          //  "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
-          new_ret = lhs.eqNode(ss);
-          node = returnRewrite(node, new_ret, "str-eq-homog-const");
+          // Add a constant string to the side with more `hchar`s to restore
+          // the difference in number of `hchar`s
+          std::vector<unsigned> vec(diff, hchar);
+          trimmed[j].push_back(nm->mkConst(String(vec)));
         }
       }
+
+      Node lhs = mkConcat(STRING_CONCAT, trimmed[i]);
+      Node ss = mkConcat(STRING_CONCAT, trimmed[1 - i]);
+      if (lhs != node[i] || ss != node[1 - i])
+      {
+        // e.g.
+        //  "AA" = y ++ x ---> "AA" = x ++ y if x < y
+        //  "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
+        new_ret = lhs.eqNode(ss);
+        node = returnRewrite(node, new_ret, "str-eq-homog-const");
+      }
     }
   }
 
@@ -2025,84 +2011,12 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   //   For example, contains( str.++( x, "b" ), str.++( "a", x ) ) ---> false
   //   since the number of a's in the second argument is greater than the number
   //   of a's in the first argument
-  std::map<Node, unsigned> num_nconst[2];
-  std::map<Node, unsigned> num_const[2];
-  for (unsigned j = 0; j < 2; j++)
+  if (checkEntailMultisetSubset(node[0], node[1]))
   {
-    std::vector<Node>& ncj = j == 0 ? nc1 : nc2;
-    for (const Node& cc : ncj)
-    {
-      if (cc.isConst())
-      {
-        num_const[j][cc]++;
-      }
-      else
-      {
-        num_nconst[j][cc]++;
-      }
-    }
-  }
-  bool ms_success = true;
-  for (std::pair<const Node, unsigned>& nncp : num_nconst[0])
-  {
-    if (nncp.second > num_nconst[1][nncp.first])
-    {
-      ms_success = false;
-      break;
-    }
-  }
-  if (ms_success)
-  {
-    // count the number of constant characters in the first argument
-    std::map<Node, unsigned> count_const[2];
-    std::vector<Node> chars;
-    for (unsigned j = 0; j < 2; j++)
-    {
-      for (std::pair<const Node, unsigned>& ncp : num_const[j])
-      {
-        Node cn = ncp.first;
-        Assert(cn.isConst());
-        std::vector<unsigned> cc_vec;
-        const std::vector<unsigned>& cvec = cn.getConst<String>().getVec();
-        for (unsigned i = 0, size = cvec.size(); i < size; i++)
-        {
-          // make the character
-          cc_vec.clear();
-          cc_vec.insert(cc_vec.end(), cvec.begin() + i, cvec.begin() + i + 1);
-          Node ch = NodeManager::currentNM()->mkConst(String(cc_vec));
-          count_const[j][ch] += ncp.second;
-          if (std::find(chars.begin(), chars.end(), ch) == chars.end())
-          {
-            chars.push_back(ch);
-          }
-        }
-      }
-    }
-    Trace("strings-rewrite-multiset") << "For " << node << " : " << std::endl;
-    for (const Node& ch : chars)
-    {
-      Trace("strings-rewrite-multiset") << "  # occurrences of substring ";
-      Trace("strings-rewrite-multiset") << ch << " in arguments is ";
-      Trace("strings-rewrite-multiset") << count_const[0][ch] << " / "
-                                        << count_const[1][ch] << std::endl;
-      if (count_const[0][ch] < count_const[1][ch])
-      {
-        Node ret = NodeManager::currentNM()->mkConst(false);
-        return returnRewrite(node, ret, "ctn-mset-nss");
-      }
-    }
-
-    // TODO (#1180): count the number of 2,3,4,.. character substrings
-    // for example:
-    // str.contains( str.++( x, "cbabc" ), str.++( "cabbc", x ) ) ---> false
-    // since the second argument contains more occurrences of "bb".
-    // note this is orthogonal reasoning to inductive reasoning
-    // via regular membership reduction in Liang et al CAV 2015.
+    Node ret = nm->mkConst(false);
+    return returnRewrite(node, ret, "ctn-mset-nss");
   }
 
-  // TODO (#1180): abstract interpretation with multi-set domain
-  // to show first argument is a strict subset of second argument
-
   if (checkEntailArith(len_n2, len_n1, false))
   {
     // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
@@ -4497,6 +4411,162 @@ void TheoryStringsRewriter::getArithApproximations(Node a,
   Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl;
 }
 
+bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  std::vector<Node> avec;
+  getConcat(getMultisetApproximation(a), avec);
+  std::vector<Node> bvec;
+  getConcat(b, bvec);
+
+  std::map<Node, unsigned> num_nconst[2];
+  std::map<Node, unsigned> num_const[2];
+  for (unsigned j = 0; j < 2; j++)
+  {
+    std::vector<Node>& jvec = j == 0 ? avec : bvec;
+    for (const Node& cc : jvec)
+    {
+      if (cc.isConst())
+      {
+        num_const[j][cc]++;
+      }
+      else
+      {
+        num_nconst[j][cc]++;
+      }
+    }
+  }
+  bool ms_success = true;
+  for (std::pair<const Node, unsigned>& nncp : num_nconst[0])
+  {
+    if (nncp.second > num_nconst[1][nncp.first])
+    {
+      ms_success = false;
+      break;
+    }
+  }
+  if (ms_success)
+  {
+    // count the number of constant characters in the first argument
+    std::map<Node, unsigned> count_const[2];
+    std::vector<Node> chars;
+    for (unsigned j = 0; j < 2; j++)
+    {
+      for (std::pair<const Node, unsigned>& ncp : num_const[j])
+      {
+        Node cn = ncp.first;
+        Assert(cn.isConst());
+        std::vector<unsigned> cc_vec;
+        const std::vector<unsigned>& cvec = cn.getConst<String>().getVec();
+        for (unsigned i = 0, size = cvec.size(); i < size; i++)
+        {
+          // make the character
+          cc_vec.clear();
+          cc_vec.insert(cc_vec.end(), cvec.begin() + i, cvec.begin() + i + 1);
+          Node ch = nm->mkConst(String(cc_vec));
+          count_const[j][ch] += ncp.second;
+          if (std::find(chars.begin(), chars.end(), ch) == chars.end())
+          {
+            chars.push_back(ch);
+          }
+        }
+      }
+    }
+    Trace("strings-entail-ms-ss")
+        << "For " << a << " and " << b << " : " << std::endl;
+    for (const Node& ch : chars)
+    {
+      Trace("strings-entail-ms-ss") << "  # occurrences of substring ";
+      Trace("strings-entail-ms-ss") << ch << " in arguments is ";
+      Trace("strings-entail-ms-ss")
+          << count_const[0][ch] << " / " << count_const[1][ch] << std::endl;
+      if (count_const[0][ch] < count_const[1][ch])
+      {
+        return true;
+      }
+    }
+
+    // TODO (#1180): count the number of 2,3,4,.. character substrings
+    // for example:
+    // str.contains( str.++( x, "cbabc" ), str.++( "cabbc", x ) ) ---> false
+    // since the second argument contains more occurrences of "bb".
+    // note this is orthogonal reasoning to inductive reasoning
+    // via regular membership reduction in Liang et al CAV 2015.
+  }
+  return false;
+}
+
+Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  std::vector<Node> avec;
+  getConcat(getMultisetApproximation(a), avec);
+
+  bool cValid = false;
+  unsigned c = 0;
+  for (const Node& ac : avec)
+  {
+    if (ac.getKind() == CONST_STRING)
+    {
+      std::vector<unsigned> acv = ac.getConst<String>().getVec();
+      for (unsigned cc : acv)
+      {
+        if (!cValid)
+        {
+          cValid = true;
+          c = cc;
+        }
+        else if (c != cc)
+        {
+          // Found a different character
+          return Node::null();
+        }
+      }
+    }
+    else
+    {
+      // Could produce a different character
+      return Node::null();
+    }
+  }
+
+  if (!cValid)
+  {
+    return nm->mkConst(String(""));
+  }
+
+  std::vector<unsigned> cv = {c};
+  return nm->mkConst(String(cv));
+}
+
+Node TheoryStringsRewriter::getMultisetApproximation(Node a)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (a.getKind() == STRING_SUBSTR)
+  {
+    return a[0];
+  }
+  else if (a.getKind() == STRING_STRREPL)
+  {
+    return getMultisetApproximation(nm->mkNode(STRING_CONCAT, a[0], a[2]));
+  }
+  else if (a.getKind() == STRING_CONCAT)
+  {
+    NodeBuilder<> nb(STRING_CONCAT);
+    for (const Node& ac : a)
+    {
+      nb << getMultisetApproximation(ac);
+    }
+    return nb.constructNode();
+  }
+  else
+  {
+    return a;
+  }
+}
+
 bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption,
                                                              Node a,
                                                              bool strict)
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index e4b76036d..8b0072f52 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -541,6 +541,52 @@ class TheoryStringsRewriter {
                                      bool isOverApprox = false);
 
   /**
+   * Checks whether it is always true that `a` is a strict subset of `b` in the
+   * multiset domain.
+   *
+   * Examples:
+   *
+   * a = (str.++ "A" x), b = (str.++ "A" x "B") ---> true
+   * a = (str.++ "A" x), b = (str.++ "B" x "AA") ---> true
+   * a = (str.++ "A" x), b = (str.++ "B" y "AA") ---> false
+   *
+   * @param a The term for which it should be checked if it is a strict subset
+   * of `b` in the multiset domain
+   * @param b The term for which it should be checked if it is a strict
+   * superset of `a` in the multiset domain
+   * @return True if it is always the case that `a` is a strict subset of `b`,
+   * false otherwise.
+   */
+  static bool checkEntailMultisetSubset(Node a, Node b);
+
+  /**
+   * Returns a character `c` if it is always the case that str.in.re(a, c*),
+   * i.e. if all possible values of `a` only consist of `c` characters, and the
+   * null node otherwise. If `a` is the empty string, the function returns an
+   * empty string.
+   *
+   * @param a The node to check for homogeneity
+   * @return If `a` is homogeneous, the only character that it may contain, the
+   * empty string if `a` is empty, and the null node otherwise
+   */
+  static Node checkEntailHomogeneousString(Node a);
+
+  /**
+   * Simplifies a given node `a` s.t. the result is a concatenation of string
+   * terms that can be interpreted as a multiset and which contains all
+   * multisets that `a` could form.
+   *
+   * Examples:
+   *
+   * (str.substr "AA" 0 n) ---> "AA"
+   * (str.replace "AAA" x "BB") ---> (str.++ "AAA" "BB")
+   *
+   * @param a The node to simplify
+   * @return A concatenation that can be interpreted as a multiset
+   */
+  static Node getMultisetApproximation(Node a);
+
+  /**
    * Checks whether assumption |= a >= 0 (if strict is false) or
    * assumption |= a > 0 (if strict is true), where assumption is an equality
    * assumption. The assumption must be in rewritten form.
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;
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 8139f1c2e..59d36d9e8 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -866,6 +866,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                        d_nm->mkNode(kind::STRING_STRREPL, x, a, empty),
                        a);
     sameNormalForm(lhs, rhs);
+
+    {
+      // (str.contains (str.++ x "A") (str.++ "B" x)) ---> false
+      Node ctn = d_nm->mkNode(kind::STRING_STRCTN,
+                              d_nm->mkNode(kind::STRING_CONCAT, x, a),
+                              d_nm->mkNode(kind::STRING_CONCAT, b, x));
+      sameNormalForm(ctn, f);
+    }
   }
 
   void testInferEqsFromContains()
@@ -929,7 +937,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     // Same normal form for:
     //
-    // (str.prefix x (str.++ x y))
+    // (str.prefix (str.++ x y) x)
     //
     // (= y "")
     Node p_xy = d_nm->mkNode(kind::STRING_PREFIX, xy, x);
@@ -938,16 +946,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     // Same normal form for:
     //
-    // (str.suffix x (str.++ x x))
+    // (str.suffix (str.++ x x) x)
     //
     // (= x "")
     Node p_xx = d_nm->mkNode(kind::STRING_SUFFIX, xx, x);
     Node empty_x = d_nm->mkNode(kind::EQUAL, x, empty);
     sameNormalForm(p_xx, empty_x);
 
-    // (str.suffix x (str.++ x x "A")) --> false
-    //
-    // (= x "")
+    // (str.suffix x (str.++ x x "A")) ---> false
     Node p_xxa = d_nm->mkNode(kind::STRING_SUFFIX, xxa, x);
     sameNormalForm(p_xxa, f);
   }
@@ -959,6 +965,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
 
     Node empty = d_nm->mkConst(::CVC4::String(""));
     Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node aaa = d_nm->mkConst(::CVC4::String("AAA"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
@@ -1075,16 +1082,88 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node eq_x = d_nm->mkNode(kind::EQUAL, x, empty);
     sameNormalForm(eq_repl, eq_x);
 
-    // Same normal form for:
-    //
-    // (= (str.replace y "A" "B") "B")
-    //
-    // (= (str.replace y "B" "A") "A")
-    Node lhs = d_nm->mkNode(
-        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b);
-    Node rhs = d_nm->mkNode(
-        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a);
-    sameNormalForm(lhs, rhs);
+    {
+      // Same normal form for:
+      //
+      // (= (str.replace y "A" "B") "B")
+      //
+      // (= (str.replace y "B" "A") "A")
+      Node lhs = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b);
+      Node rhs = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a);
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // Same normal form for:
+      //
+      // (= (str.++ x "A" y) (str.++ "A" "A" (str.substr "AAA" 0 n)))
+      //
+      // (= (str.++ y x) (str.++ (str.substr "AAA" 0 n) "A"))
+      Node lhs = d_nm->mkNode(
+          kind::EQUAL,
+          d_nm->mkNode(kind::STRING_CONCAT, x, a, y),
+          d_nm->mkNode(kind::STRING_CONCAT,
+                       a,
+                       a,
+                       d_nm->mkNode(kind::STRING_SUBSTR, aaa, zero, n)));
+      Node rhs = d_nm->mkNode(
+          kind::EQUAL,
+          d_nm->mkNode(kind::STRING_CONCAT, x, y),
+          d_nm->mkNode(kind::STRING_CONCAT,
+                       d_nm->mkNode(kind::STRING_SUBSTR, aaa, zero, n),
+                       a));
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // Same normal form for:
+      //
+      // (= (str.++ "A" x) "A")
+      //
+      // (= x "")
+      Node lhs =
+          d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, a, x), a);
+      Node rhs = d_nm->mkNode(kind::EQUAL, x, empty);
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // (= (str.++ x "A") "") ---> false
+      Node eq = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, a), empty);
+      sameNormalForm(eq, f);
+    }
+
+    {
+      // (= (str.++ x "B") "AAA") ---> false
+      Node eq = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, b), aaa);
+      sameNormalForm(eq, f);
+    }
+
+    {
+      // (= (str.++ x "AAA") "A") ---> false
+      Node eq = d_nm->mkNode(
+          kind::EQUAL, d_nm->mkNode(kind::STRING_CONCAT, x, aaa), a);
+      sameNormalForm(eq, f);
+    }
+
+    {
+      // (= (str.++ "AAA" (str.substr "A" 0 n)) (str.++ x "B")) ---> false
+      Node eq = d_nm->mkNode(
+          kind::EQUAL,
+          d_nm->mkNode(
+              kind::STRING_CONCAT,
+              aaa,
+              d_nm->mkNode(kind::STRING_CONCAT,
+                           a,
+                           a,
+                           d_nm->mkNode(kind::STRING_SUBSTR, x, zero, n))),
+          d_nm->mkNode(kind::STRING_CONCAT, x, b));
+      sameNormalForm(eq, f);
+    }
   }
 
  private: