From 1f5097cdaa40fab3e788412e3ed402fdfe372834 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 15 Apr 2013 16:53:25 -0700 Subject: [PATCH 1/6] [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/6] [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/6] 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/6] [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 Date: Tue, 16 Apr 2013 13:54:41 -0700 Subject: [PATCH 5/6] cleanup front end parameters to datalog engine Signed-off-by: Nikolaj Bjorner --- src/shell/datalog_frontend.cpp | 19 +------------------ src/shell/datalog_frontend.h | 5 ----- src/shell/main.cpp | 2 +- 3 files changed, 2 insertions(+), 24 deletions(-) diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 6cdfe1623..efcab14ea 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -43,17 +43,7 @@ static datalog::context * g_ctx = 0; static datalog::rule_set * g_orig_rules; static datalog::instruction_block * g_code; static datalog::execution_context * g_ectx; -static smt_params * g_params; -datalog_params::datalog_params(): - m_default_table("sparse"), - m_default_table_checked(false) -{} - -// void datalog_params::register_params(ini_params& p) { -// p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)"); -// p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker"); -// } static void display_statistics( std::ostream& out, @@ -61,7 +51,6 @@ static void display_statistics( datalog::rule_set& orig_rules, datalog::instruction_block& code, datalog::execution_context& ex_ctx, - smt_params& params, bool verbose ) { @@ -109,7 +98,7 @@ static void display_statistics( static void display_statistics() { if (g_ctx) { - display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, *g_params, true); + display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, true); } } @@ -127,7 +116,6 @@ static void on_ctrl_c(int) { unsigned read_datalog(char const * file) { IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";); - datalog_params dl_params; smt_params s_params; ast_manager m; g_overall_time.start(); @@ -135,8 +123,6 @@ unsigned read_datalog(char const * file) { signal(SIGINT, on_ctrl_c); params_ref params; params.set_sym("engine", symbol("datalog")); - params.set_sym("default_table", dl_params.m_default_table); - params.set_bool("default_table_checked", dl_params.m_default_table_checked); datalog::context ctx(m, s_params, params); datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); @@ -186,7 +172,6 @@ unsigned read_datalog(char const * file) { g_orig_rules = &original_rules; g_code = &rules_code; g_ectx = &ex_ctx; - g_params = &s_params; try { g_piece_timer.reset(); @@ -254,7 +239,6 @@ unsigned read_datalog(char const * file) { original_rules, rules_code, ex_ctx, - s_params, false); } @@ -266,7 +250,6 @@ unsigned read_datalog(char const * file) { original_rules, rules_code, ex_ctx, - s_params, true); return ERR_MEMOUT; } diff --git a/src/shell/datalog_frontend.h b/src/shell/datalog_frontend.h index e53e35c89..8022d5046 100644 --- a/src/shell/datalog_frontend.h +++ b/src/shell/datalog_frontend.h @@ -19,11 +19,6 @@ Revision History: #ifndef _DATALOG_FRONTEND_H_ #define _DATALOG_FRONTEND_H_ -struct datalog_params { - symbol m_default_table; - bool m_default_table_checked; - datalog_params(); -}; unsigned read_datalog(char const * file); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 63e604719..e0fa4a1f2 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -27,8 +27,8 @@ Revision History: #include"z3_log_frontend.h" #include"warning.h" #include"version.h" -#include"datalog_frontend.h" #include"dimacs_frontend.h" +#include"datalog_frontend.h" #include"timeout.h" #include"z3_exception.h" #include"error_codes.h" From 0b0e5b69121b463a42781a22b43854ff48b9673b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Apr 2013 15:14:16 -0700 Subject: [PATCH 6/6] add some constness Signed-off-by: Nuno Lopes --- src/ast/dl_decl_plugin.cpp | 4 ++-- src/ast/dl_decl_plugin.h | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 1524760e5..d8e2385ec 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -660,9 +660,9 @@ namespace datalog { return 0; } - bool dl_decl_util::is_numeral(expr* e, uint64& v) const { + bool dl_decl_util::is_numeral(const expr* e, uint64& v) const { if (is_numeral(e)) { - app* c = to_app(e); + const app* c = to_app(e); SASSERT(c->get_decl()->get_num_parameters() == 2); parameter const& p = c->get_decl()->get_parameter(0); SASSERT(p.is_rational()); diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 559aff7bd..a662de578 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -169,11 +169,11 @@ namespace datalog { app* mk_le(expr* a, expr* b); - bool is_lt(expr* a) { return is_app_of(a, m_fid, OP_DL_LT); } + bool is_lt(const expr* a) const { return is_app_of(a, m_fid, OP_DL_LT); } - bool is_numeral(expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); } + bool is_numeral(const expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); } - bool is_numeral(expr* e, uint64& v) const; + bool is_numeral(const expr* e, uint64& v) const; // // Utilities for extracting constants