From 1f5097cdaa40fab3e788412e3ed402fdfe372834 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 15 Apr 2013 16:53:25 -0700 Subject: [PATCH 1/4] [datalog] fix stratum cycle break for rules with multiple looping dependecies e.g. a -> b b-> a a -> a this change makes the cycle breaker quadratic on the number of predicates. This should be revisited later Signed-off-by: Nuno Lopes --- src/muz_qe/dl_compiler.cpp | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 9110c5edb..215a438fc 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -803,17 +803,15 @@ namespace datalog { context& m_context; item_set & m_removed; svector m_stack; - ast_mark m_stack_content; ast_mark m_visited; void traverse(T v) { - SASSERT(!m_stack_content.is_marked(v)); - if(m_visited.is_marked(v) || m_removed.contains(v)) { + SASSERT(!m_visited.is_marked(v)); + if (m_removed.contains(v)) { return; } m_stack.push_back(v); - m_stack_content.mark(v, true); m_visited.mark(v, true); const item_set & deps = m_deps.get_deps(v); @@ -821,33 +819,34 @@ namespace datalog { item_set::iterator end = deps.end(); for(; it!=end; ++it) { T d = *it; - if(m_stack_content.is_marked(d)) { + if (m_visited.is_marked(d)) { //TODO: find the best vertex to remove in the cycle remove_from_stack(); - break; + continue; } traverse(d); } SASSERT(m_stack.back()==v); m_stack.pop_back(); - m_stack_content.mark(v, false); + m_visited.mark(v, false); } void remove_from_stack() { for (unsigned i = 0; i < m_stack.size(); ++i) { func_decl* p = m_stack[i]; - rule_vector const& rules = m_rules.get_predicate_rules(p); - unsigned stratum = m_rules.get_predicate_strat(p); if (m_context.has_facts(p)) { m_removed.insert(p); return; } + + rule_vector const& rules = m_rules.get_predicate_rules(p); + unsigned stratum = m_rules.get_predicate_strat(p); for (unsigned j = 0; j < rules.size(); ++j) { rule const& r = *rules[j]; bool ok = true; for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) { - ok &= m_rules.get_predicate_strat(r.get_decl(k)) < stratum; + ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum; } if (ok) { m_removed.insert(p); @@ -858,8 +857,8 @@ namespace datalog { // nothing was found. m_removed.insert(m_stack.back()); - } + public: cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed) : m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); } From 38823d6c79b121fca6e6392a2fb4e45ca74deea1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Apr 2013 08:16:02 -0700 Subject: [PATCH 2/4] [PDR] fix expansion of BV literals Signed-off-by: Nuno Lopes --- src/muz_qe/pdr_prop_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index daa52992f..863e5c03e 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -145,7 +145,8 @@ namespace pdr { rational two(2); for (unsigned j = 0; j < bv_size; ++j) { parameter p(j); - expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c); + //expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c); + expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c)); if ((r % two).is_zero()) { e = m.mk_not(e); } From adc8224dbae9ceffd87ef1b179caa1dcb118f777 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Apr 2013 09:02:40 -0700 Subject: [PATCH 3/4] use svector instead of vector where appropriate Signed-off-by: Nuno Lopes --- src/ast/ast.cpp | 2 +- src/util/bit_vector.cpp | 6 ++---- src/util/bit_vector.h | 2 +- src/util/mpff.h | 2 +- 4 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 8d643a348..fefb400ed 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2755,7 +2755,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro app const * cls = to_app(f1); unsigned num_args = cls->get_num_args(); #ifdef Z3DEBUG - vector found; + svector found; #endif for (unsigned i = 0; i < num_args; i++) { expr * lit = cls->get_arg(i); diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index e3a2bc331..0d67f1f79 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -208,8 +208,8 @@ void bit_vector::display(std::ostream & out) const { void fr_bit_vector::reset() { unsigned sz = size(); - vector::const_iterator it = m_one_idxs.begin(); - vector::const_iterator end = m_one_idxs.end(); + unsigned_vector::const_iterator it = m_one_idxs.begin(); + unsigned_vector::const_iterator end = m_one_idxs.end(); for (; it != end; ++it) { unsigned idx = *it; if (idx < sz) @@ -217,5 +217,3 @@ void fr_bit_vector::reset() { } m_one_idxs.reset(); } - - diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 1d6083717..2c641c5a6 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -204,7 +204,7 @@ inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) { This class should be used if the reset is frequently called. */ class fr_bit_vector : private bit_vector { - svector m_one_idxs; + unsigned_vector m_one_idxs; public: void reset(); diff --git a/src/util/mpff.h b/src/util/mpff.h index de71ec75e..8d4c853af 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -107,7 +107,7 @@ class mpff_manager { unsigned m_precision; //!< Number of words in the significand. Must be an even number. unsigned m_precision_bits; //!< Number of bits in the significand. Must be 32*m_precision. - vector m_significands; //!< Array containing all significands. + unsigned_vector m_significands; //!< Array containing all significands. unsigned m_capacity; //!< Number of significands that can be stored in m_significands. bool m_to_plus_inf; //!< If True, then round to plus infinity, otherwise to minus infinity id_gen m_id_gen; From 51d3db8105facdbdaf18be56ed3afee09bc1eda9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Apr 2013 10:48:57 -0700 Subject: [PATCH 4/4] [dl] remove 2 uneeded fields from sparse_table::rename_fn Signed-off-by: Nuno Lopes --- src/muz_qe/dl_sparse_table.cpp | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/muz_qe/dl_sparse_table.cpp b/src/muz_qe/dl_sparse_table.cpp index 47f518ee2..52d9618b8 100644 --- a/src/muz_qe/dl_sparse_table.cpp +++ b/src/muz_qe/dl_sparse_table.cpp @@ -1022,19 +1022,16 @@ namespace datalog { class sparse_table_plugin::rename_fn : public convenient_table_rename_fn { - const unsigned m_cycle_len; - const unsigned m_col_cnt; unsigned_vector m_out_of_cycle; public: rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) - : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle), - m_cycle_len(permutation_cycle_len), m_col_cnt(orig_sig.size()) { + : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) { SASSERT(permutation_cycle_len>=2); idx_set cycle_cols; - for (unsigned i=0; i