Quantifier elimination for the theory of bit vectors#138

Open

AnzhelaSukhanova wants to merge 13 commits intoUnitTestBot:mainfrom

AnzhelaSukhanova:main

Commits on Jun 30, 2023

start work on QE for BV arithmetic
AnzhelaSukhanova
committed

Commits on Jul 18, 2023

add the simplest case of QE for BV theory
AnzhelaSukhanova
committed

Commits on Aug 29, 2023

Commits on Sep 11, 2023

fix problem in QE for BV theory
AnzhelaSukhanova
committed

Commits on Sep 13, 2023

Add QE result check and fix some problems
AnzhelaSukhanova
committed

Commits on Sep 19, 2023

Fix some problems in QE for BV theory
AnzhelaSukhanova
committed

Commits on Oct 18, 2023

bit-vector QE when all bound terms have the same linear coefficient
AnzhelaSukhanova
committed

Commits on Oct 27, 2023

Commits on Nov 7, 2023

Commits on Nov 9, 2023

correct bit-vector QE
AnzhelaSukhanova
committed