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