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 /src/api/cvc4cpp.cpp | |
parent | 0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5 (diff) |
Make mkOpTerm const (#3072)
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 8 |
1 files changed, 4 insertions, 4 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; |