mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-03 09:19:39 -07:00
parent 65bc77d566
commit 7fbaf71d4a
3 changed files with 71 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/sat/smt/bv_internalize.cpp
View file

@ -179,7 +179,7 @@ namespace bv {
#endif
euf::enode * solver::mk_enode(app * n, ptr_vector<euf::enode> const& args) {
euf::enode * solver::mk_enode(expr * n, ptr_vector<euf::enode> const& args) {
euf::enode * e = ctx.get_enode(n);
if (!e) {
e = ctx.mk_enode(n, args.size(), args.c_ptr());
@ -304,6 +304,46 @@ namespace bv {
fixed_var_eh(v);
}
void solver::internalize_mkbv(app* n) {
expr_ref_vector bits(m);
euf::enode * e = mk_enode(n, m_args);
bits.append(n->get_num_args(), n->get_args());
init_bits(e, bits);
}
void solver::internalize_bv2int(app* n) {
mk_enode(n, m_args);
assert_bv2int_axiom(n);
}
void solver::assert_bv2int_axiom(app * n) {
//
// create the axiom:
// n = bv2int(k) = ite(bit2bool(k[sz-1],2^{sz-1},0) + ... + ite(bit2bool(k[0],1,0))
//
expr* k = nullptr;
sort * int_sort = m.get_sort(n);
SASSERT(bv.is_bv2int(n, k));
SASSERT(bv.is_bv_sort(m.get_sort(k)));
expr_ref_vector k_bits(m);
euf::enode * k_enode = mk_enode(k, m_args);
get_bits(k_enode, k_bits);
unsigned sz = bv.get_bv_size(k);
expr_ref_vector args(m);
expr_ref zero(bv.mk_numeral(numeral(0), int_sort), m);
numeral num(1);
for (expr* b : k_bits) {
expr_ref n(m_autil.mk_numeral(num, int_sort), m);
args.push_back(m.mk_ite(b, n, zero));
num *= numeral(2);
}
expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
expr_ref eq(m.mk_eq(n, sum), m);
sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant);
s().add_clause(1, &lit, sat::status::th(m_is_redundant, get_id()));
}
void solver::internalize_add(app* n) {}
void solver::internalize_sub(app* n) {}
void solver::internalize_mul(app* n) {}
@ -333,9 +373,7 @@ namespace bv {
void solver::internalize_comp(app* n) {}
void solver::internalize_rotate_left(app* n) {}
void solver::internalize_rotate_right(app* n) {}
void solver::internalize_bv2int(app* n) {}
void solver::internalize_int2bv(app* n) {}
void solver::internalize_mkbv(app* n) {}
void solver::internalize_umul_no_overflow(app* n) {}
void solver::internalize_smul_no_overflow(app* n) {}
void solver::internalize_smul_no_underflow(app* n) {}

26
src/sat/smt/bv_solver.cpp
View file

@ -108,4 +108,30 @@ namespace bv {
#endif
return out;
}
double solver::get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const { return 0; }
bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; }
bool solver::is_external(bool_var v) { return true; }
bool solver::propagate(literal l, sat::ext_constraint_idx idx) { return false; }
void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r) {}
void solver::asserted(literal l) {}
sat::check_result solver::check() { return sat::check_result::CR_DONE; }
void solver::push() {}
void solver::pop(unsigned n) {}
void solver::pre_simplify() {}
void solver::simplify() {}
void solver::clauses_modifed() {}
lbool solver::get_phase(bool_var v) { return l_undef; }
std::ostream& solver::display(std::ostream& out) const { return out; }
std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; }
std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out; }
void solver::collect_statistics(statistics& st) const {}
sat::extension* solver::copy(sat::solver* s) { return nullptr; }
void solver::pop_reinit() {}
bool solver::validate() { return true; }
void solver::init_use_list(sat::ext_use_list& ul) {}
bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; }
bool solver::check_model(sat::model const& m) const { return true; }
unsigned solver::max_var(unsigned w) const { return 0;}
}

6
src/sat/smt/bv_solver.h
View file

@ -131,7 +131,7 @@ namespace bv {
void get_bits(euf::enode* n, expr_ref_vector& r);
void get_arg_bits(euf::enode* n, unsigned idx, expr_ref_vector& r);
void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r);
euf::enode* mk_enode(app* n, ptr_vector<euf::enode> const& args);
euf::enode* mk_enode(expr* n, ptr_vector<euf::enode> const& args);
void fixed_var_eh(theory_var v);
void register_true_false_bit(theory_var v, unsigned i);
void add_bit(theory_var v, sat::literal lit);
@ -175,6 +175,8 @@ namespace bv {
void internalize_smul_no_overflow(app *n);
void internalize_smul_no_underflow(app *n);
void assert_bv2int_axiom(app * n);
// solving
void find_wpos(theory_var v);
void find_new_diseq_axioms(var_pos_occ* occs, theory_var v, unsigned idx);
@ -196,7 +198,7 @@ namespace bv {
sat::check_result check() override;
void push() override;
void pop(unsigned n) override;
void pre_simplify() override;
void pre_simplify() override;
void simplify() override;
void clauses_modifed() override;
lbool get_phase(bool_var v) override;