Skip to content

Commit e126362

Browse files
ilanashapiroNikolajBjornerhumnrdblenunoplopesCopilot
authored
Parallel solving (#7845)
* 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](https://github.com/actions/checkout/compare/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 bba1111e1b11cd14c0e266af6c5b0bd549f081a6. * 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 c8e866f5682ed4d01a54ae714ceedf50670f09ca. * 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 * debug iterative deepening some more and add first attempt at PQ (untested) * fix some bugs and the PQ approach is working for now. the depth sets approach is actually unsound, but I am going to focus on the PQ approach for now since it has more potential for SAT problems with the right hardness metric * add new attempt at hardness function * attempt to add different hardness functions including heule schur and march, need to re-examine/debug/evaluate * implement march and heule schur hardness functions based on sat_lookahead.cpp implementations. they seem to be buggy, need to revisit. also set up experimental params for running on polytest * add a lot of debug prints that need to be removed. some bugs are resolved but others remain * debug in progress * remove the incorrect preselection functions for march and heule-schur. update explicit-hardness with bugfixes. now it works but i am not sure there is a good perf increase based on my handpicked examples. i tried several variations of hardness ratios as you can see commented out. there are debug prints still commented out. also return_cubes now takes in a single cube instead of a list C_worker to align with the single-cube hardness/should_split metrics, it doesn't change anything bc we only pass in 1 cube to begin with --------- 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 a7df159 commit e126362

File tree

3 files changed

+41
-197
lines changed

3 files changed

+41
-197
lines changed

‎src/params/smt_parallel_params.pyg‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,4 @@ def_module_params('smt_parallel',
1818
('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
1919
('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
2020
('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
21-
('march_hardness', BOOL, False, 'use naive march metric for cubes'),
22-
('heule_schur_hardness', BOOL, False, 'use heule schur hardness metric for cube'),
2321
))

‎src/smt/smt_parallel.cpp‎

Lines changed: 39 additions & 191 deletions
Original file line numberDiff line numberDiff line change
@@ -49,189 +49,54 @@ namespace smt {
4949
return ctx->m_stats.m_num_decisions / std::max(1u, ctx->m_stats.m_num_conflicts);
5050
}
5151

52-
double parallel::worker::explicit_hardness(expr_ref_vector const& cube, unsigned initial_scope_lvl) {
53-
double total = 0.0;
54-
unsigned clause_count = 0;
55-
LOG_WORKER(1, " CUBE SIZE IN EXPLICIT HARDNESS: " << cube.size() << "\n");
52+
double parallel::worker::explicit_hardness(expr_ref_vector const& cube) {
53+
double overall_hardness = 0.0;
54+
// LOG_WORKER(1, " CUBE SIZE IN EXPLICIT HARDNESS: " << cube.size() << "\n");
5655

5756
// Build a set of bool_vars corresponding to the cube literals
5857
svector<bool_var> cube_vars;
5958
for (auto& e : cube) {
60-
LOG_WORKER(1, " PROCESSING CUBE\n");
59+
// LOG_WORKER(1, " PROCESSING CUBE\n");
6160
bool_var v = ctx->get_bool_var(e);
62-
LOG_WORKER(1, " Cube contains var " << v << "\n");
61+
// LOG_WORKER(1, " Cube contains var " << v << "\n");
6362
if (v != null_bool_var) cube_vars.push_back(v);
6463
}
6564

6665
for (auto* cp : ctx->m_aux_clauses) {
6766
auto& clause = *cp;
68-
unsigned sz = 0;
6967
unsigned n_false = 0;
7068
bool satisfied = false;
7169

72-
LOG_WORKER(1, " Clause has num literals: " << clause.get_num_literals() << "\n");
70+
// LOG_WORKER(1, " Clause has num literals: " << clause.get_num_literals() << "\n");
7371
for (literal l : clause) {
72+
// LOG_WORKER(1, " Processing literal " << l << " with val: " << ctx->get_assignment(l) << "\n");
7473
bool_var v = l.var();
7574

76-
// Only consider literals that are part of the cube
77-
LOG_WORKER(1, " Cube contains " << v << ": " << (cube_vars.contains(v)) << "\n");
78-
if (!cube_vars.contains(v)) continue;
79-
8075
lbool val = ctx->get_assignment(l);
76+
if (val == l_undef) continue;
77+
8178
unsigned lvl = ctx->get_assign_level(l);
8279

8380
// Only include assignments made after the base scope level (i.e. those made by specifically assuming the cube)
84-
LOG_WORKER(1, " Literal " << l << " at level " << lvl << " is equal or below scope level " << initial_scope_lvl << ": " << bool(lvl <= initial_scope_lvl) << "\n");
85-
if (lvl <= initial_scope_lvl) continue;
81+
// LOG_WORKER(1, " Literal " << l << " at level " << lvl << " is below scope level " << ctx->get_search_level() << ": " << bool(lvl < ctx->get_search_level()) << "\n");
82+
if (lvl < ctx->get_search_level()) continue;
8683

87-
sz++;
8884
if (val == l_true) { satisfied = true; break; }
8985
if (val == l_false) n_false++;
9086
}
91-
LOG_WORKER(1, " Clause of size " << sz << " has " << n_false << " false literals in cube. Is satisfied: " << satisfied << "\n");
92-
if (satisfied || sz == 0) continue;
93-
94-
double m = static_cast<double>(sz) / std::max(1u, sz - n_false);
95-
LOG_WORKER(1, " Clause contributes " << m << " to hardness metric\n");
96-
total += m;
97-
clause_count++;
98-
}
99-
100-
return clause_count ? total / clause_count : 0.0;
101-
}
102-
103-
double parallel::worker::heule_schur_hardness(expr_ref_vector const& cube) {
104-
double total = 0.0;
105-
unsigned n = 0;
106-
107-
auto literal_occs = [&](literal l) {
108-
unsigned count = 0;
109-
110-
for (auto* cp : ctx->m_aux_clauses) {
111-
auto& clause = *cp;
112-
bool occurs = false;
113-
for (literal li : clause) {
114-
if (li == ~l) {
115-
occurs = true;
116-
break;
117-
}
118-
}
119-
120-
if (!occurs) continue;
121-
if (clause.get_num_literals() >= 2) {
122-
count += 1;
123-
}
124-
}
125-
126-
return static_cast<double>(count);
127-
};
128-
129-
for (expr* e : cube) {
130-
literal lit = ctx->get_literal(e);
131-
double score = 0.0;
132-
133-
for (auto* cp : ctx->m_aux_clauses) {
134-
auto& clause = *cp;
135-
if (clause.get_num_literals() == 2) { // binary clauses
136-
literal a = clause[0];
137-
literal b = clause[1];
138-
if (a == lit && ctx->get_assignment(b) == l_undef) {
139-
score += literal_occs(b) / 4.0;
140-
} else if (b == lit && ctx->get_assignment(a) == l_undef) {
141-
score += literal_occs(a) / 4.0;
142-
}
143-
} else if (clause.get_num_literals() == 3) { // ternary clauses containing ~lit
144-
bool has_neg = false;
145-
std::vector<literal> others;
146-
for (literal l2 : clause) {
147-
if (l2 == ~lit) {
148-
has_neg = true;
149-
} else {
150-
others.push_back(l2);
151-
}
152-
}
153-
if (has_neg && others.size() == 2) { // since lit + others is a ternary clause
154-
score += (literal_occs(others[0]) + literal_occs(others[1])) / 8.0;
155-
}
156-
} else { // n-ary clauses (size > 3) containing ~lit
157-
unsigned len = clause.get_num_literals();
158-
if (len > 3) {
159-
bool has_neg = false;
160-
double to_add = 0.0;
161-
for (literal l2 : clause) {
162-
if (l2 == ~lit) {
163-
has_neg = true;
164-
continue;
165-
}
166-
if (ctx->get_assignment(l2) == l_undef) {
167-
to_add += literal_occs(l2);
168-
}
169-
}
170-
if (has_neg) {
171-
score += pow(0.5, static_cast<double>(len)) * to_add / len;
172-
}
173-
}
174-
}
175-
}
176-
177-
total += score;
178-
n++;
179-
}
180-
181-
return n ? total / n : 0.0;
182-
}
183-
184-
double parallel::worker::march_cu_hardness(expr_ref_vector const& cube) {
185-
double total = 0.0;
186-
unsigned n = 0;
187-
188-
for (expr* e : cube) {
189-
bool_var v = ctx->get_bool_var(e);
190-
literal l(v, false);
191-
192-
auto big_occs = [&](literal lit) {
193-
unsigned count = 0;
194-
for (auto* cp : ctx->m_aux_clauses) {
195-
auto& clause = *cp;
196-
if (clause.get_num_literals() >= 3) {
197-
for (literal li : clause) {
198-
if (li == lit) { count++; break; }
199-
}
200-
}
201-
}
202-
return count;
203-
};
204-
205-
auto march_cu_score = [&](literal lit) {
206-
double sum = 1.0;
207-
// occurrences of ~lit in big clauses
208-
sum += big_occs(~lit);
209-
210-
// binary neighbors of lit
211-
for (auto* cp : ctx->m_aux_clauses) {
212-
auto& clause = *cp;
213-
if (clause.get_num_literals() == 2) { // binary clauses
214-
literal a = clause[0];
215-
literal b = clause[1];
216-
if (a == lit && ctx->get_assignment(b) == l_undef) {
217-
sum += big_occs(b);
218-
} else if (b == lit && ctx->get_assignment(a) == l_undef) {
219-
sum += big_occs(a);
220-
}
221-
}
222-
}
223-
return sum;
224-
};
225-
226-
double pos = march_cu_score(l);
227-
double neg = march_cu_score(~l);
87+
88+
if (satisfied || n_false == 0) continue; // meaning, the clause is true (at least 1 true atom), or we had no true OR false atoms so the whole thing is undefined
89+
90+
unsigned sz = clause.get_num_literals();
91+
// LOG_WORKER(1, " Clause of size " << sz << " has " << n_false << " false literals in cube. Is satisfied: " << satisfied << "\n");
22892

229-
double rating = 1024 * pos * neg + pos + neg + 1;
230-
total += rating;
231-
n++;
93+
// double reduction_ratio = static_cast<double>(sz) / n_false; // n_false/sz -> higher value=easier //std::max(1u, reduction);
94+
double reduction_ratio = pow(0.5, sz) * (1 / n_false);
95+
// LOG_WORKER(1, " Clause contributes " << reduction_ratio << " to hardness metric. n_false: " << n_false << "\n");
96+
overall_hardness += reduction_ratio;
23297
}
23398

234-
return n ? total / n : 0.0; // average the march scores of the literals in the cube
99+
return overall_hardness;
235100
}
236101

237102
void parallel::worker::run() {
@@ -247,8 +112,6 @@ namespace smt {
247112
return;
248113
}
249114

250-
LOG_WORKER(1, " checking cube\n");
251-
unsigned initial_scope_lvl = ctx->get_scope_level();
252115
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
253116
lbool r = check_cube(cube);
254117

@@ -264,29 +127,22 @@ namespace smt {
264127
// add a split literal to the batch manager.
265128
// optionally process other cubes and delay sending back unprocessed cubes to batch manager.
266129
if (!m_config.m_never_cube) {
267-
vector<expr_ref_vector> returned_cubes;
268-
returned_cubes.push_back(cube);
130+
// vector<expr_ref_vector> returned_cubes;
131+
// returned_cubes.push_back(cube);
269132
auto split_atoms = get_split_atoms();
270133

271-
LOG_WORKER(1, " CUBING\n");
272134
// let's automatically do iterative deepening for beam search.
273135
// when using more advanced metrics like explicit_hardness etc: need one of two things: (1) split if greater than OR EQUAL TO than avg hardness, or (3) enter this branch only when cube.size() > 0, or else we get stuck in a loop of never deepening.
274136
if (m_config.m_iterative_deepening || m_config.m_beam_search) {
275137
LOG_WORKER(1, " applying iterative deepening\n");
276138

277139
double cube_hardness;
278140
if (m_config.m_explicit_hardness) {
279-
cube_hardness = explicit_hardness(cube, initial_scope_lvl);
280-
LOG_WORKER(1, " explicit hardness: " << cube_hardness << "\n");
281-
} else if (m_config.m_march_hardness) {
282-
cube_hardness = march_cu_hardness(cube);
283-
LOG_WORKER(1, " march hardness: " << cube_hardness << "\n");
284-
} else if (m_config.m_heule_schur_hardness) {
285-
cube_hardness = heule_schur_hardness(cube);
286-
LOG_WORKER(1, " heule schur hardness: " << cube_hardness << "\n");
141+
cube_hardness = explicit_hardness(cube);
142+
// LOG_WORKER(1, " explicit hardness: " << cube_hardness << "\n");
287143
} else { // default to naive hardness
288144
cube_hardness = naive_hardness();
289-
LOG_WORKER(1, " naive hardness: " << cube_hardness << "\n");
145+
// LOG_WORKER(1, " naive hardness: " << cube_hardness << "\n");
290146
}
291147

292148
const double avg_hardness = b.update_avg_cube_hardness(cube_hardness);
@@ -296,9 +152,9 @@ namespace smt {
296152
LOG_WORKER(1, " cube hardness: " << cube_hardness << " avg: " << avg_hardness << " avg*factor: " << avg_hardness * factor << " should-split: " << should_split << "\n");
297153
// 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!
298154
// should_split tells return_cubes whether to further split the unsolved cube.
299-
b.return_cubes(m_l2g, returned_cubes, split_atoms, should_split);
155+
b.return_cubes(m_l2g, cube, split_atoms, should_split);
300156
} else {
301-
b.return_cubes(m_l2g, returned_cubes, split_atoms);
157+
b.return_cubes(m_l2g, cube, split_atoms);
302158
}
303159
}
304160
if (m_config.m_backbone_detection) {
@@ -379,8 +235,6 @@ namespace smt {
379235
m_config.m_iterative_deepening = pp.iterative_deepening();
380236
m_config.m_beam_search = pp.beam_search();
381237
m_config.m_explicit_hardness = pp.explicit_hardness();
382-
m_config.m_march_hardness = pp.march_hardness();
383-
m_config.m_heule_schur_hardness = pp.heule_schur_hardness();
384238

385239
// don't share initial units
386240
ctx->pop_to_base_lvl();
@@ -694,9 +548,8 @@ namespace smt {
694548
------------------------------------------------------------------------------------------------------------------------------------------------------------
695549
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
696550
*/
697-
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, const double hardness) {
551+
void parallel::batch_manager::return_cubes(ast_translation& l2g, expr_ref_vector const& c, expr_ref_vector const& A_worker, const bool should_split, const double hardness) {
698552
// SASSERT(!m_config.never_cube());
699-
IF_VERBOSE(1, verbose_stream() << " Batch manager returning " << C_worker.size() << " cubes and " << A_worker.size() << " split atoms\n");
700553
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
701554
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
702555
};
@@ -718,10 +571,9 @@ namespace smt {
718571

719572
// apply the frugal strategy to ALL incoming worker cubes, but save in the deepest cube data structure
720573
auto add_split_atom_deepest_cubes = [&](expr* atom) {
721-
for (auto& c : C_worker) {
722574
if (c.size() >= m_config.m_max_cube_depth || !should_split) {
723575
IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
724-
continue;
576+
return;
725577
}
726578
expr_ref_vector g_cube(l2g.to());
727579
for (auto& atom : c)
@@ -742,40 +594,37 @@ namespace smt {
742594

743595
m_stats.m_num_cubes += 2;
744596
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, d + 1);
745-
}
597+
746598
};
747599

748600
// apply the frugal strategy to ALL incoming worker cubes, but save in the PQ data structure for beam search
749601
auto add_split_atom_pq = [&](expr* atom) {
750602
// IF_VERBOSE(1, verbose_stream() << " Adding split atom to PQ: " << mk_bounded_pp(atom, m, 3) << "\n");
751-
for (auto& c : C_worker) {
603+
752604
if (c.size() >= m_config.m_max_cube_depth || !should_split) {
753605
// IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
754-
continue;
606+
return;
755607
}
756608

757609
expr_ref_vector g_cube(l2g.to());
758610
for (auto& atom : c)
759611
g_cube.push_back(l2g(atom));
760-
761-
// i need to split on the positive and negative atom, and add both to the PQ. the score is the depth of the cube (same for both)
762-
unsigned d = g_cube.size();
763612

764613
// Positive atom branch
765614
expr_ref_vector cube_pos = g_cube;
766615
cube_pos.push_back(atom);
767-
m_cubes_pq.push(ScoredCube(d / hardness, cube_pos));
616+
m_cubes_pq.push(ScoredCube(1 / hardness, cube_pos));
768617

769618
// Negative atom branch
770619
expr_ref_vector cube_neg = g_cube;
771620
cube_neg.push_back(m.mk_not(atom));
772-
m_cubes_pq.push(ScoredCube(d / hardness, cube_neg));
621+
m_cubes_pq.push(ScoredCube(1 / hardness, cube_neg));
773622

774623
// IF_VERBOSE(1, verbose_stream() << " PQ size now: " << m_cubes_pq.size() << ". PQ is empty: " << m_cubes_pq.empty() << "\n");
775624

776625
m_stats.m_num_cubes += 2;
777-
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, d + 1);
778-
}
626+
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, g_cube.size() + 1);
627+
779628
};
780629

781630
std::scoped_lock lock(mux);
@@ -811,7 +660,7 @@ namespace smt {
811660
unsigned initial_m_cubes_size = m_cubes.size(); // where to start processing the worker cubes after splitting the EXISTING cubes on the new worker atoms
812661

813662
// --- Phase 2: Process worker cubes (greedy) ---
814-
for (auto& c : C_worker) {
663+
815664
expr_ref_vector g_cube(l2g.to());
816665
for (auto& atom : c)
817666
g_cube.push_back(l2g(atom));
@@ -823,7 +672,7 @@ namespace smt {
823672
if ((c.size() >= m_config.m_max_cube_depth || !should_split)
824673
&& (m_config.m_depth_splitting_only || m_config.m_iterative_deepening || m_config.m_beam_search)) {
825674
if (m_config.m_beam_search) {
826-
m_cubes_pq.push(ScoredCube(g_cube.size() / hardness, g_cube)); // re-enqueue the cube as is
675+
m_cubes_pq.push(ScoredCube(1 / hardness, g_cube)); // re-enqueue the cube as is
827676
} else {
828677
// need to add the depth set if it doesn't exist yet
829678
if (m_cubes_depth_sets.find(g_cube.size()) == m_cubes_depth_sets.end()) {
@@ -855,7 +704,6 @@ namespace smt {
855704
}
856705
}
857706
}
858-
}
859707

860708
// --- Phase 3: Frugal fallback: only process NEW worker cubes with NEW atoms ---
861709
if (!greedy_mode) {

0 commit comments

Comments
 (0)