projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63e7c6b) | patch
(proof-new) Add the arrays proof checker (#5047)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 21 Sep 2020 17:09:33 +0000 (12:09 -0500)
committerGitHub <noreply@github.com>
Mon, 21 Sep 2020 17:09:33 +0000 (12:09 -0500)
commit44fd0bd8441d9dcce5aa9173757c9d8173924c17
treedb47d0c29fffeca7301d83ab6ef4320ccd37701btree
parent63e7c6bb6d9c99a5282241be8b32a04ea67dfb8dcommit | diff
(proof-new) Add the arrays proof checker (#5047)

Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
src/CMakeLists.txt diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arrays/proof_checker.cpp [new file with mode: 0644] blob
src/theory/arrays/proof_checker.h [new file with mode: 0644] blob
src/theory/arrays/skolem_cache.cpp [new file with mode: 0644] blob
src/theory/arrays/skolem_cache.h [new file with mode: 0644] blob
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history