Make mkOpTerm const (#3072)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 7750823d351553869fee78ee94c2de3a84d09201..32484a49e26a7050d91ed5ed8ee1257ed88ca6f4 100644 (file)
--- 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 c13c7919e1fd845870471061319f2fb9080e3cc4..2ff1cb91d595acb3a3e029feecd30c47a492b8a5 100644 (file)
--- 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                                                     */