From 0d400a5ad61ee457f3c53399461d347adcf0d604 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Jan 2019 07:46:53 -0800 Subject: [PATCH] fix bit2bool bug reported by Jianying Li Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 16 ++++++++++++++++ src/ast/rewriter/bv_rewriter.h | 1 + src/cmd_context/extra_cmds/dbg_cmds.cpp | 20 +++++++++++++++----- src/qe/qe_arrays.cpp | 4 ++-- src/qe/qe_mbi.cpp | 2 ++ src/qe/qe_mbi.h | 2 +- src/smt/theory_pb.cpp | 9 +++++---- src/smt/theory_seq.cpp | 5 +---- src/smt/theory_str.cpp | 10 ++++++---- 9 files changed, 49 insertions(+), 20 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 3dc76da5e..f6b760f9c 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -196,6 +196,9 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons return mk_bv_comp(args[0], args[1], result); case OP_MKBV: return mk_mkbv(num_args, args, result); + case OP_BIT2BOOL: + SASSERT(num_args == 1); + return mk_bit2bool(args[0], f->get_parameter(0).get_int(), result); case OP_BSMUL_NO_OVFL: return mk_bvsmul_no_overflow(num_args, args, result); case OP_BUMUL_NO_OVFL: @@ -2203,6 +2206,19 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re return st; } +br_status bv_rewriter::mk_bit2bool(expr * n, int idx, expr_ref & result) { + rational v, bit; + unsigned sz = 0; + if (!is_numeral(n, v, sz)) + return BR_FAILED; + if (idx < 0 || idx >= static_cast(sz)) + return BR_FAILED; + div(v, rational::power_of_two(idx), bit); + mod(bit, rational(2), bit); + result = m().mk_bool_val(bit.is_one()); + return BR_DONE; +} + br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { unsigned sz = get_bv_size(lhs); if (sz != 1) diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 205ebbf8e..8ad589a49 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -134,6 +134,7 @@ class bv_rewriter : public poly_rewriter { br_status mk_bv_redand(expr * arg, expr_ref & result); br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result); br_status mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result); + br_status mk_bit2bool(expr * lhs, int idx, expr_ref & result); br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result); br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result); br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result); diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index bdd2c8b97..6170a231e 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -524,11 +524,21 @@ public: for (func_decl* v : m_vars) vars.push_back(v); for (expr* e : m_lits) lits.push_back(e); flatten_and(lits); - qe::term_graph tg(m); - tg.set_vars(vars, false); - tg.add_lits(lits); - expr_ref_vector p = tg.project(); - ctx.regular_stream() << p << "\n"; + solver_factory& sf = ctx.get_solver_factory(); + params_ref pa; + solver_ref s = sf(m, pa, false, true, true, symbol::null); + solver_ref se = sf(m, pa, false, true, true, symbol::null); + s->assert_expr(lits); + lbool r = s->check_sat(); + if (r != l_true) { + ctx.regular_stream() << "sat check " << r << "\n"; + return; + } + model_ref mdl; + s->get_model(mdl); + qe::euf_arith_mbi_plugin plugin(s.get(), se.get()); + plugin.project(mdl, lits); + ctx.regular_stream() << lits << "\n"; } }; diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 4c81418b6..4bead6684 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -798,7 +798,7 @@ namespace qe { */ expr* reduce_core (app *a) { if (!m_arr_u.is_store (a->get_arg (0))) return a; - expr* array = a->get_arg(0); + expr* array = a->get_arg(0); unsigned arity = get_array_arity(m.get_sort(array)); expr* const* js = a->get_args() + 1; @@ -810,7 +810,7 @@ namespace qe { if (is_equals (arity, idxs, js)) { add_idx_cond (cond); - return a->get_arg (2); + return a->get_arg (a->get_num_args() - 1); } else { cond = m.mk_not (cond); diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index dd0d36418..77f910260 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -256,6 +256,8 @@ namespace qe { void euf_arith_mbi_plugin::project(model_ref& mdl, expr_ref_vector& lits) { TRACE("qe", tout << lits << "\n" << *mdl << "\n";); + TRACE("qe", tout << m_solver->get_assertions() << "\n";); + // 1. arithmetical variables - atomic and in purified positions app_ref_vector proxies(m); diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index aa5d935b4..12e6a8080 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -106,7 +106,6 @@ namespace qe { app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies); bool get_literals(model_ref& mdl, expr_ref_vector& lits); void collect_atoms(expr_ref_vector const& fmls); - void project(model_ref& mdl, expr_ref_vector& lits); void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars); void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies); void substitute(vector const& defs, expr_ref_vector& lits); @@ -115,6 +114,7 @@ namespace qe { euf_arith_mbi_plugin(solver* s, solver* emptySolver); ~euf_arith_mbi_plugin() override {} mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; + void project(model_ref& mdl, expr_ref_vector& lits); void block(expr_ref_vector const& lits) override; }; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index de86ef7e3..671184633 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -723,10 +723,11 @@ namespace smt { ineqs = alloc(ptr_vector); m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs; } - for (auto* c1 : *ineqs) { - //if (c1 == c) return; - SASSERT (c1 != c); - } + DEBUG_CODE( + for (auto* c1 : *ineqs) { + //if (c1 == c) return; + SASSERT (c1 != c); + }); ineqs->push_back(c); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 283bd4e57..e8af44d7e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3495,12 +3495,11 @@ bool theory_seq::add_itos_val_axiom(expr* e) { } bool theory_seq::add_stoi_val_axiom(expr* e) { - context& ctx = get_context(); expr* n = nullptr; rational val, val2; VERIFY(m_util.str.is_stoi(e, n)); - TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << " " << get_length(n, val) << " " << val << "\n";); + TRACE("seq", tout << mk_pp(e, m) << " " << get_context().get_scope_level () << " " << get_length(n, val) << " " << val << "\n";); if (m_util.str.is_itos(n)) { return false; @@ -3951,7 +3950,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { app* theory_seq::mk_value(app* e) { expr_ref result(m); - context& ctx = get_context(); e = get_ite_value(e); result = m_rep.find(e); @@ -4705,7 +4703,6 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) { bool theory_seq::get_length(expr* e, rational& val) const { - context& ctx = get_context(); rational val1; expr_ref len(m), len_val(m); expr* e1 = nullptr, *e2 = nullptr; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 02801648a..75ca7cf47 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1682,10 +1682,10 @@ namespace smt { expr_ref i1(mk_int_var("i1"), m); expr_ref result(mk_str_var("result"), m); - expr * replaceS; - expr * replaceT; - expr * replaceTPrime; - u.str.is_replace(ex, replaceS, replaceT, replaceTPrime); + expr * replaceS = nullptr; + expr * replaceT = nullptr; + expr * replaceTPrime = nullptr; + VERIFY(u.str.is_replace(ex, replaceS, replaceT, replaceTPrime)); // t empty => result = (str.++ t' s) expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m); @@ -4851,6 +4851,7 @@ namespace smt { bool theory_str::get_arith_value(expr* e, rational& val) const { context& ctx = get_context(); ast_manager & m = get_manager(); + (void)m; if (!ctx.e_internalized(e)) { return false; } @@ -8255,6 +8256,7 @@ namespace smt { void theory_str::check_eqc_concat_concat(std::set & eqc_concat_lhs, std::set & eqc_concat_rhs) { ast_manager & m = get_manager(); + (void)m; int hasCommon = 0; if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) {