summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r--src/api/cvc4cpp.h5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 382ffff95..1d6367b31 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3549,6 +3549,7 @@ class CVC4_PUBLIC Solver
private:
/** @return the node manager of this solver */
NodeManager* getNodeManager(void) const;
+
/** Helper to check for API misuse in mkOp functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/** Helper for mk-functions that call d_nodeMgr->mkConst(). */
@@ -3567,8 +3568,6 @@ class CVC4_PUBLIC Solver
uint32_t base) const;
/** Helper for mkBitVector functions that take an integer as argument. */
Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
- /** Helper for setLogic. */
- void setLogicHelper(const std::string& logic) const;
/** Helper for mkTerm functions that create Term from a Kind */
Term mkTermFromKind(Kind kind) const;
/** Helper for mkChar functions that take a string as argument. */
@@ -3628,7 +3627,7 @@ class CVC4_PUBLIC Solver
bool isInv = false,
Grammar* g = nullptr) const;
- /** check whether string s is a valid decimal integer */
+ /** Check whether string s is a valid decimal integer. */
bool isValidInteger(const std::string& s) const;
/** The node manager of this solver. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback