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/theory/strings/skolem_cache.h | |
| 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/theory/strings/skolem_cache.h')
| -rw-r--r-- | src/theory/strings/skolem_cache.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 0ebbb3277..7ce507f29 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -22,7 +22,7 @@ #include <unordered_set> #include "expr/node.h" -#include "expr/proof_skolem_cache.h" +#include "expr/skolem_manager.h" namespace CVC4 { namespace theory { |