From d72938ba9a7fae52624d3a0d94cc0a017651f441 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 Dec 2023 13:00:43 -0800
Subject: [PATCH] integrate intblast solver

---
 src/sat/smt/intblast_solver.cpp | 26 ++++++++++++++++++++++----
 src/sat/smt/intblast_solver.h   |  2 ++
 src/sat/smt/polysat_solver.cpp  | 30 +++++++++++++++++++++++++++++-
 src/sat/smt/polysat_solver.h    |  4 +++-
 4 files changed, 56 insertions(+), 6 deletions(-)

diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 6586408fe..80fbc845e 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -233,6 +233,7 @@ namespace intblast {
             literals.push_back(a);                
         }
 
+        m_core.reset();
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
         expr_ref_vector es(m);
@@ -241,11 +242,23 @@ namespace intblast {
 
         translate(es);
 
-        for (auto e : es)
-            m_solver->assert_expr(e);
-        
+        for (auto const& [src, vi] : m_vars) {
+            auto const& [v, b] = vi;
+            m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
+            m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
+        }
                
-        lbool r = m_solver->check_sat(0, nullptr);
+        lbool r = m_solver->check_sat(es);
+
+        if (r == l_false) {
+            expr_ref_vector core(m);
+            m_solver->get_unsat_core(core);
+            obj_map<expr, unsigned> e2index;
+            for (unsigned i = 0; i < es.size(); ++i)
+                e2index.insert(es.get(i), i);
+            for (auto e : core)
+                m_core.push_back(literals[e2index[e]]);
+        }
 
         return r;
     };
@@ -573,6 +586,7 @@ namespace intblast {
             }
             break;
         }
+<<<<<<< HEAD
         case OP_EXTRACT: {
             unsigned lo, hi;
             expr* old_arg;
@@ -846,6 +860,10 @@ namespace intblast {
             set_translated(e, e);
         else
             set_translated(e, m.mk_app(e->get_decl(), m_args));
+=======
+        for (unsigned i = 0; i < es.size(); ++i) 
+            es[i] = translated[es.get(i)];
+>>>>>>> 09c2e0dd6 (integrate intblast solver)
     }
 
     rational solver::get_value(expr* e) const {
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index ebb44c18a..c7c93be07 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -135,6 +135,8 @@ namespace intblast {
 
         void eq_internalized(euf::enode* n) override;
 
+        sat::literal_vector const& unsat_core();
+
         rational get_value(expr* e) const;
 
     };
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 460501cd0..8baf05de5 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -31,6 +31,8 @@ The result of polysat::core::check is one of:
 #include "sat/smt/polysat/polysat_umul_ovfl.h"
 
 
+
+
 namespace polysat {
 
     solver::solver(euf::solver& ctx, theory_id id):
@@ -38,6 +40,7 @@ namespace polysat {
         bv(ctx.get_manager()),
         m_autil(ctx.get_manager()),
         m_core(*this),
+        m_intblast(ctx),
         m_lemma(ctx.get_manager())
     {
         ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
@@ -56,7 +59,31 @@ namespace polysat {
     }
 
     sat::check_result solver::check() {
-        return m_core.check();
+        switch (m_core.check()) {
+        case sat::check_result::CR_DONE:
+            return sat::check_result::CR_DONE;
+        case sat::check_result::CR_CONTINUE:
+            return sat::check_result::CR_CONTINUE;
+        case sat::check_result::CR_GIVEUP: {
+            if (!m.inc())
+                return sat::check_result::CR_GIVEUP;
+            switch (m_intblast.check()) {
+            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;
+            }
+        }
+        }
     }
 
     void solver::asserted(literal l) {
@@ -136,6 +163,7 @@ namespace polysat {
 
         unsigned num_scopes = s().scope_lvl() - m_lemma_level;
 
+        NOT_IMPLEMENTED_YET();
         // s().pop_reinit(num_scopes);
 
         sat::literal_vector lits;
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index b5e69c36a..e1a9221e9 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -19,6 +19,7 @@ Author:
 #include "sat/smt/sat_th.h"
 #include "math/dd/dd_pdd.h"
 #include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/intblast_solver.h"
 
 namespace euf {
     class solver;
@@ -57,7 +58,8 @@ namespace polysat {
         arith_util               m_autil;
         stats                    m_stats;
         core                     m_core;
-        polysat_proof            m_proof;
+        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