diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-22 18:37:47 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 11:37:47 -0600 |
| commit | 1700089e7ba96a883836eddcf2a8b88824aaa3e6 (patch) | |
| tree | 9d173d5da726e2fa9f4655a8cbfb1cd335540bd2 /src/CMakeLists.txt | |
| parent | 20b0feaf3f9858a1414f5d1eef9819913aae3ded (diff) | |
Add the LazyTreeProofGenerator. (#5948)
This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.
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 3bfb248a4..5a44df141 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -612,6 +612,8 @@ libcvc4_add_sources( theory/inference_id.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h + theory/lazy_tree_proof_generator.cpp + theory/lazy_tree_proof_generator.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp |