diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-20 20:04:37 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 13:04:37 -0600 |
| commit | 20007b739555fe27a6600fcb4d156173bcc0eee3 (patch) | |
| tree | ac5b25d48fe713e0ab35839b7480d86a8cb1c2e1 /src/theory/trust_substitutions.h | |
| parent | de0d36b8972954c281f1e97b15d37c07a861cbc1 (diff) | |
(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)
This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
Diffstat (limited to 'src/theory/trust_substitutions.h')
| -rw-r--r-- | src/theory/trust_substitutions.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index d7f48d054..c316f08c5 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -20,8 +20,8 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/lazy_proof.h" -#include "expr/lazy_proof_set.h" #include "expr/proof_node_manager.h" +#include "expr/proof_set.h" #include "expr/term_conversion_proof_generator.h" #include "theory/eager_proof_generator.h" #include "theory/substitutions.h" @@ -94,6 +94,8 @@ class TrustSubstitutionMap * Moreover, it ensures that d_subsPg has a proof of the returned value. */ Node getCurrentSubstitution(); + /** The context used here */ + context::Context* d_ctx; /** The substitution map */ SubstitutionMap d_subs; /** The proof node manager */ @@ -109,7 +111,7 @@ class TrustSubstitutionMap /** * A context-dependent list of LazyCDProof, allocated for internal steps. */ - LazyCDProofSet d_helperPf; + CDProofSet<LazyCDProof> d_helperPf; /** * The formula corresponding to the current substitution. This is of the form * (and (= x1 t1) ... (= xn tn)) |