From 8e5581b4fea2ec9b41355b23369f7401b04cf61d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Feb 2013 08:19:33 -0800 Subject: [PATCH 01/10] Retract changes in the commit 39a614559cae. The fix was affecting benchmarks using the array theory map construct. Signed-off-by: Leonardo de Moura --- src/ast/arith_decl_plugin.cpp | 14 -------------- src/ast/ast.cpp | 14 -------------- src/ast/bv_decl_plugin.cpp | 14 -------------- 3 files changed, 42 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 5e346fc0d..9d1f4343f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -492,13 +492,6 @@ static bool is_const_op(decl_kind k) { func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); if (arity == 0 && !is_const_op(k)) { @@ -516,13 +509,6 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); if (num_args == 0 && !is_const_op(k)) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1ba468399..63a450094 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1010,13 +1010,6 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) { func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, BOOL_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } switch (static_cast(k)) { case OP_TRUE: return m_true_decl; case OP_FALSE: return m_false_decl; @@ -1052,13 +1045,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, BOOL_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } switch (static_cast(k)) { case OP_TRUE: return m_true_decl; case OP_FALSE: return m_false_decl; diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 823d9eaed..0ef3b60d6 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -461,13 +461,6 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) { func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, BV_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in. @@ -566,13 +559,6 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { - if (range != 0) { - if (is_sort_of(range, m_family_id, BV_SORT)) - m_manager->raise_exception("unneeded disambiguation"); - else - m_manager->raise_exception("incorrect disambiguation"); - return 0; - } int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in. From 6022d14b0241ed85f8245a5730c08ba28b5a898e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Feb 2013 15:03:45 -0800 Subject: [PATCH 02/10] remove incorrect code for double loop with widening Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_compiler.cpp | 68 +++++++------------------------------- 1 file changed, 12 insertions(+), 56 deletions(-) diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index d403b5b5c..44a449779 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -87,12 +87,12 @@ namespace datalog { acc.push_back(instruction::mk_clone(src, result)); } - void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widening, + void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool use_widening, instruction_block & acc) { SASSERT(m_reg_signatures[src]==m_reg_signatures[tgt]); SASSERT(delta==execution_context::void_register || m_reg_signatures[src]==m_reg_signatures[delta]); - if(widening) { + if (use_widening) { acc.push_back(instruction::mk_widen(src, tgt, delta)); } else { @@ -129,8 +129,7 @@ namespace datalog { func_decl_set::iterator pend = preds.end(); for(; pit!=pend; ++pit) { func_decl * pred = *pit; - reg_idx reg; - TRUSTME( m_pred_regs.find(pred, reg) ); + reg_idx reg = m_pred_regs.find(pred); SASSERT(!regs.contains(pred)); relation_signature sig = m_reg_signatures[reg]; @@ -576,8 +575,7 @@ namespace datalog { } SASSERT(t_cols.size()==neg_cols.size()); - reg_idx neg_reg; - TRUSTME( m_pred_regs.find(neg_pred, neg_reg) ); + reg_idx neg_reg = m_pred_regs.find(neg_pred); acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), t_cols.c_ptr(), neg_cols.c_ptr())); } @@ -762,15 +760,13 @@ namespace datalog { typedef svector tail_delta_infos; unsigned rule_len = r->get_uninterpreted_tail_size(); - reg_idx head_reg; - TRUSTME( m_pred_regs.find(r->get_head()->get_decl(), head_reg) ); + reg_idx head_reg = m_pred_regs.find(r->get_head()->get_decl()); svector tail_regs; tail_delta_infos tail_deltas; for(unsigned j=0;jget_tail(j)->get_decl(); - reg_idx tail_reg; - TRUSTME( m_pred_regs.find(tail_pred, tail_reg) ); + reg_idx tail_reg = m_pred_regs.find(tail_pred); tail_regs.push_back(tail_reg); if(input_deltas && !all_or_nothing_deltas()) { @@ -858,7 +854,7 @@ namespace datalog { rule_dependencies deps(m_rule_set.get_dependencies()); deps.restrict(preds); cycle_breaker(deps, global_deltas)(); - TRUSTME( deps.sort_deps(ordered_preds) ); + VERIFY( deps.sort_deps(ordered_preds) ); //the predicates that were removed to get acyclic induced subgraph are put last //so that all their local input deltas are already populated @@ -903,8 +899,7 @@ namespace datalog { for(; gdit!=gend; ++gdit) { func_decl * pred = gdit->m_key; reg_idx head_reg = gdit->m_value; - reg_idx tail_reg; - TRUSTME( global_tail_deltas.find(pred, tail_reg) ); + reg_idx tail_reg = global_tail_deltas.find(pred); acc.push_back(instruction::mk_move(head_reg, tail_reg)); } //empty local deltas @@ -939,7 +934,7 @@ namespace datalog { loop_body->set_observer(0); acc.push_back(instruction::mk_while_loop(loop_control_regs.size(), - loop_control_regs.c_ptr(),loop_body)); + loop_control_regs.c_ptr(), loop_body)); } void compiler::compile_dependent_rules(const func_decl_set & head_preds, @@ -985,50 +980,11 @@ namespace datalog { //generate code for the initial run compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc); - if(!compile_with_widening()) { - compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, - d_local, acc); + if (compile_with_widening()) { + compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc); } else { - //do the part where we zero the global predicates and run the loop saturation loop again - if(global_deltas.size() Date: Tue, 5 Feb 2013 21:19:32 -0800 Subject: [PATCH 03/10] tidy verbose mode a bit, ackermannize special cases of arrays Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_array_blast.cpp | 100 +++++++++++++++++++++++++++++-- src/muz_qe/dl_mk_array_blast.h | 4 ++ src/muz_qe/pdr_context.cpp | 33 ++++++---- 3 files changed, 119 insertions(+), 18 deletions(-) diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index 880f196a2..b22fdf7ef 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -49,6 +49,94 @@ namespace datalog { } return false; } + + bool mk_array_blast::ackermanize(expr_ref& body, expr_ref& head) { + expr_ref_vector conjs(m); + flatten_and(body, conjs); + defs_t defs; + expr_safe_replace sub(m); + ptr_vector todo; + todo.push_back(head); + for (unsigned i = 0; i < conjs.size(); ++i) { + expr* e = conjs[i].get(); + expr* x, *y; + if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) { + if (a.is_select(y)) { + std::swap(x,y); + } + if (a.is_select(x) && is_var(y)) { + // + // For the Ackermann reduction we would like the arrays + // to be variables, so that variables can be + // assumed to represent difference (alias) + // classes. + // + if (!is_var(to_app(x)->get_arg(0))) { + return false; + } + sub.insert(x, y); + defs.insert(to_app(x), to_var(y)); + } + } + todo.push_back(e); + } + // now check that all occurrences of select have been covered. + ast_mark mark; + while (!todo.empty()) { + expr* e = todo.back(); + todo.pop_back(); + if (mark.is_marked(e)) { + continue; + } + mark.mark(e, true); + if (is_var(e)) { + continue; + } + if (!is_app(e)) { + return false; + } + app* ap = to_app(e); + if (a.is_select(e) && !defs.contains(ap)) { + return false; + } + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + todo.push_back(ap->get_arg(i)); + } + } + sub(body); + sub(head); + conjs.reset(); + + // perform the Ackermann reduction by creating implications + // i1 = i2 => val1 = val2 for each equality pair: + // (= val1 (select a_i i1)) + // (= val2 (select a_i i2)) + defs_t::iterator it1 = defs.begin(), end = defs.end(); + for (; it1 != end; ++it1) { + app* a1 = it1->m_key; + var* v1 = it1->m_value; + defs_t::iterator it2 = it1; + ++it2; + for (; it2 != end; ++it2) { + app* a2 = it2->m_key; + var* v2 = it2->m_value; + if (a1->get_arg(0) != a2->get_arg(0)) { + continue; + } + expr_ref_vector eqs(m); + for (unsigned j = 1; j < a1->get_num_args(); ++j) { + eqs.push_back(m.mk_eq(a1->get_arg(j), a2->get_arg(j))); + } + conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2))); + } + } + if (!conjs.empty()) { + conjs.push_back(body); + body = m.mk_and(conjs.size(), conjs.c_ptr()); + } + m_rewriter(body); + return true; + } bool mk_array_blast::blast(rule& r, rule_set& rules) { unsigned utsz = r.get_uninterpreted_tail_size(); @@ -92,10 +180,6 @@ namespace datalog { new_conjs.push_back(tmp); } } - if (!inserted && !change) { - rules.add_rule(&r); - return false; - } rule_ref_vector new_rules(rm); expr_ref fml1(m), fml2(m), body(m), head(m); @@ -106,11 +190,17 @@ namespace datalog { m_rewriter(body); sub(head); m_rewriter(head); + change = ackermanize(body, head) || change; + if (!inserted && !change) { + rules.add_rule(&r); + return false; + } + fml2 = m.mk_implies(body, head); rm.mk_rule(fml2, new_rules, r.name()); SASSERT(new_rules.size() == 1); - TRACE("dl", tout << "new body " << mk_pp(fml2, m) << "\n";); + TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n");); rules.add_rule(new_rules[0].get()); if (m_pc) { diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h index 858b9c778..1618e4fa8 100644 --- a/src/muz_qe/dl_mk_array_blast.h +++ b/src/muz_qe/dl_mk_array_blast.h @@ -39,10 +39,14 @@ namespace datalog { th_rewriter m_rewriter; equiv_proof_converter* m_pc; + typedef obj_map defs_t; + bool blast(rule& r, rule_set& new_rules); bool is_store_def(expr* e, expr*& x, expr*& y); + bool ackermanize(expr_ref& body, expr_ref& head); + public: /** \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 574d44fb5..47655ac7b 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -52,6 +52,20 @@ namespace pdr { static bool is_infty_level(unsigned lvl) { return lvl == infty_level; } static unsigned next_level(unsigned lvl) { return is_infty_level(lvl)?lvl:(lvl+1); } + + struct pp_level { + unsigned m_level; + pp_level(unsigned l): m_level(l) {} + }; + + static std::ostream& operator<<(std::ostream& out, pp_level const& p) { + if (is_infty_level(p.m_level)) { + return out << "oo"; + } + else { + return out << p.m_level; + } + } // ---------------- // pred_tansformer @@ -263,7 +277,7 @@ namespace pdr { else if (is_invariant(tgt_level, curr, false, assumes_level)) { add_property(curr, assumes_level?tgt_level:infty_level); - TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";); + TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";); src[i] = src.back(); src.pop_back(); ++m_stats.m_num_propagations; @@ -273,14 +287,7 @@ namespace pdr { ++i; } } - IF_VERBOSE(2, verbose_stream() << "propagate: "; - if (is_infty_level(src_level)) { - verbose_stream() << "infty"; - } - else { - verbose_stream() << src_level; - } - verbose_stream() << "\n"; + IF_VERBOSE(3, verbose_stream() << "propagate: " << pp_level(src_level) << "\n"; for (unsigned i = 0; i < src.size(); ++i) { verbose_stream() << mk_pp(src[i].get(), m) << "\n"; }); @@ -304,14 +311,14 @@ namespace pdr { ensure_level(lvl); unsigned old_level; if (!m_prop2level.find(lemma, old_level) || old_level < lvl) { - TRACE("pdr", tout << "property1: " << lvl << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); + TRACE("pdr", tout << "property1: " << pp_level(lvl) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); m_levels[lvl].push_back(lemma); m_prop2level.insert(lemma, lvl); m_solver.add_level_formula(lemma, lvl); return true; } else { - TRACE("pdr", tout << "old-level: " << old_level << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); + TRACE("pdr", tout << "old-level: " << pp_level(old_level) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); return false; } } @@ -337,7 +344,7 @@ namespace pdr { for (unsigned i = 0; i < lemmas.size(); ++i) { expr* lemma_i = lemmas[i].get(); if (add_property1(lemma_i, lvl)) { - IF_VERBOSE(2, verbose_stream() << lvl << " " << mk_pp(lemma_i, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << pp_level(lvl) << " " << mk_pp(lemma_i, m) << "\n";); for (unsigned j = 0; j < m_use.size(); ++j) { m_use[j]->add_child_property(*this, lemma_i, next_level(lvl)); } @@ -1914,7 +1921,7 @@ namespace pdr { model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1); ++m_stats.m_num_nodes; m_search.add_leaf(*child); - IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";); + IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";); m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth()); } check_pre_closed(n); From 786f8029f18263d7e81e2b4615b8b13241f1e047 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Feb 2013 09:26:10 -0800 Subject: [PATCH 04/10] Add missing DLLs for Java in Windows binary distribution package Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 98d9ad6f8..b5ec691cb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1084,6 +1084,10 @@ class JavaDLLComponent(Component): mk_dir(os.path.join(dist_path, 'bin')) shutil.copy('%s.jar' % os.path.join(build_path, self.package_name), '%s.jar' % os.path.join(dist_path, 'bin', self.package_name)) + shutil.copy(os.path.join(build_path, 'libz3java.dll'), + os.path.join(dist_path, 'bin', 'libz3java.dll')) + shutil.copy(os.path.join(build_path, 'libz3java.lib'), + os.path.join(dist_path, 'bin', 'libz3java.lib')) class ExampleComponent(Component): def __init__(self, name, path): From 0fd1c00053aaf67bb622bfa8e4794eceab65bbba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Feb 2013 09:40:16 -0800 Subject: [PATCH 05/10] fix reference counting bug in qe Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe_arith_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp index 4e158229b..1baee51fa 100644 --- a/src/muz_qe/qe_arith_plugin.cpp +++ b/src/muz_qe/qe_arith_plugin.cpp @@ -524,7 +524,8 @@ namespace qe { expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m); // a*s + b*t + (a-1)(b-1) <= 0 - mk_le(m_arith.mk_add(as_bt, slack), result1); + tmp2 = m_arith.mk_add(as_bt, slack); + mk_le(tmp2, result1); rational a1 = a, b1 = b; if (abs_a < abs_b) { From 2e2fa84d40d252441cb4c8b5c1ed0d4c8779f2c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Feb 2013 19:21:52 -0800 Subject: [PATCH 06/10] experiment with arithmetic core generalizers Signed-off-by: Nikolaj Bjorner --- src/muz_qe/fixedpoint_params.pyg | 1 + src/muz_qe/pdr_context.cpp | 4 + src/muz_qe/pdr_generalizers.cpp | 159 ++++++++++++++++++++++++- src/muz_qe/pdr_generalizers.h | 31 +++++ src/muz_qe/pdr_smt_context_manager.cpp | 2 +- 5 files changed, 195 insertions(+), 2 deletions(-) diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index 25e513b78..c2cfadd14 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -44,6 +44,7 @@ def_module_params('fixedpoint', ('coalesce_rules', BOOL, False, "BMC: coalesce rules"), ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), + ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"), ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"), ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when " "checking for reachability (not only during cube weakening)"), diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 47655ac7b..73bffd4e4 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1477,6 +1477,10 @@ namespace pdr { if (m_params.inductive_reachability_check()) { m_core_generalizers.push_back(alloc(core_induction_generalizer, *this)); } + if (m_params.use_arith_inductive_generalizer()) { + m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this)); + } + } void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector& rs) const { diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 5a6ab4240..a02a1cb6e 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -28,7 +28,9 @@ Revision History: namespace pdr { - // + // ------------------------ + // core_bool_inductive_generalizer + // main propositional induction generalizer. // drop literals one by one from the core and check if the core is still inductive. // @@ -97,6 +99,9 @@ namespace pdr { } } + // ------------------------ + // core_farkas_generalizer + // // for each disjunct of core: // weaken predecessor. @@ -142,6 +147,158 @@ namespace pdr { } + // ----------------------------- + // core_arith_inductive_generalizer + + core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx): + core_generalizer(ctx), + m(ctx.get_manager()), + a(m), + m_refs(m) {} + + void core_arith_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { + if (core.size() <= 1) { + return; + } + reset(); + expr_ref e(m), t1(m), t2(m), t3(m); + rational r; + + TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; }); + + svector eqs; + get_eqs(core, eqs); + + for (unsigned eq = 0; eq < eqs.size(); ++eq) { + rational r = eqs[eq].m_value; + expr* x = eqs[eq].m_term; + unsigned k = eqs[eq].m_i; + unsigned l = eqs[eq].m_j; + + expr_ref_vector new_core(m); + for (unsigned i = 0; i < core.size(); ++i) { + if (i == k || k == l) { + new_core.push_back(m.mk_true()); + } + else { + if (!substitute_alias(r, x, core[i].get(), e)) { + e = core[i].get(); + } + new_core.push_back(e); + } + } + if (abs(r) >= rational(2) && a.is_int(x)) { + new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true)); + new_core[l] = a.mk_ge(x, a.mk_numeral(r, true)); + } + + bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); + + IF_VERBOSE(1, + verbose_stream() << (inductive?"":"non") << "inductive\n"; + for (unsigned j = 0; j < new_core.size(); ++j) { + verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; + }); + + if (inductive) { + core.reset(); + core.append(new_core); + } + } + } + + void core_arith_inductive_generalizer::insert_bound(bool is_lower, expr* x, rational const& r, unsigned i) { + if (r.is_neg()) { + expr_ref e(m); + e = a.mk_uminus(x); + m_refs.push_back(e); + x = e; + is_lower = !is_lower; + } + + if (is_lower) { + m_lb.insert(abs(r), std::make_pair(x, i)); + } + else { + m_ub.insert(abs(r), std::make_pair(x, i)); + } + } + + void core_arith_inductive_generalizer::reset() { + m_refs.reset(); + m_lb.reset(); + m_ub.reset(); + } + + void core_arith_inductive_generalizer::get_eqs(expr_ref_vector const& core, svector& eqs) { + expr* e1, *x, *y; + expr_ref e(m); + rational r; + + for (unsigned i = 0; i < core.size(); ++i) { + e = core[i]; + if (m.is_not(e, e1) && a.is_le(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { + // not (<= x r) <=> x >= r + 1 + insert_bound(true, x, r + rational(1), i); + } + else if (m.is_not(e, e1) && a.is_ge(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { + // not (>= x r) <=> x <= r - 1 + insert_bound(false, x, r - rational(1), i); + } + else if (a.is_le(e, x, y) && a.is_numeral(y, r)) { + insert_bound(false, x, r, i); + } + else if (a.is_ge(e, x, y) && a.is_numeral(y, r)) { + insert_bound(true, x, r, i); + } + } + bounds_t::iterator it = m_lb.begin(), end = m_lb.end(); + for (; it != end; ++it) { + rational r = it->m_key; + vector & terms1 = it->m_value; + vector terms2; + if (r >= rational(2) && m_ub.find(r, terms2)) { + bool done = false; + for (unsigned i = 0; !done && i < terms1.size(); ++i) { + for (unsigned j = 0; !done && j < terms2.size(); ++j) { + expr* t1 = terms1[i].first; + expr* t2 = terms2[j].first; + if (t1 == t2) { + eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); + done = true; + } + else { + e = m.mk_eq(t1, t2); + th_rewriter rw(m); + rw(e); + if (m.is_true(e)) { + eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); + done = true; + } + } + } + } + } + } + } + + bool core_arith_inductive_generalizer::substitute_alias(rational const& r, expr* x, expr* e, expr_ref& result) { + rational r2; + expr* y, *z, *e1; + if (m.is_not(e, e1) && substitute_alias(r, x, e1, result)) { + result = m.mk_not(result); + return true; + } + if (a.is_le(e, y, z) && a.is_numeral(z, r2) && r == r2) { + result = a.mk_le(y, x); + return true; + } + if (a.is_ge(e, y, z) && a.is_numeral(z, r2) && r == r2) { + result = a.mk_ge(y, x); + return true; + } + return false; + } // diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 5f3393682..03bd89c4d 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -33,6 +33,37 @@ namespace pdr { virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); }; + template + class r_map : public map { + }; + + class core_arith_inductive_generalizer : public core_generalizer { + typedef std::pair term_loc_t; + typedef r_map > bounds_t; + + ast_manager& m; + arith_util a; + expr_ref_vector m_refs; + bounds_t m_lb; + bounds_t m_ub; + + struct eq { + expr* m_term; + rational m_value; + unsigned m_i; + unsigned m_j; + eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {} + }; + void reset(); + void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i); + void get_eqs(expr_ref_vector const& core, svector& eqs); + bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result); + public: + core_arith_inductive_generalizer(context& ctx); + virtual ~core_arith_inductive_generalizer() {} + virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); + }; + class core_farkas_generalizer : public core_generalizer { farkas_learner m_farkas_learner; public: diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index 42d4b4c20..49ae35423 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -88,7 +88,6 @@ namespace pdr { for (unsigned i = 0; i < assumptions.size(); ++i) { pp.add_assumption(assumptions[i].get()); } - pp.display_smt2(tout, m.mk_true()); static unsigned lemma_id = 0; std::ostringstream strm; @@ -97,6 +96,7 @@ namespace pdr { pp.display_smt2(out, m.mk_true()); out.close(); lemma_id++; + tout << "pdr_check: " << strm.str() << "\n"; }); lbool result = m_context.check(assumptions.size(), assumptions.c_ptr()); if (!m.is_true(m_pred)) { From 91402f2060d8c88ccbc724881a996fc0a72c659e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Feb 2013 18:54:44 +0000 Subject: [PATCH 07/10] C API: fixed mk_context/mk_context_rc exception behaviour Adjusted .NET/Java APIs accordingly. Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 4 ++-- scripts/update_api.py | 35 +++++++++++++++++++++------------- src/api/api_context.cpp | 4 ++++ src/api/api_util.h | 1 + src/api/java/Context.java | 8 ++++---- 5 files changed, 33 insertions(+), 19 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index a26c21d65..c2743ece8 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2155,7 +2155,7 @@ class JavaExample // But you cannot mix numerals of different sorts // even if the size of their domains are the same: // System.out.println(ctx.mkEq(s1, t1)); - } + } public static void main(String[] args) { @@ -2226,7 +2226,7 @@ class JavaExample Context ctx = new Context(cfg); p.quantifierExample3(ctx); p.quantifierExample4(ctx); - } + } Log.close(); if (Log.isOpen()) diff --git a/scripts/update_api.py b/scripts/update_api.py index 08dd012e3..fa6111482 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -395,8 +395,7 @@ def mk_dotnet(): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public unsafe class LIB\n') dotnet.write(' {\n') - dotnet.write(' ' - ' const string Z3_DLL_NAME = \"libz3.dll\";\n' + dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' ' \n'); dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') @@ -420,7 +419,8 @@ def mk_dotnet(): dotnet.write(' }\n') -DotnetUnwrapped = [ 'Z3_del_context' ] +NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] +Unwrapped = [ 'Z3_del_context' ] def mk_dotnet_wrappers(): global Type2Str @@ -469,11 +469,15 @@ def mk_dotnet_wrappers(): dotnet.write('a%d' % i) i = i + 1 dotnet.write(');\n'); - if name not in DotnetUnwrapped: - if len(params) > 0 and param_type(params[0]) == CONTEXT: - dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") - dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") - dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") + if name not in Unwrapped: + if name in NULLWrapped: + dotnet.write(" if (r == IntPtr.Zero)\n") + dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") + dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") + dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") if result == STRING: dotnet.write(" return Marshal.PtrToStringAnsi(r);\n") elif result != VOID: @@ -550,7 +554,7 @@ def mk_java(): java_native.write('%s a%d' % (param2java(param), i)) i = i + 1 java_native.write(')') - if len(params) > 0 and param_type(params[0]) == CONTEXT: + if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped: java_native.write(' throws Z3Exception') java_native.write('\n') java_native.write(' {\n') @@ -568,10 +572,15 @@ def mk_java(): java_native.write('a%d' % i) i = i + 1 java_native.write(');\n') - if len(params) > 0 and param_type(params[0]) == CONTEXT: - java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') - java_native.write(' if (err != Z3_error_code.Z3_OK)\n') - java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + if name not in Unwrapped: + if name in NULLWrapped: + java_native.write(" if (res == 0)\n") + java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') if result != VOID: java_native.write(' return res;\n') java_native.write(' }\n\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6106cb6c7..cf179332a 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -419,17 +419,21 @@ namespace api { extern "C" { Z3_context Z3_API Z3_mk_context(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context_rc(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } void Z3_API Z3_del_context(Z3_context c) { diff --git a/src/api/api_util.h b/src/api/api_util.h index c81384f2f..58abf97bf 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -26,6 +26,7 @@ Revision History: #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE } #define Z3_CATCH Z3_CATCH_CORE(return;) #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;) +#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; } #define CHECK_REF_COUNT(a) (reinterpret_cast(a)->get_ref_count() > 0) #define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a)) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 7a1a404af..3ad136f12 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3053,10 +3053,10 @@ public class Context extends IDisposable // OK. } m_ctx = 0; - } else - /* re-queue the finalizer */ - /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount); + } + /* + else + CMW: re-queue the finalizer? */ } /** From 9e868cdef39bbd7a5b3faa3bf63978331ffa79e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Feb 2013 16:04:46 -0800 Subject: [PATCH 08/10] fix pretty printer bug found by ken Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 8 +++++--- src/muz_qe/pdr_generalizers.cpp | 8 ++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 3dc94d3b3..c6c9c7c0c 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -537,7 +537,7 @@ class smt_printer { } void print_bound(symbol const& name) { - if (name.is_numerical() || '?' != name.bare_str()[0]) { + if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { m_out << "?"; } m_out << name; @@ -561,7 +561,7 @@ class smt_printer { m_out << "("; print_bound(m_renaming.get_symbol(q->get_decl_name(i))); m_out << " "; - visit_sort(s, true); + visit_sort(s, !m_is-smt2); m_out << ") "; } if (m_is_smt2) { @@ -642,7 +642,9 @@ class smt_printer { m_out << m_var_names[m_num_var_names - idx - 1]; } else { - m_out << "?" << idx; + if (!m_is_smt2) { + m_out << "?" << idx; + } } } diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index a02a1cb6e..c9141f23e 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -188,8 +188,8 @@ namespace pdr { } } if (abs(r) >= rational(2) && a.is_int(x)) { - new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true)); - new_core[l] = a.mk_ge(x, a.mk_numeral(r, true)); + new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(rational(2), true)), a.mk_numeral(rational(0), true)); + new_core[l] = a.mk_le(x, a.mk_numeral(r, true)); } bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); @@ -258,8 +258,8 @@ namespace pdr { vector & terms1 = it->m_value; vector terms2; if (r >= rational(2) && m_ub.find(r, terms2)) { - bool done = false; - for (unsigned i = 0; !done && i < terms1.size(); ++i) { + for (unsigned i = 0; i < terms1.size(); ++i) { + bool done = false; for (unsigned j = 0; !done && j < terms2.size(); ++j) { expr* t1 = terms1[i].first; expr* t2 = terms2[j].first; From dd90667cc7173d9b449a692f06fbdb5017b509ed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Feb 2013 16:32:53 -0800 Subject: [PATCH 09/10] fix pretty printer bug found by ken Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index c6c9c7c0c..420961b4e 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -537,7 +537,7 @@ class smt_printer { } void print_bound(symbol const& name) { - if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { + if (!is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { m_out << "?"; } m_out << name; @@ -561,7 +561,7 @@ class smt_printer { m_out << "("; print_bound(m_renaming.get_symbol(q->get_decl_name(i))); m_out << " "; - visit_sort(s, !m_is-smt2); + visit_sort(s, true); m_out << ") "; } if (m_is_smt2) { From ef7bc637478743456bfaa65c3d340101d5d7949b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Feb 2013 19:22:43 -0800 Subject: [PATCH 10/10] Fix compilation error Signed-off-by: Leonardo de Moura --- src/ast/ast_smt_pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 420961b4e..5bdc70dc2 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -537,7 +537,7 @@ class smt_printer { } void print_bound(symbol const& name) { - if (!is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { + if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { m_out << "?"; } m_out << name;