projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b02977f) | patch
(proof-new) Make proofs mandatory in proof equality engine (#5059)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Sep 2020 01:47:43 +0000 (20:47 -0500)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 01:47:43 +0000 (20:47 -0500)
commit33f51490a9df73d8fee25fb88b19a87339b28e95
tree49348f42447860781a573dd61494bfee277d62ectree
parentb02977f0076ade00b631e8ee79a31b96bf7a24c4commit | diff
(proof-new) Make proofs mandatory in proof equality engine (#5059)

All uses of proof equality engine are now guarded such that the ordinary equality engine is used when proofs are not enabled. Thus, we can make proofs mandatory in proof equality engine. This eliminates the need for some guards.

Some indentation changed, but there are no additions in this PR.
src/theory/uf/proof_equality_engine.cpp diff | blob | history
src/theory/uf/proof_equality_engine.h diff | blob | history