(proof-new) Updates to builtin proof checker (#4962)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 2 Sep 2020 19:32:24 +0000 (14:32 -0500)
committerGitHub <noreply@github.com>
Wed, 2 Sep 2020 19:32:24 +0000 (14:32 -0500)
commitf9a4549c3dab3cd91f0d9973b24b7891048ed1d9
tree245ee9c0d3cf262f6b0ec598978d5b6e51f102b3
parentc17f9b25cac7c0d2941ef136466cb750cf4c3e7b
(proof-new) Updates to builtin proof checker (#4962)

This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.
src/expr/proof_rule.cpp
src/expr/proof_rule.h
src/theory/builtin/proof_checker.cpp
src/theory/builtin/proof_checker.h
src/theory/rewriter.cpp
src/theory/rewriter.h