api: Unify mkOp variants. (#8369)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp
index 999d89d7f75716380366af745fc0e631eb47c351..e6d57d896375348efc39ac04882887b01c28eb0e 100644 (file)
--- a/examples/api/cpp/bitvectors.cpp
+++ b/examples/api/cpp/bitvectors.cpp
@@ -116,7 +116,7 @@ int main()
   cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl;
 
   // Assert that a is odd
-  Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+  Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, {0, 0});
   Term lsb_of_a = slv.mkTerm(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)});

diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp
index 87e91e0b54638f75fb69f7b078cafc60d719b3cd..5d81d812284a1ae6dd9a4db6bf7101bcc05ccb64 100644 (file)
--- a/examples/api/cpp/extract.cpp
+++ b/examples/api/cpp/extract.cpp
@@ -31,16 +31,16 @@ int main()
 
   Term x = slv.mkConst(bitvector32, "a");
 
-  Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1);
+  Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, {31, 1});
   Term x_31_1 = slv.mkTerm(ext_31_1, {x});
 
-  Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0);
+  Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, {30, 0});
   Term x_30_0 = slv.mkTerm(ext_30_0, {x});
 
-  Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31);
+  Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, {31, 31});
   Term x_31_31 = slv.mkTerm(ext_31_31, {x});
 
-  Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+  Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, {0, 0});
   Term x_0_0 = slv.mkTerm(ext_0_0, {x});
 
   Term eq = slv.mkTerm(EQUAL, {x_31_1, x_30_0});

diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp
index 6233102cbf7a0aaeec69fb85905ac09a6fb4d4f4..d77cdee3f6ce8f26ba666e9232b2f64382e98a45 100644 (file)
--- a/examples/api/cpp/floating_point_arith.cpp
+++ b/examples/api/cpp/floating_point_arith.cpp
@@ -73,7 +73,7 @@ int main()
   // different rounding modes.
   Term rtp = solver.mkRoundingMode(ROUND_TOWARD_POSITIVE);
   Term rtn = solver.mkRoundingMode(ROUND_TOWARD_NEGATIVE);
-  Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, 16);  // (_ fp.to_sbv 16)
+  Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, {16});  // (_ fp.to_sbv 16)
   lhs = solver.mkTerm(op, {rtp, d});
   rhs = solver.mkTerm(op, {rtn, d});
   solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, {d}));

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index fa9afe101230cc3cc8c9a96075a79b5e77be76e0..a4dc4e427fca16c7fa5c6de926ed9973c5459622 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3101,7 +3101,7 @@ std::tuple<std::uint32_t, std::uint32_t, Term> Term::getFloatingPointValue()
   const auto& fp = d_node->getConst<FloatingPoint>();
   return std::make_tuple(fp.getSize().exponentWidth(),
                          fp.getSize().significandWidth(),
-                         d_solver->mkValHelper<BitVector>(fp.pack()));
+                         d_solver->mkValHelper(fp.pack()));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -4855,6 +4855,15 @@ void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const
 /* Split out to avoid nested API calls (problematic with API tracing).        */
 /* .......................................................................... */
 
+template <typename T>
+Op Solver::mkOpHelper(Kind kind, const T& t) const
+{
+  //////// all checks before this line
+  Node res = getNodeManager()->mkConst(t);
+  static_cast<void>(res.getType(true)); /* kick off type checking */
+  return Op(this, kind, res);
+}
+
 template <typename T>
 Term Solver::mkValHelper(const T& t) const
 {
@@ -4905,7 +4914,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
 {
   CVC5_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
   //////// all checks before this line
-  return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
+  return mkValHelper(cvc5::BitVector(size, val));
 }
 
 Term Solver::mkBVFromStrHelper(uint32_t size,
@@ -4932,7 +4941,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
   }
-  return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
+  return mkValHelper(cvc5::BitVector(size, val));
 }
 
 Term Solver::getValueHelper(const Term& term) const
@@ -5754,7 +5763,7 @@ Term Solver::mkEmptySet(const Sort& sort) const
   CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort)
       << "set sort associated with this solver object";
   //////// all checks before this line
-  return mkValHelper<cvc5::EmptySet>(cvc5::EmptySet(*sort.d_type));
+  return mkValHelper(cvc5::EmptySet(*sort.d_type));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5767,7 +5776,7 @@ Term Solver::mkEmptyBag(const Sort& sort) const
   CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort)
       << "bag sort associated with this solver object";
   //////// all checks before this line
-  return mkValHelper<cvc5::EmptyBag>(cvc5::EmptyBag(*sort.d_type));
+  return mkValHelper(cvc5::EmptyBag(*sort.d_type));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5801,7 +5810,7 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::String>(cvc5::String(s, useEscSequences));
+  return mkValHelper(cvc5::String(s, useEscSequences));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5810,7 +5819,7 @@ Term Solver::mkString(const std::wstring& s) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::String>(cvc5::String(s));
+  return mkValHelper(cvc5::String(s));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5879,8 +5888,7 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const
     // this is safe because the constant array stores its type
     n = n[0];
   }
-  Term res =
-      mkValHelper<cvc5::ArrayStoreAll>(cvc5::ArrayStoreAll(*sort.d_type, n));
+  Term res = mkValHelper(cvc5::ArrayStoreAll(*sort.d_type, n));
   return res;
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -5890,7 +5898,7 @@ Term Solver::mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
+  return mkValHelper(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -5900,8 +5908,7 @@ Term Solver::mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
-      FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
+  return mkValHelper(FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5910,8 +5917,7 @@ Term Solver::mkFloatingPointNaN(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
-      FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
+  return mkValHelper(FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5920,7 +5926,7 @@ Term Solver::mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
+  return mkValHelper(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -5930,7 +5936,7 @@ Term Solver::mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
+  return mkValHelper(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -5940,7 +5946,7 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm));
+  return mkValHelper(s_rmodes.at(rm));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -5959,7 +5965,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
       val.d_node->getType().isBitVector() && val.d_node->isConst(), val)
       << "bit-vector constant";
   //////// all checks before this line
-  return mkValHelper<cvc5::FloatingPoint>(
+  return mkValHelper(
       cvc5::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>()));
   ////////
   CVC5_API_TRY_CATCH_END;
@@ -6131,186 +6137,107 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
 /* Create operators                                                           */
 /* -------------------------------------------------------------------------- */
 
-Op Solver::mkOp(Kind kind) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_KIND_CHECK(kind);
-  CVC5_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
-      << "Expected a kind for a non-indexed operator.";
-  //////// all checks before this line
-  return Op(this, kind);
-  ////////
-  CVC5_API_TRY_CATCH_END
-}
-
-Op Solver::mkOp(Kind kind, const std::string& arg) const
+Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
-  CVC5_API_KIND_CHECK_EXPECTED((kind == DIVISIBLE), kind) << "DIVISIBLE";
   //////// all checks before this line
-  Op res;
-  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-   * throws an std::invalid_argument exception. For consistency, we treat it
-   * as invalid. */
-  CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg)
-      << "a string representing an integer, real or rational value.";
-  res = Op(this,
-           kind,
-           *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg)))
-                .d_node);
-  return res;
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
+  size_t nargs = args.size();
 
-Op Solver::mkOp(Kind kind, uint32_t arg) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_KIND_CHECK(kind);
-  //////// all checks before this line
   Op res;
   switch (kind)
   {
-    case DIVISIBLE:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::Divisible>(cvc5::Divisible(arg)).d_node);
+    case BITVECTOR_EXTRACT:
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorExtract(args[0], args[1]));
       break;
     case BITVECTOR_REPEAT:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorRepeat>(cvc5::BitVectorRepeat(arg))
-                    .d_node);
-      break;
-    case BITVECTOR_ZERO_EXTEND:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorZeroExtend>(
-                    cvc5::BitVectorZeroExtend(arg))
-                    .d_node);
-      break;
-    case BITVECTOR_SIGN_EXTEND:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorSignExtend>(
-                    cvc5::BitVectorSignExtend(arg))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorRepeat(args[0]));
       break;
     case BITVECTOR_ROTATE_LEFT:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorRotateLeft>(
-                    cvc5::BitVectorRotateLeft(arg))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorRotateLeft(args[0]));
       break;
     case BITVECTOR_ROTATE_RIGHT:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorRotateRight>(
-                    cvc5::BitVectorRotateRight(arg))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorRotateRight(args[0]));
       break;
-    case INT_TO_BITVECTOR:
-      res = Op(
-          this,
-          kind,
-          *mkValHelper<cvc5::IntToBitVector>(cvc5::IntToBitVector(arg)).d_node);
+    case BITVECTOR_SIGN_EXTEND:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorSignExtend(args[0]));
       break;
-    case IAND:
-      res =
-          Op(this, kind, *mkValHelper<cvc5::IntAnd>(cvc5::IntAnd(arg)).d_node);
+    case BITVECTOR_ZERO_EXTEND:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::BitVectorZeroExtend(args[0]));
       break;
-    case FLOATINGPOINT_TO_UBV:
-      res = Op(
-          this,
-          kind,
-          *mkValHelper<cvc5::FloatingPointToUBV>(cvc5::FloatingPointToUBV(arg))
-               .d_node);
+    case DIVISIBLE:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::Divisible(args[0]));
       break;
     case FLOATINGPOINT_TO_SBV:
-      res = Op(
-          this,
-          kind,
-          *mkValHelper<cvc5::FloatingPointToSBV>(cvc5::FloatingPointToSBV(arg))
-               .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::FloatingPointToSBV(args[0]));
       break;
-    case REGEXP_REPEAT:
-      res =
-          Op(this,
-             kind,
-             *mkValHelper<cvc5::RegExpRepeat>(cvc5::RegExpRepeat(arg)).d_node);
-      break;
-    default:
-      CVC5_API_KIND_CHECK_EXPECTED(false, kind)
-          << "operator kind with uint32_t argument";
-  }
-  Assert(!res.isNull());
-  return res;
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
-Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_KIND_CHECK(kind);
-  //////// all checks before this line
-
-  Op res;
-  switch (kind)
-  {
-    case BITVECTOR_EXTRACT:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::BitVectorExtract>(
-                    cvc5::BitVectorExtract(arg1, arg2))
-                    .d_node);
+    case FLOATINGPOINT_TO_UBV:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::FloatingPointToUBV(args[0]));
       break;
     case FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::FloatingPointToFPIEEEBitVector>(
-                    cvc5::FloatingPointToFPIEEEBitVector(arg1, arg2))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(kind,
+                       cvc5::FloatingPointToFPIEEEBitVector(args[0], args[1]));
       break;
     case FLOATINGPOINT_TO_FP_FROM_FP:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::FloatingPointToFPFloatingPoint>(
-                    cvc5::FloatingPointToFPFloatingPoint(arg1, arg2))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(kind,
+                       cvc5::FloatingPointToFPFloatingPoint(args[0], args[1]));
       break;
     case FLOATINGPOINT_TO_FP_FROM_REAL:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::FloatingPointToFPReal>(
-                    cvc5::FloatingPointToFPReal(arg1, arg2))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(kind, cvc5::FloatingPointToFPReal(args[0], args[1]));
       break;
     case FLOATINGPOINT_TO_FP_FROM_SBV:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::FloatingPointToFPSignedBitVector>(
-                    cvc5::FloatingPointToFPSignedBitVector(arg1, arg2))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(
+          kind, cvc5::FloatingPointToFPSignedBitVector(args[0], args[1]));
       break;
     case FLOATINGPOINT_TO_FP_FROM_UBV:
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::FloatingPointToFPUnsignedBitVector>(
-                    cvc5::FloatingPointToFPUnsignedBitVector(arg1, arg2))
-                    .d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(
+          kind, cvc5::FloatingPointToFPUnsignedBitVector(args[0], args[1]));
+      break;
+    case IAND:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::IntAnd(args[0]));
+      break;
+    case INT_TO_BITVECTOR:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::IntToBitVector(args[0]));
+      break;
+    case REGEXP_REPEAT:
+      CVC5_API_OP_CHECK_ARITY(nargs, 1, kind);
+      res = mkOpHelper(kind, cvc5::RegExpRepeat(args[0]));
       break;
     case REGEXP_LOOP:
-      res = Op(
-          this,
-          kind,
-          *mkValHelper<cvc5::RegExpLoop>(cvc5::RegExpLoop(arg1, arg2)).d_node);
+      CVC5_API_OP_CHECK_ARITY(nargs, 2, kind);
+      res = mkOpHelper(kind, cvc5::RegExpLoop(args[0], args[1]));
+      break;
+    case TUPLE_PROJECT:
+      res = mkOpHelper(kind, cvc5::TupleProjectOp(args));
       break;
     default:
-      CVC5_API_KIND_CHECK_EXPECTED(false, kind)
-          << "operator kind with two uint32_t arguments";
+      if (nargs == 0)
+      {
+        CVC5_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
+            << "Expected a kind for a non-indexed operator.";
+        return Op(this, kind);
+      }
+      else
+      {
+        CVC5_API_KIND_CHECK_EXPECTED(false, kind)
+            << "operator kind with " << nargs << " uint32_t arguments";
+      }
   }
   Assert(!res.isNull());
   return res;
@@ -6318,31 +6245,24 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
+Op Solver::mkOp(Kind kind, const std::initializer_list<uint32_t>& args) const
+{
+  return mkOp(kind, std::vector<uint32_t>(args));
+}
+
+Op Solver::mkOp(Kind kind, const std::string& arg) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
+  CVC5_API_KIND_CHECK_EXPECTED((kind == DIVISIBLE), kind) << "DIVISIBLE";
   //////// all checks before this line
-
   Op res;
-  switch (kind)
-  {
-    case TUPLE_PROJECT:
-    {
-      res = Op(this,
-               kind,
-               *mkValHelper<cvc5::TupleProjectOp>(cvc5::TupleProjectOp(args))
-                    .d_node);
-    }
-    break;
-    default:
-    {
-      std::string message = "operator kind with " + std::to_string(args.size())
-                            + " uint32_t arguments";
-      CVC5_API_KIND_CHECK_EXPECTED(false, kind) << message;
-    }
-  }
-  Assert(!res.isNull());
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg)
+      << "a string representing an integer, real or rational value.";
+  res = mkOpHelper(kind, cvc5::Divisible(cvc5::Integer(arg)));
   return res;
   ////////
   CVC5_API_TRY_CATCH_END;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 7a81dacb67658a178652aaf48d5cb28174516d56..a9e5de81c6ec15273930409374f730ea91fab126 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3331,70 +3331,49 @@ class CVC5_EXPORT Solver
   /* .................................................................... */
 
   /**
-   * Create an operator for a builtin Kind.
-   *
-   * The Kind may not be the Kind for an indexed operator
-   * (e.g. BITVECTOR_EXTRACT).
+   * Create operator of Kind:
+   *   - #BITVECTOR_EXTRACT
+   *   - #BITVECTOR_REPEAT
+   *   - #BITVECTOR_ROTATE_LEFT
+   *   - #BITVECTOR_ROTATE_RIGHT
+   *   - #BITVECTOR_SIGN_EXTEND
+   *   - #BITVECTOR_ZERO_EXTEND
+   *   - #DIVISIBLE
+   *   - #FLOATINGPOINT_TO_FP_FROM_FP
+   *   - #FLOATINGPOINT_TO_FP_FROM_IEEE_BV
+   *   - #FLOATINGPOINT_TO_FP_FROM_REAL
+   *   - #FLOATINGPOINT_TO_FP_FROM_SBV
+   *   - #FLOATINGPOINT_TO_FP_FROM_UBV
+   *   - #FLOATINGPOINT_TO_SBV
+   *   - #FLOATINGPOINT_TO_UBV
+   *   - #INT_TO_BITVECTOR
+   *   - #TUPLE_PROJECT
+   *
+   * See cvc5::api::Kind for a description of the parameters.
+   * @param kind the kind of the operator
+   * @param args the arguments (indices) of the operator
    *
-   * @note In this case, the ``Op`` simply wraps the ``Kind``.  The Kind can be
-   *       used in ``Solver::mkTerm`` directly without creating an ``Op`` first.
-   * @param kind the kind to wrap
+   * @note If ``args`` is empty, the Op simply wraps the cvc5::api::Kind.  The
+   * Kind can be used in Solver::mkTerm directly without creating an Op
+   * first.
    */
-  Op mkOp(Kind kind) const;
+  Op mkOp(Kind kind, const std::vector<uint32_t>& args = {}) const;
+
+#ifndef DOXYGEN_SKIP
+  // Overload is only used to disambiguate the std::vector and std::string
+  // overloads.
+  Op mkOp(Kind kind, const std::initializer_list<uint32_t>& args) const;
+#endif
 
   /**
    * Create operator of kind:
    *   - DIVISIBLE (to support arbitrary precision integers)
-   * See enum Kind for a description of the parameters.
+   * See cvc5::api::Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param arg the string argument to this operator
    */
   Op mkOp(Kind kind, const std::string& arg) const;
 
-  /**
-   * Create operator of kind:
-   *   - DIVISIBLE
-   *   - BITVECTOR_REPEAT
-   *   - BITVECTOR_ZERO_EXTEND
-   *   - BITVECTOR_SIGN_EXTEND
-   *   - BITVECTOR_ROTATE_LEFT
-   *   - BITVECTOR_ROTATE_RIGHT
-   *   - INT_TO_BITVECTOR
-   *   - FLOATINGPOINT_TO_UBV
-   *   - FLOATINGPOINT_TO_UBV_TOTAL
-   *   - FLOATINGPOINT_TO_SBV
-   *   - FLOATINGPOINT_TO_SBV_TOTAL
-   *   - TUPLE_UPDATE
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the operator
-   * @param arg the uint32_t argument to this operator
-   */
-  Op mkOp(Kind kind, uint32_t arg) const;
-
-  /**
-   * Create operator of Kind:
-   *   - BITVECTOR_EXTRACT
-   *   - FLOATINGPOINT_TO_FP_FROM_IEEE_BV
-   *   - FLOATINGPOINT_TO_FP_FROM_FP
-   *   - FLOATINGPOINT_TO_FP_FROM_REAL
-   *   - FLOATINGPOINT_TO_FP_FROM_SBV
-   *   - FLOATINGPOINT_TO_FP_FROM_UBV
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the operator
-   * @param arg1 the first uint32_t argument to this operator
-   * @param arg2 the second uint32_t argument to this operator
-   */
-  Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
-
-  /**
-   * Create operator of Kind:
-   *   - TUPLE_PROJECT
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the operator
-   * @param args the arguments (indices) of the operator
-   */
-  Op mkOp(Kind kind, const std::vector<uint32_t>& args) const;
-
   /* .................................................................... */
   /* Create Constants                                                     */
   /* .................................................................... */
@@ -4825,6 +4804,9 @@ class CVC5_EXPORT Solver
 
   /** Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
+  /** Helper for creating operators. */
+  template <typename T>
+  Op mkOpHelper(Kind kind, const T& t) const;
   /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
   template <typename T>
   Term mkValHelper(const T& t) const;

diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index ca54ef00708234831e884bbb422f8bdfd3265f3f..bbb7e287526c45121a066c771cfd054a50836754 100644 (file)
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -666,6 +666,15 @@ namespace api {
       i += 1;                                                                  \
     }                                                                          \
   } while (0)
+
+/**
+ * Argument number checks for mkOp.
+ */
+#define CVC5_API_OP_CHECK_ARITY(nargs, expected, kind)                      \
+  CVC5_API_CHECK(nargs == expected)                                         \
+      << "Invalid number of indices for operator " << kind << ". Expected " \
+      << expected << " but got " << nargs << "."
+
 }  // namespace api
 }  // namespace cvc5
 #endif

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 598b65b6cf7ea227db613a1e024fbdde9f16434c..d757406d009ab26c658d1fabe74803f8bbf53c00 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -89,7 +89,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   EQUAL,
   /**
@@ -103,7 +103,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   DISTINCT,
   /**
@@ -136,7 +136,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEXPR,
   /**
@@ -151,7 +151,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   LAMBDA,
   /**
@@ -210,7 +210,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   WITNESS,
 
@@ -220,9 +220,9 @@ enum Kind : int32_t
    * Boolean constant.
    *
    * - Create Term of this Kind with:
-   *   - `Solver::mkTrue() const`
-   *   - `Solver::mkFalse() const`
-   *   - `Solver::mkBoolean(bool) const`
+   *   - Solver::mkTrue() const
+   *   - Solver::mkFalse() const
+   *   - Solver::mkBoolean(bool) const
    */
   CONST_BOOLEAN,
   /**
@@ -236,7 +236,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   NOT,
   /**
@@ -250,7 +250,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   AND,
   /**
@@ -264,7 +264,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   IMPLIES,
   /**
@@ -278,7 +278,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   OR,
   /**
@@ -292,7 +292,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   XOR,
   /**
@@ -308,7 +308,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ITE,
 
@@ -326,7 +326,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   APPLY_UF,
   /**
@@ -346,7 +346,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   CARDINALITY_CONSTRAINT,
   /**
@@ -362,7 +362,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   HO_APPLY,
 
@@ -379,7 +379,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ADD,
   /**
@@ -393,7 +393,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   MULT,
   /**
@@ -426,7 +426,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   IAND,
   /**
@@ -442,7 +442,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   POW2,
   /**
@@ -456,7 +456,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SUB,
   /**
@@ -470,7 +470,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   NEG,
   /**
@@ -484,7 +484,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   DIVISION,
   /**
@@ -498,7 +498,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INTS_DIVISION,
   /**
@@ -513,7 +513,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INTS_MODULUS,
   /**
@@ -527,7 +527,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ABS,
   /**
@@ -541,7 +541,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   POW,
   /**
@@ -555,7 +555,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   EXPONENTIAL,
   /**
@@ -569,7 +569,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SINE,
   /**
@@ -583,7 +583,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   COSINE,
   /**
@@ -597,7 +597,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   TANGENT,
   /**
@@ -611,7 +611,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   COSECANT,
   /**
@@ -625,7 +625,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SECANT,
   /**
@@ -639,7 +639,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   COTANGENT,
   /**
@@ -653,7 +653,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCSINE,
   /**
@@ -667,7 +667,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCCOSINE,
   /**
@@ -681,7 +681,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCTANGENT,
   /**
@@ -695,7 +695,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCCOSECANT,
   /**
@@ -709,7 +709,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCSECANT,
   /**
@@ -723,7 +723,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   ARCCOTANGENT,
   /**
@@ -737,7 +737,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SQRT,
   /**
@@ -753,7 +753,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   DIVISIBLE,
   /**
@@ -778,7 +778,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   LT,
   /**
@@ -792,7 +792,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   LEQ,
   /**
@@ -806,7 +806,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   GT,
   /**
@@ -820,7 +820,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   GEQ,
   /**
@@ -834,7 +834,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   IS_INTEGER,
   /**
@@ -848,7 +848,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   TO_INTEGER,
   /**
@@ -862,7 +862,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   TO_REAL,
   /**
@@ -882,8 +882,8 @@ enum Kind : int32_t
    * Fixed-size bit-vector constant.
    *
    * - Create Term of this Kind with:
-   *   - `Solver::mkBitVector(uint32_t, uint64_t) const`
-   *   - `Solver::mkBitVector(uint32_t, const std::string&, uint32_t) const`
+   *   - Solver::mkBitVector(uint32_t, uint64_t) const
+   *   - Solver::mkBitVector(uint32_t, const std::string&, uint32_t) const
    */
   CONST_BITVECTOR,
   /**
@@ -897,7 +897,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_CONCAT,
   /**
@@ -911,7 +911,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_AND,
   /**
@@ -925,7 +925,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_OR,
   /**
@@ -939,7 +939,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_XOR,
   /**
@@ -953,7 +953,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_NOT,
   /**
@@ -967,7 +967,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_NAND,
   /**
@@ -981,7 +981,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_NOR,
   /**
@@ -995,7 +995,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_XNOR,
   /**
@@ -1009,7 +1009,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_COMP,
   /**
@@ -1023,7 +1023,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_MULT,
   /**
@@ -1037,7 +1037,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ADD,
   /**
@@ -1051,7 +1051,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SUB,
   /**
@@ -1065,7 +1065,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_NEG,
   /**
@@ -1081,7 +1081,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_UDIV,
   /**
@@ -1098,7 +1098,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_UREM,
   /**
@@ -1116,7 +1116,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SDIV,
   /**
@@ -1133,7 +1133,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SREM,
   /**
@@ -1150,7 +1150,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SMOD,
   /**
@@ -1164,7 +1164,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SHL,
   /**
@@ -1178,7 +1178,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_LSHR,
   /**
@@ -1192,7 +1192,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ASHR,
   /**
@@ -1206,7 +1206,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ULT,
   /**
@@ -1220,7 +1220,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ULE,
   /**
@@ -1234,7 +1234,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_UGT,
   /**
@@ -1248,7 +1248,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_UGE,
   /**
@@ -1262,7 +1262,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SLT,
   /**
@@ -1276,7 +1276,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SLE,
   /**
@@ -1290,7 +1290,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SGT,
   /**
@@ -1304,7 +1304,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SGE,
   /**
@@ -1318,7 +1318,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ULTBV,
   /**
@@ -1332,7 +1332,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SLTBV,
   /**
@@ -1349,7 +1349,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ITE,
   /**
@@ -1363,7 +1363,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_REDOR,
   /**
@@ -1377,7 +1377,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_REDAND,
   /**
@@ -1394,7 +1394,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_EXTRACT,
   /**
@@ -1410,7 +1410,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_REPEAT,
   /**
@@ -1426,7 +1426,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ZERO_EXTEND,
   /**
@@ -1443,7 +1443,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_SIGN_EXTEND,
   /**
@@ -1459,7 +1459,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ROTATE_LEFT,
   /**
@@ -1475,7 +1475,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_ROTATE_RIGHT,
   /**
@@ -1491,7 +1491,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INT_TO_BITVECTOR,
   /**
@@ -1505,7 +1505,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BITVECTOR_TO_NAT,
 
@@ -1523,7 +1523,7 @@ enum Kind : int32_t
    * RoundingMode constant.
    *
    * - Create Term of this Kind with:
-   *   - `Solver::mkRoundingMode(RoundingMode rm) const`
+   *   - Solver::mkRoundingMode(RoundingMode rm) const
    */
   CONST_ROUNDINGMODE,
   /**
@@ -1540,7 +1540,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_FP,
   /**
@@ -1554,7 +1554,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_EQ,
   /**
@@ -1568,7 +1568,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_ABS,
   /**
@@ -1582,7 +1582,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_NEG,
   /**
@@ -1597,7 +1597,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_ADD,
   /**
@@ -1612,7 +1612,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_SUB,
   /**
@@ -1627,7 +1627,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_MULT,
   /**
@@ -1642,7 +1642,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_DIV,
   /**
@@ -1657,7 +1657,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_FMA,
   /**
@@ -1672,7 +1672,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_SQRT,
   /**
@@ -1686,7 +1686,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_REM,
   /**
@@ -1700,7 +1700,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_RTI,
   /**
@@ -1714,7 +1714,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_MIN,
   /**
@@ -1728,7 +1728,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_MAX,
   /**
@@ -1742,7 +1742,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_LEQ,
   /**
@@ -1756,7 +1756,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_LT,
   /**
@@ -1770,7 +1770,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_GEQ,
   /**
@@ -1784,7 +1784,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_GT,
   /**
@@ -1798,7 +1798,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_NORMAL,
   /**
@@ -1812,7 +1812,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_SUBNORMAL,
   /**
@@ -1826,7 +1826,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_ZERO,
   /**
@@ -1840,7 +1840,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_INF,
   /**
@@ -1854,7 +1854,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_NAN,
   /**
@@ -1868,7 +1868,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_NEG,
   /**
@@ -1882,7 +1882,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_IS_POS,
   /**
@@ -1899,7 +1899,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
   /**
@@ -1917,7 +1917,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_FP_FROM_FP,
   /**
@@ -1935,7 +1935,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_FP_FROM_REAL,
   /**
@@ -1953,7 +1953,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_FP_FROM_SBV,
   /**
@@ -1971,7 +1971,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_FP_FROM_UBV,
   /**
@@ -1987,7 +1987,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_UBV,
   /**
@@ -2003,7 +2003,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_SBV,
   /**
@@ -2017,7 +2017,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FLOATINGPOINT_TO_REAL,
 
@@ -2035,7 +2035,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SELECT,
   /**
@@ -2051,7 +2051,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STORE,
   /**
@@ -2066,7 +2066,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   CONST_ARRAY,
   /**
@@ -2093,7 +2093,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    *
    */
   EQ_RANGE,
@@ -2114,7 +2114,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   APPLY_CONSTRUCTOR,
   /**
@@ -2133,7 +2133,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   APPLY_SELECTOR,
   /**
@@ -2150,7 +2150,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   APPLY_TESTER,
   /**
@@ -2171,7 +2171,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   APPLY_UPDATER,
   /**
@@ -2206,7 +2206,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   MATCH,
   /**
@@ -2223,7 +2223,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   MATCH_CASE,
   /**
@@ -2251,7 +2251,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   MATCH_BIND_CASE,
   /**
@@ -2268,7 +2268,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   DT_SIZE,
   /**
@@ -2332,7 +2332,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEP_PTO,
   /**
@@ -2347,7 +2347,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEP_STAR,
   /**
@@ -2364,7 +2364,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEP_WAND,
 
@@ -2374,7 +2374,7 @@ enum Kind : int32_t
    * Empty set.
    *
    * - Create Term of this Kind with:
-   *   - `Solver::mkEmptySet(const Sort&) const`
+   *   - Solver::mkEmptySet(const Sort&) const
    */
   SET_EMPTY,
   /**
@@ -2388,7 +2388,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_UNION,
   /**
@@ -2402,7 +2402,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_INTER,
   /**
@@ -2416,7 +2416,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_MINUS,
   /**
@@ -2432,7 +2432,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_SUBSET,
   /**
@@ -2450,7 +2450,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_MEMBER,
   /**
@@ -2467,7 +2467,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_SINGLETON,
   /**
@@ -2483,7 +2483,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_INSERT,
   /**
@@ -2497,7 +2497,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_CARD,
   /**
@@ -2511,7 +2511,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_COMPLEMENT,
   /**
@@ -2552,7 +2552,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_COMPREHENSION,
   /**
@@ -2571,7 +2571,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_CHOOSE,
   /**
@@ -2585,7 +2585,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SET_IS_SINGLETON,
   /**
@@ -2605,7 +2605,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
    SET_MAP,
 
@@ -2622,7 +2622,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_JOIN,
   /**
@@ -2636,7 +2636,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_PRODUCT,
   /**
@@ -2650,7 +2650,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_TRANSPOSE,
   /**
@@ -2664,7 +2664,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_TCLOSURE,
   /**
@@ -2678,7 +2678,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_JOIN_IMAGE,
   /**
@@ -2692,7 +2692,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   RELATION_IDEN,
 
@@ -2716,7 +2716,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_UNION_MAX,
   /**
@@ -2730,7 +2730,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_UNION_DISJOINT,
   /**
@@ -2744,7 +2744,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_INTER_MIN,
   /**
@@ -2760,7 +2760,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_DIFFERENCE_SUBTRACT,
   /**
@@ -2776,7 +2776,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_DIFFERENCE_REMOVE,
   /**
@@ -2793,7 +2793,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_SUBBAG,
   /**
@@ -2803,8 +2803,8 @@ enum Kind : int32_t
    *   - 1..2: Terms of bag sort (Bag E), [1] an element of sort E
    *
    * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+   *   - Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const
+   *   - Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
    */
   BAG_COUNT,
   /**
@@ -2820,7 +2820,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_MEMBER,
   /**
@@ -2837,7 +2837,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_DUPLICATE_REMOVAL,
   /**
@@ -2854,7 +2854,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_MAKE,
   /**
@@ -2868,7 +2868,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_CARD,
   /**
@@ -2889,7 +2889,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_CHOOSE,
   /**
@@ -2903,7 +2903,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_IS_SINGLETON,
   /**
@@ -2917,7 +2917,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_FROM_SET,
   /**
@@ -2931,7 +2931,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_TO_SET,
   /**
@@ -2951,7 +2951,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_MAP,
   /**
@@ -2973,7 +2973,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
    BAG_FILTER,
   /**
@@ -2993,7 +2993,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   BAG_FOLD,
   /**
@@ -3007,7 +3007,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   TABLE_PRODUCT,
 
@@ -3024,7 +3024,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_CONCAT,
   /**
@@ -3039,7 +3039,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_IN_REGEXP,
   /**
@@ -3053,7 +3053,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_LENGTH,
   /**
@@ -3074,7 +3074,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_SUBSTR,
   /**
@@ -3095,7 +3095,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_UPDATE,
   /**
@@ -3114,7 +3114,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_CHARAT,
   /**
@@ -3132,7 +3132,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_CONTAINS,
   /**
@@ -3153,7 +3153,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_INDEXOF,
   /**
@@ -3174,7 +3174,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_INDEXOF_RE,
   /**
@@ -3194,7 +3194,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_REPLACE,
   /**
@@ -3214,7 +3214,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_REPLACE_ALL,
   /**
@@ -3234,7 +3234,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_REPLACE_RE,
   /**
@@ -3254,7 +3254,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_REPLACE_RE_ALL,
   /**
@@ -3268,7 +3268,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_TOLOWER,
   /**
@@ -3282,7 +3282,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_TOUPPER,
   /**
@@ -3296,7 +3296,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_REV,
   /**
@@ -3313,7 +3313,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_TO_CODE,
   /**
@@ -3331,7 +3331,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_FROM_CODE,
   /**
@@ -3349,7 +3349,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_LT,
   /**
@@ -3367,7 +3367,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_LEQ,
   /**
@@ -3385,7 +3385,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_PREFIX,
   /**
@@ -3403,7 +3403,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_SUFFIX,
   /**
@@ -3419,7 +3419,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_IS_DIGIT,
   /**
@@ -3435,7 +3435,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_FROM_INT,
   /**
@@ -3452,7 +3452,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_TO_INT,
   /**
@@ -3474,7 +3474,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   STRING_TO_REGEXP,
   /**
@@ -3488,7 +3488,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_CONCAT,
   /**
@@ -3502,7 +3502,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_UNION,
   /**
@@ -3516,7 +3516,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_INTER,
   /**
@@ -3530,7 +3530,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_DIFF,
   /**
@@ -3544,7 +3544,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_STAR,
   /**
@@ -3558,7 +3558,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_PLUS,
   /**
@@ -3572,7 +3572,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_OPT,
   /**
@@ -3587,7 +3587,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_RANGE,
   /**
@@ -3603,7 +3603,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_REPEAT,
   /**
@@ -3624,7 +3624,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_LOOP,
   /**
@@ -3659,7 +3659,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   REGEXP_COMPLEMENT,
 
@@ -3674,7 +3674,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_CONCAT,
   /**
@@ -3688,7 +3688,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_LENGTH,
   /**
@@ -3709,7 +3709,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_EXTRACT,
   /**
@@ -3730,7 +3730,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_UPDATE,
   /**
@@ -3750,7 +3750,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_AT,
   /**
@@ -3768,7 +3768,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_CONTAINS,
   /**
@@ -3789,7 +3789,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_INDEXOF,
   /**
@@ -3809,7 +3809,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_REPLACE,
   /**
@@ -3829,7 +3829,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_REPLACE_ALL,
   /**
@@ -3843,7 +3843,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_REV,
   /**
@@ -3861,7 +3861,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_PREFIX,
   /**
@@ -3879,7 +3879,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_SUFFIX,
   /**
@@ -3911,7 +3911,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_UNIT,
   /**
@@ -3928,7 +3928,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SEQ_NTH,
 
@@ -3947,7 +3947,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   FORALL,
   /**
@@ -3963,7 +3963,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   EXISTS,
   /**
@@ -3979,7 +3979,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   VARIABLE_LIST,
   /**
@@ -3996,7 +3996,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_PATTERN,
   /**
@@ -4013,7 +4013,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_NO_PATTERN,
   /**
@@ -4030,7 +4030,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_POOL,
   /**
@@ -4044,7 +4044,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_ADD_TO_POOL,
   /**
@@ -4058,7 +4058,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   SKOLEM_ADD_TO_POOL,
   /**
@@ -4076,7 +4076,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_ATTRIBUTE,
   /**
@@ -4091,7 +4091,7 @@ enum Kind : int32_t
    *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
    *
    * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, uint32_t, uint32_t) const
+   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   INST_PATTERN_LIST,
 

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index b8a2e27390eedbe286558fe784bc85caf85ace31..718d63da8cccffa222a8ae47d225abae9dbb3df0 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -796,7 +796,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JII(
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Kind kind = (Kind)kindValue;
-  Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg));
+  Op* retPointer = new Op(solver->mkOp(kind, {(uint32_t)arg}));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
@@ -812,7 +812,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JIII(
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Kind kind = (Kind)kindValue;
-  Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg1, (uint32_t)arg2));
+  Op* retPointer = new Op(solver->mkOp(kind, {(uint32_t)arg1, (uint32_t)arg2}));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index f923a0263bc517303d2f54b44e93d38bc69898c6..4f482da9ed458656e91c9c0da1c7627babfa0cc7 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -241,8 +241,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except +
         Op mkOp(Kind kind) except +
         Op mkOp(Kind kind, const string& arg) except +
-        Op mkOp(Kind kind, uint32_t arg) except +
-        Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except +
         Op mkOp(Kind kind, const vector[uint32_t]& args) except +
         # Sygus related functions
         Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 963ab70b8a17da644807b2bd80f89beebe2be143..18e6a1e79d3706cc232322cf40b34647c56ecc35 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1063,40 +1063,28 @@ cdef class Solver:
         Supports the following uses:
 
         - ``Op mkOp(Kind kind)``
-        - ``Op mkOp(Kind kind, Kind k)``
         - ``Op mkOp(Kind kind, const string& arg)``
-        - ``Op mkOp(Kind kind, uint32_t arg)``
-        - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
-        - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
+        - ``Op mkOp(Kind kind, uint32_t arg0, ...)``
         """
         cdef Op op = Op(self)
         cdef vector[uint32_t] v
 
         if len(args) == 0:
             op.cop = self.csolver.mkOp(<c_Kind> k.value)
-        elif len(args) == 1:
-            if isinstance(args[0], str):
-                op.cop = self.csolver.mkOp(<c_Kind> k.value,
-                                           <const string &>
-                                           args[0].encode())
-            elif isinstance(args[0], int):
-                op.cop = self.csolver.mkOp(<c_Kind> k.value, <int?> args[0])
-            elif isinstance(args[0], list):
-                for a in args[0]:
-                    if a < 0 or a >= 2 ** 31:
-                        raise ValueError("Argument {} must fit in a uint32_t".format(a))
-
-                    v.push_back((<uint32_t?> a))
-                op.cop = self.csolver.mkOp(<c_Kind> k.value, <const vector[uint32_t]&> v)
-            else:
-                raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
-        elif len(args) == 2:
-            if isinstance(args[0], int) and isinstance(args[1], int):
-                op.cop = self.csolver.mkOp(<c_Kind> k.value, <int> args[0], <int> args[1])
-            else:
-                raise ValueError("Unsupported signature"
-                                 " mkOp: {}".format(" X ".join([k, args[0], args[1]])))
+        elif len(args) == 1 and isinstance(args[0], str):
+            op.cop = self.csolver.mkOp(<c_Kind> k.value,
+                                       <const string &>
+                                       args[0].encode())
+        else:
+            for a in args:
+                if not isinstance(a, int):
+                  raise ValueError(
+                            "Expected uint32_t for argument {}".format(a))
+                if a < 0 or a >= 2 ** 31:
+                    raise ValueError(
+                            "Argument {} must fit in a uint32_t".format(a))
+                v.push_back((<uint32_t?> a))
+            op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
         return op
 
     def mkTrue(self):

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fc9aab8ef68d6fda7bbe0c86a53cf36f0efdfdc6..e0caa77e7dde0bfe31b18c9962f50fe9184a2af7 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1597,7 +1597,7 @@ identifier[cvc5::ParseOp& p]
 @init {
   cvc5::api::Term f;
   cvc5::api::Term f2;
-  std::vector<uint64_t> numerals;
+  std::vector<uint32_t> numerals;
 }
 : functionName[p.d_name, CHECK_NONE]
 
@@ -1644,13 +1644,7 @@ identifier[cvc5::ParseOp& p]
         // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
         // i_1, ..., i_n are numerals
         p.d_kind = api::TUPLE_PROJECT;
-        std::vector<uint32_t> indices(numerals.size());
-        for(size_t i = 0; i < numerals.size(); ++i)
-        {
-          // convert uint64_t to uint32_t
-          indices[i] = numerals[i];
-        }
-        p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
+        p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, numerals);
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
@@ -1661,12 +1655,8 @@ identifier[cvc5::ParseOp& p]
           // We don't know which kind to use until we know the type of the
           // arguments
           p.d_name = opName;
+          p.d_indices = numerals;
           p.d_kind = api::UNDEFINED_KIND;
-          // convert uint64_t to uint32_t
-          for(uint32_t numeral : numerals)
-          {
-            p.d_indices.push_back(numeral);
-          }
         }
         else if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER)
         {
@@ -1683,13 +1673,9 @@ identifier[cvc5::ParseOp& p]
           p.d_kind = k;
           p.d_expr = SOLVER->mkInteger(numerals[0]);
         }
-        else if (numerals.size() == 1)
-        {
-          p.d_op = SOLVER->mkOp(k, numerals[0]);
-        }
-        else if (numerals.size() == 2)
+        else if (numerals.size() == 1 || numerals.size() == 2)
         {
-          p.d_op = SOLVER->mkOp(k, numerals[0], numerals[1]);
+          p.d_op = SOLVER->mkOp(k, numerals);
         }
         else
         {
@@ -1709,7 +1695,7 @@ termAtomic[cvc5::api::Term& atomTerm]
 @init {
   cvc5::api::Sort t;
   std::string s;
-  std::vector<uint64_t> numerals;
+  std::vector<uint32_t> numerals;
 }
     /* constants */
   : INTEGER_LITERAL
@@ -1975,7 +1961,7 @@ sortSymbol[cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check]
 @declarations {
   std::string name;
   std::vector<cvc5::api::Sort> args;
-  std::vector<uint64_t> numerals;
+  std::vector<uint32_t> numerals;
   bool indexed = false;
 }
   : sortName[name,CHECK_NONE]
@@ -2142,7 +2128,7 @@ symbol[std::string& id,
  * Matches a nonempty list of numerals.
  * @param numerals the (empty) vector to house the numerals.
  */
-nonemptyNumeralList[std::vector<uint64_t>& numerals]
+nonemptyNumeralList[std::vector<uint32_t>& numerals]
   : ( INTEGER_LITERAL
       { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); }
     )+

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 13f7b66132b0f88d6a2e16021b70abe51d6b8d0e..027d7e588ef74760c9cefe1265a42a5e56b8fcdb 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -329,7 +329,7 @@ bool Smt2::getTesterName(api::Term cons, std::string& name)
 }
 
 api::Term Smt2::mkIndexedConstant(const std::string& name,
-                                  const std::vector<uint64_t>& numerals)
+                                  const std::vector<uint32_t>& numerals)
 {
   if (d_logic.isTheoryEnabled(theory::THEORY_FP))
   {
@@ -911,7 +911,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     if (nchildren == 1)
     {
       kind = api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV;
-      op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
+      op = d_solver->mkOp(kind, p.d_indices);
     }
     else if (nchildren > 2)
     {
@@ -935,17 +935,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       if (t.isFloatingPoint())
       {
         kind = api::FLOATINGPOINT_TO_FP_FROM_FP;
-        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
+        op = d_solver->mkOp(kind, p.d_indices);
       }
       else if (t.isInteger() || t.isReal())
       {
         kind = api::FLOATINGPOINT_TO_FP_FROM_REAL;
-        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
+        op = d_solver->mkOp(kind, p.d_indices);
       }
       else
       {
         kind = api::FLOATINGPOINT_TO_FP_FROM_SBV;
-        op = d_solver->mkOp(kind, p.d_indices[0], p.d_indices[1]);
+        op = d_solver->mkOp(kind, p.d_indices);
       }
     }
   }

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index a03384aba8d06049a3d5954a4d388a01aa34e961..a945e373d5857e030c94af7fe4ac5345713b2b81 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -129,7 +129,7 @@ class Smt2 : public Parser
    *         not valid.
    */
   api::Term mkIndexedConstant(const std::string& name,
-                              const std::vector<uint64_t>& numerals);
+                              const std::vector<uint32_t>& numerals);
 
   /**
    * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".

diff --git a/test/api/cpp/issue6111.cpp b/test/api/cpp/issue6111.cpp
index 8d458ad8f8b9fee163e1dbbb43f792bd55c429c7..2780f3257b43ccc05516cb827f4a4f351e918afd 100644 (file)
--- a/test/api/cpp/issue6111.cpp
+++ b/test/api/cpp/issue6111.cpp
@@ -42,14 +42,14 @@ int main()
 
   vector<Term> args2;
   args2.push_back(concat_result_42);
-  args2.push_back(
-      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
+  args2.push_back(solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, {7, 4}),
+                                {concat_result_43}));
   solver.assertFormula(solver.mkTerm(EQUAL, {args2}));
 
   vector<Term> args3;
   args3.push_back(concat_result_42);
-  args3.push_back(
-      solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
+  args3.push_back(solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, {3, 0}),
+                                {concat_result_43}));
   solver.assertFormula(solver.mkTerm(EQUAL, {args3}));
 
   cout << solver.checkSat() << endl;

diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp
index 3d0f43777fd5b12defbcdcfdd0ec487947a4da05..6d91f72fa62471861ebfb946aba038de0cfe8456 100644 (file)
--- a/test/api/cpp/proj-issue344.cpp
+++ b/test/api/cpp/proj-issue344.cpp
@@ -26,7 +26,7 @@ int main(void)
   slv.setOption("solve-bv-as-int", "iand");
   Sort s12 = slv.getIntegerSort();
   Term t13 = slv.mkConst(s12, "_x11");
-  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, {4124876294}), {t13});
   Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25});
   Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
   Term query = slv.mkTerm(Kind::AND, {t154, t154, t154, t154});

diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp
index 95b93952e6aa27e33ef8fc3779e83951ad52889b..f5484e30646e47e128e1a21b8e66942ad3ff8771 100644 (file)
--- a/test/api/cpp/proj-issue345.cpp
+++ b/test/api/cpp/proj-issue345.cpp
@@ -26,7 +26,7 @@ int main(void)
   slv.setOption("solve-bv-as-int", "iand");
   Sort s12 = slv.getIntegerSort();
   Term t13 = slv.mkConst(s12, "_x11");
-  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, {4124876294}), {t13});
   Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25});
   Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
   Term query = slv.mkTerm(Kind::AND, {t154, t154, t154, t154});

diff --git a/test/api/cpp/proj-issue377.cpp b/test/api/cpp/proj-issue377.cpp
index c92f7b94f8ec02e276e767015df762ed146d1e94..137b12c44863fe0cc375ef1674b403d53b5c6180 100644 (file)
--- a/test/api/cpp/proj-issue377.cpp
+++ b/test/api/cpp/proj-issue377.cpp
@@ -34,7 +34,7 @@ int main(void)
   Term t37 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, {t35});
   Term t40 = slv.mkTerm(Kind::PI);
   Term t43 = slv.mkTerm(Kind::ADD, {t40, t40});
-  Term t45 = slv.mkTerm(slv.mkOp(Kind::IAND, 31), {t37, t5});
+  Term t45 = slv.mkTerm(slv.mkOp(Kind::IAND, {31}), {t37, t5});
   Term t66 = slv.mkTerm(Kind::EQUAL, {t43, t40});
   Term t101 = slv.mkTerm(Kind::LT, {t37, t45});
   slv.assertFormula({t66});

diff --git a/test/api/cpp/proj-issue484.cpp b/test/api/cpp/proj-issue484.cpp
index 10db4c8d053f87e249ec84169a31bf16d84624ea..91d551897a186fe954462b01c317a0e568376847 100644 (file)
--- a/test/api/cpp/proj-issue484.cpp
+++ b/test/api/cpp/proj-issue484.cpp
@@ -27,7 +27,7 @@ int main(void)
   Term t1 = slv.mkVar(s1, "_x0");
   Term t3 = slv.mkInteger("8072314426184292007005683562403");
   Term t7 = slv.mkTerm(Kind::ADD, {t1, t1, t1, t3});
-  Term t8 = slv.mkTerm(slv.mkOp(Kind::DIVISIBLE, 2319436191), {t7});
+  Term t8 = slv.mkTerm(slv.mkOp(Kind::DIVISIBLE, {2319436191}), {t7});
   Term vl = slv.mkTerm(Kind::VARIABLE_LIST, {t1});
   Term t10 = slv.mkTerm(Kind::FORALL, {vl, t8});
   slv.checkSatAssuming({t10});

diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp
index 60137c56fc87172d1abfc68d2ece974a697460ac..c994003a9e08d1027a36a064caf6ee2f690f0d2f 100644 (file)
--- a/test/unit/api/cpp/op_black.cpp
+++ b/test/unit/api/cpp/op_black.cpp
@@ -28,7 +28,7 @@ class TestApiBlackOp : public TestApi
 TEST_F(TestApiBlackOp, getKind)
 {
   Op x;
-  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
+  x = d_solver.mkOp(BITVECTOR_EXTRACT, {31, 1});
   ASSERT_NO_THROW(x.getKind());
 }
 
@@ -36,7 +36,7 @@ TEST_F(TestApiBlackOp, isNull)
 {
   Op x;
   ASSERT_TRUE(x.isNull());
-  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
+  x = d_solver.mkOp(BITVECTOR_EXTRACT, {31, 1});
   ASSERT_FALSE(x.isNull());
 }
 
@@ -54,16 +54,16 @@ TEST_F(TestApiBlackOp, getNumIndices)
   ASSERT_EQ(0, plus.getNumIndices());
 
   // Operators with 1 index
-  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
-  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
-  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
-  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
-  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
-  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
-  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
-  Op iand = d_solver.mkOp(IAND, 11);
-  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
-  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+  Op divisible = d_solver.mkOp(DIVISIBLE, {4});
+  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, {5});
+  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, {6});
+  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, {7});
+  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, {8});
+  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, {9});
+  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, {10});
+  Op iand = d_solver.mkOp(IAND, {11});
+  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, {12});
+  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, {13});
 
   ASSERT_EQ(1, divisible.getNumIndices());
   ASSERT_EQ(1, bvRepeat.getNumIndices());
@@ -77,13 +77,13 @@ TEST_F(TestApiBlackOp, getNumIndices)
   ASSERT_EQ(1, fpToSbv.getNumIndices());
 
   // Operators with 2 indices
-  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
-  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
-  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
-  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
-  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
-  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
-  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, {1, 0});
+  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, {3, 2});
+  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, {5, 4});
+  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, {7, 6});
+  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, {9, 8});
+  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, {11, 10});
+  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, {15, 14});
 
   ASSERT_EQ(2, bvExtract.getNumIndices());
   ASSERT_EQ(2, toFpFromIeeeBv.getNumIndices());
@@ -107,16 +107,16 @@ TEST_F(TestApiBlackOp, subscriptOperator)
   ASSERT_THROW(plus[0], CVC5ApiException);
 
   // Operators with 1 index
-  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
-  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
-  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
-  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
-  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
-  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
-  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, 10);
-  Op iand = d_solver.mkOp(IAND, 11);
-  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12);
-  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
+  Op divisible = d_solver.mkOp(DIVISIBLE, {4});
+  Op bvRepeat = d_solver.mkOp(BITVECTOR_REPEAT, {5});
+  Op bvZeroExtend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, {6});
+  Op bvSignExtend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, {7});
+  Op bvRotateLeft = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, {8});
+  Op bvRotateRight = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, {9});
+  Op intToBv = d_solver.mkOp(INT_TO_BITVECTOR, {10});
+  Op iand = d_solver.mkOp(IAND, {11});
+  Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, {12});
+  Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, {13});
 
   ASSERT_EQ(4, divisible[0].getUInt32Value());
   ASSERT_EQ(5, bvRepeat[0].getUInt32Value());
@@ -130,13 +130,13 @@ TEST_F(TestApiBlackOp, subscriptOperator)
   ASSERT_EQ(13, fpToSbv[0].getUInt32Value());
 
   // Operators with 2 indices
-  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0);
-  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 3, 2);
-  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 5, 4);
-  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
-  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
-  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
-  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
+  Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, {1, 0});
+  Op toFpFromIeeeBv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, {3, 2});
+  Op toFpFromFp = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, {5, 4});
+  Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, {7, 6});
+  Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, {9, 8});
+  Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, {11, 10});
+  Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, {15, 14});
 
   ASSERT_EQ(1, bvExtract[0].getUInt32Value());
   ASSERT_EQ(0, bvExtract[1].getUInt32Value());
@@ -164,7 +164,7 @@ TEST_F(TestApiBlackOp, subscriptOperator)
 
 TEST_F(TestApiBlackOp, opScopingToString)
 {
-  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, {5});
   std::string op_repr = bitvector_repeat_ot.toString();
   Solver solver2;
   ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr);

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index c9b47e2de62c943a5e9b27c07cc3364c09978af9..2c9b4ee48ad86a58306043e6b8ffe7e646b7939a 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -69,7 +69,7 @@ TEST_F(TestApiBlackSolver, pow2Large3)
   Sort s4 = d_solver.getIntegerSort();
   Term t203 = d_solver.mkInteger("6135470354240554220207");
   Term t262 = d_solver.mkTerm(POW2, {t203});
-  Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, 49), {t262});
+  Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, {49}), {t262});
   ASSERT_THROW(d_solver.simplify(t536), CVC5ApiException);
 }
 
@@ -545,26 +545,20 @@ TEST_F(TestApiBlackSolver, mkFloatingPointPosZero)
 
 TEST_F(TestApiBlackSolver, mkOp)
 {
-  // mkOp(Kind kind, Kind k)
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException);
-
   // mkOp(Kind kind, const std::string& arg)
   ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException);
 
-  // mkOp(Kind kind, uint32_t arg)
-  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, 1));
-  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1));
-  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC5ApiException);
+  // mkOp(Kind kind, std::vector<uint32_t> args)
+  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, {1}));
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, {1}));
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, {1}));
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, {1}), CVC5ApiException);
 
-  // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
-  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
-  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC5ApiException);
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, {1, 1}));
+  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, {1, 2}), CVC5ApiException);
 
-  // mkOp(Kind kind, std::vector<uint32_t> args)
-  std::vector<uint32_t> args = {1, 2, 2};
-  ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, args));
+  ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, {1, 2, 2}));
 }
 
 TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
@@ -828,8 +822,8 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   Solver slv;
 
   // simple operator terms
-  Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
-  Op opterm2 = d_solver.mkOp(DIVISIBLE, 1);
+  Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, {2, 1});
+  Op opterm2 = d_solver.mkOp(DIVISIBLE, {1});
 
   // list datatype
   Sort sort = d_solver.mkParamSort("T");
@@ -1479,7 +1473,7 @@ TEST_F(TestApiBlackSolver, getOp)
 {
   Sort bv32 = d_solver.mkBitVectorSort(32);
   Term a = d_solver.mkConst(bv32, "a");
-  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, {2, 1});
   Term exta = d_solver.mkTerm(ext, {a});
 
   ASSERT_FALSE(a.hasOp());
@@ -3226,7 +3220,7 @@ TEST_F(TestApiBlackSolver, proj_issue422)
   Term t60 = slv.mkTerm(Kind::SET_SINGLETON, {t1});
   Term t66 = slv.mkTerm(Kind::BITVECTOR_COMP, {t2, t11});
   Term t92 = slv.mkRegexpAll();
-  Term t96 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, 51), {t66});
+  Term t96 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {51}), {t66});
   Term t105 = slv.mkTerm(Kind::BITVECTOR_ADD, {t96, t96});
   Term t113 = slv.mkTerm(Kind::BITVECTOR_SUB, {t105, t105});
   Term t137 = slv.mkTerm(Kind::BITVECTOR_XOR, {t113, t105});
@@ -3237,7 +3231,7 @@ TEST_F(TestApiBlackSolver, proj_issue422)
   Term t259 = slv.mkTerm(Kind::STRING_REPLACE_ALL, {t234, t234, t250});
   Term t263 = slv.mkTerm(Kind::STRING_TOLOWER, {t259});
   Term t272 = slv.mkTerm(Kind::BITVECTOR_SDIV, {t211, t66});
-  Term t276 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, 71), {t272});
+  Term t276 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {71}), {t272});
   Term t288 = slv.mkTerm(Kind::EQUAL, {t263, t1});
   Term t300 = slv.mkTerm(Kind::BITVECTOR_SLT, {t276, t276});
   Term t301 = slv.mkTerm(Kind::EQUAL, {t288, t300});

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 965a935c53a15e96ce89921fd3f3f5a8d7c670e9..81dfd2e43cefa3a8139ce70051e4e13cb9a9cb50 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -155,7 +155,7 @@ TEST_F(TestApiBlackTerm, getOp)
   ASSERT_THROW(x.getOp(), CVC5ApiException);
 
   Term ab = d_solver.mkTerm(SELECT, {a, b});
-  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, {4, 0});
   Term extb = d_solver.mkTerm(ext, {b});
 
   ASSERT_TRUE(ab.hasOp());

diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp
index be8e7cf08e2bb5855670edae927e7e314d42bffd..878c872f00ed558ccb851b637eee4a020d3b326c 100644 (file)
--- a/test/unit/api/cpp/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
@@ -37,7 +37,7 @@ TEST_F(TestApiWhiteTerm, getOp)
   Term b = d_solver.mkConst(bvsort, "b");
 
   Term ab = d_solver.mkTerm(SELECT, {a, b});
-  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, {4, 0});
   Term extb = d_solver.mkTerm(ext, {b});
 
   ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));

diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py
index 2ce7126890084f286a73fc9c35149166f4e92b1f..c174886c472b67ff9090e0a619e2419af0b2e588 100644 (file)
--- a/test/unit/api/python/test_op.py
+++ b/test/unit/api/python/test_op.py
@@ -94,7 +94,7 @@ def test_get_num_indices(solver):
 
     # Operators with n indices
     indices = [0, 3, 2, 0, 1, 2]
-    tuple_project_op = solver.mkOp(Kind.TupleProject, indices)
+    tuple_project_op = solver.mkOp(Kind.TupleProject, *indices)
     assert len(indices) == tuple_project_op.getNumIndices()
 
 
@@ -154,7 +154,7 @@ def test_subscript_operator(solver):
 
     # Operators with n indices
     indices = [0, 3, 2, 0, 1, 2]
-    tuple_project_op = solver.mkOp(Kind.TupleProject, indices)
+    tuple_project_op = solver.mkOp(Kind.TupleProject, *indices)
     for i in range(len(indices)):
         assert indices[i] == tuple_project_op[i].getIntegerValue()
 

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 099b1171ba8d61ffb578f1276474f78675d8d91f..de82dd1a49526e5e2d16a8c7a714154924bf2778 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -520,7 +520,7 @@ def test_mk_op(solver):
         solver.mkOp(Kind.Divisible, 1, 2)
 
     args = [1, 2, 2]
-    solver.mkOp(Kind.TupleProject, args)
+    solver.mkOp(Kind.TupleProject, *args)
 
 
 def test_mk_pi(solver):
@@ -2548,22 +2548,22 @@ def test_tuple_project(solver):
     indices5 = [4]
     indices6 = [0, 4]
 
-    solver.mkTerm(solver.mkOp(Kind.TupleProject, indices1), tuple)
+    solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices1), tuple)
 
-    solver.mkTerm(solver.mkOp(Kind.TupleProject, indices2), tuple)
+    solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices2), tuple)
 
-    solver.mkTerm(solver.mkOp(Kind.TupleProject, indices3), tuple)
+    solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices3), tuple)
 
-    solver.mkTerm(solver.mkOp(Kind.TupleProject, indices4), tuple)
+    solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices4), tuple)
 
     with pytest.raises(RuntimeError):
-        solver.mkTerm(solver.mkOp(Kind.TupleProject, indices5), tuple)
+        solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices5), tuple)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(solver.mkOp(Kind.TupleProject, indices6), tuple)
+        solver.mkTerm(solver.mkOp(Kind.TupleProject, *indices6), tuple)
 
     indices = [0, 3, 2, 0, 1, 2]
 
-    op = solver.mkOp(Kind.TupleProject, indices)
+    op = solver.mkOp(Kind.TupleProject, *indices)
     projection = solver.mkTerm(op, tuple)
 
     datatype = tuple.getSort().getDatatype()