From 3777d6c940818a8085dbcc7a83f6d82adf4ced0f Mon Sep 17 00:00:00 2001 From: makaimann Date: Fri, 28 Jun 2019 02:36:16 -0700 Subject: [PATCH] Make mkOpTerm const (#3072) --- src/api/cvc4cpp.cpp | 8 ++++---- 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 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(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(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 */ -- 2.30.2