Interpolation step 1 (#4638)
authorYing Sheng <sqy1415@gmail.com>
Tue, 30 Jun 2020 11:50:40 +0000 (04:50 -0700)
committerGitHub <noreply@github.com>
Tue, 30 Jun 2020 11:50:40 +0000 (08:50 -0300)
commit724d8cf23ae74158b36b408643298c49c3b20833
tree737db246271ec879aaae7e62e49b858faf473e35
parent6303c25fc375f33b27398f9b8c4b70901785a5f1
Interpolation step 1 (#4638)

This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The first step creates the API framework, while omits the implementation for getting interpolation.
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/options/smt_options.toml
src/parser/smt2/Smt2.g
src/smt/command.cpp
src/smt/command.h
src/smt/set_defaults.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/datatypes/sygus_extension.cpp
test/unit/api/solver_black.h