mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-06-05 14:36:18 +01:00
commit d301bd35a9
4 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/fixedpoint_params.pyg
View file

@ -60,7 +60,7 @@ def_module_params('fixedpoint',
('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
('print_statistics', BOOL, False, 'print statistics'), ('print_statistics', BOOL, False, 'print statistics'),
('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'), ('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'),
('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
)) ))

4
src/muz_qe/qe_lite.cpp
View file

@ -1417,6 +1417,7 @@ namespace fm {
fm(ast_manager & _m): fm(ast_manager & _m):
m(_m), m(_m),
m_is_variable(0),
m_allocator("fm-elim"), m_allocator("fm-elim"),
m_util(m), m_util(m),
m_bvar2expr(m), m_bvar2expr(m),
@ -1424,6 +1425,9 @@ namespace fm {
m_new_fmls(m), m_new_fmls(m),
m_inconsistent_core(m) { m_inconsistent_core(m) {
m_cancel = false; m_cancel = false;
updt_params();
m_counter = 0;
m_inconsistent = false;
} }
~fm() { ~fm() {

10
src/util/bit_vector.cpp
View file

@ -22,6 +22,8 @@ Revision History:
#define DEFAULT_CAPACITY 2 #define DEFAULT_CAPACITY 2
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
void bit_vector::expand_to(unsigned new_capacity) { void bit_vector::expand_to(unsigned new_capacity) {
unsigned * new_data = alloc_svect(unsigned, new_capacity); unsigned * new_data = alloc_svect(unsigned, new_capacity);
memset(new_data, 0, new_capacity * sizeof(unsigned)); memset(new_data, 0, new_capacity * sizeof(unsigned));
@ -51,7 +53,7 @@ void bit_vector::resize(unsigned new_size, bool val) {
unsigned ewidx = num_words(new_size); unsigned ewidx = num_words(new_size);
unsigned * begin = m_data + bwidx; unsigned * begin = m_data + bwidx;
unsigned pos = m_num_bits % 32; unsigned pos = m_num_bits % 32;
unsigned mask = (1 << pos) - 1; unsigned mask = MK_MASK(pos);
int cval; int cval;
if (val) { if (val) {
@ -128,7 +130,7 @@ bool bit_vector::operator==(bit_vector const & source) const {
return false; return false;
} }
unsigned bit_rest = source.m_num_bits % 32; unsigned bit_rest = source.m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
if (mask == 0) mask = UINT_MAX; if (mask == 0) mask = UINT_MAX;
return (m_data[i] & mask) == (source.m_data[i] & mask); return (m_data[i] & mask) == (source.m_data[i] & mask);
} }
@ -149,7 +151,7 @@ bit_vector & bit_vector::operator|=(bit_vector const & source) {
unsigned i = 0; unsigned i = 0;
for (i = 0; i < n2 - 1; i++) for (i = 0; i < n2 - 1; i++)
m_data[i] |= source.m_data[i]; m_data[i] |= source.m_data[i];
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
m_data[i] |= source.m_data[i] & mask; m_data[i] |= source.m_data[i] & mask;
} }
return *this; return *this;
@ -175,7 +177,7 @@ bit_vector & bit_vector::operator&=(bit_vector const & source) {
else { else {
for (i = 0; i < n2 - 1; i++) for (i = 0; i < n2 - 1; i++)
m_data[i] &= source.m_data[i]; m_data[i] &= source.m_data[i];
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
m_data[i] &= (source.m_data[i] & mask); m_data[i] &= (source.m_data[i] & mask);
} }

1
src/util/bit_vector.h
View file

@ -69,6 +69,7 @@ public:
m_num_bits(0), m_num_bits(0),
m_capacity(num_words(reserve_num_bits)), m_capacity(num_words(reserve_num_bits)),
m_data(alloc_svect(unsigned, m_capacity)) { m_data(alloc_svect(unsigned, m_capacity)) {
memset(m_data, 0, m_capacity * sizeof(unsigned));
} }
bit_vector(bit_vector const & source): bit_vector(bit_vector const & source):