From 5f298b69659a9955b50e96100f541989e2ce58b8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 5 Apr 2013 18:02:41 -0700 Subject: [PATCH 1/8] spread some static love Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_similarity_compressor.cpp | 28 +++++++++++----------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index 9868c82f6..9855196c9 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -42,7 +42,7 @@ namespace datalog { /** Allows to traverse head and positive tails in a single for loop starting from -1 */ - app * get_by_tail_index(rule * r, int idx) { + static app * get_by_tail_index(rule * r, int idx) { if(idx==-1) { return r->get_head(); } @@ -51,11 +51,11 @@ namespace datalog { } template - int aux_compare(T a, T b) { + static int aux_compare(T a, T b) { return (a>b) ? 1 : ( (a==b) ? 0 : -1); } - int compare_var_args(app* t1, app* t2) { + static int compare_var_args(app* t1, app* t2) { SASSERT(t1->get_num_args()==t2->get_num_args()); int res; unsigned n = t1->get_num_args(); @@ -73,7 +73,7 @@ namespace datalog { return 0; } - int compare_args(app* t1, app* t2, int & skip_countdown) { + static int compare_args(app* t1, app* t2, int & skip_countdown) { SASSERT(t1->get_num_args()==t2->get_num_args()); int res; unsigned n = t1->get_num_args(); @@ -98,7 +98,7 @@ namespace datalog { Two rules are in the same rough similarity class if they differ only in constant arguments of positive uninterpreted predicates. */ - int rough_compare(rule * r1, rule * r2) { + static int rough_compare(rule * r1, rule * r2) { int res = aux_compare(r1->get_tail_size(), r2->get_tail_size()); if(res!=0) { return res; } res = aux_compare(r1->get_uninterpreted_tail_size(), r2->get_uninterpreted_tail_size()); @@ -129,7 +129,7 @@ namespace datalog { \c r1 and \c r2 must be equal according to the \c rough_compare function for this function to be called. */ - int total_compare(rule * r1, rule * r2, int skipped_arg_index = INT_MAX) { + static int total_compare(rule * r1, rule * r2, int skipped_arg_index = INT_MAX) { SASSERT(rough_compare(r1, r2)==0); int pos_tail_sz = r1->get_positive_tail_size(); for(int i=-1; i info_vector; - void collect_const_indexes(app * t, int tail_index, info_vector & res) { + static void collect_const_indexes(app * t, int tail_index, info_vector & res) { unsigned n = t->get_num_args(); for(unsigned i=0; iget_arg(i))) { @@ -175,7 +175,7 @@ namespace datalog { } } - void collect_const_indexes(rule * r, info_vector & res) { + static void collect_const_indexes(rule * r, info_vector & res) { collect_const_indexes(r->get_head(), -1, res); unsigned pos_tail_sz = r->get_positive_tail_size(); for(unsigned i=0; i - void collect_orphan_consts(rule * r, const info_vector & const_infos, T & tgt) { + static void collect_orphan_consts(rule * r, const info_vector & const_infos, T & tgt) { unsigned const_cnt = const_infos.size(); tgt.reset(); for(unsigned i=0; i - void collect_orphan_sorts(rule * r, const info_vector & const_infos, T & tgt) { + static void collect_orphan_sorts(rule * r, const info_vector & const_infos, T & tgt) { unsigned const_cnt = const_infos.size(); tgt.reset(); for(unsigned i=0; i1); unsigned const_cnt = const_infos.size(); @@ -252,7 +252,7 @@ namespace datalog { first constant that is equal to it in all the rules. If there is no such, it will contain its own index. */ - void detect_equal_constants(rule_vector::iterator first, rule_vector::iterator after_last, + static void detect_equal_constants(rule_vector::iterator first, rule_vector::iterator after_last, info_vector & const_infos) { SASSERT(first!=after_last); unsigned const_cnt = const_infos.size(); @@ -302,7 +302,7 @@ namespace datalog { } } - unsigned get_constant_count(rule * r) { + static unsigned get_constant_count(rule * r) { unsigned res = r->get_head()->get_num_args() - count_variable_arguments(r->get_head()); unsigned pos_tail_sz = r->get_positive_tail_size(); for(unsigned i=0; i0; } return total_compare(r1, r2)>0; From 1ef17cbe679884c434a95c2039959f2c0cd61034 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 5 Apr 2013 18:12:58 -0700 Subject: [PATCH 2/8] add dl_context::has_facts(pred) Signed-off-by: Nuno Lopes --- src/muz_qe/dl_context.cpp | 4 ++++ src/muz_qe/dl_context.h | 1 + src/muz_qe/rel_context.cpp | 5 +++++ src/muz_qe/rel_context.h | 7 ++++++- 4 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 852d8f847..7a1e3b8fc 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -780,6 +780,10 @@ namespace datalog { add_fact(head->get_decl(), fact); } + bool context::has_facts(func_decl * pred) const { + return m_rel && m_rel->has_facts(pred); + } + void context::add_table_fact(func_decl * pred, const table_fact & fact) { if (get_engine() == DATALOG_ENGINE) { ensure_rel(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index cb432d4e9..d23cf2c0c 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -249,6 +249,7 @@ namespace datalog { void add_fact(app * head); void add_fact(func_decl * pred, const relation_fact & fact); + bool has_facts(func_decl * pred) const; void add_rule(rule_ref& r); void add_rules(rule_ref_vector& rs); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 12045047b..58263b9d0 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -497,6 +497,11 @@ namespace datalog { } } + bool rel_context::has_facts(func_decl * pred) const { + relation_base* r = try_get_relation(pred); + return r && !r->empty(); + } + void rel_context::store_relation(func_decl * pred, relation_base * rel) { get_rmanager().store_relation(pred, rel); } diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 08ee868c0..d2f6973da 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -92,9 +92,14 @@ namespace datalog { */ bool result_contains_fact(relation_fact const& f); + /** \brief add facts to relation + */ void add_fact(func_decl* pred, relation_fact const& fact); - void add_fact(func_decl* pred, table_fact const& fact); + + /** \brief check if facts were added to relation + */ + bool has_facts(func_decl * pred) const; /** \brief Store the relation \c rel under the predicate \c pred. The \c context object From 03c1b24dea7a5eec1747968a829ae7e014aa4809 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Apr 2013 14:25:25 -0700 Subject: [PATCH 3/8] Fix get_int64 and is_int64 methods in mpz. Fix INT64_MAX constant definition. Signed-off-by: Leonardo de Moura --- src/util/mpz.cpp | 15 ++++----------- src/util/mpz.h | 24 ++++++++++++++++++++++++ src/util/util.h | 2 +- 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index c77978647..9473621cf 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1299,9 +1299,9 @@ bool mpz_manager::is_int64(mpz const & a) const { if (is_small(a)) return true; #ifndef _MP_GMP - if (!is_uint64(a)) + if (!is_abs_uint64(a)) return false; - uint64 num = get_uint64(a); + uint64 num = big_abs_to_uint64(a); uint64 msb = static_cast(1) << 63; uint64 msb_val = msb & num; if (a.m_val >= 0) { @@ -1327,14 +1327,7 @@ uint64 mpz_manager::get_uint64(mpz const & a) const { return static_cast(a.m_val); #ifndef _MP_GMP SASSERT(a.m_ptr->m_size > 0); - if (a.m_ptr->m_size == 1) - return digits(a)[0]; - if (sizeof(digit_t) == sizeof(uint64)) - // 64-bit machine - return digits(a)[0]; - else - // 32-bit machine - return ((static_cast(digits(a)[1]) << 32) | (static_cast(digits(a)[0]))); + return big_abs_to_uint64(a); #else // GMP version if (sizeof(uint64) == sizeof(unsigned long)) { @@ -1359,7 +1352,7 @@ int64 mpz_manager::get_int64(mpz const & a) const { return static_cast(a.m_val); #ifndef _MP_GMP SASSERT(is_int64(a)); - uint64 num = get_uint64(a); + uint64 num = big_abs_to_uint64(a); if (a.m_val < 0) { if (num != 0 && (num << 1) == 0) return INT64_MIN; diff --git a/src/util/mpz.h b/src/util/mpz.h index b5c301d82..7b40a89f5 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -211,6 +211,30 @@ class mpz_manager { static digit_t * digits(mpz const & c) { return c.m_ptr->m_digits; } + // Return true if the absolute value fits in a UINT64 + static bool is_abs_uint64(mpz const & a) { + if (is_small(a)) + return true; + if (sizeof(digit_t) == sizeof(uint64)) + return size(a) <= 1; + else + return size(a) <= 2; + } + + // CAST the absolute value into a UINT64 + static uint64 big_abs_to_uint64(mpz const & a) { + SASSERT(is_abs_uint64(a)); + SASSERT(!is_small(a)); + if (a.m_ptr->m_size == 1) + return digits(a)[0]; + if (sizeof(digit_t) == sizeof(uint64)) + // 64-bit machine + return digits(a)[0]; + else + // 32-bit machine + return ((static_cast(digits(a)[1]) << 32) | (static_cast(digits(a)[0]))); + } + template void get_sign_cell(mpz const & a, int & sign, mpz_cell * & cell) { if (is_small(a)) { diff --git a/src/util/util.h b/src/util/util.h index 8bcbce4a3..0aa8f881d 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -45,7 +45,7 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8); #define INT64_MIN static_cast(0x8000000000000000ull) #endif #ifndef INT64_MAX -#define INT64_MAX static_cast(0x0fffffffffffffffull) +#define INT64_MAX static_cast(0x7fffffffffffffffull) #endif #ifndef UINT64_MAX #define UINT64_MAX 0xffffffffffffffffull From 3d34aa7f010cab7dceacd756ddbf7dbd8c74687a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Apr 2013 14:50:17 -0700 Subject: [PATCH 4/8] Fix is_int64 bug in mpz when compiling with GMP Signed-off-by: Leonardo de Moura --- src/test/rational.cpp | 2 +- src/util/mpz.cpp | 5 ++++- src/util/mpz.h | 1 + 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/test/rational.cpp b/src/test/rational.cpp index 9cbcdb00e..834aab92f 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -171,7 +171,7 @@ static void tst2() { rational int64_max("9223372036854775807"); - rational int64_min(-int64_max - rational(1)); + rational int64_min((-int64_max) - rational(1)); // is_int64 SASSERT(int64_max.is_int64()); SASSERT(int64_min.is_int64()); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 9473621cf..a7c904c64 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -128,6 +128,8 @@ mpz_manager::mpz_manager(): mpz_mul(m_int64_max, m_tmp, m_int64_max); mpz_set_ui(m_tmp, max_l); mpz_add(m_int64_max, m_tmp, m_int64_max); + mpz_neg(m_int64_min, m_int64_max); + mpz_sub_ui(m_int64_min, m_int64_min, 1); #endif mpz one(1); @@ -152,6 +154,7 @@ mpz_manager::~mpz_manager() { deallocate(m_arg[1]); mpz_clear(m_uint64_max); mpz_clear(m_int64_max); + mpz_clear(m_int64_min); #endif if (SYNCH) omp_destroy_nest_lock(&m_lock); @@ -1317,7 +1320,7 @@ bool mpz_manager::is_int64(mpz const & a) const { } #else // GMP version - return mpz_cmp(*a.m_ptr, m_int64_max) <= 0; + return mpz_cmp(m_int64_min, *a.m_ptr) <= 0 && mpz_cmp(*a.m_ptr, m_int64_max) <= 0; #endif } diff --git a/src/util/mpz.h b/src/util/mpz.h index 7b40a89f5..923d5b3a7 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -168,6 +168,7 @@ class mpz_manager { mpz_t * m_arg[2]; mpz_t m_uint64_max; mpz_t m_int64_max; + mpz_t m_int64_min; mpz_t * allocate() { mpz_t * cell = reinterpret_cast(m_allocator.allocate(sizeof(mpz_t))); From 75ad174567627e7da15fa365e8a564f1ee96122c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Apr 2013 15:02:51 -0700 Subject: [PATCH 5/8] Initialize int64_min constant when using GMP Signed-off-by: Leonardo de Moura --- src/util/mpz.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index a7c904c64..bd7f30a76 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -120,6 +120,7 @@ mpz_manager::mpz_manager(): mpz_set_ui(m_tmp, max_l); mpz_add(m_uint64_max, m_uint64_max, m_tmp); mpz_init(m_int64_max); + mpz_init(m_int64_min); max_l = static_cast(INT64_MAX % static_cast(UINT_MAX)); max_h = static_cast(INT64_MAX / static_cast(UINT_MAX)); From 90c808bde91fc010b699003076345327017f074b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 8 Apr 2013 17:14:43 -0700 Subject: [PATCH 6/8] [datalog] fix memory leak in union instructions the source operand was never cleaned up Signed-off-by: Nuno Lopes --- src/muz_qe/dl_compiler.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index c898f7964..acedc3619 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -707,6 +707,7 @@ namespace datalog { //update the head relation make_union(new_head_reg, head_reg, delta_reg, use_widening, acc); + make_dealloc_non_void(new_head_reg, acc); } finish: From 93297fa9e72f750fc8115f0568217f474888563e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Apr 2013 18:00:43 -0700 Subject: [PATCH 7/8] Fix bug in purify_arith reported at https://z3.codeplex.com/workitem/32 Signed-off-by: Leonardo de Moura --- src/tactic/arith/purify_arith_tactic.cpp | 61 +++++++++++------------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 169e27927..1a38ac10e 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -29,6 +29,7 @@ Revision History: #include"th_rewriter.h" #include"filter_model_converter.h" #include"ast_smt2_pp.h" +#include"expr_replacer.h" /* ---- @@ -131,18 +132,16 @@ struct purify_arith_proc { proof_ref_vector m_new_cnstr_prs; expr_ref m_subst; proof_ref m_subst_pr; - bool m_in_q; - unsigned m_var_idx; + expr_ref_vector m_new_vars; - rw_cfg(purify_arith_proc & o, bool in_q): + rw_cfg(purify_arith_proc & o): m_owner(o), m_pinned(o.m()), m_new_cnstrs(o.m()), m_new_cnstr_prs(o.m()), m_subst(o.m()), m_subst_pr(o.m()), - m_in_q(in_q), - m_var_idx(0) { + m_new_vars(o.m()) { } ast_manager & m() { return m_owner.m(); } @@ -155,14 +154,9 @@ struct purify_arith_proc { bool elim_inverses() const { return m_owner.m_elim_inverses; } expr * mk_fresh_var(bool is_int) { - if (m_in_q) { - unsigned idx = m_var_idx; - m_var_idx++; - return m().mk_var(idx, is_int ? u().mk_int() : u().mk_real()); - } - else { - return m().mk_fresh_const(0, is_int ? u().mk_int() : u().mk_real()); - } + expr * r = m().mk_fresh_const(0, is_int ? u().mk_int() : u().mk_real()); + m_new_vars.push_back(r); + return r; } expr * mk_fresh_real_var() { return mk_fresh_var(false); } @@ -596,9 +590,9 @@ struct purify_arith_proc { struct rw : public rewriter_tpl { rw_cfg m_cfg; - rw(purify_arith_proc & o, bool in_q): + rw(purify_arith_proc & o): rewriter_tpl(o.m(), o.m_produce_proofs, m_cfg), - m_cfg(o, in_q) { + m_cfg(o) { } }; @@ -661,40 +655,43 @@ struct purify_arith_proc { void process_quantifier(quantifier * q, expr_ref & result, proof_ref & result_pr) { result_pr = 0; - num_vars_proc p(u(), m_elim_root_objs); - expr_ref body(m()); - unsigned num_vars = p(q->get_expr()); - if (num_vars > 0) { - // open space for aux vars - var_shifter shifter(m()); - shifter(q->get_expr(), num_vars, body); - } - else { - body = q->get_expr(); - } - - rw r(*this, true); + rw r(*this); expr_ref new_body(m()); proof_ref new_body_pr(m()); - r(body, new_body, new_body_pr); + r(q->get_expr(), new_body, new_body_pr); + unsigned num_vars = r.cfg().m_new_vars.size(); TRACE("purify_arith", tout << "num_vars: " << num_vars << "\n"; - tout << "body: " << mk_ismt2_pp(body, m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";); + tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";); if (num_vars == 0) { + SASSERT(r.cfg().m_new_cnstrs.empty()); result = m().update_quantifier(q, new_body); if (m_produce_proofs) result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr); } else { + // Add new constraints expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs; cnstrs.push_back(new_body); new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr()); + // Open space for new variables + var_shifter shifter(m()); + shifter(new_body, num_vars, new_body); + // Rename fresh constants in r.cfg().m_new_vars to variables ptr_buffer sorts; buffer names; + expr_substitution subst(m(), false, false); for (unsigned i = 0; i < num_vars; i++) { - sorts.push_back(u().mk_real()); + expr * c = r.cfg().m_new_vars.get(i); + sort * s = get_sort(c); + sorts.push_back(s); names.push_back(m().mk_fresh_var_name("x")); + unsigned idx = num_vars - i - 1; + subst.insert(c, m().mk_var(idx, s)); } + scoped_ptr replacer = mk_default_expr_replacer(m()); + replacer->set_substitution(&subst); + (*replacer)(new_body, new_body); new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body); result = m().update_quantifier(q, new_body); if (m_produce_proofs) { @@ -708,7 +705,7 @@ struct purify_arith_proc { } void operator()(goal & g, model_converter_ref & mc, bool produce_models) { - rw r(*this, false); + rw r(*this); // purify expr_ref new_curr(m()); proof_ref new_pr(m()); From 8627f6f1d5e5afc23335c29ad150ef375d07cb16 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Apr 2013 18:02:28 -0700 Subject: [PATCH 8/8] Remove dead code Signed-off-by: Leonardo de Moura --- src/tactic/arith/purify_arith_tactic.cpp | 57 ------------------------ 1 file changed, 57 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 1a38ac10e..f2ddd86ce 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -595,63 +595,6 @@ struct purify_arith_proc { m_cfg(o) { } }; - - /** - \brief Return the number of (auxiliary) variables needed for converting an expression. - */ - struct num_vars_proc { - arith_util & m_util; - expr_fast_mark1 m_visited; - ptr_vector m_todo; - unsigned m_num_vars; - bool m_elim_root_objs; - - num_vars_proc(arith_util & u, bool elim_root_objs): - m_util(u), - m_elim_root_objs(elim_root_objs) { - } - - void visit(expr * t) { - if (m_visited.is_marked(t)) - return; - m_visited.mark(t); - m_todo.push_back(t); - } - - void process(app * t) { - if (t->get_family_id() == m_util.get_family_id()) { - if (m_util.is_power(t)) { - rational k; - if (m_util.is_numeral(t->get_arg(1), k) && (k.is_zero() || !k.is_int())) { - m_num_vars++; - } - } - else if (m_util.is_div(t) || - m_util.is_idiv(t) || - m_util.is_mod(t) || - m_util.is_to_int(t) || - (m_util.is_irrational_algebraic_numeral(t) && m_elim_root_objs)) { - m_num_vars++; - } - } - unsigned num_args = t->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - visit(t->get_arg(i)); - } - - unsigned operator()(expr * t) { - m_num_vars = 0; - visit(t); - while (!m_todo.empty()) { - expr * t = m_todo.back(); - m_todo.pop_back(); - if (is_app(t)) - process(to_app(t)); - } - m_visited.reset(); - return m_num_vars; - } - }; void process_quantifier(quantifier * q, expr_ref & result, proof_ref & result_pr) { result_pr = 0;