From c3f498a64045ae848a4d25f68e28cabb694566a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 May 2016 12:26:47 -0700 Subject: [PATCH] strengthen support for int.to.str and length reasoning. Issue #589 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 22 ++++++++++- src/ast/ast.h | 13 +------ src/cmd_context/cmd_context.cpp | 14 +++---- src/muz/rel/dl_compiler.cpp | 18 ++++++--- src/muz/rel/dl_compiler.h | 2 +- src/muz/rel/dl_instruction.cpp | 3 +- src/muz/rel/dl_relation_manager.cpp | 4 +- src/smt/theory_seq.cpp | 57 +++++++++++++++++++++++++++-- src/smt/theory_seq.h | 1 + 9 files changed, 103 insertions(+), 31 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fcf9365e3..fa5a8297e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1420,7 +1420,7 @@ ast_manager::~ast_manager() { std::cout << to_sort(a)->get_name() << "\n"; } else { - std::cout << mk_ll_pp(a, *this, false); + std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n"; } } }); @@ -1575,6 +1575,26 @@ bool ast_manager::are_equal(expr * a, expr * b) const { return false; } +void ast_manager::inc_ref(ast * n) { + + if (n && n->get_id() == 362568) { + std::cout << "inc-ref " << n->get_ref_count() << "\n"; + } + if (n) + n->inc_ref(); +} + +void ast_manager::dec_ref(ast* n) { + if (n && n->get_id() == 362568) { + std::cout << "dec-ref " << n->get_ref_count() << "\n"; + } + if (n) { + n->dec_ref(); + if (n->get_ref_count() == 0) + delete_node(n); + } +} + bool ast_manager::are_distinct(expr* a, expr* b) const { if (is_app(a) && is_app(b)) { app* ap = to_app(a), *bp = to_app(b); diff --git a/src/ast/ast.h b/src/ast/ast.h index a7db78ca2..3f941b8d1 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1571,18 +1571,9 @@ public: void debug_ref_count() { m_debug_ref_count = true; } - void inc_ref(ast * n) { - if (n) - n->inc_ref(); - } + void inc_ref(ast * n); - void dec_ref(ast * n) { - if (n) { - n->dec_ref(); - if (n->get_ref_count() == 0) - delete_node(n); - } - } + void dec_ref(ast * n); template void inc_array_ref(unsigned sz, T * const * a) { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index cfad0d394..55b61d0da 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1487,18 +1487,18 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions return; } display_sat_result(r); + if (r == l_true) { + validate_model(); + } validate_check_sat_result(r); if (was_opt && r != l_false && !was_pareto) { get_opt()->display_assignment(regular_stream()); } - if (r == l_true) { - validate_model(); - if (m_params.m_dump_models) { - model_ref md; - get_check_sat_result()->get_model(md); - display_model(md); - } + if (r == l_true && m_params.m_dump_models) { + model_ref md; + get_check_sat_result()->get_model(md); + display_model(md); } } diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 67227e7d9..7fb2afd9e 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -26,7 +26,8 @@ Revision History: #include"dl_util.h" #include"dl_compiler.h" #include"ast_pp.h" -#include"ast_smt2_pp.h" +// include"ast_smt2_pp.h" +#include"ast_util.h" namespace datalog { @@ -185,10 +186,11 @@ namespace datalog { } } - void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, + void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result, bool & dealloc, instruction_block & acc) { - TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); + TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) + << " " << m_context.get_rel_context()->get_rmanager().to_nice_string(s) << "\n";); IF_VERBOSE(3, { expr_ref e(m_context.get_manager()); m_context.get_rule_manager().to_formula(*compiled_rule, e); @@ -328,13 +330,15 @@ namespace datalog { continue; } unsigned bound_column_index; - if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) { + if(acis[i].kind != ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) { bound_column_index=curr_sig->size(); if(acis[i].kind==ACK_CONSTANT) { make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, curr, dealloc, acc); } else { SASSERT(acis[i].kind==ACK_UNBOUND_VAR); + TRACE("dl", tout << head_pred->get_name() << " index: " << i + << " " << m_context.get_rel_context()->get_rmanager().to_nice_string(acis[i].domain) << "\n";); make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, curr, dealloc, acc); handled_unbound.insert(acis[i].var_index,bound_column_index); } @@ -598,14 +602,15 @@ namespace datalog { // add unbounded columns for interpreted filter unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ft_len = r->get_tail_size(); // full tail - ptr_vector tail; + expr_ref_vector tail(m); for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { tail.push_back(r->get_tail(tail_index)); } expr_ref_vector binding(m); if (!tail.empty()) { - app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); + expr_ref filter_cond = mk_and(tail); + m_free_vars.reset(); m_free_vars(filter_cond); // create binding binding.resize(m_free_vars.size()+1); @@ -620,6 +625,7 @@ namespace datalog { } else { // we have an unbound variable, so we add an unbound column for it relation_sort unbound_sort = m_free_vars[v]; + TRACE("dl", tout << "unbound: " << v << "\n" << filter_cond << " " << mk_pp(unbound_sort, m) << "\n";); make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, filtered_res, dealloc, acc); src_col = single_res_expr.size(); diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 4126833d1..33d92d805 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -180,7 +180,7 @@ namespace datalog { void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val, reg_idx & result, bool & dealloc, instruction_block & acc); - void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result, + void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort& s, reg_idx & result, bool & dealloc, instruction_block & acc); void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, instruction_block & acc); diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 2c1850bf4..f0b88cae1 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -1052,7 +1052,8 @@ namespace datalog { } virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "mk_total into " << m_tgt << " sort:" - << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig); + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig) + << " " << m_pred->get_name(); } virtual void make_annotations(execution_context & ctx) { std::string s; diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 1127dbb31..0b0dae12c 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -488,7 +488,9 @@ namespace datalog { } std::string relation_manager::to_nice_string(const relation_sort & s) const { - return std::string(s->get_name().bare_str()); + std::ostringstream strm; + strm << mk_pp(s, get_context().get_manager()); + return strm.str(); } std::string relation_manager::to_nice_string(const relation_signature & s) const { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 8a1ee2946..04efc79e6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1398,7 +1398,9 @@ bool theory_seq::is_var(expr* a) { !m_util.str.is_concat(a) && !m_util.str.is_empty(a) && !m_util.str.is_string(a) && - !m_util.str.is_unit(a); + !m_util.str.is_unit(a) && + !m_util.str.is_itos(a) && + !m.is_ite(a); } @@ -2216,7 +2218,10 @@ bool theory_seq::add_itos_axiom(expr* e) { m_itos_axioms.insert(val); app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); expr_ref n1(arith_util(m).mk_numeral(val, true), m); - add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false)); + + add_axiom(~mk_eq(n1, n , false), mk_eq(e, e1, false)); + add_axiom(mk_eq(n1, n, false), ~mk_eq(e, e1, false)); + m_trail_stack.push(insert_map(m_itos_axioms, val)); m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); return true; @@ -2883,7 +2888,7 @@ void theory_seq::add_length_axiom(expr* n) { add_axiom(mk_eq(len, n, false)); } else if (m_util.str.is_itos(x)) { - add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(1)))); + add_itos_length_axiom(n); } else { add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0)))); @@ -2891,6 +2896,52 @@ void theory_seq::add_length_axiom(expr* n) { if (!ctx.at_base_level()) { m_trail_stack.push(push_replay(alloc(replay_axiom, m, n))); } +} + +void theory_seq::add_itos_length_axiom(expr* len) { + expr* x, *n; + VERIFY(m_util.str.is_length(len, x)); + VERIFY(m_util.str.is_itos(x, n)); + + add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1)))); + rational val; + if (get_value(n, val)) { + bool neg = val.is_neg(); + rational ten(10); + if (neg) val.neg(); + unsigned num_char = neg?2:1; + // 0 < x < 10 + // 10 < x < 100 + // 100 < x < 1000 + rational hi(10); + while (val > hi) { + ++num_char; + hi *= ten; + } + rational lo(div(hi - rational(1), ten)); + + literal len_le(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char)))); + literal len_ge(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char)))); + if (neg) { + // n <= -lo => len >= num_char + // -hi < n <= 0 => len <= num_char + // n <= -hi or ~(n <= 0) or len <= num_char + literal l1(mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-lo, true)))); + add_axiom(~l1, len_ge); + literal l3(mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-hi, true)))); + literal l4(mk_literal(m_autil.mk_le(n, m_autil.mk_int(0)))); + add_axiom(l3, ~l4, len_le); + } + else { + // n >= lo => len >= num_char + // 0 <= n < hi => len <= num_char + literal l1(mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(lo, true)))); + add_axiom(~l1, len_ge); + literal l3(mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(hi, true)))); + literal l4(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0)))); + add_axiom(l3, ~l4, len_le); + } + } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 4107f3d05..136a84520 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -494,6 +494,7 @@ namespace smt { void add_at_axiom(expr* n); void add_in_re_axiom(expr* n); bool add_itos_axiom(expr* n); + void add_itos_length_axiom(expr* n); literal mk_literal(expr* n); literal mk_eq_empty(expr* n, bool phase = true); literal mk_seq_eq(expr* a, expr* b);