projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 30aa15c) | patch
Make BVInstantiatorUtil an EnvObj (#8633)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 25 Apr 2022 18:21:57 +0000 (13:21 -0500)
committerGitHub <noreply@github.com>
Mon, 25 Apr 2022 18:21:57 +0000 (18:21 +0000)
commiteb6c4c958b8c363c603510672fd8a9e2dc4d832e
treeb1da072b11d3609a3a6c2017510e5020fcb21f50tree
parent30aa15ca61677b53db95cd7ee4210ae90c8b6d3ccommit | diff
Make BVInstantiatorUtil an EnvObj (#8633)

Eliminates 5 of the remaining 8 static calls to Rewriter::rewrite.
src/smt/solver_engine.h diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h diff | blob | history
test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp diff | blob | history