projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3a180a2) | patch
proof: Add eqrange expansion rule. (#6936)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 27 Jul 2021 19:39:53 +0000 (12:39 -0700)
committerGitHub <noreply@github.com>
Tue, 27 Jul 2021 19:39:53 +0000 (19:39 +0000)
commit4c87b04c95b60c34d2e8313e82579fbb0415eaf7
tree097ecca3b4494722a4cc36dd136b37f274e3fcebtree
parent3a180a2f8ffe8ad5756119ce0cbe61ab4ab28127commit | diff
proof: Add eqrange expansion rule. (#6936)

Adds proof support for the eqrange operator.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
src/proof/proof_rule.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/theory/arrays/proof_checker.cpp diff | blob | history
src/theory/arrays/skolem_cache.cpp diff | blob | history
src/theory/arrays/skolem_cache.h diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays_rewriter.cpp diff | blob | history
src/theory/arrays/theory_arrays_rewriter.h diff | blob | history