From cc808da53dc0644232576c5c1ba0ced03610b7fb Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 25 Mar 2022 16:57:10 -0700 Subject: [PATCH] api: Unify mkOp variants. (#8369) Co-authored-by: Gereon Kremer --- examples/api/cpp/bitvectors.cpp | 2 +- examples/api/cpp/extract.cpp | 8 +- examples/api/cpp/floating_point_arith.cpp | 2 +- src/api/cpp/cvc5.cpp | 288 +++++-------- src/api/cpp/cvc5.h | 88 ++-- src/api/cpp/cvc5_checks.h | 9 + src/api/cpp/cvc5_kind.h | 488 +++++++++++----------- src/api/java/jni/solver.cpp | 4 +- src/api/python/cvc5.pxd | 2 - src/api/python/cvc5.pxi | 42 +- src/parser/smt2/Smt2.g | 30 +- src/parser/smt2/smt2.cpp | 10 +- src/parser/smt2/smt2.h | 2 +- test/api/cpp/issue6111.cpp | 8 +- test/api/cpp/proj-issue344.cpp | 2 +- test/api/cpp/proj-issue345.cpp | 2 +- test/api/cpp/proj-issue377.cpp | 2 +- test/api/cpp/proj-issue484.cpp | 2 +- test/unit/api/cpp/op_black.cpp | 74 ++-- test/unit/api/cpp/solver_black.cpp | 34 +- test/unit/api/cpp/term_black.cpp | 2 +- test/unit/api/cpp/term_white.cpp | 2 +- test/unit/api/python/test_op.py | 4 +- test/unit/api/python/test_solver.py | 16 +- 24 files changed, 500 insertions(+), 623 deletions(-) diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 999d89d7f..e6d57d896 100644 --- 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 87e91e0b5..5d81d8122 100644 --- 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 6233102cb..d77cdee3f 100644 --- 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 fa9afe101..a4dc4e427 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3101,7 +3101,7 @@ std::tuple Term::getFloatingPointValue() const auto& fp = d_node->getConst(); return std::make_tuple(fp.getSize().exponentWidth(), fp.getSize().significandWidth(), - d_solver->mkValHelper(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 +Op Solver::mkOpHelper(Kind kind, const T& t) const +{ + //////// all checks before this line + Node res = getNodeManager()->mkConst(t); + static_cast(res.getType(true)); /* kick off type checking */ + return Op(this, kind, res); +} + template 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(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(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(*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(*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(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(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(*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( + 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( - 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( - 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( + 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( + 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(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( + return mkValHelper( cvc5::FloatingPoint(exp, sig, val.d_node->getConst())); //////// CVC5_API_TRY_CATCH_END; @@ -6131,186 +6137,107 @@ Term Solver::mkTuple(const std::vector& 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& 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::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(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(arg)) - .d_node); - break; - case BITVECTOR_ZERO_EXTEND: - res = Op(this, - kind, - *mkValHelper( - cvc5::BitVectorZeroExtend(arg)) - .d_node); - break; - case BITVECTOR_SIGN_EXTEND: - res = Op(this, - kind, - *mkValHelper( - 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(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(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(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(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(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(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(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(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(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(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(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(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(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(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& args) const +Op Solver::mkOp(Kind kind, const std::initializer_list& args) const +{ + return mkOp(kind, std::vector(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(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 7a81dacb6..a9e5de81c 100644 --- 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& 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& 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& 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 + Op mkOpHelper(Kind kind, const T& t) const; /** Helper for mk-functions that call d_nodeMgr->mkConst(). */ template Term mkValHelper(const T& t) const; diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index ca54ef007..bbb7e2875 100644 --- 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 598b65b6c..d757406d0 100644 --- 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&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ EQUAL, /** @@ -103,7 +103,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ DISTINCT, /** @@ -136,7 +136,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEXPR, /** @@ -151,7 +151,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ LAMBDA, /** @@ -210,7 +210,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) 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&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ NOT, /** @@ -250,7 +250,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ AND, /** @@ -264,7 +264,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ IMPLIES, /** @@ -278,7 +278,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ OR, /** @@ -292,7 +292,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ XOR, /** @@ -308,7 +308,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ITE, @@ -326,7 +326,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_UF, /** @@ -346,7 +346,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ CARDINALITY_CONSTRAINT, /** @@ -362,7 +362,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ HO_APPLY, @@ -379,7 +379,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ADD, /** @@ -393,7 +393,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ MULT, /** @@ -426,7 +426,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ IAND, /** @@ -442,7 +442,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ POW2, /** @@ -456,7 +456,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SUB, /** @@ -470,7 +470,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ NEG, /** @@ -484,7 +484,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ DIVISION, /** @@ -498,7 +498,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ INTS_DIVISION, /** @@ -513,7 +513,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ INTS_MODULUS, /** @@ -527,7 +527,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ABS, /** @@ -541,7 +541,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ POW, /** @@ -555,7 +555,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ EXPONENTIAL, /** @@ -569,7 +569,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SINE, /** @@ -583,7 +583,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ COSINE, /** @@ -597,7 +597,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ TANGENT, /** @@ -611,7 +611,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ COSECANT, /** @@ -625,7 +625,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SECANT, /** @@ -639,7 +639,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ COTANGENT, /** @@ -653,7 +653,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCSINE, /** @@ -667,7 +667,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOSINE, /** @@ -681,7 +681,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCTANGENT, /** @@ -695,7 +695,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOSECANT, /** @@ -709,7 +709,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCSECANT, /** @@ -723,7 +723,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ ARCCOTANGENT, /** @@ -737,7 +737,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SQRT, /** @@ -753,7 +753,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ DIVISIBLE, /** @@ -778,7 +778,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ LT, /** @@ -792,7 +792,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ LEQ, /** @@ -806,7 +806,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ GT, /** @@ -820,7 +820,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ GEQ, /** @@ -834,7 +834,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ IS_INTEGER, /** @@ -848,7 +848,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ TO_INTEGER, /** @@ -862,7 +862,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) 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&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_CONCAT, /** @@ -911,7 +911,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_AND, /** @@ -925,7 +925,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_OR, /** @@ -939,7 +939,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_XOR, /** @@ -953,7 +953,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NOT, /** @@ -967,7 +967,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NAND, /** @@ -981,7 +981,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NOR, /** @@ -995,7 +995,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_XNOR, /** @@ -1009,7 +1009,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_COMP, /** @@ -1023,7 +1023,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_MULT, /** @@ -1037,7 +1037,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ADD, /** @@ -1051,7 +1051,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SUB, /** @@ -1065,7 +1065,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_NEG, /** @@ -1081,7 +1081,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UDIV, /** @@ -1098,7 +1098,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UREM, /** @@ -1116,7 +1116,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SDIV, /** @@ -1133,7 +1133,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SREM, /** @@ -1150,7 +1150,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SMOD, /** @@ -1164,7 +1164,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SHL, /** @@ -1178,7 +1178,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_LSHR, /** @@ -1192,7 +1192,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ASHR, /** @@ -1206,7 +1206,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULT, /** @@ -1220,7 +1220,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULE, /** @@ -1234,7 +1234,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UGT, /** @@ -1248,7 +1248,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_UGE, /** @@ -1262,7 +1262,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLT, /** @@ -1276,7 +1276,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLE, /** @@ -1290,7 +1290,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SGT, /** @@ -1304,7 +1304,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SGE, /** @@ -1318,7 +1318,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ULTBV, /** @@ -1332,7 +1332,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SLTBV, /** @@ -1349,7 +1349,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ITE, /** @@ -1363,7 +1363,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REDOR, /** @@ -1377,7 +1377,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REDAND, /** @@ -1394,7 +1394,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_EXTRACT, /** @@ -1410,7 +1410,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_REPEAT, /** @@ -1426,7 +1426,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ZERO_EXTEND, /** @@ -1443,7 +1443,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_SIGN_EXTEND, /** @@ -1459,7 +1459,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ROTATE_LEFT, /** @@ -1475,7 +1475,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ BITVECTOR_ROTATE_RIGHT, /** @@ -1491,7 +1491,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INT_TO_BITVECTOR, /** @@ -1505,7 +1505,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) 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&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_FP, /** @@ -1554,7 +1554,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_EQ, /** @@ -1568,7 +1568,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_ABS, /** @@ -1582,7 +1582,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_NEG, /** @@ -1597,7 +1597,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_ADD, /** @@ -1612,7 +1612,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_SUB, /** @@ -1627,7 +1627,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MULT, /** @@ -1642,7 +1642,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_DIV, /** @@ -1657,7 +1657,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_FMA, /** @@ -1672,7 +1672,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_SQRT, /** @@ -1686,7 +1686,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_REM, /** @@ -1700,7 +1700,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_RTI, /** @@ -1714,7 +1714,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MIN, /** @@ -1728,7 +1728,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_MAX, /** @@ -1742,7 +1742,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_LEQ, /** @@ -1756,7 +1756,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_LT, /** @@ -1770,7 +1770,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_GEQ, /** @@ -1784,7 +1784,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_GT, /** @@ -1798,7 +1798,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NORMAL, /** @@ -1812,7 +1812,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_SUBNORMAL, /** @@ -1826,7 +1826,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_ZERO, /** @@ -1840,7 +1840,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_INF, /** @@ -1854,7 +1854,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NAN, /** @@ -1868,7 +1868,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_NEG, /** @@ -1882,7 +1882,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_IS_POS, /** @@ -1899,7 +1899,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_IEEE_BV, /** @@ -1917,7 +1917,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_FP, /** @@ -1935,7 +1935,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_REAL, /** @@ -1953,7 +1953,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_SBV, /** @@ -1971,7 +1971,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_FP_FROM_UBV, /** @@ -1987,7 +1987,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_UBV, /** @@ -2003,7 +2003,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_SBV, /** @@ -2017,7 +2017,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ FLOATINGPOINT_TO_REAL, @@ -2035,7 +2035,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SELECT, /** @@ -2051,7 +2051,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STORE, /** @@ -2066,7 +2066,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ CONST_ARRAY, /** @@ -2093,7 +2093,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const * */ EQ_RANGE, @@ -2114,7 +2114,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_CONSTRUCTOR, /** @@ -2133,7 +2133,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_SELECTOR, /** @@ -2150,7 +2150,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_TESTER, /** @@ -2171,7 +2171,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ APPLY_UPDATER, /** @@ -2206,7 +2206,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ MATCH, /** @@ -2223,7 +2223,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ MATCH_CASE, /** @@ -2251,7 +2251,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ MATCH_BIND_CASE, /** @@ -2268,7 +2268,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ DT_SIZE, /** @@ -2332,7 +2332,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEP_PTO, /** @@ -2347,7 +2347,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEP_STAR, /** @@ -2364,7 +2364,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) 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&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_UNION, /** @@ -2402,7 +2402,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_INTER, /** @@ -2416,7 +2416,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_MINUS, /** @@ -2432,7 +2432,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_SUBSET, /** @@ -2450,7 +2450,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_MEMBER, /** @@ -2467,7 +2467,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_SINGLETON, /** @@ -2483,7 +2483,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_INSERT, /** @@ -2497,7 +2497,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_CARD, /** @@ -2511,7 +2511,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_COMPLEMENT, /** @@ -2552,7 +2552,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_COMPREHENSION, /** @@ -2571,7 +2571,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_CHOOSE, /** @@ -2585,7 +2585,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_IS_SINGLETON, /** @@ -2605,7 +2605,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ SET_MAP, @@ -2622,7 +2622,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_JOIN, /** @@ -2636,7 +2636,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_PRODUCT, /** @@ -2650,7 +2650,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_TRANSPOSE, /** @@ -2664,7 +2664,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_TCLOSURE, /** @@ -2678,7 +2678,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_JOIN_IMAGE, /** @@ -2692,7 +2692,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ RELATION_IDEN, @@ -2716,7 +2716,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_UNION_MAX, /** @@ -2730,7 +2730,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_UNION_DISJOINT, /** @@ -2744,7 +2744,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_INTER_MIN, /** @@ -2760,7 +2760,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_DIFFERENCE_SUBTRACT, /** @@ -2776,7 +2776,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_DIFFERENCE_REMOVE, /** @@ -2793,7 +2793,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) 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& children) const` + * - Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const + * - Solver::mkTerm(Kind kind, const std::vector& children) const */ BAG_COUNT, /** @@ -2820,7 +2820,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_MEMBER, /** @@ -2837,7 +2837,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_DUPLICATE_REMOVAL, /** @@ -2854,7 +2854,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_MAKE, /** @@ -2868,7 +2868,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_CARD, /** @@ -2889,7 +2889,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_CHOOSE, /** @@ -2903,7 +2903,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_IS_SINGLETON, /** @@ -2917,7 +2917,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_FROM_SET, /** @@ -2931,7 +2931,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_TO_SET, /** @@ -2951,7 +2951,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_MAP, /** @@ -2973,7 +2973,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_FILTER, /** @@ -2993,7 +2993,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ BAG_FOLD, /** @@ -3007,7 +3007,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ TABLE_PRODUCT, @@ -3024,7 +3024,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CONCAT, /** @@ -3039,7 +3039,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_IN_REGEXP, /** @@ -3053,7 +3053,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LENGTH, /** @@ -3074,7 +3074,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_SUBSTR, /** @@ -3095,7 +3095,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_UPDATE, /** @@ -3114,7 +3114,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CHARAT, /** @@ -3132,7 +3132,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_CONTAINS, /** @@ -3153,7 +3153,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_INDEXOF, /** @@ -3174,7 +3174,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_INDEXOF_RE, /** @@ -3194,7 +3194,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE, /** @@ -3214,7 +3214,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_ALL, /** @@ -3234,7 +3234,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_RE, /** @@ -3254,7 +3254,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REPLACE_RE_ALL, /** @@ -3268,7 +3268,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TOLOWER, /** @@ -3282,7 +3282,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TOUPPER, /** @@ -3296,7 +3296,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_REV, /** @@ -3313,7 +3313,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_CODE, /** @@ -3331,7 +3331,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_FROM_CODE, /** @@ -3349,7 +3349,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LT, /** @@ -3367,7 +3367,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_LEQ, /** @@ -3385,7 +3385,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_PREFIX, /** @@ -3403,7 +3403,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_SUFFIX, /** @@ -3419,7 +3419,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_IS_DIGIT, /** @@ -3435,7 +3435,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_FROM_INT, /** @@ -3452,7 +3452,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_INT, /** @@ -3474,7 +3474,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ STRING_TO_REGEXP, /** @@ -3488,7 +3488,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_CONCAT, /** @@ -3502,7 +3502,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_UNION, /** @@ -3516,7 +3516,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_INTER, /** @@ -3530,7 +3530,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_DIFF, /** @@ -3544,7 +3544,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_STAR, /** @@ -3558,7 +3558,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_PLUS, /** @@ -3572,7 +3572,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_OPT, /** @@ -3587,7 +3587,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_RANGE, /** @@ -3603,7 +3603,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_REPEAT, /** @@ -3624,7 +3624,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_LOOP, /** @@ -3659,7 +3659,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ REGEXP_COMPLEMENT, @@ -3674,7 +3674,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_CONCAT, /** @@ -3688,7 +3688,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_LENGTH, /** @@ -3709,7 +3709,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_EXTRACT, /** @@ -3730,7 +3730,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_UPDATE, /** @@ -3750,7 +3750,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_AT, /** @@ -3768,7 +3768,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_CONTAINS, /** @@ -3789,7 +3789,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_INDEXOF, /** @@ -3809,7 +3809,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REPLACE, /** @@ -3829,7 +3829,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REPLACE_ALL, /** @@ -3843,7 +3843,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_REV, /** @@ -3861,7 +3861,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_PREFIX, /** @@ -3879,7 +3879,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_SUFFIX, /** @@ -3911,7 +3911,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_UNIT, /** @@ -3928,7 +3928,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SEQ_NTH, @@ -3947,7 +3947,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ FORALL, /** @@ -3963,7 +3963,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ EXISTS, /** @@ -3979,7 +3979,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ VARIABLE_LIST, /** @@ -3996,7 +3996,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_PATTERN, /** @@ -4013,7 +4013,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_NO_PATTERN, /** @@ -4030,7 +4030,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_POOL, /** @@ -4044,7 +4044,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_ADD_TO_POOL, /** @@ -4058,7 +4058,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ SKOLEM_ADD_TO_POOL, /** @@ -4076,7 +4076,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_ATTRIBUTE, /** @@ -4091,7 +4091,7 @@ enum Kind : int32_t * - Solver::mkTerm(const Op&, const std::vector&) const * * - Create Op of this kind with: - * - Solver::mkOp(Kind, uint32_t, uint32_t) const + * - Solver::mkOp(Kind, const std::vector&) const */ INST_PATTERN_LIST, diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index b8a2e2739..718d63da8 100644 --- 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(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(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(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(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 f923a0263..4f482da9e 100644 --- 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 963ab70b8..18e6a1e79 100644 --- 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( k.value) - elif len(args) == 1: - if isinstance(args[0], str): - op.cop = self.csolver.mkOp( k.value, - - args[0].encode()) - elif isinstance(args[0], int): - op.cop = self.csolver.mkOp( k.value, 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(( a)) - op.cop = self.csolver.mkOp( k.value, 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( k.value, args[0], 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( k.value, + + 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(( a)) + op.cop = self.csolver.mkOp( k.value, v) return op def mkTrue(self): diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fc9aab8ef..e0caa77e7 100644 --- 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 numerals; + std::vector 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 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 numerals; + std::vector numerals; } /* constants */ : INTEGER_LITERAL @@ -1975,7 +1961,7 @@ sortSymbol[cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check] @declarations { std::string name; std::vector args; - std::vector numerals; + std::vector 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& numerals] +nonemptyNumeralList[std::vector& 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 13f7b6613..027d7e588 100644 --- 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& numerals) + const std::vector& numerals) { if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { @@ -911,7 +911,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& 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& 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 a03384aba..a945e373d 100644 --- 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& numerals); + const std::vector& 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 8d458ad8f..2780f3257 100644 --- a/test/api/cpp/issue6111.cpp +++ b/test/api/cpp/issue6111.cpp @@ -42,14 +42,14 @@ int main() vector 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 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 3d0f43777..6d91f72fa 100644 --- 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 95b93952e..f5484e306 100644 --- 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 c92f7b94f..137b12c44 100644 --- 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 10db4c8d0..91d551897 100644 --- 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 60137c56f..c994003a9 100644 --- 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 c9b47e2de..2c9b4ee48 100644 --- 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 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 args) - std::vector 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 965a935c5..81dfd2e43 100644 --- 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 be8e7cf08..878c872f0 100644 --- 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 2ce712689..c174886c4 100644 --- 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 099b1171b..de82dd1a4 100644 --- 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() -- 2.30.2