diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-02 16:15:16 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-02 16:15:16 -0500 |
| commit | 51b9c07af2001e961911e59f3e7e80728c88550a (patch) | |
| tree | bd3e2139979fc183474d3254ddc59df88934b75b /src/smt | |
| parent | 26601663d6cc8fb8613df5a1d253eba8743e57cb (diff) | |
(proof-new) Fixes for theory preprocessing proofs (#5171)
This fixes several subtle issues with theory preprocessing.
The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.
It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 5 | ||||
| -rw-r--r-- | src/smt/term_formula_removal.h | 10 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 5034119e8..cf7c00e2b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -552,6 +552,11 @@ void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm) } } +ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() +{ + return d_tpg.get(); +} + bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; } }/* CVC4 namespace */ diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 30972c1cc..25dcd0295 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -107,11 +107,19 @@ class RemoveTermFormulas { /** * Set proof node manager, which signals this class to enable proofs using the - * given checker. + * given proof node manager. */ void setProofNodeManager(ProofNodeManager* pnm); /** + * Get proof generator that is responsible for all proofs for removing term + * formulas from nodes. When proofs are enabled, the returned trust node + * of the run method use this proof generator (the trust nodes in newAsserts + * do not use this generator). + */ + ProofGenerator* getTConvProofGenerator(); + + /** * Get axiom for term n. This returns the axiom that this class uses to * eliminate the term n, which is determined by its top-most symbol. For * example, if n is (ite n1 n2 n3), this returns the formula: |