diff options
| author | makaimann <makaim@stanford.edu> | 2019-06-28 02:36:16 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-06-28 02:36:16 -0700 |
| commit | 3777d6c940818a8085dbcc7a83f6d82adf4ced0f (patch) | |
| tree | 0a13fab8ea58d0ae920f15371771090928a0976b | |
| parent | 0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5 (diff) | |
Make mkOpTerm const (#3072)
| -rw-r--r-- | src/api/cvc4cpp.cpp | 8 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7750823d3..32484a49e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2726,20 +2726,20 @@ std::vector<Expr> Solver::termVectorToExprs( /* Create operator terms */ /* -------------------------------------------------------------------------- */ -OpTerm Solver::mkOpTerm(Kind kind, Kind k) +OpTerm Solver::mkOpTerm(Kind kind, Kind k) const { CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get(); } -OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) +OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const { CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind) << "RECORD_UPDATE_OP"; return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get(); } -OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) +OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const { CVC4_API_KIND_CHECK(kind); OpTerm res; @@ -2808,7 +2808,7 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) return res; } -OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) +OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const { CVC4_API_KIND_CHECK(kind); OpTerm res; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index c13c7919e..2ff1cb91d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1813,7 +1813,7 @@ class CVC4_PUBLIC Solver * @param kind the kind of the operator * @param k the kind argument to this operator */ - OpTerm mkOpTerm(Kind kind, Kind k); + OpTerm mkOpTerm(Kind kind, Kind k) const; /** * Create operator of kind: @@ -1822,7 +1822,7 @@ class CVC4_PUBLIC Solver * @param kind the kind of the operator * @param arg the string argument to this operator */ - OpTerm mkOpTerm(Kind kind, const std::string& arg); + OpTerm mkOpTerm(Kind kind, const std::string& arg) const; /** * Create operator of kind: @@ -1842,7 +1842,7 @@ class CVC4_PUBLIC Solver * @param kind the kind of the operator * @param arg the uint32_t argument to this operator */ - OpTerm mkOpTerm(Kind kind, uint32_t arg); + OpTerm mkOpTerm(Kind kind, uint32_t arg) const; /** * Create operator of Kind: @@ -1858,7 +1858,7 @@ class CVC4_PUBLIC Solver * @param arg1 the first uint32_t argument to this operator * @param arg2 the second uint32_t argument to this operator */ - OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2); + OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const; /* .................................................................... */ /* Create Constants */ |