diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-17 21:06:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-17 21:06:44 -0500 |
| commit | cb438c1aca9e205359313f2e661fef910e1132b6 (patch) | |
| tree | c13f405d9065846619fcc8e1008bfa3433542a13 /src/expr/term_context.h | |
| parent | 6341581d4b6797e8a9169a2ad88638987da255a4 (diff) | |
(proof-new) Rewrites involving operators in term conversion proof generator (#5072)
In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
Diffstat (limited to 'src/expr/term_context.h')
| -rw-r--r-- | src/expr/term_context.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/expr/term_context.h b/src/expr/term_context.h index 87f91f2df..0c51dd493 100644 --- a/src/expr/term_context.h +++ b/src/expr/term_context.h @@ -48,6 +48,11 @@ class TermContext * is the term context identifier of t. */ virtual uint32_t computeValue(TNode t, uint32_t tval, size_t index) const = 0; + /** + * Returns the term context identifier of the operator of t, where tval + * is the term context identifier of t. + */ + virtual uint32_t computeValueOp(TNode t, uint32_t tval) const; }; /** |