projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54991eb) | patch
bv-to-int-module: implementations and stubs for translating operators (#7086)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 31 Aug 2021 16:45:48 +0000 (19:45 +0300)
committerGitHub <noreply@github.com>
Tue, 31 Aug 2021 16:45:48 +0000 (16:45 +0000)
commit70baef755ad939040c9a670da224512eb076f61b
treed6310805f0c19614567b8dfe60fb417e5c8d496ftree
parent54991eb9fa2e21c8c4705c5522ad99a9ccd9b41bcommit | diff
bv-to-int-module: implementations and stubs for translating operators (#7086)

This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.
src/theory/bv/int_blaster.cpp diff | blob | history
src/theory/bv/int_blaster.h diff | blob | history
test/unit/theory/theory_bv_int_blaster_white.cpp diff | blob | history