mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

comments

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-05 10:15:06 -07:00
parent 3982b291a3
commit 2fce048c61
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_parallel.cpp
View file

@ -66,7 +66,7 @@ namespace smt {
return; return;
} }
case l_false: case l_false:
// if unsat core only contains assumptions, then unsat // if unsat core only contains (external) assumptions (i.e. all the unsat core are asms), then unsat and return as this does NOT depend on cubes
// otherwise, extract lemmas that can be shared (units (and unsat core?)). // otherwise, extract lemmas that can be shared (units (and unsat core?)).
// share with batch manager. // share with batch manager.
// process next cube. // process next cube.
@ -88,6 +88,9 @@ namespace smt {
} }
// PUT THE LOGIC FOR LEARNING FROM UNSAT CORE HERE IF THE CUBE INTERSECTS WITH IT!!!
// THERE IS AN EDGE CASE: IF ALL THE CUBES ARE UNSAT, BUT DEPEND ON NONEMPTY ASSUMPTIONS, NEED TO TAKE THE UNION OF THESE ASMS WHEN LEARNING FROM UNSAT CORE
// DON'T CODE THIS CASE YET: WE ARE JUST TESTING WITH EMPTY ASMS FOR NOW (I.E. WE ARE NOT PASSING IN ASMS). THIS DOES NOT APPLY TO THE INTERNAL "LEARNED" UNSAT CORE
lbool parallel::worker::check_cube(expr_ref_vector const& cube) { lbool parallel::worker::check_cube(expr_ref_vector const& cube) {
for (auto& atom : cube) { for (auto& atom : cube) {
asms.push_back(atom); asms.push_back(atom);
@ -132,6 +135,7 @@ namespace smt {
} }
} }
// CALL GET_SPLIT_ATOMS AS ARGUMENT TO RETURN_CUBES
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms) { void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
for (auto & c : cubes) { for (auto & c : cubes) {
@ -270,6 +274,8 @@ namespace smt {
unsigned_vector unit_lim; unsigned_vector unit_lim;
for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0); for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0);
// we just want to share lemmas and have a way of remembering how they are shared -- this is the next step
// (this needs to be reworked)
std::function<void(void)> collect_units = [&,this]() { std::function<void(void)> collect_units = [&,this]() {
//return; -- has overhead //return; -- has overhead
for (unsigned i = 0; i < num_threads; ++i) { for (unsigned i = 0; i < num_threads; ++i) {

3
src/smt/smt_parallel.h
View file

@ -32,7 +32,7 @@ namespace smt {
std::mutex mux; std::mutex mux;
expr_ref_vector m_split_atoms; // atoms to split on expr_ref_vector m_split_atoms; // atoms to split on
vector<expr_ref_vector> m_cubes; vector<expr_ref_vector> m_cubes;
lbool m_result = l_false; lbool m_result = l_false; // want states: init/undef, canceled/exception, sat, unsat
unsigned m_max_batch_size = 10; unsigned m_max_batch_size = 10;
public: public:
@ -55,6 +55,7 @@ namespace smt {
// //
void return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms); void return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms);
void share_lemma(ast_translation& l2g, expr* lemma); void share_lemma(ast_translation& l2g, expr* lemma);
void cancel_workers(); // called from batch manager to cancel other workers if we've reached a verdict
lbool get_result() const { return m.limit().is_canceled() ? l_undef : m_result; } lbool get_result() const { return m.limit().is_canceled() ? l_undef : m_result; }
}; };