-
Notifications
You must be signed in to change notification settings - Fork 1.5k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
659e384
commit cf72a91
Showing
7 changed files
with
146 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) { | ||
|
||
} | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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<lbool> m_result; | ||
std::atomic<bool> m_completed; | ||
std::thread m_thread; | ||
scoped_ptr<reslimit> 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; } | ||
|
||
}; | ||
|
||
} |