mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-08 16:25:48 +00:00
Code Activity

tbv utilities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-15 21:23:03 -07:00
parent cd12fa8461
commit d9dafe7b94
6 changed files with 282 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/test/tbv.cpp Normal file
View file

@ -0,0 +1,39 @@
#include "tbv.h"
static void tst1(unsigned num_bits) {
tbv_manager m(num_bits);
tbv* b1 = m.allocate1();
tbv* b0 = m.allocate0();
tbv* bX = m.allocateX();
tbv* bN = m.allocate(31);
m.display(std::cout, *b0) << "\n";
m.display(std::cout, *b1) << "\n";
m.display(std::cout, *bX) << "\n";
m.display(std::cout, *bN) << "\n";
SASSERT(!m.equals(*b1,*b0));
SASSERT(!m.equals(*b1,*bX));
SASSERT(!m.equals(*b0,*bX));
m.set_and(*bX,*b0);
SASSERT(m.equals(*b0,*bX));
SASSERT(!m.equals(*b1,*bX));
m.copy(*bX,*b1);
SASSERT(m.equals(*b1,*bX));
SASSERT(!m.equals(*b0,*bX));
m.fillX(*bX);
VERIFY(m.intersect(*bX,*b0,*bN));
SASSERT(m.equals(*b0, *bN));
VERIFY(!m.intersect(*b0,*b1,*bN));
m.deallocate(b0);
m.deallocate(b1);
m.deallocate(bX);
m.deallocate(bN);
}
void tst_tbv() {
tst1(31);
tst1(11);
tst1(15);
tst1(16);
tst1(17);
}