Skip to content

Commit a7df159

Browse files
ilanashapiroNikolajBjornerhumnrdblenunoplopesCopilot
authored
Parallel solving (#7840)
* very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add python file Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> * debug under defined calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more untangle params Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename a Python file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * remove unused square-free check Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add some debug prints and impelement internal polynomial fix * restore the square-free check Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * Remove test_example binary file from repository Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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] <support@github.com> 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 <nbjorner@microsoft.com> * added notes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * more notes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * process cubes as lists of individual lits --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> * snapshot Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * pair programming Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * pair programming Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * updates Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * updates Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simplify output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * 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 <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add python file Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> * debug under defined calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more untangle params Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename a Python file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> * 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 <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add python file Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> * debug under defined calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more untangle params Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename a Python file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * remove unused square-free check Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add some debug prints and impelement internal polynomial fix * add some comments and debug m_assumptions_used * redo greedy->frugal strategy so we don't split on existing cubes in frugal at all (eliminate the incorrect/wasteful step by processing current batch first) * set up initial scaffolding for sharing clauses between threads and batch manager. needs some reworking/debug still --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> * sign of life Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add notes on parameter tuning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * turn off logging at level 0 for testing * add max thread conflicts backoff --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * Add documentation for the translate method in solver_factory Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert "Parallel solving (#7775)" (#7777) This reverts commit c8e866f5682ed4d01a54ae714ceedf50670f09ca. * remove upload artifact for azure-pipeline Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove NugetPublishNightly stage from nightly.yaml (#7787) * Initial plan * Remove NugetPublishNightly stage from nightly.yaml Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * add more params * enable pypi public Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <nbjorner@microsoft.com> * fix #7753 * fix #7796 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * Complete centralized version management system Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Create centralized version management with VERSION.txt Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * read version from VERSION.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix version parse Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix parsing of version Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <nbjorner@microsoft.com> * remove resources directive again Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix Julia bindings linker errors on Windows MSVC (#7794) * Initial plan * Fix Julia bindings linker errors on Windows MSVC Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete Julia bindings fix validation and testing Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix Julia bindings linker errors on Windows MSVC Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * add print for version file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add more logging to setup.py Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * try diferennt dirs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * try src_dir_repo Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * try other dir Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove extra characters Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * print dirs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * copy VERSION from SRC_DIR Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * clean up a little of the handling of VERSION.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * 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 --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Solal Pirelli <SolalPirelli@users.noreply.github.com> Co-authored-by: Shiwei Weng 翁士伟 <arbipher@gmail.com>
1 parent 28d316f commit a7df159

File tree

3 files changed

+164
-50
lines changed

3 files changed

+164
-50
lines changed

‎src/params/smt_parallel_params.pyg‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,4 +17,7 @@ def_module_params('smt_parallel',
1717
('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
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'),
20+
('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'),
2023
))

‎src/smt/smt_parallel.cpp‎

Lines changed: 155 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -45,17 +45,21 @@ namespace smt {
4545

4646
namespace smt {
4747

48-
double parallel::worker::explicit_hardness(expr_ref_vector const& cube) {
48+
double parallel::worker::naive_hardness() {
49+
return ctx->m_stats.m_num_decisions / std::max(1u, ctx->m_stats.m_num_conflicts);
50+
}
51+
52+
double parallel::worker::explicit_hardness(expr_ref_vector const& cube, unsigned initial_scope_lvl) {
4953
double total = 0.0;
5054
unsigned clause_count = 0;
51-
52-
// Get the scope level before the cube is assumed
53-
unsigned scope_lvl = ctx->get_scope_level();
55+
LOG_WORKER(1, " CUBE SIZE IN EXPLICIT HARDNESS: " << cube.size() << "\n");
5456

5557
// Build a set of bool_vars corresponding to the cube literals
5658
svector<bool_var> cube_vars;
57-
for (expr* e : cube) {
59+
for (auto& e : cube) {
60+
LOG_WORKER(1, " PROCESSING CUBE\n");
5861
bool_var v = ctx->get_bool_var(e);
62+
LOG_WORKER(1, " Cube contains var " << v << "\n");
5963
if (v != null_bool_var) cube_vars.push_back(v);
6064
}
6165

@@ -65,26 +69,30 @@ namespace smt {
6569
unsigned n_false = 0;
6670
bool satisfied = false;
6771

72+
LOG_WORKER(1, " Clause has num literals: " << clause.get_num_literals() << "\n");
6873
for (literal l : clause) {
6974
bool_var v = l.var();
7075

7176
// Only consider literals that are part of the cube
77+
LOG_WORKER(1, " Cube contains " << v << ": " << (cube_vars.contains(v)) << "\n");
7278
if (!cube_vars.contains(v)) continue;
7379

7480
lbool val = ctx->get_assignment(l);
7581
unsigned lvl = ctx->get_assign_level(l);
7682

77-
// Only include assignments made after the scope level
78-
if (lvl <= scope_lvl) continue;
83+
// 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;
7986

8087
sz++;
8188
if (val == l_true) { satisfied = true; break; }
8289
if (val == l_false) n_false++;
8390
}
84-
91+
LOG_WORKER(1, " Clause of size " << sz << " has " << n_false << " false literals in cube. Is satisfied: " << satisfied << "\n");
8592
if (satisfied || sz == 0) continue;
8693

8794
double m = static_cast<double>(sz) / std::max(1u, sz - n_false);
95+
LOG_WORKER(1, " Clause contributes " << m << " to hardness metric\n");
8896
total += m;
8997
clause_count++;
9098
}
@@ -96,27 +104,77 @@ namespace smt {
96104
double total = 0.0;
97105
unsigned n = 0;
98106

99-
for (expr* e : cube) {
100-
double literal_score = 0.0;
107+
auto literal_occs = [&](literal l) {
108+
unsigned count = 0;
101109

102110
for (auto* cp : ctx->m_aux_clauses) {
103111
auto& clause = *cp;
104-
unsigned sz = 0;
105112
bool occurs = false;
113+
for (literal li : clause) {
114+
if (li == ~l) {
115+
occurs = true;
116+
break;
117+
}
118+
}
106119

107-
for (literal l : clause) {
108-
expr* lit_expr = ctx->bool_var2expr(l.var());
109-
if (asms.contains(lit_expr)) continue; // ignore assumptions
110-
sz++;
111-
if (lit_expr == e) occurs = true;
120+
if (!occurs) continue;
121+
if (clause.get_num_literals() >= 2) {
122+
count += 1;
112123
}
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;
113132

114-
if (occurs && sz > 0) {
115-
literal_score += 1.0 / pow(2.0, sz); // weight inversely by clause size
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+
}
116174
}
117175
}
118176

119-
total += literal_score;
177+
total += score;
120178
n++;
121179
}
122180

@@ -128,35 +186,52 @@ namespace smt {
128186
unsigned n = 0;
129187

130188
for (expr* e : cube) {
131-
double score = 1.0; // start with 1 to avoid zero
132-
133-
for (auto* cp : ctx->m_aux_clauses) {
134-
auto& clause = *cp;
135-
bool occurs = false;
136-
137-
unsigned sz = 0; // clause size counting only non-assumption literals
138-
139-
for (literal l : clause) {
140-
expr* lit_expr = ctx->bool_var2expr(l.var());
141-
142-
if (asms.contains(lit_expr)) continue; // ignore assumptions
143-
sz++;
144-
145-
if (lit_expr == e) {
146-
occurs = true;
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+
}
147200
}
148201
}
202+
return count;
203+
};
149204

150-
if (occurs && sz > 0) {
151-
score += pow(0.5, static_cast<double>(sz)); // approximate March weight
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+
}
152222
}
153-
}
223+
return sum;
224+
};
154225

155-
total += score;
226+
double pos = march_cu_score(l);
227+
double neg = march_cu_score(~l);
228+
229+
double rating = 1024 * pos * neg + pos + neg + 1;
230+
total += rating;
156231
n++;
157232
}
158233

159-
return n ? total / n : 0.0;
234+
return n ? total / n : 0.0; // average the march scores of the literals in the cube
160235
}
161236

162237
void parallel::worker::run() {
@@ -173,7 +248,14 @@ namespace smt {
173248
}
174249

175250
LOG_WORKER(1, " checking cube\n");
251+
unsigned initial_scope_lvl = ctx->get_scope_level();
252+
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
176253
lbool r = check_cube(cube);
254+
255+
if (m.limit().is_canceled()) {
256+
LOG_WORKER(1, " cancelled\n");
257+
return;
258+
}
177259

178260
switch (r) {
179261
case l_undef: {
@@ -187,15 +269,29 @@ namespace smt {
187269
auto split_atoms = get_split_atoms();
188270

189271
LOG_WORKER(1, " CUBING\n");
190-
if (m_config.m_iterative_deepening || m_config.m_beam_search) { // let's automatically do iterative deepening for beam search
272+
// let's automatically do iterative deepening for beam search.
273+
// 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.
274+
if (m_config.m_iterative_deepening || m_config.m_beam_search) {
191275
LOG_WORKER(1, " applying iterative deepening\n");
192-
193-
// const double cube_hardness = ctx->m_stats.m_num_decisions / std::max(1u, ctx->m_stats.m_num_conflicts);
194-
const double cube_hardness = explicit_hardness(cube); // huele_schur_hardness(cube); march_cu_hardness(cube);
276+
277+
double cube_hardness;
278+
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");
287+
} else { // default to naive hardness
288+
cube_hardness = naive_hardness();
289+
LOG_WORKER(1, " naive hardness: " << cube_hardness << "\n");
290+
}
195291

196292
const double avg_hardness = b.update_avg_cube_hardness(cube_hardness);
197293
const double factor = 1; // can tune for multiple of avg hardness later
198-
bool should_split = cube_hardness > avg_hardness * factor;
294+
bool should_split = cube_hardness >= avg_hardness * factor;
199295

200296
LOG_WORKER(1, " cube hardness: " << cube_hardness << " avg: " << avg_hardness << " avg*factor: " << avg_hardness * factor << " should-split: " << should_split << "\n");
201297
// 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!
@@ -282,6 +378,9 @@ namespace smt {
282378
m_config.m_backbone_detection = pp.backbone_detection();
283379
m_config.m_iterative_deepening = pp.iterative_deepening();
284380
m_config.m_beam_search = pp.beam_search();
381+
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();
285384

286385
// don't share initial units
287386
ctx->pop_to_base_lvl();
@@ -422,6 +521,7 @@ namespace smt {
422521
|| m_config.m_depth_splitting_only && m_cubes_depth_sets.empty()) {
423522
// special initialization: the first cube is emtpy, have the worker work on an empty cube.
424523
cubes.push_back(expr_ref_vector(g2l.to()));
524+
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out empty cube.\n");
425525
return;
426526
}
427527

@@ -444,6 +544,7 @@ namespace smt {
444544
} else if (m_config.m_beam_search) {
445545
// get the highest ranked cube
446546
SASSERT(!m_cubes_pq.empty());
547+
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out cube with score " << m_cubes_pq.top().score << ".\n");
447548

448549
ScoredCube const& scored_cube = m_cubes_pq.top();
449550
auto& cube = scored_cube.cube;
@@ -455,6 +556,7 @@ namespace smt {
455556
cubes.push_back(l_cube);
456557
m_cubes_pq.pop();
457558
} else {
559+
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out cube.\n");
458560
auto& cube = m_cubes.back();
459561
expr_ref_vector l_cube(g2l.to());
460562
for (auto& e : cube) {
@@ -594,7 +696,7 @@ namespace smt {
594696
*/
595697
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) {
596698
// SASSERT(!m_config.never_cube());
597-
699+
IF_VERBOSE(1, verbose_stream() << " Batch manager returning " << C_worker.size() << " cubes and " << A_worker.size() << " split atoms\n");
598700
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
599701
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
600702
};
@@ -645,9 +747,10 @@ namespace smt {
645747

646748
// apply the frugal strategy to ALL incoming worker cubes, but save in the PQ data structure for beam search
647749
auto add_split_atom_pq = [&](expr* atom) {
750+
// IF_VERBOSE(1, verbose_stream() << " Adding split atom to PQ: " << mk_bounded_pp(atom, m, 3) << "\n");
648751
for (auto& c : C_worker) {
649752
if (c.size() >= m_config.m_max_cube_depth || !should_split) {
650-
IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
753+
// IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
651754
continue;
652755
}
653756

@@ -668,6 +771,8 @@ namespace smt {
668771
cube_neg.push_back(m.mk_not(atom));
669772
m_cubes_pq.push(ScoredCube(d / hardness, cube_neg));
670773

774+
// IF_VERBOSE(1, verbose_stream() << " PQ size now: " << m_cubes_pq.size() << ". PQ is empty: " << m_cubes_pq.empty() << "\n");
775+
671776
m_stats.m_num_cubes += 2;
672777
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, d + 1);
673778
}
@@ -759,9 +864,10 @@ namespace smt {
759864
if (!m_split_atoms.contains(g_atom))
760865
m_split_atoms.push_back(g_atom);
761866
if (should_split && (m_config.m_depth_splitting_only || m_config.m_iterative_deepening)) {
762-
IF_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom " << mk_bounded_pp(g_atom, m, 3) << "\n");
867+
IF_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom for depth sets " << mk_bounded_pp(g_atom, m, 3) << "\n");
763868
add_split_atom_deepest_cubes(g_atom);
764-
} else if (m_config.m_beam_search) {
869+
} else if (should_split && m_config.m_beam_search) {
870+
IF_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom for PQ " << mk_bounded_pp(g_atom, m, 3) << "\n");
765871
add_split_atom_pq(g_atom);
766872
} else {
767873
add_split_atom(g_atom, initial_m_cubes_size);

‎src/smt/smt_parallel.h‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,9 @@ namespace smt {
165165
bool m_backbone_detection = false;
166166
bool m_iterative_deepening = false;
167167
bool m_beam_search = false;
168+
bool m_explicit_hardness = false;
169+
bool m_march_hardness = false;
170+
bool m_heule_schur_hardness = false;
168171
};
169172

170173
unsigned id; // unique identifier for the worker
@@ -187,7 +190,9 @@ namespace smt {
187190

188191
expr_ref_vector find_backbone_candidates();
189192
expr_ref_vector get_backbones_from_candidates(expr_ref_vector const& candidates);
190-
double explicit_hardness(expr_ref_vector const& cube);
193+
194+
double naive_hardness();
195+
double explicit_hardness(expr_ref_vector const& cube, unsigned initial_scope_lvl);
191196
double heule_schur_hardness(expr_ref_vector const& cube);
192197
double march_cu_hardness(expr_ref_vector const& cube);
193198
public:

0 commit comments

Comments
 (0)