New C++ API: Remove support for (reset). (#4037)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 12 Mar 2020 19:04:48 +0000 (12:04 -0700)
committerGitHub <noreply@github.com>
Thu, 12 Mar 2020 19:04:48 +0000 (14:04 -0500)
commit83a18f98dddbd635db3823dd18b7bdf22b020869
treef2efd227b8896ded2e97cb8bbc956443885aede6
parentf906530aa75e9c21e7877cac30cd3cb8245e3058
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.
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/python/cvc4.pxi
src/main/command_executor.cpp
src/main/command_executor.h
src/main/driver_unified.cpp
test/regress/CMakeLists.txt
test/regress/regress0/smtlib/reset.smt2 [new file with mode: 0644]