From 7fbaf71d4a3d622d3886365b80ba0743d8c9f42d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Sep 2020 09:19:39 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/sat/smt/bv_internalize.cpp | 44 +++++++++++++++++++++++++++++++--- src/sat/smt/bv_solver.cpp | 26 ++++++++++++++++++++ src/sat/smt/bv_solver.h | 6 +++-- 3 files changed, 71 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 9ee3a62f737..0f03e6db15a 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -179,7 +179,7 @@ namespace bv { #endif - euf::enode * solver::mk_enode(app * n, ptr_vector const& args) { + euf::enode * solver::mk_enode(expr * n, ptr_vector 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) {} diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index d033d565f3a..4555a37cba9 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -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;} + } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 4a926dbe086..1e32362faa3 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -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 const& args); + euf::enode* mk_enode(expr* n, ptr_vector 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;