projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bdc1b22) | patch
Compute fact or lemma in datatypes prior to buffering (#5914)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 17 Feb 2021 17:00:41 +0000 (11:00 -0600)
committerGitHub <noreply@github.com>
Wed, 17 Feb 2021 17:00:41 +0000 (11:00 -0600)
commitd107bf9b8b4dd206580681e601a033742029ec79
treed430fc6b653eac528c209782b9877718580e7ca9tree
parentbdc1b222fbc674ab1f8a48fad9f78759c3baea23commit | diff
Compute fact or lemma in datatypes prior to buffering (#5914)

This is necessary for the planned refactoring of TheoryInference::process. This forces datatypes to decide lemma vs. fact prior to buffering inferences.
src/theory/datatypes/inference.cpp diff | blob | history
src/theory/datatypes/inference_manager.cpp diff | blob | history