(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 5 Jun 2020 15:19:10 +0000 (10:19 -0500)
committerGitHub <noreply@github.com>
Fri, 5 Jun 2020 15:19:10 +0000 (10:19 -0500)
commite9c29bb348bd8fab5cedc48ab96ce2a0e6f98078
treebd23e59f1cefd4cd7bf062130e978327d33a8c55
parent7aa98fa461932db12c05820e685772d2aa983993
(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.
13 files changed:
src/expr/CMakeLists.txt
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/proof_checker.cpp
src/expr/proof_checker.h
src/expr/proof_skolem_cache.cpp [deleted file]
src/expr/proof_skolem_cache.h [deleted file]
src/expr/skolem_manager.cpp [new file with mode: 0644]
src/expr/skolem_manager.h [new file with mode: 0644]
src/theory/arith/theory_arith_private.cpp
src/theory/builtin/proof_checker.cpp
src/theory/strings/skolem_cache.cpp
src/theory/strings/skolem_cache.h