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/proof_checker.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/expr/proof_checker.h')
| -rw-r--r-- | src/expr/proof_checker.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 99c02b8dc..f04587a7d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -77,7 +77,7 @@ class ProofRuleChecker /** * This checks a single step in a proof. It is identical to check above * except that children and args have been converted to "witness form" - * (see ProofSkolemCache). Likewise, its output should be in witness form. + * (see SkolemManager). Likewise, its output should be in witness form. * * @param id The id of the proof node to check * @param children The premises of the proof node to check. These are nodes @@ -100,6 +100,8 @@ class ProofCheckerStatistics ~ProofCheckerStatistics(); /** Counts the number of checks for each kind of proof rule */ HistogramStat<PfRule> d_ruleChecks; + /** Total number of rule checks */ + IntStat d_totalRuleChecks; }; /** A class for checking proofs */ |