projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6210af) | patch
New InferenceIds for BV theory (#5909)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 18 Feb 2021 20:37:30 +0000 (21:37 +0100)
committerGitHub <noreply@github.com>
Thu, 18 Feb 2021 20:37:30 +0000 (21:37 +0100)
commitba30b690b29e7e52dd8ea1ea953525c401abf3d9
treecf2f9aae0c0a31a0290b8a65cce7b98719b8dae7tree
parentc6210af1db67701495efa263207b91064a3bcd0bcommit | diff
New InferenceIds for BV theory (#5909)

This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
src/theory/bv/bitblast/lazy_bitblaster.cpp diff | blob | history
src/theory/bv/bv_solver_bitblast.cpp diff | blob | history
src/theory/bv/bv_solver_lazy.cpp diff | blob | history
src/theory/bv/bv_solver_lazy.h diff | blob | history
src/theory/bv/bv_solver_simple.cpp diff | blob | history
src/theory/bv/bv_subtheory_core.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history