Embed mkAssociative utilities within the API. (#3801)

Towards parser/API migration.

3 files changed, 125 insertions, 69 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 41a374283..622d48ac9 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2390,6 +2390,70 @@ Term Solver::mkTermFromKind(Kind kind) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkTermInternal(Kind kind, const std::vector<Term>& children) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  for (size_t i = 0, size = children.size(); i < size; ++i)
+  {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !children[i].isNull(), "parameter term", children[i], i)
+        << "non-null term";
+  }
+
+  std::vector<Expr> echildren = termVectorToExprs(children);
+  CVC4::Kind k = extToIntKind(kind);
+  Assert(isDefinedIntKind(k));
+
+  Term res;
+  if (echildren.size() > 2)
+  {
+    if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
+        || kind == DIVISION || kind == BITVECTOR_XNOR || kind == HO_APPLY)
+    {
+      // left-associative, but CVC4 internally only supports 2 args
+      res = d_exprMgr->mkLeftAssociative(k, echildren);
+    }
+    else if (kind == IMPLIES)
+    {
+      // right-associative, but CVC4 internally only supports 2 args
+      res = d_exprMgr->mkRightAssociative(k, echildren);
+    }
+    else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ
+             || kind == GEQ)
+    {
+      // "chainable", but CVC4 internally only supports 2 args
+      res = d_exprMgr->mkChain(k, echildren);
+    }
+    else if (kind::isAssociative(k))
+    {
+      // mkAssociative has special treatment for associative operators with lots
+      // of children
+      res = d_exprMgr->mkAssociative(k, echildren);
+    }
+    else
+    {
+      // default case, must check kind
+      checkMkTerm(kind, children.size());
+      res = d_exprMgr->mkExpr(k, echildren);
+    }
+  }
+  else if (kind::isAssociative(k))
+  {
+    // associative case, same as above
+    res = d_exprMgr->mkAssociative(k, echildren);
+  }
+  else
+  {
+    // default case, same as above
+    checkMkTerm(kind, children.size());
+    res = d_exprMgr->mkExpr(k, echildren);
+  }
+
+  (void)res.d_expr->getType(true); /* kick off type checking */
+  return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 /* Helpers for converting vectors.                                            */
 /* .......................................................................... */
 
@@ -3142,43 +3206,13 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
 {
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  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";
-  checkMkTerm(kind, 3);
-
-  std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
-  CVC4::Kind k = extToIntKind(kind);
-  Assert(isDefinedIntKind(k));
-  Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
-                                    : d_exprMgr->mkExpr(k, echildren);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  // need to use internal term call to check e.g. associative construction
+  return mkTermInternal(kind, std::vector<Term>{child1, child2, child3});
 }
 
 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 {
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  for (size_t i = 0, size = children.size(); i < size; ++i)
-  {
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !children[i].isNull(), "parameter term", children[i], i)
-        << "non-null term";
-  }
-  checkMkTerm(kind, children.size());
-
-  std::vector<Expr> echildren = termVectorToExprs(children);
-  CVC4::Kind k = extToIntKind(kind);
-  Assert(isDefinedIntKind(k));
-  Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
-                                    : d_exprMgr->mkExpr(k, echildren);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermInternal(kind, children);
 }
 
 Term Solver::mkTerm(Op op) const
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 103637a7d..3317348fe 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2862,6 +2862,16 @@ class CVC4_PUBLIC Solver
    */
   Term ensureRealSort(Term expr) const;
 
+  /**
+   * Create n-ary term of given kind. This handles the cases of left/right
+   * associative operators, chainable operators, and cases when the number of
+   * children exceeds the maximum arity for the kind.
+   * @param kind the kind of the term
+   * @param children the children of the term
+   * @return the Term
+   */
+  Term mkTermInternal(Kind kind, const std::vector<Term>& children) const;
+
   /* The expression manager of this solver. */
   std::unique_ptr<ExprManager> d_exprMgr;
   /* The SMT engine of this solver. */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 27c28cec6..591ff9b1e 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -78,18 +78,19 @@ enum CVC4_PUBLIC Kind : int32_t
   BUILTIN,
 #endif
   /**
-   * Equality.
-   * Parameters: 2
-   *   -[1]..[2]: Terms with same sort
+   * Equality, chainable.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms with same sorts
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   EQUAL,
   /**
    * Disequality.
    * Parameters: n > 1
-   *   -[1]..[n]: Terms with same sort
+   *   -[1]..[n]: Terms with same sorts
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
@@ -173,10 +174,11 @@ enum CVC4_PUBLIC Kind : int32_t
   AND,
   /**
    * Logical implication.
-   * Parameters: 2
-   *   -[1]..[2]: Boolean Terms, [1] implies [2]
+   * Parameters: n > 1
+   *   -[1]..[n]: Boolean Terms, right associative
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   IMPLIES,
@@ -189,11 +191,12 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   OR,
-  /* Logical exclusive or.
-   * Parameters: 2
-   *   -[1]..[2]: Boolean Terms, [1] xor [2]
+  /* Logical exclusive or, left associative.
+   * Parameters: n > 1
+   *   -[1]..[n]: Boolean Terms, [1] xor ... xor [n]
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   XOR,
@@ -255,12 +258,14 @@ enum CVC4_PUBLIC Kind : int32_t
   PARTIAL_APPLY_UF,
 #endif
   /**
-   * Higher-order applicative encoding of function application.
-   * Parameters: 2
+   * Higher-order applicative encoding of function application, left
+   * associative.
+   * Parameters: n > 1
    *   -[1]: Function to apply
-   *   -[2]: Argument of the function
+   *   -[2] ... [n]: Arguments of the function
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   HO_APPLY,
@@ -292,11 +297,12 @@ enum CVC4_PUBLIC Kind : int32_t
   NONLINEAR_MULT,
 #endif
   /**
-   * Arithmetic subtraction.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real (sorts must match)
+   * Arithmetic subtraction, left associative.
+   * Parameters: n
+   *   -[1]..[n]: Terms of sort Integer, Real (sorts must match)
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   MINUS,
@@ -309,20 +315,22 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   UMINUS,
   /**
-   * Real division, division by 0 undefined
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real
+   * Real division, division by 0 undefined, left associative.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   DIVISION,
   /**
-   * Integer division, division by 0 undefined.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer
+   * Integer division, division by 0 undefined, left associative.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   INTS_DIVISION,
@@ -504,38 +512,41 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   CONST_RATIONAL,
   /**
-   * Less than.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real; [1] < [2]
+   * Less than, chainable.
+   * Parameters: n
+   *   -[1]..[n]: Terms of sort Integer, Real; [1] < ... < [n]
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   LT,
   /**
-   * Less than or equal.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real; [1] <= [2]
+   * Less than or equal, chainable.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real; [1] <= ... <= [n]
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   LEQ,
   /**
-   * Greater than.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real, [1] > [2]
+   * Greater than, chainable.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real, [1] > ... > [n]
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   GT,
   /**
-   * Greater than or equal.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of sort Integer, Real; [1] >= [2]
+   * Greater than or equal, chainable.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real; [1] >= ... >= [n]
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   GEQ,
@@ -649,9 +660,9 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   BITVECTOR_NOR,
   /**
-   * Bit-wise xnor.
-   * Parameters: 2
-   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Bit-wise xnor, left associative.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
@@ -663,6 +674,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   BITVECTOR_COMP,