diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-12 12:04:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-12 14:04:48 -0500 |
| commit | 83a18f98dddbd635db3823dd18b7bdf22b020869 (patch) | |
| tree | f2efd227b8896ded2e97cb8bbc956443885aede6 /src/api/cvc4cpp.h | |
| parent | f906530aa75e9c21e7877cac30cd3cb8245e3058 (diff) | |
New C++ API: Remove support for (reset). (#4037)
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 7ccb73bc3..3c99d2480 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2762,12 +2762,6 @@ class CVC4_PUBLIC Solver void push(uint32_t nscopes = 1) const; /** - * Reset the solver. - * SMT-LIB: ( reset ) - */ - void reset() const; - - /** * Remove all assertions. * SMT-LIB: ( reset-assertions ) */ |