diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-15 13:30:23 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-15 13:30:23 -0500 |
| commit | f1351ca7462d3d601e0dec78b71f54e0c7ee381f (patch) | |
| tree | 59c12b9b7c124e12776d973813009c230c43574e /src/CMakeLists.txt | |
| parent | 9975291763425e0aba9ae135ccd86d1fbc176d9d (diff) | |
Split abduction solver from SmtEngine (#4733)
This splits everything related to abducts into its own standalone module, AbductionSolver.
It furthermore converts some of the interfaces of SmtEngine to make them take Node instead of Expr (this will be done for every method eventually).
The code for interpolation should follow a similar pattern, e.g. InterpolantSolver.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 199c14330..28d943ced 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -219,6 +219,8 @@ libcvc4_add_sources( prop/sat_solver_types.h prop/theory_proxy.cpp prop/theory_proxy.h + smt/abduction_solver.cpp + smt/abduction_solver.h smt/command.cpp smt/command.h smt/command_list.cpp |