From f1351ca7462d3d601e0dec78b71f54e0c7ee381f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Jul 2020 13:30:23 -0500 Subject: 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. --- src/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/CMakeLists.txt') 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 -- cgit v1.2.3