diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 10:29:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 10:29:46 -0500 |
| commit | ee00caa684da76ce494d57d30b22ad20c082b652 (patch) | |
| tree | f173c6921065258def2771bbaf05040475b642f3 /src/expr/CMakeLists.txt | |
| parent | 835c79635e241366feec5fa34656dc98d1a77fef (diff) | |
(proof-new) Callbacks for term-context-sensitive terms (#4842)
Callbacks for term-context-sensitive terms.
It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.
These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.
Diffstat (limited to 'src/expr/CMakeLists.txt')
| -rw-r--r-- | src/expr/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 993df2594..0092b78c6 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -61,6 +61,8 @@ libcvc4_add_sources( symbol_table.h term_canonize.cpp term_canonize.h + term_context.cpp + term_context.h term_conversion_proof_generator.cpp term_conversion_proof_generator.h type.cpp |