projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6341581) | patch
(proof-new) Rewrites involving operators in term conversion proof generator (#5072)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 18 Sep 2020 02:06:44 +0000 (21:06 -0500)
committerGitHub <noreply@github.com>
Fri, 18 Sep 2020 02:06:44 +0000 (21:06 -0500)
commitcb438c1aca9e205359313f2e661fef910e1132b6
treec13f405d9065846619fcc8e1008bfa3433542a13tree
parent6341581d4b6797e8a9169a2ad88638987da255a4commit | 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.
src/expr/term_context.cpp diff | blob | history
src/expr/term_context.h diff | blob | history
src/expr/term_context_stack.cpp diff | blob | history
src/expr/term_context_stack.h diff | blob | history
src/expr/term_conversion_proof_generator.cpp diff | blob | history
src/expr/term_conversion_proof_generator.h diff | blob | history
src/smt/witness_form.cpp diff | blob | history