diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 685463e19..bb4263730 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -102,6 +102,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ MK_BV_PUNARY(Z3_mk_sign_ext, OP_SIGN_EXT); MK_BV_PUNARY(Z3_mk_zero_ext, OP_ZERO_EXT); MK_BV_PUNARY(Z3_mk_repeat, OP_REPEAT); + MK_BV_PUNARY(Z3_mk_bit2bool, OP_BIT2BOOL); MK_BV_PUNARY(Z3_mk_rotate_left, OP_ROTATE_LEFT); MK_BV_PUNARY(Z3_mk_rotate_right, OP_ROTATE_RIGHT); MK_BV_PUNARY(Z3_mk_int2bv, OP_INT2BV); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 04e0b78e2..e817a5859 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1359,6 +1359,7 @@ namespace z3 { friend expr operator~(expr const & a); expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); } + expr bit2bool(unsigned i) const { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); } unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast(Z3_get_decl_int_parameter(ctx(), decl(), 1)); } unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast(Z3_get_decl_int_parameter(ctx(), decl(), 0)); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2680b6f82..a9e0c6b7c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2914,6 +2914,16 @@ extern "C" { def_API('Z3_mk_repeat', AST, (_in(CONTEXT), _in(UINT), _in(AST))) */ Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1); + + /** + \brief Extracts the bit at position \ccode{i} of a bit-vector and + yields a boolean. + + The node \c t1 must have a bit-vector sort. + + def_API('Z3_mk_bit2bool', AST, (_in(CONTEXT), _in(UINT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1); /** \brief Shift left. @@ -6755,16 +6765,16 @@ extern "C" { void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh); /** - * \brief register a callback when a new expression with a registered function is used by the solver - * The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare. + \brief register a callback when a new expression with a registered function is used by the solver + The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare. */ void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh); /** - * \brief register a callback when a the solver decides to split on a registered expression - * The callback may set passed expression to another registered expression which will be selected instead. - * In case the expression is a bitvector the bit to split on is determined by the bit argument and the - * truth-value to try first is given by is_pos + \brief register a callback when the solver decides to split on a registered expression. + The callback may set the passed expression to another registered expression which will be selected instead. + In case the expression is a bitvector the bit to split on is determined by the bit argument and the + truth-value to try first is given by is_pos. In case the truth value is undefined the solver will decide. */ void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 682f4d6f9..90c8cd89e 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1842,11 +1842,11 @@ namespace smt { unsigned sz = bits.size(); for (unsigned i = start_bit; i < sz; ++i) { - if (ctx.get_assignment(bits[i].var()) != l_undef) + if (ctx.get_assignment(bits[i].var()) == l_undef) return bits[i].var(); } for (unsigned i = 0; i < start_bit; ++i) { - if (ctx.get_assignment(bits[i].var()) != l_undef) + if (ctx.get_assignment(bits[i].var()) == l_undef) return bits[i].var(); } diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 1b0cc429d..e5b1a9c0d 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -159,37 +159,53 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu void theory_user_propagator::decide(bool_var& var, bool& is_pos) { const bool_var_data& d = ctx.get_bdata(var); - - if (!d.is_theory_atom()) + + if (!d.is_enode() && !d.is_theory_atom()) return; - - theory* th = ctx.get_theory(d.get_theory()); - - bv_util bv(m); - enode* original_enode = nullptr; + + enode* original_enode = nullptr; unsigned original_bit = 0; - - if (d.is_enode() && th->get_family_id() == get_family_id()) { - // variable is just a registered expression + bv_util bv(m); + theory* th = nullptr; + theory_var v = null_theory_var; + + // get the associated theory + if (!d.is_enode()) { + // it might be a value that does not have an enode + th = ctx.get_theory(d.get_theory()); + } + else { original_enode = ctx.bool_var2enode(var); + v = original_enode->get_th_var(get_family_id()); + if (v == null_theory_var) { + // it is not a registered boolean expression + th = ctx.get_theory(d.get_theory()); + } } - else if (th->get_family_id() == bv.get_fid()) { - // it might be a registered bit-vector - auto registered_bv = ((theory_bv*)th)->get_bv_with_theory(var, get_family_id()); - if (!registered_bv.first) - // there is no registered bv associated with the bit - return; - original_enode = registered_bv.first; - original_bit = registered_bv.second; - } - else + + if (!th && v == null_theory_var) return; + if (v == null_theory_var) { + if (th->get_family_id() == bv.get_fid()) { + // it is not a registered boolean value but it is a bitvector + auto registered_bv = ((theory_bv*)th)->get_bv_with_theory(var, get_family_id()); + if (!registered_bv.first) + // there is no registered bv associated with the bit + return; + original_enode = registered_bv.first; + original_bit = registered_bv.second; + v = original_enode->get_th_var(get_family_id()); + } + else + return; + } + // call the registered callback unsigned new_bit = original_bit; lbool phase = is_pos ? l_true : l_false; - - expr* e = var2expr(original_enode->get_th_var(get_family_id())); + + expr* e = var2expr(v); m_decide_eh(m_user_context, this, &e, &new_bit, &phase); enode* new_enode = ctx.get_enode(e); @@ -201,7 +217,6 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { return; } - bool_var old_var = var; if (new_enode->is_bool()) { // expression was set to a boolean bool_var new_var = ctx.enode2bool_var(new_enode);