updates to poly

src/sat/smt/arith_solver.cpp

@@ -628,9 +628,6 @@ namespace arith {
         }
         else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
             anum const& an = nl_value(v, m_nla->tmp1());
-
-
-
             if (a.is_int(o) && !m_nla->am().is_int(an))
                 value = a.mk_numeral(rational::zero(), a.is_int(o));
             else

src/sat/smt/polysat/core.cpp

@@ -177,10 +177,9 @@ namespace polysat {
             s.set_lemma(m_viable.get_core(), m_viable.explain());
             // propagate_unsat_core();        
             return sat::check_result::CR_CONTINUE;
-        case find_t::singleton: {
+        case find_t::singleton: 
             s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
             return sat::check_result::CR_CONTINUE;        
-        }
         case find_t::multiple:  
             s.add_eq_literal(m_var, m_value);
             return sat::check_result::CR_CONTINUE;

src/sat/smt/polysat/core.h

@@ -60,10 +60,10 @@ namespace polysat {
         // attributes associated with variables
         vector<pdd>             m_vars;                       // for each variable a pdd
         vector<rational>        m_values;                     // current value of assigned variable
-        svector<dependency>     m_justification;  // justification for assignment
+        svector<dependency>     m_justification;              // justification for assignment
-        activity                m_activity;                  // activity of variables
+        activity                m_activity;                   // activity of variables
-        var_queue<activity>     m_var_queue;                 // priority queue of variables to assign
+        var_queue<activity>     m_var_queue;                  // priority queue of variables to assign
-        vector<unsigned_vector> m_watch;                     // watch lists for variables for constraints on m_prop_queue where they occur
+        vector<unsigned_vector> m_watch;                      // watch lists for variables for constraints on m_prop_queue where they occur
 
         // values to split on
         rational    m_value;
@@ -101,6 +101,7 @@ namespace polysat {
         constraint_id register_constraint(signed_constraint& sc, dependency d);
         bool propagate();
         void assign_eh(constraint_id idx, bool sign, unsigned level);
+        pvar next_var() { return m_var_queue.next_var(); }
 
         pdd value(rational const& v, unsigned sz);
         pdd subst(pdd const&);

src/sat/smt/polysat/op_constraint.cpp

@@ -96,7 +96,21 @@ namespace polysat {
     }
 
     lbool op_constraint::eval_ashr(pdd const& p, pdd const& q, pdd const& r) {
-        NOT_IMPLEMENTED_YET();
+        auto& m = p.manager();
+        if (r.is_val() && p.is_val() && q.is_val()) {
+            auto M = m.max_value();
+            auto N = M + 1;
+            if (p.val() >= N/2) {
+                if (q.val() >= m.power_of_2())
+                    return to_lbool(r.val() == M);
+                unsigned k = q.val().get_unsigned();
+                return to_lbool(r.val() == p.val() - rational::power_of_two(k));
+            }
+            else
+                return eval_lshr(p, q, r);
+        }
+        if (q.is_val() && q.is_zero() && p == r)
+            return l_true;
         return l_undef;
     }
 

src/sat/smt/polysat_model.cpp

@@ -24,11 +24,6 @@ namespace polysat {
 
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {        
-        
-        if (m_use_intblast_model) {
-            m_intblast.add_value(n, mdl, values);
-            return;
-        }
         auto p = expr2pdd(n->get_expr());
         rational val;
         if (!m_core.try_eval(p, val)) {
@@ -82,8 +77,7 @@ 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);
-            m_intblast.display(out);
         return out;
     }
 }

src/sat/smt/polysat_solver.cpp

@@ -61,25 +61,36 @@ namespace polysat {
             return sat::check_result::CR_DONE;
         case sat::check_result::CR_CONTINUE:
             return sat::check_result::CR_CONTINUE;
-        case sat::check_result::CR_GIVEUP: {
+        case sat::check_result::CR_GIVEUP: 
-            if (!m.inc())
+            return intblast();        
-                return sat::check_result::CR_GIVEUP;
-            switch (m_intblast.check_solver_state()) {
-            case l_true:
-                trail().push(value_trail(m_use_intblast_model));
-                m_use_intblast_model = true;
-                return sat::check_result::CR_DONE;
-            case l_false: {
-                auto core = m_intblast.unsat_core();
-                for (auto& lit : core)
-                    lit.neg();
-                s().add_clause(core.size(), core.data(), sat::status::th(true, get_id(), nullptr));
-                return sat::check_result::CR_CONTINUE;
-            }
-            case l_undef:
-                return sat::check_result::CR_GIVEUP;
-            }
         }
+        UNREACHABLE();
+        return sat::check_result::CR_GIVEUP;
+    }
+
+    sat::check_result solver::intblast() {
+        if (!m.inc())
+            return sat::check_result::CR_GIVEUP;
+        switch (m_intblast.check_solver_state()) {
+        case l_true: {
+            pvar pv = m_core.next_var();
+            auto v = m_pddvar2var[pv];
+            auto n = var2expr(v);
+            auto val = m_intblast.get_value(n);
+            sat::literal lit = eq_internalize(n, bv.mk_numeral(val, get_bv_size(v)));
+            s().set_phase(lit);
+            return sat::check_result::CR_CONTINUE;
+        }
+        case l_false: {
+            IF_VERBOSE(2, verbose_stream() << "unsat core: " << m_intblast.unsat_core() << "\n");
+            auto core = m_intblast.unsat_core();
+            for (auto& lit : core)
+                lit.neg();
+            s().add_clause(core.size(), core.data(), sat::status::th(true, get_id(), nullptr));
+            return sat::check_result::CR_CONTINUE;
+        }
+        case l_undef:
+            return sat::check_result::CR_GIVEUP;
         }
         UNREACHABLE();
         return sat::check_result::CR_GIVEUP;

src/sat/smt/polysat_solver.h

@@ -59,7 +59,6 @@ namespace polysat {
         stats                    m_stats;
         core                     m_core;
         intblast::solver         m_intblast;
-        bool                     m_use_intblast_model = false;
 
         vector<pdd>              m_var2pdd;                   // theory_var 2 pdd
         bool_vector              m_var2pdd_valid;             // valid flag
@@ -73,6 +72,8 @@ namespace polysat {
         unsigned m_lemma_level = 0;
         expr_ref_vector m_lemma;
 
+        sat::check_result intblast();
+
         // internalize
         bool visit(expr* e) override;
         bool visited(expr* e) override;