diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-03 14:01:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-03 14:01:13 -0500 |
| commit | f70e265cd4e7df46a1b3b7e3cc67fbf9b9b1b528 (patch) | |
| tree | 289b34fd775c89b2d44b464b18d40f43d16e0630 /src/CMakeLists.txt | |
| parent | 145b9367255d2925b6b4e43818e223b9186bcfad (diff) | |
(proof-new) Add builtin proof checker (#4537)
This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
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 20e110b2b..4fb1606bc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -366,6 +366,8 @@ libcvc4_add_sources( theory/builtin/theory_builtin_rewriter.cpp theory/builtin/theory_builtin_rewriter.h theory/builtin/theory_builtin_type_rules.h + theory/builtin/proof_checker.cpp + theory/builtin/proof_checker.h theory/builtin/type_enumerator.cpp theory/builtin/type_enumerator.h theory/bv/abstraction.cpp |