diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 33753254451..d2f9792777f 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -91,7 +91,7 @@ namespace bv { lbool sls::search() { // init and init_eval were invoked - unsigned n = 0; + unsigned n = 0; for (; n++ < m_config.m_max_repairs && m.inc(); ) { ++m_stats.m_moves; auto [down, e] = next_to_repair(); @@ -164,7 +164,7 @@ namespace bv { return was_repaired; } - void sls::try_repair_up(app* e) { + void sls::try_repair_up(app* e) { m_repair_up.remove(e->get_id()); if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) m_repair_down.insert(e->get_id()); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index f64326d22cd..0e2ecc76835 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -130,7 +130,7 @@ namespace bv { void sls_eval::init_eval_bv(app* e) { if (bv.is_bv(e)) { auto& v = wval0(e); - v.set(wval1(e)); + v.set(wval1(e).bits); } else if (m.is_bool(e)) m_eval.setx(e->get_id(), bval1_bv(e), false); @@ -299,10 +299,10 @@ namespace bv { return bval0(e); } - svector& sls_eval::wval1(app* e) const { + sls_valuation& sls_eval::wval1(app* e) const { auto& val = *m_values1[e->get_id()]; wval1(e, val); - return val.bits; + return val; } void sls_eval::wval1(app* e, sls_valuation& val) const { @@ -429,8 +429,6 @@ namespace bv { break; } case OP_CONCAT: { - if (e->get_num_args() != 2) - verbose_stream() << mk_bounded_pp(e, m) << "\n"; SASSERT(e->get_num_args() == 2); auto const& a = wval0(e->get_arg(0)); auto const& b = wval0(e->get_arg(1)); @@ -1005,8 +1003,8 @@ namespace bv { } else { // b := a - e - a.set_sub(m_tmp, a.bits, e.bits); - a.set_repair(random_bool(), m_tmp); + b.set_sub(m_tmp, a.bits, e.bits); + b.set_repair(random_bool(), m_tmp); } return true; } @@ -1186,7 +1184,6 @@ namespace bv { if (a.is_zero(m_tmp2)) return false; if (!a.get_at_least(m_tmp2, m_tmp)) { - verbose_stream() << "could not get at least\n"; return false; } } @@ -1571,7 +1568,7 @@ namespace bv { return true; } if (bv.is_bv(e)) - return wval0(e).try_set(wval1(to_app(e))); + return wval0(e).try_set(wval1(to_app(e)).bits); return false; } } diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index ad9a06fb5ad..3c8025fe7c6 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -136,8 +136,8 @@ namespace bv { */ bool bval1(app* e) const; bool can_eval1(app* e) const; - - svector& wval1(app* e) const; + + sls_valuation& wval1(app* e) const; /** * Override evaluaton. diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index a1ec5257fb7..0a020c290a3 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -202,6 +202,7 @@ namespace bv { } std::ostream& display(std::ostream& out) const { + out << "V:"; out << std::hex; auto print_bits = [&](svector const& v) { bool nz = false; @@ -215,7 +216,7 @@ namespace bv { }; print_bits(bits); - out << " "; + out << " fix:"; print_bits(fixed); if (!eq(lo, hi)) { diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index e5d35a4f968..7747b65cb90 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -46,6 +46,7 @@ z3_add_component(sat_smt q_solver.cpp recfun_solver.cpp sat_th.cpp + sls_solver.cpp specrel_solver.cpp tseitin_theory_checker.cpp user_solver.cpp diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp new file mode 100644 index 00000000000..1466b1b4115 --- /dev/null +++ b/src/sat/smt/sls_solver.cpp @@ -0,0 +1,74 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + sls_solver + +Abstract: + + Interface to Concurrent SLS solver + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-21 + +--*/ + +#include "sat/smt/sls_solver.h" +#include "sat/smt/euf_solver.h" +#include "ast/sls/bv_sls.h" + + +namespace sls { + + solver::solver(euf::solver& ctx): + th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {} + + solver::~solver() { + if (m_rlimit) { + m_rlimit->cancel(); + m_thread.join(); + } + } + + void solver::push_core() { + if (s().scope_lvl() == s().search_lvl() + 1) + init_local_search(); + } + + void solver::pop_core(unsigned n) { + if (s().scope_lvl() - n <= s().search_lvl()) + sample_local_search(); + } + + void solver::simplify() { + + } + + + void solver::init_local_search() { + if (m_rlimit) { + m_rlimit->cancel(); + m_thread.join(); + } + // set up state for local search solver here + auto* bvsls = alloc(bv::sls, m); + // walk clauses, add them + // walk trail stack until search level, add units + // encapsulate bvsls within the arguments of run-local-search. + // ensure bvsls does not touch ast-manager. + m_thread = std::thread([this]() { run_local_search(*this); }); + m_rlimit = alloc(reslimit); + m_rlimit->push_child(&s().rlimit()); + } + + void solver::sample_local_search() { + + } + + void solver::run_local_search(solver& s) { + + } + +} diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h new file mode 100644 index 00000000000..2a8f07c0b6a --- /dev/null +++ b/src/sat/smt/sls_solver.h @@ -0,0 +1,59 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + sls_solver + +Abstract: + + Interface to Concurrent SLS solver + +Author: + + Nikolaj Bjorner (nbjorner) 2024-02-21 + +--*/ +#pragma once + +#include "sat/smt/sat_th.h" +#include "util/rlimit.h" + +namespace euf { + class solver; +} + +namespace sls { + + class solver : public euf::th_euf_solver { + std::atomic m_result; + std::atomic m_completed; + std::thread m_thread; + scoped_ptr m_rlimit; + + void run_local_search(solver& s); + void init_local_search(); + void sample_local_search(); + public: + solver(euf::solver& ctx); + ~solver(); + + void push_core() override; + void pop_core(unsigned n) override; + void simplify() override; + + sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; } + void internalize(expr* e) override { UNREACHABLE(); } + th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } + + + bool unit_propagate() override { return false; } + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); } + sat::check_result check() override { return sat::check_result::CR_DONE; } + std::ostream & display(std::ostream & out) const override { return out; } + std::ostream & display_justification(std::ostream & out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; } + std::ostream & display_constraint(std::ostream & out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; } + + }; + +}