mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

Parallel solving (#7778)

Browse source 
* very basic setup

* ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* respect smt configuration parameter in elim_unconstrained simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* indentation

* add bash files for test runs

* add option to selectively disable variable solving for only ground expressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove verbose output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #7745

axioms for len(substr(...)) escaped due to nested rewriting

* ensure atomic constraints are processed by arithmetic solver

* #7739 optimization

add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.

* fix unsound len(substr) axiom

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* FreshConst is_sort (#7748)

* #7750

add pre-processing simplification

* Add parameter validation for selected API functions

* updates to ac-plugin

fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.

* enable passive, add check for bloom up-to-date

* add top-k fixed-sized min-heap priority queue for top scoring literals

* set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still

* fix bug in parallel solving batch setup

* fix bug

* allow for internalize implies

* disable pre-processing during cubing

* debugging

* remove default constructor

* remove a bunch of string copies

* Update euf_ac_plugin.cpp

include reduction rules in forward simplification

* Update euf_completion.cpp

try out restricting scope of equalities added by instantation

* Update smt_parallel.cpp

Drop non-relevant units from shared structures.

* process cubes as lists of individual lits

* merge

* Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734)

* Initial plan

* Add datatype type definitions to types.ts (work in progress)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype type definitions with working TypeScript compilation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Implement core datatype functionality with TypeScript compilation success

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype implementation with full Context integration and tests

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* chipping away at the new code structure

* comments

* debug infinite recursion and split cubes on existing split atoms that aren't in the cube

* share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing

* merge

* fix #7603: race condition in Ctrl-C handling (#7755)

* fix #7603: race condition in Ctrl-C handling

* fix race in cancel_eh

* fix build

* add arithemtic saturation

* add an option to register callback on quantifier instantiation

Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation

* missing new closure

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add Z3_solver_propagate_on_binding to ml callback declarations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add python file

Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local>

* debug under defined calls

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more untangle params

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* precalc parameters to define the eval order

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove a printout

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename a Python file

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add on_binding callbacks across APIs

update release notes,
add to Java, .Net, C++

* use jboolean in Native interface

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* register on_binding attribute

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix java build for java bindings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid interferring side-effects in function calls

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove theory_str and classes that are only used by it

* remove automata from python build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove ref to theory_str

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* get the finest factorizations before project

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename add_lcs to add_lc

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints

* initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel?

* Update RELEASE_NOTES.md

* resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback

* remove unused square-free check

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add some debug prints and impelement internal polynomial fix

* add some comments and debug m_assumptions_used

* redo greedy->frugal strategy so we don't split on existing cubes in frugal at all (eliminate the incorrect/wasteful step by processing current batch first)

* set up initial scaffolding for sharing clauses between threads and batch manager. needs some reworking/debug still

* turn off logging at level 0 for testing

* add max thread conflicts backoff

* resolve bug about not popping local ctx to base level before collecting shared lits

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com>
Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Ilana Shapiro 2025-08-13 11:40:36 -07:00 • committed by GitHub
parent 49056db676
commit 0cb821ba30
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 22 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/smt_parallel.cpp
View file

@ -54,15 +54,15 @@ namespace smt {
b.set_exception("context cancelled"); b.set_exception("context cancelled");
return; return;
} }
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n");
lbool r = check_cube(cube); lbool r = check_cube(cube);
if (m.limit().is_canceled()) { if (m.limit().is_canceled()) {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " context cancelled\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " context cancelled\n");
return; return;
} }
switch (r) { switch (r) {
case l_undef: { case l_undef: {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found undef cube\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found undef cube\n");
// return unprocessed cubes to the batch manager // return unprocessed cubes to the batch manager
// add a split literal to the batch manager. // add a split literal to the batch manager.
// optionally process other cubes and delay sending back unprocessed cubes to batch manager. // optionally process other cubes and delay sending back unprocessed cubes to batch manager.
@ -74,7 +74,7 @@ namespace smt {
break; break;
} }
case l_true: { case l_true: {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found sat cube\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found sat cube\n");
model_ref mdl; model_ref mdl;
ctx->get_model(mdl); ctx->get_model(mdl);
b.set_sat(l2g, *mdl); b.set_sat(l2g, *mdl);
@ -86,11 +86,11 @@ namespace smt {
// share with batch manager. // share with batch manager.
// process next cube. // process next cube.
expr_ref_vector const& unsat_core = ctx->unsat_core(); expr_ref_vector const& unsat_core = ctx->unsat_core();
IF_VERBOSE(0, verbose_stream() << "unsat core: " << unsat_core << "\n"); IF_VERBOSE(1, verbose_stream() << "unsat core: " << unsat_core << "\n");
// If the unsat core only contains assumptions, // If the unsat core only contains assumptions,
// unsatisfiability does not depend on the current cube and the entire problem is unsat. // unsatisfiability does not depend on the current cube and the entire problem is unsat.
if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " determined formula unsat\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " determined formula unsat\n");
b.set_unsat(l2g, unsat_core); b.set_unsat(l2g, unsat_core);
return; return;
} }
@ -98,7 +98,7 @@ namespace smt {
if (asms.contains(e)) if (asms.contains(e))
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n");
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
break; break;
} }
@ -112,7 +112,7 @@ namespace smt {
ast_translation g2l(p.ctx.m, m); ast_translation g2l(p.ctx.m, m);
for (auto e : _asms) for (auto e : _asms)
asms.push_back(g2l(e)); asms.push_back(g2l(e));
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n");
m_smt_params.m_preprocess = false; m_smt_params.m_preprocess = false;
ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
context::copy(p.ctx, *ctx, true); context::copy(p.ctx, *ctx, true);
@ -124,8 +124,9 @@ namespace smt {
void parallel::worker::share_units(ast_translation& l2g) { void parallel::worker::share_units(ast_translation& l2g) {
// Collect new units learned locally by this worker and send to batch manager // Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl();
unsigned sz = ctx->assigned_literals().size(); unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
literal lit = ctx->assigned_literals()[j]; literal lit = ctx->assigned_literals()[j];
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
if (lit.sign()) if (lit.sign())
@ -151,7 +152,7 @@ namespace smt {
for (expr* e : new_clauses) { for (expr* e : new_clauses) {
expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!! expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!!
ctx->assert_expr(local_clause); // assert the clause in the local context ctx->assert_expr(local_clause); // assert the clause in the local context
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n");
} }
} }
@ -169,6 +170,7 @@ namespace smt {
} }
lbool parallel::worker::check_cube(expr_ref_vector const& cube) { lbool parallel::worker::check_cube(expr_ref_vector const& cube) {
IF_VERBOSE(1, verbose_stream() << "Worker " << id << " checking cube\n";);
for (auto& atom : cube) for (auto& atom : cube)
asms.push_back(atom); asms.push_back(atom);
lbool r = l_undef; lbool r = l_undef;
@ -187,7 +189,7 @@ namespace smt {
b.set_exception("unknown exception"); b.set_exception("unknown exception");
} }
asms.shrink(asms.size() - cube.size()); asms.shrink(asms.size() - cube.size());
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";);
return r; return r;
} }
@ -433,7 +435,7 @@ namespace smt {
if (top_lits.size() >= k) if (top_lits.size() >= k)
break; break;
} }
IF_VERBOSE(0, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n"); IF_VERBOSE(1, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n");
return top_lits; return top_lits;
} }

14
src/smt/smt_parallel.h
View file

@ -55,7 +55,7 @@ namespace smt {
// called from batch manager to cancel other workers if we've reached a verdict // called from batch manager to cancel other workers if we've reached a verdict
void cancel_workers() { void cancel_workers() {
IF_VERBOSE(0, verbose_stream() << "Canceling workers\n"); IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
for (auto& w : p.m_workers) for (auto& w : p.m_workers)
w->cancel(); w->cancel();
} }
@ -96,13 +96,15 @@ namespace smt {
expr_ref_vector asms; expr_ref_vector asms;
smt_params m_smt_params; smt_params m_smt_params;
scoped_ptr<context> ctx; scoped_ptr<context> ctx;
unsigned m_max_conflicts = 0; unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run.
unsigned m_max_thread_conflicts = 100; unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on
unsigned m_num_shared_units = 0; unsigned m_num_shared_units = 0;
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
void share_units(ast_translation& l2g); void share_units(ast_translation& l2g);
lbool check_cube(expr_ref_vector const& cube); lbool check_cube(expr_ref_vector const& cube);
void update_max_thread_conflicts() {} // allow for backoff scheme of conflicts within the thread for cube timeouts. void update_max_thread_conflicts() {
m_max_thread_conflicts *= 2;
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
public: public:
worker(unsigned id, parallel& p, expr_ref_vector const& _asms); worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
void run(); void run();
@ -110,11 +112,11 @@ namespace smt {
void collect_shared_clauses(ast_translation& g2l); void collect_shared_clauses(ast_translation& g2l);
void cancel() { void cancel() {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " canceling\n"); IF_VERBOSE(1, verbose_stream() << "Worker " << id << " canceling\n");
m.limit().cancel(); m.limit().cancel();
} }
void collect_statistics(::statistics& st) const { void collect_statistics(::statistics& st) const {
IF_VERBOSE(0, verbose_stream() << "Collecting statistics for worker " << id << "\n"); IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n");
ctx->collect_statistics(st); ctx->collect_statistics(st);
} }
reslimit& limit() { reslimit& limit() {