mirror of
https://github.com/Z3Prover/z3
synced 2025-08-25 20:46:01 +00:00
Parallel solving (#7814)
* 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 commitbba1111e1b. * 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 commitc8e866f568. * 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 --------- 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>
This commit is contained in:
Ilana Shapiro
GitHub
parent
7b40d086ba
commit
8cb093752a
17 changed files with 214 additions and 83 deletions
|
|
@ -4,7 +4,7 @@ cmake_minimum_required(VERSION 3.16)
|
|||
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
||||
|
||||
# Read version from VERSION.txt file
|
||||
file(READ "${CMAKE_CURRENT_SOURCE_DIR}/VERSION.txt" Z3_VERSION_FROM_FILE)
|
||||
file(READ "${CMAKE_CURRENT_SOURCE_DIR}/scripts/VERSION.txt" Z3_VERSION_FROM_FILE)
|
||||
string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE)
|
||||
|
||||
project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
module(
|
||||
name = "z3",
|
||||
version = "4.16.0", # TODO: Read from VERSION.txt - currently manual sync required
|
||||
version = "4.15.4", # TODO: Read from VERSION.txt - currently manual sync required
|
||||
bazel_compatibility = [">=7.0.0"],
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -302,6 +302,13 @@ threads-4-cube
|
|||
threads-4-cube-shareconflicts
|
||||
-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=false smt_parallel.share_conflicts=true smt_parallel.share_units=false
|
||||
|
||||
|
||||
threads-4-cube-maxdepth-10
|
||||
-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.share_conflicts=false smt_parallel.share_units=false smt_parallel.max_cube_depth=10
|
||||
|
||||
threads-4-cube-shareconflicts
|
||||
-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.share_conflicts=true smt_parallel.share_units=false smt_parallel.frugal_depth_splitting_only=true
|
||||
|
||||
</pre>
|
||||
|
||||
Ideas for other knobs that can be tested
|
||||
|
|
|
|||
|
|
@ -119,6 +119,30 @@ target_link_libraries(yourTarget libz3)
|
|||
```
|
||||
Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`).
|
||||
|
||||
#### Using system-installed Z3
|
||||
|
||||
If you have Z3 installed on your system (e.g., via package manager or by building and installing Z3 yourself), you can use CMake's `find_package` to locate it:
|
||||
|
||||
```cmake
|
||||
find_package(Z3 REQUIRED CONFIG)
|
||||
```
|
||||
|
||||
Once found, you can use the Z3 include directories and libraries:
|
||||
|
||||
```cmake
|
||||
# For C projects
|
||||
target_include_directories(yourTarget PRIVATE ${Z3_C_INCLUDE_DIRS})
|
||||
target_link_libraries(yourTarget PRIVATE ${Z3_LIBRARIES})
|
||||
|
||||
# For C++ projects
|
||||
target_include_directories(yourTarget PRIVATE ${Z3_CXX_INCLUDE_DIRS})
|
||||
target_link_libraries(yourTarget PRIVATE ${Z3_LIBRARIES})
|
||||
```
|
||||
|
||||
The `find_package(Z3 CONFIG)` approach uses Z3's provided `Z3Config.cmake` file, which is installed to a standard location (typically `<prefix>/lib/cmake/z3/`). If CMake cannot automatically find Z3, you can help it by setting `-DZ3_DIR=<path>` where `<path>` is the directory containing the `Z3Config.cmake` file.
|
||||
|
||||
**Note**: This approach requires that Z3 was built and installed using CMake. Z3 installations from the Python build system may not provide the necessary CMake configuration files.
|
||||
|
||||
|
||||
|
||||
### Ninja
|
||||
|
|
|
|||
|
|
@ -103,7 +103,7 @@ def mk_targets(source_root):
|
|||
def mk_icon(source_root):
|
||||
mk_dir("out/content")
|
||||
shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg")
|
||||
# shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
|
||||
shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md")
|
||||
|
||||
|
||||
|
||||
|
|
@ -124,6 +124,7 @@ Linux Dependencies:
|
|||
<copyright>© Microsoft Corporation. All rights reserved.</copyright>
|
||||
<tags>smt constraint solver theorem prover</tags>
|
||||
<icon>content/icon.jpg</icon>
|
||||
<readme>content/README.md</readme>
|
||||
<projectUrl>https://github.com/Z3Prover/z3</projectUrl>
|
||||
<license type="expression">MIT</license>
|
||||
<repository type="git" url="{1}" branch="{2}" commit="{3}" />
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ from mk_util import *
|
|||
|
||||
def init_version():
|
||||
# Read version from VERSION.txt file
|
||||
version_file_path = os.path.join(os.path.dirname(os.path.dirname(__file__)), 'VERSION.txt')
|
||||
version_file_path = os.path.join(os.path.dirname(__file__), 'VERSION.txt')
|
||||
try:
|
||||
with open(version_file_path, 'r') as f:
|
||||
version_str = f.read().strip()
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
variables:
|
||||
# Version components read from VERSION.txt (updated manually when VERSION.txt changes)
|
||||
Major: '4'
|
||||
Minor: '16'
|
||||
Patch: '0'
|
||||
Minor: '15'
|
||||
Patch: '4'
|
||||
ReleaseVersion: $(Major).$(Minor).$(Patch)
|
||||
AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
|
||||
NightlyVersion: $(AssemblyVersion)-$(Build.buildId)
|
||||
|
|
@ -254,9 +254,9 @@ stages:
|
|||
inputs:
|
||||
artifact: 'MacArm64'
|
||||
path: $(Agent.TempDirectory)\package
|
||||
- task: NuGetToolInstaller@0
|
||||
- task: NuGetToolInstaller@1
|
||||
inputs:
|
||||
versionSpec: 5.x
|
||||
versionSpec: 6.x
|
||||
checkLatest: false
|
||||
- task: PythonScript@0
|
||||
displayName: 'Python: assemble files'
|
||||
|
|
@ -302,9 +302,9 @@ stages:
|
|||
inputs:
|
||||
artifact: 'WindowsBuild-x86'
|
||||
path: $(Agent.TempDirectory)\package
|
||||
- task: NuGetToolInstaller@0
|
||||
- task: NuGetToolInstaller@1
|
||||
inputs:
|
||||
versionSpec: 5.x
|
||||
versionSpec: 6.x
|
||||
checkLatest: false
|
||||
- task: PythonScript@0
|
||||
displayName: 'Python: assemble files'
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
trigger: none
|
||||
|
||||
variables:
|
||||
ReleaseVersion: '4.16.0' # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
|
||||
ReleaseVersion: '4.15.4' # TODO: Auto-read from VERSION.txt when Azure DevOps supports it better
|
||||
|
||||
stages:
|
||||
|
||||
|
|
@ -261,9 +261,9 @@ stages:
|
|||
artifact: 'MacArm64'
|
||||
path: $(Agent.TempDirectory)\package
|
||||
|
||||
- task: NuGetToolInstaller@0
|
||||
- task: NuGetToolInstaller@1
|
||||
inputs:
|
||||
versionSpec: 5.x
|
||||
versionSpec: 6.x
|
||||
checkLatest: false
|
||||
- task: PythonScript@0
|
||||
displayName: 'Python: assemble files'
|
||||
|
|
@ -305,9 +305,9 @@ stages:
|
|||
inputs:
|
||||
artifact: 'WindowsBuild-x86'
|
||||
path: $(Agent.TempDirectory)\package
|
||||
- task: NuGetToolInstaller@0
|
||||
- task: NuGetToolInstaller@1
|
||||
inputs:
|
||||
versionSpec: 5.x
|
||||
versionSpec: 6.x
|
||||
checkLatest: false
|
||||
- task: PythonScript@0
|
||||
displayName: 'Python: assemble files'
|
||||
|
|
@ -471,7 +471,7 @@ stages:
|
|||
|
||||
|
||||
- job: NuGetPublish
|
||||
condition: eq(1,0)
|
||||
condition: eq(1,1)
|
||||
displayName: "Publish to NuGet.org"
|
||||
steps:
|
||||
- task: DownloadPipelineArtifact@2
|
||||
|
|
@ -479,9 +479,9 @@ stages:
|
|||
inputs:
|
||||
artifact: 'NuGetPackage'
|
||||
path: $(Agent.TempDirectory)
|
||||
- task: NuGetToolInstaller@0
|
||||
- task: NuGetToolInstaller@1
|
||||
inputs:
|
||||
versionSpec: 5.x
|
||||
versionSpec: 6.x
|
||||
checkLatest: false
|
||||
- task: NuGetCommand@2
|
||||
inputs:
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ import sys
|
|||
def read_version():
|
||||
"""Read version from VERSION.txt file."""
|
||||
script_dir = os.path.dirname(os.path.abspath(__file__))
|
||||
version_file = os.path.join(os.path.dirname(script_dir), 'VERSION.txt')
|
||||
version_file = os.path.join(script_dir, 'VERSION.txt')
|
||||
|
||||
try:
|
||||
with open(version_file, 'r') as f:
|
||||
|
|
|
|||
|
|
@ -1,5 +1,32 @@
|
|||
find_package(JlCxx REQUIRED)
|
||||
|
||||
# Check for Windows MSVC + MinGW library compatibility issues
|
||||
if(WIN32 AND CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
|
||||
# Get the JlCxx library path to check its format
|
||||
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION)
|
||||
if(NOT JLCXX_LIB_PATH)
|
||||
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION_RELEASE)
|
||||
endif()
|
||||
if(NOT JLCXX_LIB_PATH)
|
||||
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB)
|
||||
endif()
|
||||
if(NOT JLCXX_LIB_PATH)
|
||||
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB_RELEASE)
|
||||
endif()
|
||||
|
||||
if(JLCXX_LIB_PATH AND JLCXX_LIB_PATH MATCHES "\\.dll\\.a$")
|
||||
message(FATAL_ERROR
|
||||
"Julia bindings build error: Incompatible CxxWrap library format detected.\n"
|
||||
"The found libcxxwrap_julia library (${JLCXX_LIB_PATH}) is a MinGW import library (.dll.a), "
|
||||
"but Z3 is being built with MSVC which requires .lib format.\n\n"
|
||||
"Solutions:\n"
|
||||
"1. Use MinGW/GCC instead of MSVC to build Z3\n"
|
||||
"2. Install a MSVC-compatible version of CxxWrap\n"
|
||||
"3. Disable Julia bindings with -DZ3_BUILD_JULIA_BINDINGS=OFF\n\n"
|
||||
"For more information, see: https://github.com/JuliaInterop/CxxWrap.jl#compiling-the-c-code")
|
||||
endif()
|
||||
endif()
|
||||
|
||||
add_library(z3jl SHARED z3jl.cpp)
|
||||
target_link_libraries(z3jl PRIVATE JlCxx::cxxwrap_julia libz3)
|
||||
target_include_directories(z3jl PRIVATE
|
||||
|
|
|
|||
|
|
@ -113,8 +113,15 @@ def _clean_native_build():
|
|||
|
||||
def _z3_version():
|
||||
post = os.getenv('Z3_VERSION_SUFFIX', '')
|
||||
print("z3_version", "release dir", RELEASE_DIR)
|
||||
if RELEASE_DIR is None:
|
||||
fn = os.path.join(SRC_DIR_REPO, 'VERSION.txt')
|
||||
dirs = [SRC_DIR, ROOT_DIR, SRC_DIR_REPO, SRC_DIR_LOCAL, os.path.join(ROOT_DIR, '..', '..')]
|
||||
for d in dirs:
|
||||
if os.path.exists(d):
|
||||
print(d, ": ", os.listdir(d))
|
||||
fns = [os.path.join(d, 'scripts', 'VERSION.txt') for d in dirs]
|
||||
for fn in fns:
|
||||
print("loading version file", fn, "exists", os.path.exists(fn))
|
||||
if os.path.exists(fn):
|
||||
with open(fn) as f:
|
||||
for line in f:
|
||||
|
|
|
|||
|
|
@ -11,4 +11,7 @@ def_module_params('smt_parallel',
|
|||
('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'),
|
||||
('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
|
||||
('max_cube_size', UINT, 20, 'maximum size of a cube to share'),
|
||||
('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
|
||||
('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
|
||||
('frugal_deepest_cube_only', BOOL, False, 'only apply frugal cube strategy, and only on a deepest (biggest) cube from the batch manager'),
|
||||
))
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ namespace smt {
|
|||
unsigned_vector m_lit_occs; //!< occurrence count of literals
|
||||
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
|
||||
svector<double> m_activity;
|
||||
updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
|
||||
// updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
|
||||
|
||||
struct lit_node : dll_base<lit_node> {
|
||||
literal lit;
|
||||
|
|
@ -199,7 +199,6 @@ namespace smt {
|
|||
};
|
||||
lit_node* m_dll_lits;
|
||||
|
||||
// svector<std::array<double, 2>> m_lit_scores;
|
||||
svector<double> m_lit_scores[2];
|
||||
|
||||
clause_vector m_aux_clauses;
|
||||
|
|
@ -952,7 +951,7 @@ namespace smt {
|
|||
e = 0;
|
||||
for (auto& e : m_lit_scores[1])
|
||||
e = 0;
|
||||
m_pq_scores.clear(); // Clear the priority queue heap as well
|
||||
// m_pq_scores.clear(); // Clear the priority queue heap as well
|
||||
}
|
||||
double get_score(literal l) const {
|
||||
return m_lit_scores[l.sign()][l.var()];
|
||||
|
|
|
|||
|
|
@ -1532,14 +1532,6 @@ namespace smt {
|
|||
}}
|
||||
}
|
||||
|
||||
// void context::add_scores(unsigned n, literal const* lits) {
|
||||
// for (unsigned i = 0; i < n; ++i) {
|
||||
// auto lit = lits[i];
|
||||
// unsigned v = lit.var();
|
||||
// m_lit_scores[v][lit.sign()] += 1.0 / n;
|
||||
// }
|
||||
// }
|
||||
|
||||
void context::add_scores(unsigned n, literal const* lits) {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
auto lit = lits[i];
|
||||
|
|
@ -1547,8 +1539,8 @@ namespace smt {
|
|||
|
||||
m_lit_scores[lit.sign()][v] += 1.0 / n;
|
||||
|
||||
auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
|
||||
m_pq_scores.set(v, new_score);
|
||||
// auto new_score = m_lit_scores[0][v] * m_lit_scores[1][v];
|
||||
// m_pq_scores.set(v, new_score);
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -137,6 +137,8 @@ namespace smt {
|
|||
m_config.m_share_units_initial_only = pp.share_units_initial_only();
|
||||
m_config.m_cube_initial_only = pp.cube_initial_only();
|
||||
m_config.m_max_conflict_mul = pp.max_conflict_mul();
|
||||
m_config.m_max_greedy_cubes = pp.max_greedy_cubes();
|
||||
m_config.m_num_split_lits = pp.num_split_lits();
|
||||
|
||||
// don't share initial units
|
||||
ctx->pop_to_base_lvl();
|
||||
|
|
@ -272,13 +274,29 @@ namespace smt {
|
|||
|
||||
void parallel::batch_manager::get_cubes(ast_translation& g2l, vector<expr_ref_vector>& cubes) {
|
||||
std::scoped_lock lock(mux);
|
||||
if (m_cubes.size() == 1 && m_cubes[0].size() == 0) {
|
||||
if (m_cubes.size() == 1 && m_cubes[0].empty()) {
|
||||
// special initialization: the first cube is emtpy, have the worker work on an empty cube.
|
||||
cubes.push_back(expr_ref_vector(g2l.to()));
|
||||
return;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) {
|
||||
if (m_config.m_frugal_deepest_cube_only) {
|
||||
// get the deepest set of cubes
|
||||
auto& deepest_cubes = m_cubes_depth_sets.rbegin()->second;
|
||||
unsigned idx = rand() % deepest_cubes.size();
|
||||
auto& cube = deepest_cubes[idx]; // get a random cube from the deepest set
|
||||
|
||||
expr_ref_vector l_cube(g2l.to());
|
||||
for (auto& e : cube) {
|
||||
l_cube.push_back(g2l(e));
|
||||
}
|
||||
cubes.push_back(l_cube);
|
||||
|
||||
deepest_cubes.erase(deepest_cubes.begin() + idx); // remove the cube from the set
|
||||
if (deepest_cubes.empty())
|
||||
m_cubes_depth_sets.erase(m_cubes_depth_sets.size() - 1);
|
||||
} else {
|
||||
auto& cube = m_cubes.back();
|
||||
expr_ref_vector l_cube(g2l.to());
|
||||
for (auto& e : cube) {
|
||||
|
|
@ -288,6 +306,7 @@ namespace smt {
|
|||
m_cubes.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void parallel::batch_manager::set_sat(ast_translation& l2g, model& m) {
|
||||
std::scoped_lock lock(mux);
|
||||
|
|
@ -341,7 +360,7 @@ namespace smt {
|
|||
return l_undef; // the main context was cancelled, so we return undef.
|
||||
switch (m_state) {
|
||||
case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat
|
||||
if (!m_cubes.empty())
|
||||
if (!m_cubes.empty() || (m_config.m_frugal_deepest_cube_only && !m_cubes_depth_sets.empty()))
|
||||
throw default_exception("inconsistent end state");
|
||||
if (!p.m_assumptions_used.empty()) {
|
||||
// collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core
|
||||
|
|
@ -439,9 +458,36 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
// apply the frugal strategy to ALL incoming worker cubes, but save in the deepest cube data structure
|
||||
auto add_split_atom_deepest_cubes = [&](expr* atom) {
|
||||
for (auto& c : C_worker) {
|
||||
expr_ref_vector g_cube(l2g.to());
|
||||
for (auto& atom : c)
|
||||
g_cube.push_back(l2g(atom));
|
||||
if (g_cube.size() >= m_config.m_max_cube_size) // we already added this before!! we just need to add the splits now
|
||||
continue;
|
||||
|
||||
// add depth set d+1 if it doesn't exist yet
|
||||
unsigned d = g_cube.size();
|
||||
if (m_cubes_depth_sets.find(d + 1) == m_cubes_depth_sets.end())
|
||||
m_cubes_depth_sets[d + 1] = vector<expr_ref_vector>();
|
||||
|
||||
// split on the negative atom
|
||||
m_cubes_depth_sets[d + 1].push_back(g_cube);
|
||||
m_cubes_depth_sets[d + 1].back().push_back(m.mk_not(atom));
|
||||
|
||||
// need to split on the positive atom too
|
||||
g_cube.push_back(atom);
|
||||
m_cubes_depth_sets[d + 1].push_back(g_cube);
|
||||
|
||||
m_stats.m_num_cubes += 2;
|
||||
m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, d + 1);
|
||||
}
|
||||
};
|
||||
|
||||
std::scoped_lock lock(mux);
|
||||
unsigned max_cubes = 1000;
|
||||
bool greedy_mode = (m_cubes.size() <= max_cubes) && !m_config.m_frugal_cube_only;
|
||||
unsigned max_greedy_cubes = 1000;
|
||||
bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only && !m_config.m_frugal_deepest_cube_only;
|
||||
unsigned a_worker_start_idx = 0;
|
||||
|
||||
//
|
||||
|
|
@ -455,7 +501,7 @@ namespace smt {
|
|||
m_split_atoms.push_back(g_atom);
|
||||
|
||||
add_split_atom(g_atom, 0); // split all *existing* cubes
|
||||
if (m_cubes.size() > max_cubes) {
|
||||
if (m_cubes.size() > max_greedy_cubes) {
|
||||
greedy_mode = false;
|
||||
++a_worker_start_idx; // start frugal from here
|
||||
break;
|
||||
|
|
@ -470,16 +516,26 @@ namespace smt {
|
|||
expr_ref_vector g_cube(l2g.to());
|
||||
for (auto& atom : c)
|
||||
g_cube.push_back(l2g(atom));
|
||||
|
||||
unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added
|
||||
|
||||
if (m_config.m_frugal_deepest_cube_only) {
|
||||
// need to add the depth set if it doesn't exist yet
|
||||
if (m_cubes_depth_sets.find(g_cube.size()) == m_cubes_depth_sets.end()) {
|
||||
m_cubes_depth_sets[g_cube.size()] = vector<expr_ref_vector>();
|
||||
}
|
||||
m_cubes_depth_sets[g_cube.size()].push_back(g_cube);
|
||||
m_stats.m_num_cubes += 1;
|
||||
m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, g_cube.size());
|
||||
} else {
|
||||
m_cubes.push_back(g_cube);
|
||||
}
|
||||
|
||||
if (greedy_mode) {
|
||||
// Split new cube on all existing m_split_atoms not in it
|
||||
for (auto g_atom : m_split_atoms) {
|
||||
if (!atom_in_cube(g_cube, g_atom)) {
|
||||
add_split_atom(g_atom, start);
|
||||
if (m_cubes.size() > max_cubes) {
|
||||
if (m_cubes.size() > max_greedy_cubes) {
|
||||
greedy_mode = false;
|
||||
break;
|
||||
}
|
||||
|
|
@ -494,53 +550,57 @@ namespace smt {
|
|||
expr_ref g_atom(l2g(A_worker[i]), l2g.to());
|
||||
if (!m_split_atoms.contains(g_atom))
|
||||
m_split_atoms.push_back(g_atom);
|
||||
if (m_config.m_frugal_deepest_cube_only) {
|
||||
add_split_atom_deepest_cubes(g_atom);
|
||||
} else {
|
||||
add_split_atom(g_atom, initial_m_cubes_size);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref_vector parallel::worker::get_split_atoms() {
|
||||
#if false
|
||||
unsigned k = 2;
|
||||
|
||||
// auto candidates = ctx->m_pq_scores.get_heap();
|
||||
auto candidates = ctx->m_lit_scores;
|
||||
std::vector<std::pair<double, expr*>> top_k; // will hold at most k elements
|
||||
|
||||
for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
|
||||
if (ctx->get_assignment(v) != l_undef)
|
||||
continue;
|
||||
expr* e = ctx->bool_var2expr(v);
|
||||
if (!e)
|
||||
continue;
|
||||
auto v_score = ctx->m_lit_scores[0][v] * ctx->m_lit_scores[1][v];
|
||||
// if v_score is maximal then v is our split atom..
|
||||
|
||||
double score = ctx->m_lit_scores[0][v] * ctx->m_lit_scores[1][v];
|
||||
|
||||
// decay the scores
|
||||
ctx->m_lit_scores[0][v] /= 2;
|
||||
ctx->m_lit_scores[1][v] /= 2;
|
||||
|
||||
// insert into top_k. linear scan since k is very small
|
||||
if (top_k.size() < k) {
|
||||
top_k.push_back({score, e});
|
||||
} else {
|
||||
// find the smallest in top_k and replace if we found a new min
|
||||
size_t min_idx = 0;
|
||||
for (size_t i = 1; i < k; ++i)
|
||||
if (top_k[i].first < top_k[min_idx].first)
|
||||
min_idx = i;
|
||||
|
||||
if (score > top_k[min_idx].first) {
|
||||
top_k[min_idx] = {score, e};
|
||||
}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
unsigned k = 2;
|
||||
|
||||
auto candidates = ctx->m_pq_scores.get_heap();
|
||||
|
||||
std::sort(candidates.begin(), candidates.end(),
|
||||
[](const auto& a, const auto& b) { return a.priority > b.priority; });
|
||||
|
||||
expr_ref_vector top_lits(m);
|
||||
for (const auto& node: candidates) {
|
||||
for (auto& p : top_k)
|
||||
top_lits.push_back(expr_ref(p.second, m));
|
||||
|
||||
if (ctx->get_assignment(node.key) != l_undef)
|
||||
continue;
|
||||
IF_VERBOSE(3, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_lit_scores->size() << " num vars " << ctx->get_num_bool_vars() << "\n");
|
||||
|
||||
if (m_config.m_cube_initial_only && node.key >= m_num_initial_atoms) {
|
||||
LOG_WORKER(2, " Skipping non-initial atom from cube: " << node.key << "\n");
|
||||
continue; // skip non-initial atoms if configured to do so
|
||||
}
|
||||
|
||||
expr* e = ctx->bool_var2expr(node.key);
|
||||
if (!e)
|
||||
continue;
|
||||
|
||||
top_lits.push_back(expr_ref(e, m));
|
||||
if (top_lits.size() >= k)
|
||||
break;
|
||||
}
|
||||
IF_VERBOSE(3, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n");
|
||||
return top_lits;
|
||||
}
|
||||
|
||||
|
|
@ -548,11 +608,17 @@ namespace smt {
|
|||
m_state = state::is_running;
|
||||
m_cubes.reset();
|
||||
m_cubes.push_back(expr_ref_vector(m)); // push empty cube
|
||||
|
||||
if (m_config.m_frugal_deepest_cube_only) {
|
||||
m_cubes_depth_sets.clear();
|
||||
}
|
||||
|
||||
m_split_atoms.reset();
|
||||
smt_parallel_params sp(p.ctx.m_params);
|
||||
m_config.m_max_cube_size = sp.max_cube_size();
|
||||
m_config.m_frugal_cube_only = sp.frugal_cube_only();
|
||||
m_config.m_never_cube = sp.never_cube();
|
||||
m_config.m_frugal_deepest_cube_only = sp.frugal_deepest_cube_only();
|
||||
}
|
||||
|
||||
void parallel::batch_manager::collect_statistics(::statistics& st) const {
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
|
||||
#include "smt/smt_context.h"
|
||||
#include <thread>
|
||||
#include <map>
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -49,6 +50,7 @@ namespace smt {
|
|||
unsigned m_max_cube_size = 20;
|
||||
bool m_frugal_cube_only = false;
|
||||
bool m_never_cube = false;
|
||||
bool m_frugal_deepest_cube_only = false;
|
||||
};
|
||||
struct stats {
|
||||
unsigned m_max_cube_size = 0;
|
||||
|
|
@ -63,6 +65,7 @@ namespace smt {
|
|||
stats m_stats;
|
||||
expr_ref_vector m_split_atoms; // atoms to split on
|
||||
vector<expr_ref_vector> m_cubes;
|
||||
std::map<unsigned, vector<expr_ref_vector>> m_cubes_depth_sets; // map<vec<cube>> contains sets of cubes, key is depth/size of cubes in the set
|
||||
unsigned m_max_batch_size = 10;
|
||||
unsigned m_exception_code = 0;
|
||||
std::string m_exception_msg;
|
||||
|
|
@ -120,6 +123,8 @@ namespace smt {
|
|||
double m_max_conflict_mul = 1.5;
|
||||
bool m_share_units_initial_only = false;
|
||||
bool m_cube_initial_only = false;
|
||||
bool m_max_greedy_cubes = 1000;
|
||||
unsigned m_num_split_lits = 2;
|
||||
};
|
||||
|
||||
unsigned id; // unique identifier for the worker
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue