diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-21 21:21:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-21 21:21:42 -0500 |
| commit | 0e7ebfa3ba5d5049c81b2c5ac113af62c35f5c64 (patch) | |
| tree | c5a9d62c560592003f9fd0003faece8585c7c30a /src/theory/theory_preprocessor.h | |
| parent | a99f5aaa46702a4894aaddeed3a7ff5cbf69bdfd (diff) | |
(proof-new) Make theory preprocessor user-context dependent (#5296)
Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.
This PR also makes the theory preprocess pass proof producing.
Diffstat (limited to 'src/theory/theory_preprocessor.h')
| -rw-r--r-- | src/theory/theory_preprocessor.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 769d548d9..e34b10b1d 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -19,6 +19,8 @@ #include <unordered_map> +#include "context/cdhashmap.h" +#include "context/context.h" #include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/tconv_seq_proof_generator.h" @@ -38,17 +40,16 @@ namespace theory { */ class TheoryPreprocessor { - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; public: /** Constructs a theory preprocessor */ TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr, + context::UserContext* userContext, ProofNodeManager* pnm = nullptr); /** Destroys a theory preprocessor */ ~TheoryPreprocessor(); - /** Clear the cache of this class */ - void clearCache(); /** * Preprocesses the given assertion node. It returns a TrustNode of kind * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores @@ -84,8 +85,6 @@ class TheoryPreprocessor NodeMap d_ppCache; /** The term formula remover */ RemoveTermFormulas& d_tfr; - /** The context for the proof generator below */ - context::Context d_pfContext; /** The term context, which computes hash values for term contexts. */ InQuantTermContext d_iqtc; /** |