diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-05 10:19:10 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-05 10:19:10 -0500 |
| commit | e9c29bb348bd8fab5cedc48ab96ce2a0e6f98078 (patch) | |
| tree | bd23e59f1cefd4cd7bf062130e978327d33a8c55 /src/expr/CMakeLists.txt | |
| parent | 7aa98fa461932db12c05820e685772d2aa983993 (diff) | |
(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
Diffstat (limited to 'src/expr/CMakeLists.txt')
| -rw-r--r-- | src/expr/CMakeLists.txt | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 3d41b7a72..6415e2132 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -49,10 +49,10 @@ libcvc4_add_sources( proof_node_manager.h proof_rule.cpp proof_rule.h - proof_skolem_cache.cpp - proof_skolem_cache.h proof_step_buffer.cpp proof_step_buffer.h + skolem_manager.cpp + skolem_manager.h symbol_table.cpp symbol_table.h term_canonize.cpp |