intblast debugging

src/sat/smt/intblast_solver.cpp

@@ -237,6 +237,7 @@ namespace intblast {
         m_core.reset();
         m_vars.reset();
         m_trail.reset();
+        m_new_funs.reset();
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
         expr_ref_vector es(m);

src/sat/smt/intblast_solver.h

@@ -139,6 +139,7 @@ namespace intblast {
 
         rational get_value(expr* e) const;
 
+
     };
 
 }

src/sat/smt/polysat/core.h

@@ -115,11 +115,12 @@ namespace polysat {
         signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
 
 
-        pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("lshr nyi"); }
+        void lshr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("lshr nyi"); }
-        pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("ashr nyi"); }
+        void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("ashr nyi"); }
-        pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("shlh nyi"); }
+        void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("shlh nyi"); }
-        pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("band nyi"); }
+        void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("band nyi"); }
-        pdd bnot(pdd a) { return -a - 1; }
+
+        pdd bnot(pdd p) { return -p - 1; }
 
         
         pvar add_var(unsigned sz);

src/sat/smt/polysat_internalize.cpp

@@ -84,9 +84,9 @@ namespace polysat {
         case OP_BMUL:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
         case OP_BADD:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
         case OP_BSUB:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
-        case OP_BLSHR:            internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break;
+        case OP_BLSHR:            internalize_lshr(a); break;
-        case OP_BSHL:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break;
+        case OP_BSHL:             internalize_shl(a); break;
-        case OP_BAND:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break;
+        case OP_BAND:             internalize_band(a); break;
         case OP_BOR:              internalize_bor(a); break;
         case OP_BXOR:             internalize_bxor(a); break;
         case OP_BNAND:            if_unary(m_core.bnot); internalize_bnand(a); break;
@@ -230,6 +230,34 @@ namespace polysat {
         internalize_binary(n, [&](expr* const& x, expr* const& y) { return bv.mk_bv_not(bv.mk_bv_xor(x, y)); });
     }
 
+    void solver::internalize_band(app* n) {
+        if (n->get_num_args() == 2) {
+            expr* x, * y;
+            VERIFY(bv.is_bv_and(n, x, y));
+            m_core.band(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+        }
+        else {
+            expr_ref z(n->get_arg(0), m);
+            for (unsigned i = 1; i < n->get_num_args(); ++i) {
+                z = bv.mk_bv_and(z, n->get_arg(i));
+                ctx.internalize(z);
+            }
+            internalize_set(n, expr2pdd(z));
+        }
+    }
+
+    void solver::internalize_lshr(app* n) {
+        expr* x, * y;
+        VERIFY(bv.is_bv_lshr(n, x, y));
+        m_core.lshr(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+    }
+
+    void solver::internalize_shl(app* n) {
+        expr* x, * y;
+        VERIFY(bv.is_bv_shl(n, x, y));
+        m_core.shl(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+    }  
+
     void solver::internalize_urem_i(app* rem) {
         expr* x, *y;
         euf::enode* n = expr2enode(rem);
@@ -389,14 +417,12 @@ namespace polysat {
     }
 
     void solver::internalize_extract(app* e) {
-        auto p = var2pdd(expr2enode(e)->get_th_var(get_id()));
+        var2pdd(expr2enode(e)->get_th_var(get_id()));
-        internalize_set(e, p);
     }
 
     void solver::internalize_concat(app* e) {
         SASSERT(bv.is_concat(e));
-        auto p = var2pdd(expr2enode(e)->get_th_var(get_id()));
+        var2pdd(expr2enode(e)->get_th_var(get_id()));
-        internalize_set(e, p);
     }
 
     void solver::internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn) {

src/sat/smt/polysat_model.cpp

@@ -18,11 +18,34 @@ Author:
 #include "params/bv_rewriter_params.hpp"
 #include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
+#include "ast/rewriter/bv_rewriter.h"
 
 namespace polysat {
 
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+        
+        if (m_use_intblast_model) {
+            expr_ref value(m);            
+            if (n->interpreted()) 
+                value = n->get_expr();
+            else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {
+                bv_rewriter rw(m);                
+                expr_ref_vector args(m);
+                for (auto arg : euf::enode_args(n))
+                    args.push_back(values.get(arg->get_root_id()));                    
+                rw.mk_app(n->get_decl(), args.size(), args.data(), value);
+                VERIFY(value);
+            }
+            else {
+                rational r = m_intblast.get_value(n->get_expr());
+                verbose_stream() << ctx.bpp(n) << " := " << r << "\n";
+                value = bv.mk_numeral(r, get_bv_size(n));
+            }
+            values.set(n->get_root_id(), value);
+            TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
+            return;
+        }
 #if 0
         auto p = expr2pdd(n->get_expr());
         rational val;
@@ -31,9 +54,24 @@ namespace polysat {
 #endif
     }   
 
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+        if (!is_app(n->get_expr()))
+            return false;
+        app* e = to_app(n->get_expr());
+        if (n->num_args() == 0) {
+            dep.insert(n, nullptr);
+            return true;
+        }
+        if (e->get_family_id() != bv.get_family_id())
+            return false;
+        for (euf::enode* arg : euf::enode_args(n))
+            dep.add(n, arg->get_root());
+        return true;
+    }
+
 
     bool solver::check_model(sat::model const& m) const {
-        return false;
+        return true;
     }
 
     void solver::finalize_model(model& mdl) {
@@ -53,6 +91,8 @@ namespace polysat {
         for (unsigned v = 0; v < get_num_vars(); ++v)
             if (m_var2pdd_valid.get(v, false))
                 out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
+        if (m_use_intblast_model)
+            m_intblast.display(out);
         return out;
     }
 }

src/sat/smt/polysat_solver.cpp

@@ -40,7 +40,7 @@ namespace polysat {
         m_intblast(ctx),
         m_lemma(ctx.get_manager())
     {
-        ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
+        // ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
     }
 
     unsigned solver::get_bv_size(euf::enode* n) {

src/sat/smt/polysat_solver.h

@@ -119,6 +119,9 @@ namespace polysat {
         void internalize_bnor(app* n);
         void internalize_bnand(app* n);
         void internalize_bxnor(app* n);
+        void internalize_band(app* n);
+        void internalize_lshr(app* n);
+        void internalize_shl(app* n);
         template<bool Signed, bool Reverse, bool Negated>
         void internalize_le(app* n);
         void internalize_zero_extend(app* n);
@@ -172,7 +175,7 @@ namespace polysat {
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override {}
-        euf::th_solver* clone(euf::solver& ctx) override { throw default_exception("nyi"); }
+        euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx, get_id()); }
         extension* copy(sat::solver* s) override { throw default_exception("nyi"); }
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
         void gc() override {}
@@ -190,6 +193,7 @@ namespace polysat {
         bool unit_propagate() override;
 
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
+        bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
 
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }