na

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/sat/smt/CMakeLists.txt

@@ -4,13 +4,14 @@ z3_add_component(sat_smt
     ba_internalize.cpp
     ba_solver.cpp
     bv_internalize.cpp
-    xor_solver.cpp
+    bv_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
     euf_model.cpp
     euf_proof.cpp
     euf_solver.cpp
     sat_th.cpp
+    xor_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast

src/sat/smt/bv_internalize.cpp

@@ -23,53 +23,227 @@ Module Name:
 namespace bv {
 
     euf::theory_var solver::mk_var(euf::enode* n) {
-        theory_var r  = euf::th_euf_solver::mk_var(n);
+        theory_var r = euf::th_euf_solver::mk_var(n);
         m_find.mk_var();
         m_bits.push_back(sat::literal_vector());
         m_wpos.push_back(0);
-        m_zero_one_bits.push_back(zero_one_bits());        
+        m_zero_one_bits.push_back(zero_one_bits());
         ctx.attach_th_var(n, this, r);
         return r;
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
-        flet<bool> _is_learned(m_is_redundant, learned);
-        sat::scoped_stack _sc(m_stack);
-        unsigned sz = m_stack.size();
-        visit(e);
-        while (m_stack.size() > sz) {
-        loop:
-            if (!m.inc())
-                throw tactic_exception(m.limit().get_cancel_msg());
-            sat::eframe & fr = m_stack.back();
-            expr* e = fr.m_e;
-            if (visited(e)) {
-                m_stack.pop_back();
-                continue;
-            }
-            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
-
-            while (fr.m_idx < num) {
-                expr* arg = to_app(e)->get_arg(fr.m_idx);
-                fr.m_idx++;
-                visit(arg);
-                if (!visited(arg))
-                    goto loop;
-            }
-            visit(e);
-            SASSERT(visited(e));
-            m_stack.pop_back();
-        }        
-        SASSERT(visited(e));
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        if (!visit_rec(m, e, sign, root, redundant))
+            return sat::null_literal;
         return sat::null_literal;
     }
 
     bool solver::visit(expr* e) {
-        return false;
+        if (!bv.is_bv(e)) {
+            ctx.internalize(e, false, false, m_is_redundant);
+            return true;
+        }
+        m_args.reset();
+        app* a = to_app(e);
+        for (expr* arg : *a) {
+            euf::enode* n = get_enode(arg);
+            if (n)
+                m_args.push_back(n);
+            else
+                m_stack.push_back(sat::eframe(arg));
+        }
+        if (m_args.size() != a->get_num_args())
+            return false;
+        if (!smt_params().m_bv_reflect)
+            m_args.reset();
+        euf::enode* n = mk_enode(a, m_args);
+        SASSERT(n->interpreted());
+        theory_var v = n->get_th_var(get_id());
+
+        switch (a->get_decl_kind()) {
+        case OP_BV_NUM:         internalize_num(a, v); break;
+        default:                break;
+        }
+        return true;
     }
 
     bool solver::visited(expr* e) {
-        return false;
+        return get_enode(e) != nullptr;
+    }
+
+    euf::enode * solver::mk_enode(app * 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());
+            mk_var(e);
+        }
+        return e;
+    }
+
+    void solver::register_true_false_bit(theory_var v, unsigned i) {
+
+    }
+
+    /**
+       \brief Add bit l to the given variable.
+    */
+    void solver::add_bit(theory_var v, literal l) {
+        literal_vector & bits = m_bits[v];
+        unsigned idx          = bits.size();
+        bits.push_back(l);
+#if 0
+        if (l.var() == true_bool_var) {
+            register_true_false_bit(v, idx);
+        }
+        else {
+            theory_id th_id = ctx.get_var_theory(l.var());
+            if (th_id == get_id()) {
+                atom * a = get_bv2a(l.var());
+                SASSERT(a && a->is_bit());
+                bit_atom * b = static_cast<bit_atom*>(a);
+                find_new_diseq_axioms(b->m_occs, v, idx);
+                ctx.push(add_var_pos_trail(b));
+                b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
+            }
+            else {
+                SASSERT(th_id == null_theory_id);
+                ctx.set_var_theory(l.var(), get_id());
+                SASSERT(ctx.get_var_theory(l.var()) == get_id());
+                bit_atom * b = new (get_region()) bit_atom();
+                insert_bv2a(l.var(), b);
+                ctx.push(mk_atom_trail(l.var()));
+                SASSERT(b->m_occs == 0);
+                b->m_occs = new (get_region()) var_pos_occ(v, idx);
+            }
+        }
+#endif
+    }
+
+    void solver::init_bits(euf::enode * n, expr_ref_vector const & bits) {
+        SASSERT(get_bv_size(n) == bits.size());
+        SASSERT(euf::null_theory_var != n->get_th_var(get_id()));
+        theory_var v = n->get_th_var(get_id());
+        unsigned sz = bits.size();
+        m_bits[v].reset();
+        for (expr* bit : bits)
+            add_bit(v, get_literal(bit));
+        find_wpos(v);
+    }
+
+    unsigned solver::get_bv_size(euf::enode* n) {
+        return bv.get_bv_size(n->get_owner());
+    }
+
+    void solver::internalize_num(app* n, theory_var v) {
+        numeral val;
+        unsigned sz = 0;
+        VERIFY(bv.is_numeral(n, val, sz));
+        expr_ref_vector bits(m);
+        m_bb.num2bits(val, sz, bits); 
+        literal_vector & c_bits = m_bits[v];
+        SASSERT(bits.size() == sz);
+        SASSERT(c_bits.empty());
+        for (unsigned i = 0; i < sz; i++) {
+            expr * l = bits.get(i);
+            SASSERT(m.is_true(l) || m.is_false(l));
+            c_bits.push_back(m.is_true(l) ? true_literal : false_literal);
+            register_true_false_bit(v, i);
+        }
+        fixed_var_eh(v);
+    }
+
+    void solver::internalize_add(app* n) {}
+    void solver::internalize_sub(app* n) {}
+    void solver::internalize_mul(app* n) {}
+    void solver::internalize_udiv(app* n) {}
+    void solver::internalize_sdiv(app* n) {}
+    void solver::internalize_urem(app* n) {}
+    void solver::internalize_srem(app* n) {}
+    void solver::internalize_smod(app* n) {}
+    void solver::internalize_shl(app* n) {}
+    void solver::internalize_lshr(app* n) {}
+    void solver::internalize_ashr(app* n) {}
+    void solver::internalize_ext_rotate_left(app* n) {}
+    void solver::internalize_ext_rotate_right(app* n) {}
+    void solver::internalize_and(app* n) {}
+    void solver::internalize_or(app* n) {}
+    void solver::internalize_not(app* n) {}
+    void solver::internalize_nand(app* n) {}
+    void solver::internalize_nor(app* n) {}
+    void solver::internalize_xor(app* n) {}
+    void solver::internalize_xnor(app* n) {}
+    void solver::internalize_concat(app* n) {}
+    void solver::internalize_sign_extend(app* n) {}
+    void solver::internalize_zero_extend(app* n) {}
+    void solver::internalize_extract(app* n) {}
+    void solver::internalize_redand(app* n) {}
+    void solver::internalize_redor(app* n) {}
+    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) {}
+
+}
+
+
+
+#if 0
+
+        case OP_BADD:           internalize_add(term); return true;
+        case OP_BSUB:           internalize_sub(term); return true;
+        case OP_BMUL:           internalize_mul(term); return true;
+        case OP_BSDIV_I:        internalize_sdiv(term); return true;
+        case OP_BUDIV_I:        internalize_udiv(term); return true;
+        case OP_BSREM_I:        internalize_srem(term); return true;
+        case OP_BUREM_I:        internalize_urem(term); return true;
+        case OP_BSMOD_I:        internalize_smod(term); return true;
+        case OP_BAND:           internalize_and(term); return true;
+        case OP_BOR:            internalize_or(term); return true;
+        case OP_BNOT:           internalize_not(term); return true;
+        case OP_BXOR:           internalize_xor(term); return true;
+        case OP_BNAND:          internalize_nand(term); return true;
+        case OP_BNOR:           internalize_nor(term); return true;
+        case OP_BXNOR:          internalize_xnor(term); return true;
+        case OP_CONCAT:         internalize_concat(term); return true;
+        case OP_SIGN_EXT:       internalize_sign_extend(term); return true;
+        case OP_ZERO_EXT:       internalize_zero_extend(term); return true;
+        case OP_EXTRACT:        internalize_extract(term); return true;
+        case OP_BREDOR:         internalize_redor(term); return true;
+        case OP_BREDAND:        internalize_redand(term); return true;
+        case OP_BCOMP:          internalize_comp(term); return true;
+        case OP_BSHL:           internalize_shl(term); return true;
+        case OP_BLSHR:          internalize_lshr(term); return true;
+        case OP_BASHR:          internalize_ashr(term); return true;
+        case OP_ROTATE_LEFT:    internalize_rotate_left(term); return true;
+        case OP_ROTATE_RIGHT:   internalize_rotate_right(term); return true;
+        case OP_EXT_ROTATE_LEFT:  internalize_ext_rotate_left(term); return true;
+        case OP_EXT_ROTATE_RIGHT: internalize_ext_rotate_right(term); return true;
+        case OP_BSDIV0:         return false;
+        case OP_BUDIV0:         return false;
+        case OP_BSREM0:         return false;
+        case OP_BUREM0:         return false;
+        case OP_BSMOD0:         return false;
+        case OP_MKBV:           internalize_mkbv(term); return true;
+        case OP_INT2BV:
+            if (params().m_bv_enable_int2bv2int) {
+                internalize_int2bv(term);
+            }
+            return params().m_bv_enable_int2bv2int;
+        case OP_BV2INT:
+            if (params().m_bv_enable_int2bv2int) {
+                internalize_bv2int(term);
+            }
+            return params().m_bv_enable_int2bv2int;
+        default:
+            TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";);
+            UNREACHABLE();
+            return false;
     }
 
 }
+#endif

src/sat/smt/bv_solver.cpp

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_internalize.cpp
+
+Abstract:
+
+    Internalize utilities for bit-vector solver plugin.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-02
+
+--*/
+
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/sat_th.h"
+#include "tactic/tactic_exception.h"
+
+namespace bv {
+
+    void solver::fixed_var_eh(theory_var v) {
+
+    }
+
+    /**
+       \brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh
+    */
+    void solver::find_wpos(theory_var v) {
+        literal_vector const & bits = m_bits[v];
+        unsigned sz                 = bits.size();
+        unsigned & wpos             = m_wpos[v];
+        unsigned init               = wpos;
+        for (; wpos < sz; wpos++) {
+            TRACE("find_wpos", tout << "curr bit: " << bits[wpos] << "\n";);
+            if (s().value(bits[wpos]) == l_undef) {
+                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
+                return;
+            }
+        }
+        wpos = 0;
+        for (; wpos < init; wpos++) {
+            if (s().value(bits[wpos]) == l_undef) {
+                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
+                return;
+            }
+        }
+        TRACE("find_wpos", tout << "v" << v << " is a fixed variable.\n";);
+        fixed_var_eh(v);
+    }
+
+
+}