summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.h
diff options
context:
space:
mode:
authormakaimann <makaim@stanford.edu>2019-06-28 02:36:16 -0700
committerAina Niemetz <aina.niemetz@gmail.com>2019-06-28 02:36:16 -0700
commit3777d6c940818a8085dbcc7a83f6d82adf4ced0f (patch)
tree0a13fab8ea58d0ae920f15371771090928a0976b /src/api/cvc4cpp.h
parent0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5 (diff)
Make mkOpTerm const (#3072)
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r--src/api/cvc4cpp.h8
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback