From bd064bf5d06145a6638d78f565469f571929248e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Jun 2013 11:46:13 -0700 Subject: [PATCH 1/2] enable UTVPI by default Signed-off-by: Nikolaj Bjorner --- src/muz_qe/fixedpoint_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c2d33cb05..d38c3c9b0 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -60,7 +60,7 @@ def_module_params('fixedpoint', ('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('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'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) From b6d9d8a60127da23318dd776bc186539b1530014 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jun 2013 12:55:35 -0700 Subject: [PATCH 2/2] fix bugs reported by Nuno Lopes Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe_lite.cpp | 4 ++++ src/util/bit_vector.cpp | 10 ++++++---- src/util/bit_vector.h | 1 + 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 50c3347ee..f840f19d6 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -1417,6 +1417,7 @@ namespace fm { fm(ast_manager & _m): m(_m), + m_is_variable(0), m_allocator("fm-elim"), m_util(m), m_bvar2expr(m), @@ -1424,6 +1425,9 @@ namespace fm { m_new_fmls(m), m_inconsistent_core(m) { m_cancel = false; + updt_params(); + m_counter = 0; + m_inconsistent = false; } ~fm() { diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 0d67f1f79..6885b93e8 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -22,6 +22,8 @@ Revision History: #define DEFAULT_CAPACITY 2 +#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1) + void bit_vector::expand_to(unsigned new_capacity) { unsigned * new_data = alloc_svect(unsigned, new_capacity); 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 * begin = m_data + bwidx; unsigned pos = m_num_bits % 32; - unsigned mask = (1 << pos) - 1; + unsigned mask = MK_MASK(pos); int cval; if (val) { @@ -128,7 +130,7 @@ bool bit_vector::operator==(bit_vector const & source) const { return false; } 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; 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; for (i = 0; i < n2 - 1; 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; } return *this; @@ -175,7 +177,7 @@ bit_vector & bit_vector::operator&=(bit_vector const & source) { else { for (i = 0; i < n2 - 1; 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); } diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index cbe7a0618..0ccdeae9e 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -69,6 +69,7 @@ public: m_num_bits(0), m_capacity(num_words(reserve_num_bits)), m_data(alloc_svect(unsigned, m_capacity)) { + memset(m_data, 0, m_capacity * sizeof(unsigned)); } bit_vector(bit_vector const & source):