Merge branch 'ctnRew' into cav2019strings

12 files changed, 376 insertions, 144 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index cd34a5130..7070f6748 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -24,9 +24,8 @@ using namespace CVC4::api;
 
 int main()
 {
-
   Solver slv;
-  slv.setLogic("QF_BV"); // Set the logic
+  slv.setLogic("QF_BV");  // Set the logic
 
   // The following example has been adapted from the book A Hacker's Delight by
   // Henry S. Warren.
@@ -64,8 +63,9 @@ int main()
   slv.assertFormula(assumption);
 
   // Introduce a new variable for the new value of x after assignment.
-  Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0)
-  Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2)
+  Term new_x = slv.mkVar("new_x", bitvector32);  // x after executing code (0)
+  Term new_x_ =
+      slv.mkVar("new_x_", bitvector32);  // x after executing code (1) or (2)
 
   // Encoding code (0)
   // new_x = x == a ? b : a;
@@ -114,9 +114,9 @@ int main()
   cout << " Expect invalid. " << endl;
   cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
 
-  // Assert that a is odd 
+  // Assert that a is odd
   OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term  lsb_of_a = slv.mkTerm(extract_op, a);
+  Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a);
   cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
   Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
   cout << "Assert " << a_odd << endl;
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 48560e894..14ddcd383 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -57,18 +57,15 @@ void test(Solver& slv, Sort& consListSort)
       slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
 
   std::cout << "t2 is " << t2 << std::endl
-            << "simplify(t2) is " << slv.simplify(t2)
-            << std::endl << std::endl;
+            << "simplify(t2) is " << slv.simplify(t2) << std::endl
+            << std::endl;
 
   // You can also iterate over a Datatype to get all its constructors,
   // and over a DatatypeConstructor to get all its "args" (selectors)
-  for (Datatype::const_iterator i = consList.begin();
-       i != consList.end();
-       ++i)
+  for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i)
   {
     std::cout << "ctor: " << *i << std::endl;
-    for (DatatypeConstructor::const_iterator j = (*i).begin();
-         j != (*i).end();
+    for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end();
          ++j)
     {
       std::cout << " + arg: " << *j << std::endl;
@@ -91,7 +88,8 @@ void test(Solver& slv, Sort& consListSort)
   // This example builds a simple parameterized list of sort T, with one
   // constructor "cons".
   Sort sort = slv.mkParamSort("T");
-  DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name
+  DatatypeDecl paramConsListSpec("paramlist",
+                                 sort);  // give the datatype a name
   DatatypeConstructorDecl paramCons("cons");
   DatatypeConstructorDecl paramNil("nil");
   DatatypeSelectorDecl paramHead("head", sort);
@@ -122,7 +120,7 @@ void test(Solver& slv, Sort& consListSort)
 
   Term head_a = slv.mkTerm(
       APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
-  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() 
+  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
             << std::endl
             << "sort of cons is "
             << paramConsList.getConstructorTerm("cons").getSort() << std::endl
@@ -145,7 +143,7 @@ int main()
   // Second, it is "resolved" to an actual sort, at which point function
   // symbols are assigned to its constructors, selectors, and testers.
 
-  DatatypeDecl consListSpec("list"); // give the datatype a name
+  DatatypeDecl consListSpec("list");  // give the datatype a name
   DatatypeConstructorDecl cons("cons");
   DatatypeSelectorDecl head("head", slv.getIntegerSort());
   DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
@@ -155,8 +153,7 @@ int main()
   DatatypeConstructorDecl nil("nil");
   consListSpec.addConstructor(nil);
 
-  std::cout << "spec is:" << std::endl
-            << consListSpec << std::endl;
+  std::cout << "spec is:" << std::endl << consListSpec << std::endl;
 
   // Keep in mind that "DatatypeDecl" is the specification class for
   // datatypes---"DatatypeDecl" is not itself a CVC4 Sort.
@@ -168,13 +165,13 @@ int main()
 
   test(slv, consListSort);
 
-  std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl;
+  std::cout << std::endl
+            << ">>> Alternatively, use declareDatatype" << std::endl;
   std::cout << std::endl;
 
-  std::vector<DatatypeConstructorDecl> ctors = { cons, nil };
+  std::vector<DatatypeConstructorDecl> ctors = {cons, nil};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
   test(slv, consListSort2);
 
-
   return 0;
 }
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 8d31c1b12..96961458e 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -32,16 +32,16 @@ int main()
   Term x = slv.mkVar("a", bitvector32);
 
   OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
-  Term x_31_1 = slv.mkTerm(ext_31_1, x);
+  Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
 
   OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0);
-  Term x_30_0 = slv.mkTerm(ext_30_0, x);
+  Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x);
 
   OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31);
-  Term x_31_31 = slv.mkTerm(ext_31_31, x);
+  Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x);
 
   OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term x_0_0 = slv.mkTerm(ext_0_0, x);
+  Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x);
 
   Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
   cout << " Asserting: " << eq << endl;
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 123613797..ddb17c3a7 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1444,6 +1444,14 @@ DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
 
 DatatypeSelector::~DatatypeSelector() {}
 
+bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
+
+OpTerm DatatypeSelector::getSelectorTerm() const
+{
+  CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
+  return d_stor->getSelector();
+}
+
 std::string DatatypeSelector::toString() const
 {
   std::stringstream ss;
@@ -1478,10 +1486,10 @@ DatatypeConstructor::~DatatypeConstructor() {}
 
 bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
 
-Term DatatypeConstructor::getConstructorTerm() const
+OpTerm DatatypeConstructor::getConstructorTerm() const
 {
   CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
-  return Term(d_ctor->getConstructor());
+  return OpTerm(d_ctor->getConstructor());
 }
 
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
@@ -1498,7 +1506,7 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
   return (*d_ctor)[name];
 }
 
-Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
+OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
@@ -1627,7 +1635,7 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const
   return (*d_dtype)[name];
 }
 
-Term Datatype::getConstructorTerm(const std::string& name) const
+OpTerm Datatype::getConstructorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
@@ -2451,40 +2459,41 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       << "Only operator-style terms are created with mkTerm(), "
          "to create variables and constants see mkVar(), mkBoundVar(), "
          "and mkConst().";
-  if (nchildren)
-  {
-    const uint32_t n =
-        nchildren - (mk == CVC4::kind::metakind::PARAMETERIZED ? 1 : 0);
-    CVC4_API_KIND_CHECK_EXPECTED(n >= minArity(kind) && n <= maxArity(kind),
-                                 kind)
-        << "Terms with kind " << kindToString(kind) << " must have at least "
-        << minArity(kind) << " children and at most " << maxArity(kind)
-        << " children (the one under construction has " << n << ")";
-  }
+  CVC4_API_KIND_CHECK_EXPECTED(
+      nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
+      << "Terms with kind " << kindToString(kind) << " must have at least "
+      << minArity(kind) << " children and at most " << maxArity(kind)
+      << " children (the one under construction has " << nchildren << ")";
 }
 
-void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const
+void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
 {
-  const Kind kind = opTerm.getKind();
   Assert(isDefinedIntKind(extToIntKind(kind)));
   const CVC4::Kind int_kind = extToIntKind(kind);
-  const CVC4::Kind int_op_kind =
+  const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
+  const CVC4::Kind int_op_to_kind =
       NodeManager::operatorToKind(opTerm.d_expr->getNode());
-  CVC4_API_ARG_CHECK_EXPECTED(int_kind == kind::BUILTIN
-                                  || CVC4::kind::metaKindOf(int_op_kind)
-                                         == kind::metakind::PARAMETERIZED,
-                              opTerm)
+  CVC4_API_ARG_CHECK_EXPECTED(
+      int_kind == int_op_to_kind
+          || (kind == APPLY_CONSTRUCTOR
+              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+          || (kind == APPLY_SELECTOR
+              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+          || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
+      kind)
+      << "kind that matches kind associated with given operator term";
+  CVC4_API_ARG_CHECK_EXPECTED(
+      int_op_kind == CVC4::kind::BUILTIN
+          || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
+      opTerm)
       << "This term constructor is for parameterized kinds only";
-  if (nchildren)
-  {
-    uint32_t min_arity = ExprManager::minArity(int_op_kind);
-    uint32_t max_arity = ExprManager::maxArity(int_op_kind);
-    CVC4_API_KIND_CHECK_EXPECTED(
-        nchildren >= min_arity && nchildren <= max_arity, kind)
-        << "Terms with kind " << kindToString(kind) << " must have at least "
-        << min_arity << " children and at most " << max_arity
-        << " children (the one under construction has " << nchildren << ")";
-  }
+  uint32_t min_arity = ExprManager::minArity(int_kind);
+  uint32_t max_arity = ExprManager::maxArity(int_kind);
+  CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
+                               kind)
+      << "Terms with kind " << kindToString(kind) << " must have at least "
+      << min_arity << " children and at most " << max_arity
+      << " children (the one under construction has " << nchildren << ")";
 }
 
 Term Solver::mkTerm(Kind kind) const
@@ -2611,13 +2620,30 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
   }
 }
 
-Term Solver::mkTerm(OpTerm opTerm, Term child) const
+Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
+{
+  try
+  {
+    checkMkOpTerm(kind, opTerm, 0);
+    const CVC4::Kind int_kind = extToIntKind(kind);
+    Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (const CVC4::TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
+
+Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
 {
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
-    checkMkOpTerm(opTerm, 1);
-    Term res = d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+    checkMkOpTerm(kind, opTerm, 1);
+    const CVC4::Kind int_kind = extToIntKind(kind);
+    Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
@@ -2627,15 +2653,16 @@ Term Solver::mkTerm(OpTerm opTerm, Term child) const
   }
 }
 
-Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
+Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
 {
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
     CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-    checkMkOpTerm(opTerm, 2);
-    Term res =
-        d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+    checkMkOpTerm(kind, opTerm, 2);
+    const CVC4::Kind int_kind = extToIntKind(kind);
+    Term res = d_exprMgr->mkExpr(
+        int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
@@ -2645,16 +2672,21 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
   }
 }
 
-Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
+Term Solver::mkTerm(
+    Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const
 {
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
     CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
     CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
-    checkMkOpTerm(opTerm, 3);
-    Term res = d_exprMgr->mkExpr(
-        *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+    checkMkOpTerm(kind, opTerm, 3);
+    const CVC4::Kind int_kind = extToIntKind(kind);
+    Term res = d_exprMgr->mkExpr(int_kind,
+                                 *opTerm.d_expr,
+                                 *child1.d_expr,
+                                 *child2.d_expr,
+                                 *child3.d_expr);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
@@ -2664,7 +2696,9 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
   }
 }
 
-Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
+Term Solver::mkTerm(Kind kind,
+                    OpTerm opTerm,
+                    const std::vector<Term>& children) const
 {
   try
   {
@@ -2674,9 +2708,10 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
           !children[i].isNull(), "parameter term", children[i], i)
           << "non-null term";
     }
-    checkMkOpTerm(opTerm, children.size());
+    checkMkOpTerm(kind, opTerm, children.size());
+    const CVC4::Kind int_kind = extToIntKind(kind);
     std::vector<Expr> echildren = termVectorToExprs(children);
-    Term res = d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+    Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
@@ -2691,16 +2726,26 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
 {
   CVC4_API_CHECK(sorts.size() == terms.size())
       << "Expected the same number of sorts and elements";
-  std::vector<Term> args;
-  for (size_t i = 0, size = sorts.size(); i < size; i++)
+  try
   {
-    args.push_back(ensureTermSort(terms[i], sorts[i]));
-  }
+    std::vector<CVC4::Expr> args;
+    for (size_t i = 0, size = sorts.size(); i < size; i++)
+    {
+      args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
+    }
 
-  Sort s = mkTupleSort(sorts);
-  Datatype dt = s.getDatatype();
-  args.insert(args.begin(), dt[0].getConstructorTerm());
-  return mkTerm(APPLY_CONSTRUCTOR, args);
+    Sort s = mkTupleSort(sorts);
+    Datatype dt = s.getDatatype();
+    Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
+                                 *dt[0].getConstructorTerm().d_expr,
+                                 args);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (const CVC4::TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 std::vector<Expr> Solver::termVectorToExprs(
@@ -3458,28 +3503,32 @@ void Solver::setOption(const std::string& option,
   }
 }
 
-Term Solver::ensureTermSort(const Term& t, const Sort& s) const
+Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
 {
-  CVC4_API_CHECK(t.getSort() == s || (t.getSort().isInteger() && s.isReal()))
+  CVC4_API_CHECK(term.getSort() == sort
+                 || (term.getSort().isInteger() && sort.isReal()))
       << "Expected conversion from Int to Real";
 
-  if (t.getSort() == s)
+  Sort t = term.getSort();
+  if (term.getSort() == sort)
   {
-    return t;
+    return term;
   }
 
   // Integers are reals, too
-  Assert(t.getSort().isReal());
-  Term res = t;
-  if (t.getSort().isInteger())
+  Assert(t.isReal());
+  Term res = term;
+  if (t.isInteger())
   {
     // Must cast to Real to ensure correct type is passed to parametric type
     // constructors. We do this cast using division with 1. This has the
     // advantage wrt using TO_REAL since (constant) division is always included
     // in the theory.
-    res = mkTerm(DIVISION, *t.d_expr, mkReal(1));
+    res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
+                                 *res.d_expr,
+                                 d_exprMgr->mkConst(CVC4::Rational(1))));
   }
-  Assert(res.getSort() == s);
+  Assert(res.getSort() == sort);
   return res;
 }
 
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index a06f2e415..b8da070fc 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1100,6 +1100,17 @@ class CVC4_PUBLIC DatatypeSelector
   ~DatatypeSelector();
 
   /**
+   * @return true if this datatype selector has been resolved.
+   */
+  bool isResolved() const;
+
+  /**
+   * Get the selector operator of this datatype selector.
+   * @return the selector operator
+   */
+  OpTerm getSelectorTerm() const;
+
+  /**
    * @return a string representation of this datatype selector
    */
   std::string toString() const;
@@ -1154,7 +1165,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * Get the constructor operator of this datatype constructor.
    * @return the constructor operator
    */
-  Term getConstructorTerm() const;
+  OpTerm getConstructorTerm() const;
 
   /**
    * Get the datatype selector with the given name.
@@ -1173,7 +1184,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param name the name of the datatype selector
    * @return a term representing the datatype selector with the given name
    */
-  Term getSelectorTerm(const std::string& name) const;
+  OpTerm getSelectorTerm(const std::string& name) const;
 
   /**
    * @return a string representation of this datatype constructor
@@ -1320,7 +1331,7 @@ class CVC4_PUBLIC Datatype
    * similarly-named constructors, the
    * first is returned.
    */
-  Term getConstructorTerm(const std::string& name) const;
+  OpTerm getConstructorTerm(const std::string& name) const;
 
   /** Get the number of constructors for this Datatype. */
   size_t getNumConstructors() const;
@@ -1725,43 +1736,59 @@ class CVC4_PUBLIC Solver
   Term mkTerm(Kind kind, const std::vector<Term>& children) const;
 
   /**
-   * Create unary term from a given operator term.
+   * Create nullary term of given kind from a given operator term.
+   * Create operator terms with mkOpTerm().
+   * @param kind the kind of the term
+   * @param the operator term
+   * @return the Term
+   */
+  Term mkTerm(Kind kind, OpTerm opTerm) const;
+
+  /**
+   * Create unary term of given kind from a given operator term.
    * Create operator terms with mkOpTerm().
+   * @param kind the kind of the term
    * @param the operator term
    * @child the child of the term
    * @return the Term
    */
-  Term mkTerm(OpTerm opTerm, Term child) const;
+  Term mkTerm(Kind kind, OpTerm opTerm, Term child) const;
 
   /**
-   * Create binary term from a given operator term.
+   * Create binary term of given kind from a given operator term.
+   * @param kind the kind of the term
    * Create operator terms with mkOpTerm().
    * @param the operator term
    * @child1 the first child of the term
    * @child2 the second child of the term
    * @return the Term
    */
-  Term mkTerm(OpTerm opTerm, Term child1, Term child2) const;
+  Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const;
 
   /**
-   * Create ternary term from a given operator term.
+   * Create ternary term of given kind from a given operator term.
    * Create operator terms with mkOpTerm().
+   * @param kind the kind of the term
    * @param the operator term
    * @child1 the first child of the term
    * @child2 the second child of the term
    * @child3 the third child of the term
    * @return the Term
    */
-  Term mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const;
+  Term mkTerm(
+      Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const;
 
   /**
-   * Create n-ary term from a given operator term.
+   * Create n-ary term of given kind from a given operator term.
    * Create operator terms with mkOpTerm().
+   * @param kind the kind of the term
    * @param the operator term
    * @children the children of the term
    * @return the Term
    */
-  Term mkTerm(OpTerm opTerm, const std::vector<Term>& children) const;
+  Term mkTerm(Kind kind,
+              OpTerm opTerm,
+              const std::vector<Term>& children) const;
 
   /**
    * Create a tuple term. Terms are automatically converted if sorts are
@@ -2485,7 +2512,7 @@ class CVC4_PUBLIC Solver
   /* Helper to convert a vector of sorts to internal types. */
   std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
   /* Helper to check for API misuse in mkTerm functions. */
-  void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const;
+  void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const;
   /* Helper to check for API misuse in mkOpTerm functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index a7f6926bb..4e69ddfe1 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1649,30 +1649,32 @@ enum CVC4_PUBLIC Kind : int32_t
   /**
    * Constructor application.
    * Paramters: n > 0
-   *   -[1]: Constructor
+   *   -[1]: Constructor (operator term)
    *   -[2]..[n]: Parameters to the constructor
    * Create with:
-   *   mkTerm(Kind kind)
-   *   mkTerm(Kind kind, Term child)
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkTerm(Kind kind, OpTerm opTerm)
+   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
+   *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2)
+   *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children)
    */
-  APPLY_SELECTOR,
+  APPLY_CONSTRUCTOR,
   /**
    * Datatype selector application.
    * Parameters: 1
-   *   -[1]: Datatype term (undefined if mis-applied)
+   *   -[1]: Selector (operator term)
+   *   -[2]: Datatype term (undefined if mis-applied)
    * Create with:
-   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
    */
-  APPLY_CONSTRUCTOR,
+  APPLY_SELECTOR,
   /**
    * Datatype selector application.
    * Parameters: 1
-   *   -[1]: Datatype term (defined rigidly if mis-applied)
+   *   -[1]: Selector (operator term)
+   *   -[2]: Datatype term (defined rigidly if mis-applied)
    * Create with:
-   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
    */
   APPLY_SELECTOR_TOTAL,
   /**
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index e6b89b498..d0d36508f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -301,21 +301,30 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children)
+{
+  const size_t nchildren = children.size();
   const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
   PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
+      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
+      kind,
       "Only operator-style expressions are made with mkExpr(); "
       "to make variables and constants, see mkVar(), mkBoundVar(), "
       "and mkConst().");
   PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
+      mk != kind::metakind::PARAMETERIZED || nchildren > 0,
+      kind,
+      "Terms with kind %s must have an operator expression as first argument",
+      kind::kindToString(kind).c_str());
+  const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+  PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind),
+                      kind,
+                      "Exprs with kind %s must have at least %u children and "
+                      "at most %u children (the one under construction has %u)",
+                      kind::kindToString(kind).c_str(),
+                      minArity(kind),
+                      maxArity(kind),
+                      n);
 
   NodeManagerScope nms(d_nodeManager);
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 3ec38e306..60084d535 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2049,8 +2049,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
         if( node[0][i].isConst() ){
           CVC4::String s = node[0][i].getConst<String>();
           // if no overlap, we can split into disjunction
-          if (t.find(s) == std::string::npos && s.overlap(t) == 0
-              && t.overlap(s) == 0)
+          if (s.noOverlapWith(t))
           {
             std::vector<Node> nc0;
             getConcat(node[0], nc0);
@@ -2076,6 +2075,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   }
   else if (node[0].getKind() == kind::STRING_STRREPL)
   {
+    if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
+    {
+      String c = node[1].getConst<String>();
+      if (c.noOverlapWith(node[0][1].getConst<String>())
+          && c.noOverlapWith(node[0][2].getConst<String>()))
+      {
+        // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
+        // if there is no overlap between c1 and c3 and none between c2 and c3
+        Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
+        return returnRewrite(node, ret, "ctn-repl-cnsts-to-ctn");
+      }
+    }
+
     if (node[0][0] == node[0][2])
     {
       // (str.contains (str.replace x y x) y) ---> (str.contains x y)
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2ab6b659c..1588b5174 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -149,6 +149,22 @@ class CVC4_PUBLIC String {
 
   String prefix(std::size_t i) const { return substr(0, i); }
   String suffix(std::size_t i) const { return substr(size() - i, i); }
+
+  /**
+   * Checks if there is any overlap between this string and another string. This
+   * corresponds to checking whether one string contains the other and wether a
+   * substring of one is a prefix of the other and vice-versa.
+   *
+   * @param y The other string
+   * @return True if there is an overlap, false otherwise
+   */
+  bool noOverlapWith(const String& y) const
+  {
+    return y.find(*this) == std::string::npos
+           && this->find(y) == std::string::npos && this->overlap(y) == 0
+           && y.overlap(*this) == 0;
+  }
+
   /** string overlap
   *
   * if overlap returns m>0,
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index d2226f278..fcc68d981 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -69,6 +69,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkSepNil();
   void testMkString();
   void testMkTerm();
+  void testMkTermFromOpTerm();
   void testMkTrue();
   void testMkTuple();
   void testMkUninterpretedConst();
@@ -537,9 +538,7 @@ void SolverBlack::testMkTerm()
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
   std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
   std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
-  OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
-  OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
-  OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
+  std::vector<Term> v6 = {};
 
   // mkTerm(Kind kind) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
@@ -584,33 +583,112 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&);
+}
 
-  // mkTerm(OpTerm opTerm, Term child) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
+void SolverBlack::testMkTermFromOpTerm()
+{
+  Sort bv32 = d_solver->mkBitVectorSort(32);
+  Term a = d_solver->mkVar("a", bv32);
+  Term b = d_solver->mkVar("b", bv32);
+  std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
+  std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
+  std::vector<Term> v3 = {};
+  // simple operator terms
+  OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
+  OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
+  OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
+  // list datatype
+  Sort sort = d_solver->mkParamSort("T");
+  DatatypeDecl listDecl("paramlist", sort);
+  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl nil("nil");
+  DatatypeSelectorDecl head("head", sort);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(tail);
+  listDecl.addConstructor(cons);
+  listDecl.addConstructor(nil);
+  Sort listSort = d_solver->mkDatatypeSort(listDecl);
+  Sort intListSort =
+      listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
+  Term c = d_solver->declareFun("c", intListSort);
+  Datatype list = listSort.getDatatype();
+  // list datatype constructor and selector operator terms
+  OpTerm consTerm1 = list.getConstructorTerm("cons");
+  OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm();
+  OpTerm nilTerm1 = list.getConstructorTerm("nil");
+  OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+  OpTerm headTerm1 = list["cons"].getSelectorTerm("head");
+  OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+  OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail");
+  OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+  // mkTerm(Kind kind, OpTerm opTerm) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1),
+                   CVC4ApiException&);
 
-  // mkTerm(OpTerm opTerm, Term child1, Term child2) const
+  // mkTerm(Kind kind, OpTerm opTerm, Term child) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a));
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)),
+      d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
+  TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+      CVC4ApiException&);
 
-  // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
+  // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
-      opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
+      CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkTerm(APPLY_CONSTRUCTOR,
+                       consTerm1,
+                       d_solver->mkReal(0),
+                       d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)),
+      CVC4ApiException&);
+
+  // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+  // const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN,
+                                            opterm3,
+                                            d_solver->mkReal(1),
+                                            d_solver->mkReal(1),
+                                            d_solver->mkReal(2)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a),
+                   CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
-          opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+          CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
       CVC4ApiException&);
 
   // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v4));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v5), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1));
+  TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&);
 }
 
 void SolverBlack::testMkTrue()
diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
index 63c8839b9..946597bea 100644
--- a/test/unit/proof/drat_proof_black.h
+++ b/test/unit/proof/drat_proof_black.h
@@ -81,19 +81,19 @@ void DratProofBlack::testParseLiteralIsTooBig()
 {
   std::string input("a\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f\x00",
                     14);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException);
+  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
 }
 
 void DratProofBlack::testParseLiteralOverflow()
 {
   std::string input("a\x80", 2);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException);
+  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
 }
 
 void DratProofBlack::testParseClauseOverflow()
 {
   std::string input("a\x80\x01", 3);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException);
+  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
 }
 
 void DratProofBlack::testParseTwo()
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index f98ac233b..494c886b8 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -652,6 +652,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node aac = d_nm->mkConst(::CVC4::String("AAC"));
     Node b = d_nm->mkConst(::CVC4::String("B"));
     Node c = d_nm->mkConst(::CVC4::String("C"));
+    Node abc = d_nm->mkConst(::CVC4::String("ABC"));
+    Node def = d_nm->mkConst(::CVC4::String("DEF"));
+    Node ghi = d_nm->mkConst(::CVC4::String("GHI"));
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y);
@@ -892,6 +895,45 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                               d_nm->mkNode(kind::STRING_CONCAT, b, x));
       sameNormalForm(ctn, f);
     }
+
+    {
+      // Same normal form for:
+      //
+      // (str.contains (str.replace x "ABC" "DEF") "GHI")
+      //
+      // (str.contains x "GHI")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, abc, def),
+                         ghi);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ghi);
+      sameNormalForm(lhs, rhs);
+    }
+
+    {
+      // Different normal forms for:
+      //
+      // (str.contains (str.replace x "ABC" "DEF") "B")
+      //
+      // (str.contains x "B")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, abc, def),
+                         b);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b);
+      differentNormalForms(lhs, rhs);
+    }
+
+    {
+      // Different normal forms for:
+      //
+      // (str.contains (str.replace x "B" "DEF") "ABC")
+      //
+      // (str.contains x "ABC")
+      lhs = d_nm->mkNode(kind::STRING_STRCTN,
+                         d_nm->mkNode(kind::STRING_STRREPL, x, b, def),
+                         abc);
+      rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc);
+      differentNormalForms(lhs, rhs);
+    }
   }
 
   void testInferEqsFromContains()