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 | |
| 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')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 5 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 6 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxi | 3 |
3 files changed, 0 insertions, 14 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 037243ea4..f563e83f5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4106,11 +4106,6 @@ void Solver::push(uint32_t nscopes) const } /** - * ( reset ) - */ -void Solver::reset(void) const { d_smtEngine->reset(); } - -/** * ( reset-assertions ) */ void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); } 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 ) */ diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index d61fed0fc..188753122 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -935,9 +935,6 @@ cdef class Solver: def push(self, nscopes=1): self.csolver.push(nscopes) - def reset(self): - self.csolver.reset() - def resetAssertions(self): self.csolver.resetAssertions() |