mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Added bit2bool to the API (#5992)
* Fixed registering expressions in push/pop * Reused existing function * Reverted reusing can_propagate * Added decide-callback to user-propagator * Refactoring * Fixed index * Added bit2bool to the API Fixed bug in user-propagator's decide callback * Fixed typo
This commit is contained in:
parent
0dd0fd26d4
commit
81189d6fdd
|
@ -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);
|
||||
|
|
|
@ -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<unsigned>(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<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue