projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5f51e8) | patch
(proof-new) Add quantifiers proof checker (#4593)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 16 Jun 2020 00:04:29 +0000 (19:04 -0500)
committerGitHub <noreply@github.com>
Tue, 16 Jun 2020 00:04:29 +0000 (19:04 -0500)
commitdf98bc96168869e1615bc0756bde3b2c5dba160e
treed6f1d3bfcae647b3ed3c6d9a657db847f010ebf6tree
parente5f51e82aceda35642acd92b417bfeb74edfdcddcommit | diff
(proof-new) Add quantifiers proof checker (#4593)

Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.

This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
src/CMakeLists.txt diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/quantifiers/proof_checker.cpp [new file with mode: 0644] blob
src/theory/quantifiers/proof_checker.h [new file with mode: 0644] blob