Skip to content

Commit 5061125

Browse files
ilanashapiroNikolajBjornerhumnrdblenunoplopesCopilot
authored
Parallel solving (#7832)
* very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 <[email protected]> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <[email protected]> * add python file Signed-off-by: Lev Nachmanson <[email protected]> * debug under defined calls Signed-off-by: Lev Nachmanson <[email protected]> * more untangle params Signed-off-by: Lev Nachmanson <[email protected]> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <[email protected]> * remove a printout Signed-off-by: Lev Nachmanson <[email protected]> * rename a Python file Signed-off-by: Lev Nachmanson <[email protected]> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <[email protected]> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <[email protected]> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <[email protected]> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <[email protected]> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <[email protected]> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <[email protected]> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <[email protected]> * 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 <[email protected]> * add some debug prints and impelement internal polynomial fix * restore the square-free check Signed-off-by: Lev Nachmanson <[email protected]> * 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 * Add .github/copilot-instructions.md with comprehensive Z3 development guide (#7766) * Initial plan * Add comprehensive .github/copilot-instructions.md with validated build commands and timing Co-authored-by: NikolajBjorner <[email protected]> * Remove test_example binary file from repository Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Bump actions/checkout from 4 to 5 (#7773) Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v4...v5) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '5' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * turn off logging at level 0 for testing * add max thread conflicts backoff * Parallel solving (#7775) * very basic setup * very basic setup (#7741) * add score access and reset Signed-off-by: Nikolaj Bjorner <[email protected]> * added notes Signed-off-by: Nikolaj Bjorner <[email protected]> * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * add bash files for test runs * fix compilation Signed-off-by: Nikolaj Bjorner <[email protected]> * more notes Signed-off-by: Nikolaj Bjorner <[email protected]> * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * Update PARALLEL_PROJECT_NOTES.md * add top-k fixed-sized min-heap priority queue for top scoring literals * fixed-size min-heap for tracking top-k literals (#7752) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> * 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 * debugging * process cubes as lists of individual lits * Parallel solving (#7756) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 * process cubes as lists of individual lits --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> * snapshot Signed-off-by: Nikolaj Bjorner <[email protected]> * pair programming Signed-off-by: Nikolaj Bjorner <[email protected]> * pair programming Signed-off-by: Nikolaj Bjorner <[email protected]> * merge * chipping away at the new code structure * Parallel solving (#7758) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * chipping away at the new code structure --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * updates Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 * Parallel solving (#7759) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * updates Signed-off-by: Nikolaj Bjorner <[email protected]> * simplify output Signed-off-by: Nikolaj Bjorner <[email protected]> * merge * 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? * Parallel solving (#7769) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 * 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? --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * Parallel solving (#7771) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 <[email protected]> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <[email protected]> * add python file Signed-off-by: Lev Nachmanson <[email protected]> * debug under defined calls Signed-off-by: Lev Nachmanson <[email protected]> * more untangle params Signed-off-by: Lev Nachmanson <[email protected]> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <[email protected]> * remove a printout Signed-off-by: Lev Nachmanson <[email protected]> * rename a Python file Signed-off-by: Lev Nachmanson <[email protected]> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <[email protected]> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <[email protected]> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <[email protected]> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <[email protected]> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <[email protected]> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <[email protected]> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <[email protected]> * 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 --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]> * code and notes * 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 * Parallel solving (#7774) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 <[email protected]> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <[email protected]> * add python file Signed-off-by: Lev Nachmanson <[email protected]> * debug under defined calls Signed-off-by: Lev Nachmanson <[email protected]> * more untangle params Signed-off-by: Lev Nachmanson <[email protected]> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <[email protected]> * remove a printout Signed-off-by: Lev Nachmanson <[email protected]> * rename a Python file Signed-off-by: Lev Nachmanson <[email protected]> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <[email protected]> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <[email protected]> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <[email protected]> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <[email protected]> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <[email protected]> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <[email protected]> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <[email protected]> * 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 <[email protected]> * 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 --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]> * sign of life Signed-off-by: Nikolaj Bjorner <[email protected]> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <[email protected]> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <[email protected]> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <[email protected]> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <[email protected]> * turn off logging at level 0 for testing * add max thread conflicts backoff --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]> * fix #7776 * add > operator as shorthand for Array * updates to euf completion * resolve bug about not popping local ctx to base level before collecting shared lits * Add virtual translate method to solver_factory class (#7780) * Initial plan * Add virtual translate method to solver_factory base class and all implementations Co-authored-by: NikolajBjorner <[email protected]> * Add documentation for the translate method in solver_factory Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * put return_cubes under lock * Revert "resolve bug about not popping local ctx to base level before collecting shared lits" This reverts commit bba1111. * Update seq_rewriter.cpp * fix releaseNotesSource to inline Signed-off-by: Nikolaj Bjorner <[email protected]> * Use solver factory translate method in Z3_solver_translate (#7782) * Initial plan * Fix Z3_solver_translate to use solver factory translate method Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Revert "Parallel solving (#7775)" (#7777) This reverts commit c8e866f. * remove upload artifact for azure-pipeline Signed-off-by: Nikolaj Bjorner <[email protected]> * Fix compilation warning: add missing is_passive_eq case to switch statement (#7785) * Initial plan * Fix compilation warning: add missing is_passive_eq case to switch statement Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Remove NugetPublishNightly stage from nightly.yaml (#7787) * Initial plan * Remove NugetPublishNightly stage from nightly.yaml Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * add more params * enable pypi public Signed-off-by: Nikolaj Bjorner <[email protected]> * Fix nullptr dereference in pp_symbol when handling null symbol names (#7790) * Initial plan * Fix nullptr dereference in pp_symbol with null symbol names Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * add option to control epsilon #7791 #7791 reports on using model values during lex optimization that break soft constraints. This is an artifact of using optimization where optimal values can be arbitrarily close to a rational. In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals. * update on euf * check for internalized in solve_for * fix #7792 add missing revert operations * update version number to 4.15.4 Signed-off-by: Nikolaj Bjorner <[email protected]> * fix #7753 * fix #7796 Signed-off-by: Nikolaj Bjorner <[email protected]> * Create centralized version management with VERSION.txt (#7802) * Initial plan * Create VERSION.txt and update CMakeLists.txt to read version from file Co-authored-by: NikolajBjorner <[email protected]> * Complete centralized version management system Co-authored-by: NikolajBjorner <[email protected]> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <[email protected]> * Create centralized version management with VERSION.txt Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * read version from VERSION.txt Signed-off-by: Nikolaj Bjorner <[email protected]> * fix version parse Signed-off-by: Nikolaj Bjorner <[email protected]> * fix parsing of version Signed-off-by: Nikolaj Bjorner <[email protected]> * add param tuning experiment in python * Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution (#7808) * Initial plan * Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Update nightly.yaml to match release.yml NuGet tool installer changes (#7810) * Initial plan * Update nightly.yaml to match release.yml NuGet tool installer changes Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Attempt at adding the README to the NuGet package (#7807) * Attempt at adding README to NuGet package * Forgot to enable publishing * add resources Signed-off-by: Nikolaj Bjorner <[email protected]> * remove resources directive again Signed-off-by: Nikolaj Bjorner <[email protected]> * Document how to use system-installed Z3 with CMake projects (#7809) * Initial plan * Add documentation for using system-installed Z3 with CMake Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Fix Julia bindings linker errors on Windows MSVC (#7794) * Initial plan * Fix Julia bindings linker errors on Windows MSVC Co-authored-by: NikolajBjorner <[email protected]> * Complete Julia bindings fix validation and testing Co-authored-by: NikolajBjorner <[email protected]> * Fix Julia bindings linker errors on Windows MSVC Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * add print for version file Signed-off-by: Nikolaj Bjorner <[email protected]> * add more logging to setup.py Signed-off-by: Nikolaj Bjorner <[email protected]> * try diferennt dirs Signed-off-by: Nikolaj Bjorner <[email protected]> * try src_dir_repo Signed-off-by: Nikolaj Bjorner <[email protected]> * try other dir Signed-off-by: Nikolaj Bjorner <[email protected]> * remove extra characters Signed-off-by: Nikolaj Bjorner <[email protected]> * more output Signed-off-by: Nikolaj Bjorner <[email protected]> * print dirs Signed-off-by: Nikolaj Bjorner <[email protected]> * copy VERSION from SRC_DIR Signed-off-by: Nikolaj Bjorner <[email protected]> * Move VERSION.txt to scripts directory and update all references (#7811) * Initial plan * Move VERSION.txt to scripts/ and update all references Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * clean up a little of the handling of VERSION.txt Signed-off-by: Nikolaj Bjorner <[email protected]> * add implementation and toggleable param for splitting frugal + choosing deepest cubes only * remove priority queue for top-k lits and replace with simple linear scan. the PQ implementation backend still remains in case we want to switch back * Add new configurations for SMT parallel settings * Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815) * fix: add generating META for ocamlfind. * Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers. * Trigger CI. * Debug. * Debug. * Debug. * Debug. * Debug. * Debug. * Hacky fix for ocaml building warning. * Fix typo and rename variables. * Fix cmake for ocaml test, using local libz3 explicit. * Rename configuration from 'shareconflicts' to 'depthsplitting' * Fix configuration for depth splitting in notes * rename variables * remove double tweak versioning Signed-off-by: Nikolaj Bjorner <[email protected]> * attempting to add backbone code, it does not work. still debugging the error: ASSERTION VIOLATION File: /home/t-ilshapiro/z3/src/ast/ast.cpp Line: 388 UNEXPECTED CODE WAS REACHED. I left a comment on the line where it's crashing * depth splitting now applies to greedy+frugal unless specified otherwise * debug the backbone crash (it was references not being counted) * iterative deepening experiment (no PQ yet). the hardness heuristic is still naive! * fix iterative deepening bug: unsolved cube needs to get re-enqueued even if we don't split it further --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Solal Pirelli <[email protected]> Co-authored-by: Shiwei Weng 翁士伟 <[email protected]>
1 parent 631a3a2 commit 5061125

File tree

3 files changed

+72
-17
lines changed

3 files changed

+72
-17
lines changed

‎src/params/smt_parallel_params.pyg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,4 +15,5 @@ def_module_params('smt_parallel',
1515
('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
1616
('depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'),
1717
('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
18+
('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
1819
))

‎src/smt/smt_parallel.cpp‎

Lines changed: 59 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -73,9 +73,50 @@ namespace smt {
7373
// optionally process other cubes and delay sending back unprocessed cubes to batch manager.
7474
if (!m_config.m_never_cube) {
7575
vector<expr_ref_vector> returned_cubes;
76-
returned_cubes.push_back(cube);
76+
returned_cubes.push_back(cube);
7777
auto split_atoms = get_split_atoms();
78-
b.return_cubes(m_l2g, returned_cubes, split_atoms);
78+
79+
if (m_config.m_iterative_deepening) {
80+
unsigned conflicts_before = ctx->m_stats.m_num_conflicts;
81+
unsigned propagations_before = ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations;
82+
unsigned decisions_before = ctx->m_stats.m_num_decisions;
83+
unsigned restarts_before = ctx->m_stats.m_num_restarts;
84+
85+
lbool r = check_cube(cube);
86+
87+
unsigned conflicts_after = ctx->m_stats.m_num_conflicts;
88+
unsigned propagations_after = ctx->m_stats.m_num_propagations + ctx->m_stats.m_num_bin_propagations;
89+
unsigned decisions_after = ctx->m_stats.m_num_decisions;
90+
unsigned restarts_after = ctx->m_stats.m_num_restarts;
91+
92+
// per-cube deltas
93+
unsigned conflicts_delta = conflicts_after - conflicts_before;
94+
unsigned propagations_delta = propagations_after - propagations_before;
95+
unsigned decisions_delta = decisions_after - decisions_before;
96+
unsigned restarts_delta = restarts_after - restarts_before;
97+
LOG_WORKER(1, " cube deltas: conflicts: " << conflicts_delta << " propagations: " << propagations_delta << " decisions: " << decisions_delta << " restarts: " << restarts_delta << "\n");
98+
99+
// tuned experimentally
100+
const double w_conflicts = 1.0;
101+
const double w_propagations = 0.001;
102+
const double w_decisions = 0.1;
103+
const double w_restarts = 0.5;
104+
105+
const double cube_hardness = w_conflicts * conflicts_delta +
106+
w_propagations * propagations_delta +
107+
w_decisions * decisions_delta +
108+
w_restarts * restarts_delta;
109+
110+
const double avg_hardness = b.update_avg_cube_hardness(cube_hardness);
111+
const double factor = 1; // can tune for multiple of avg hardness later
112+
bool should_split = cube_hardness >= avg_hardness * factor;
113+
LOG_WORKER(1, " cube hardness: " << cube_hardness << " avg: " << avg_hardness << " should-split: " << should_split << "\n");
114+
// we still need to call return_cubes, even if we don't split, since we need to re-enqueue the current unsolved cube to the batch manager!
115+
// should_split tells return_cubes whether to further split the unsolved cube.
116+
b.return_cubes(m_l2g, returned_cubes, split_atoms, should_split);
117+
} else {
118+
b.return_cubes(m_l2g, returned_cubes, split_atoms);
119+
}
79120
}
80121
if (m_config.m_backbone_detection) {
81122
expr_ref_vector backbone_candidates = find_backbone_candidates();
@@ -152,6 +193,7 @@ namespace smt {
152193
m_config.m_max_greedy_cubes = pp.max_greedy_cubes();
153194
m_config.m_num_split_lits = pp.num_split_lits();
154195
m_config.m_backbone_detection = pp.backbone_detection();
196+
m_config.m_iterative_deepening = pp.iterative_deepening();
155197

156198
// don't share initial units
157199
ctx->pop_to_base_lvl();
@@ -287,14 +329,16 @@ namespace smt {
287329

288330
void parallel::batch_manager::get_cubes(ast_translation& g2l, vector<expr_ref_vector>& cubes) {
289331
std::scoped_lock lock(mux);
290-
if (m_cubes.size() == 1 && m_cubes[0].empty()) {
332+
if (m_config.m_beam_search) {
333+
334+
} else if (m_cubes.size() == 1 && m_cubes[0].empty()) {
291335
// special initialization: the first cube is emtpy, have the worker work on an empty cube.
292336
cubes.push_back(expr_ref_vector(g2l.to()));
293337
return;
294338
}
295339

296340
for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) {
297-
if (m_config.m_depth_splitting_only) {
341+
if (m_config.m_depth_splitting_only || m_config.m_iterative_deepening) {
298342
// get the deepest set of cubes
299343
auto& deepest_cubes = m_cubes_depth_sets.rbegin()->second;
300344
unsigned idx = rand() % deepest_cubes.size();
@@ -447,9 +491,7 @@ namespace smt {
447491
------------------------------------------------------------------------------------------------------------------------------------------------------------
448492
Final thought (do this!): use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". -- want to do this. switch to frugal strategy after reaching size limit
449493
*/
450-
451-
// currenly, the code just implements the greedy strategy
452-
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker) {
494+
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker, const bool should_split) {
453495
// SASSERT(!m_config.never_cube());
454496

455497
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
@@ -500,7 +542,7 @@ namespace smt {
500542

501543
std::scoped_lock lock(mux);
502544
unsigned max_greedy_cubes = 1000;
503-
bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only;
545+
bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only && !m_config.m_iterative_deepening; // for iterative deepening, our hardness metric is cube-specific, so it only makes sense for frugal approach for now
504546
unsigned a_worker_start_idx = 0;
505547

506548
//
@@ -533,9 +575,8 @@ namespace smt {
533575
expr_ref_vector g_cube(l2g.to());
534576
for (auto& atom : c)
535577
g_cube.push_back(l2g(atom));
536-
unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added
537578

538-
if (m_config.m_depth_splitting_only) {
579+
if (m_config.m_depth_splitting_only || m_config.m_iterative_deepening) {
539580
// need to add the depth set if it doesn't exist yet
540581
if (m_cubes_depth_sets.find(g_cube.size()) == m_cubes_depth_sets.end()) {
541582
m_cubes_depth_sets[g_cube.size()] = vector<expr_ref_vector>();
@@ -571,7 +612,8 @@ namespace smt {
571612
expr_ref g_atom(l2g(A_worker[i]), l2g.to());
572613
if (!m_split_atoms.contains(g_atom))
573614
m_split_atoms.push_back(g_atom);
574-
if (m_config.m_depth_splitting_only) {
615+
if (should_split && (m_config.m_depth_splitting_only || m_config.m_iterative_deepening)) {
616+
IF_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom " << mk_bounded_pp(g_atom, m, 3) << "\n");
575617
add_split_atom_deepest_cubes(g_atom);
576618
} else {
577619
add_split_atom(g_atom, initial_m_cubes_size);
@@ -606,7 +648,7 @@ namespace smt {
606648

607649
double score_ratio = INFINITY; // score_pos / score_neg;
608650

609-
LOG_WORKER(0, " backbone candidate: " << mk_bounded_pp(candidate, m, 3) << " score_pos " << score_pos << " score_neg " << score_neg << "\n");
651+
LOG_WORKER(1, " backbone candidate: " << mk_bounded_pp(candidate, m, 3) << " score_pos " << score_pos << " score_neg " << score_neg << "\n");
610652

611653
// if score_neg is zero (and thus score_pos > 0 since at this point score_pos != score_neg)
612654
// then not(e) is a backbone candidate with score_ratio=infinity
@@ -643,8 +685,8 @@ namespace smt {
643685
backbone_candidates.push_back(p.second);
644686

645687
for (expr* e : backbone_candidates)
646-
LOG_WORKER(0, "selected backbone candidate: " << mk_bounded_pp(e, m, 3) << " head size " << ctx->m_lit_scores->size() << " num vars " << ctx->get_num_bool_vars() << "\n");
647-
688+
LOG_WORKER(1, "selected backbone candidate: " << mk_bounded_pp(e, m, 3) << " head size " << ctx->m_lit_scores->size() << " num vars " << ctx->get_num_bool_vars() << "\n");
689+
648690
return backbone_candidates;
649691
}
650692

@@ -680,12 +722,12 @@ namespace smt {
680722

681723
asms.shrink(sz); // restore assumptions
682724

683-
LOG_WORKER(0, " BACKBONE CHECK RESULT: " << r << "\n");
725+
LOG_WORKER(1, " BACKBONE CHECK RESULT: " << r << "\n");
684726

685727
if (r == l_false) {
686728
// c must be true in all models → backbone
687729
auto core = ctx->unsat_core();
688-
LOG_WORKER(0, "core: " << core << "\n");
730+
LOG_WORKER(1, "core: " << core << "\n");
689731
if (core.size() == 1) {
690732
expr* e = core.get(0);
691733
backbones.push_back(mk_not(m, e));
@@ -755,6 +797,7 @@ namespace smt {
755797
m_config.m_frugal_cube_only = sp.frugal_cube_only();
756798
m_config.m_never_cube = sp.never_cube();
757799
m_config.m_depth_splitting_only = sp.depth_splitting_only();
800+
m_config.m_iterative_deepening = sp.iterative_deepening();
758801
}
759802

760803
void parallel::batch_manager::collect_statistics(::statistics& st) const {

‎src/smt/smt_parallel.h‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ namespace smt {
5151
bool m_frugal_cube_only = false;
5252
bool m_never_cube = false;
5353
bool m_depth_splitting_only = false;
54+
bool m_iterative_deepening = false;
5455
};
5556
struct stats {
5657
unsigned m_max_cube_depth = 0;
@@ -73,6 +74,9 @@ namespace smt {
7374
obj_hashtable<expr> shared_clause_set; // for duplicate filtering on per-thread clause expressions
7475
vector<parameter_state> m_parameters_state;
7576

77+
double m_avg_cube_hardness = 0.0;
78+
unsigned m_solved_cube_count = 0;
79+
7680
// called from batch manager to cancel other workers if we've reached a verdict
7781
void cancel_workers() {
7882
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
@@ -103,11 +107,17 @@ namespace smt {
103107
// worker threads return unprocessed cubes to the batch manager together with split literal candidates.
104108
// the batch manager re-enqueues unprocessed cubes and optionally splits them using the split_atoms returned by this and workers.
105109
//
106-
void return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms);
110+
void return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms, const bool should_split=true);
107111
void report_assumption_used(ast_translation& l2g, expr* assumption);
108112
void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* e);
109113
expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
110114

115+
double update_avg_cube_hardness(double hardness) {
116+
m_avg_cube_hardness = (m_avg_cube_hardness * m_solved_cube_count + hardness) / (m_solved_cube_count + 1);
117+
m_solved_cube_count++;
118+
return m_avg_cube_hardness;
119+
}
120+
111121
void collect_statistics(::statistics& st) const;
112122
lbool get_result() const;
113123
};
@@ -126,6 +136,7 @@ namespace smt {
126136
unsigned m_max_greedy_cubes = 1000;
127137
unsigned m_num_split_lits = 2;
128138
bool m_backbone_detection = false;
139+
bool m_iterative_deepening = false;
129140
};
130141

131142
unsigned id; // unique identifier for the worker

0 commit comments

Comments
 (0)