diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-03 09:18:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-03 09:18:59 -0600 |
| commit | 0cd812af4a6db43a7d6c2c95fff7e58f86e90a78 (patch) | |
| tree | ab35d8c8dd7ee7c7c8ba085d42ef834fe17e2dbd /src/CMakeLists.txt | |
| parent | 1d44edf91762b837adf3db5ed40af9383e883b28 (diff) | |
Standardize the interface for SMT engine subsolvers (#3836)
This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
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 52f46147c..201b6a21d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -665,6 +665,8 @@ libcvc4_add_sources( theory/sets/theory_sets_type_rules.h theory/shared_terms_database.cpp theory/shared_terms_database.h + theory/smt_engine_subsolver.cpp + theory/smt_engine_subsolver.h theory/sort_inference.cpp theory/sort_inference.h theory/strings/base_solver.cpp |