Embed mkAssociative utilities within the API. (#3801)

Towards parser/API migration.

9 files changed, 153 insertions, 101 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,
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 8bf8d9e54..76992e1ba 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1013,6 +1013,22 @@ Expr ExprManager::mkRightAssociative(Kind kind,
   return n.toExpr();
 }
 
+Expr ExprManager::mkChain(Kind kind, const std::vector<Expr>& children)
+{
+  if (children.size() == 2)
+  {
+    // if this is the case exactly 1 pair will be generated so the
+    // AND is not required
+    return mkExpr(kind, children[0], children[1]);
+  }
+  std::vector<Expr> cchildren;
+  for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++)
+  {
+    cchildren.push_back(mkExpr(kind, children[i], children[i + 1]));
+  }
+  return mkExpr(kind::AND, cchildren);
+}
+
 unsigned ExprManager::minArity(Kind kind) {
   return metakind::getLowerBoundForKind(kind);
 }
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index c61c7e012..0fd5bb4fa 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -306,6 +306,16 @@ private:
    */
   Expr mkRightAssociative(Kind kind, const std::vector<Expr>& children);
 
+  /** make chain
+   *
+   * Given a kind k and arguments t_1, ..., t_n, this returns the
+   * conjunction of:
+   *  (k t_1 t_2) .... (k t_{n-1} t_n)
+   * It is expected that k is a kind denoting a predicate, and args is a list
+   * of terms of size >= 2 such that the terms above are well-typed.
+   */
+  Expr mkChain(Kind kind, const std::vector<Expr>& children);
+
   /**
    * Determine whether Exprs of a particular Kind have operators.
    * @returns true if Exprs of Kind k have operators.
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 447fb5d76..663be7f1f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -515,22 +515,6 @@ Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args)
   return expr;
 }
 
-api::Term Parser::mkChain(api::Kind k, const std::vector<api::Term>& args)
-{
-  if (args.size() == 2)
-  {
-    // if this is the case exactly 1 pair will be generated so the
-    // AND is not required
-    return d_solver->mkTerm(k, args[0], args[1]);
-  }
-  std::vector<api::Term> children;
-  for (size_t i = 0, nargsmo = args.size() - 1; i < nargsmo; i++)
-  {
-    children.push_back(d_solver->mkTerm(k, args[i], args[i + 1]));
-  }
-  return d_solver->mkTerm(api::AND, children);
-}
-
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch (type) {
     case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0c1f3822b..8447eb4dc 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -678,16 +678,6 @@ public:
    */
   Expr mkHoApply(Expr expr, std::vector<Expr>& args);
 
-  /** make chain
-   *
-   * Given a kind k and argument terms t_1, ..., t_n, this returns the
-   * conjunction of:
-   *  (k t_1 t_2) .... (k t_{n-1} t_n)
-   * It is expected that k is a kind denoting a predicate, and args is a list
-   * of terms of size >= 2 such that the terms above are well-typed.
-   */
-  api::Term mkChain(api::Kind k, const std::vector<api::Term>& args);
-
   /**
    * Add an operator to the current legal set.
    *
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7b7e9dd82..88d8b527b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1897,9 +1897,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
                || kind == kind::LEQ || kind == kind::GEQ)
       {
         /* "chainable", but CVC4 internally only supports 2 args */
-        api::Term ret =
-            mkChain(intToExtKind(kind), api::exprVectorToTerms(args));
-        return ret.getExpr();
+        return em->mkChain(kind, args);
       }
     }
 
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index bf699ae3c..2b1edf15b 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -326,9 +326,7 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
           || kind == kind::LEQ || kind == kind::GEQ)
       {
         /* "chainable", but CVC4 internally only supports 2 args */
-        api::Term ret =
-            mkChain(intToExtKind(kind), api::exprVectorToTerms(args));
-        return ret.getExpr();
+        return em->mkChain(kind, args);
       }
     }