na

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Sep 3, 2020 · 7fbaf71 · 7fbaf71
1 parent 65bc77d
commit 7fbaf71
Show file tree

Hide file tree

Showing 3 changed files with 71 additions and 5 deletions.
diff --git 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<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) {}

diff --git 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
@@ -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;