From: makaimann <makaim@stanford.edu>
Date: Fri, 28 Jun 2019 09:36:16 +0000 (-0700)
Subject: Make mkOpTerm const (#3072)
X-Git-Tag: cvc5-1.0.0~4101
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3777d6c940818a8085dbcc7a83f6d82adf4ced0f;p=cvc5.git

Make mkOpTerm const (#3072)
---

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                                                     */