3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00

Parallel solving (#7849)

* 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 bba1111e1b.

* 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 c8e866f568.

* 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

* debug in progress

* remove the incorrect preselection functions for march and heule-schur. update explicit-hardness with bugfixes. now it works but i am not sure there is a good perf increase based on my handpicked examples. i tried several variations of hardness ratios as you can see commented out. there are debug prints still commented out. also return_cubes now takes in a single cube instead of a list C_worker to align with the single-cube hardness/should_split metrics, it doesn't change anything bc we only pass in 1 cube to begin with

* debug a couple of things and change the hardness function

* tree version in progress

* cube tree data structure version for sharing maximal solver context. it compiles but segfaults immediately so it needs a lot of debugging

* slowly debugging (committing for saving progress)

* debugged get_next_cube to align with how we're storing the prev_cube and active status. other things are still wrong

* debug manager translation problem

* don't actually prune tree for UNSAT, too risky with multithreads. instead marks all such 'removed' nodes as inactive

* it runs! but then crashes after a while

---------

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>
This commit is contained in:
Ilana Shapiro 2025-09-06 09:31:55 -07:00 committed by GitHub
parent 09cc4c4f5f
commit e3ef4fa3f5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 105 additions and 79 deletions

View file

@ -34,7 +34,7 @@ public:
}
void clear() {
delete_leaf(root);
delete_subtree(root); // actually delete all nodes
root = nullptr;
}
@ -47,6 +47,7 @@ public:
void add_children(CubeNode* parent,
const Cube& left_cube,
const Cube& right_cube) {
IF_VERBOSE(1, verbose_stream() << "CubeTree: adding children of sizes " << left_cube.size() << " and " << right_cube.size() << " under parent of size " << (parent ? parent->cube.size() : 0) << "\n");
CubeNode* left = new CubeNode(left_cube, parent);
CubeNode* right = new CubeNode(right_cube, parent);
parent->children.push_back(left);
@ -55,6 +56,7 @@ public:
// Add a new node under an existing parent
void add_node(CubeNode* node, CubeNode* parent) {
IF_VERBOSE(1, verbose_stream() << "CubeTree: adding node of size " << (node ? node->cube.size() : 0) << " under parent of size " << (parent ? parent->cube.size() : 0) << "\n");
if (!node) return;
// If no parent is specified, assume it's the root
@ -67,111 +69,116 @@ public:
}
}
// remove node and propagate upward if parent becomes leaf
// return pointer to last removed ancestor (or nullptr if none) so we can select one of its siblings as the next cube
// mark node as inactive and propagate upward if parent becomes a leaf (all children inactive)
// return pointer to last affected ancestor (or nullptr if none) so we can select one of its siblings as the next cube
CubeNode* remove_node_and_propagate(CubeNode* node) {
if (!node || node == root || node->children.empty()) return nullptr; // error or root or not a leaf
if (!node || node == root || !node->is_leaf()) return nullptr; // error, root, or not a leaf
CubeNode* parent = node->parent;
CubeNode* last_removed = node;
CubeNode* last_marked = node;
// erase node from parent's children
for (size_t i = 0; i < parent->children.size(); ++i) {
if (parent->children[i] == node) {
delete_leaf(node);
parent->children.erase(parent->children.begin() + i);
break;
}
}
// mark this node as inactive
node->active = false;
// propagate upward if parent became leaf
while (parent && parent != root && parent->is_leaf()) {
SASSERT(parent->active); // parent only just became a leaf node -- no thread should be working on it! i.e. must NOT be inactive!
CubeNode* gp = parent->parent;
for (size_t i = 0; i < gp->children.size(); ++i) {
if (gp->children[i] == parent) {
last_removed = parent; // track the last ancestor we delete
delete parent;
gp->children.erase(gp->children.begin() + i);
// propagate upward if parent became a "leaf" (all children inactive)
while (parent && parent != root) {
bool all_inactive = true;
for (CubeNode* child : parent->children) {
if (child->active) {
all_inactive = false;
break;
}
}
parent = gp;
if (!all_inactive) break; // stop propagating
SASSERT(parent->active); // parent must not be currently worked on
last_marked = parent; // track the last ancestor we mark
parent->active = false; // mark parent inactive
parent = parent->parent;
}
return last_removed;
return last_marked;
}
// get closest cube to current by getting a random sibling of current (if current was UNSAT and we removed it from the tree)
// or by descending randomly to a leaf (if we split the current node) to get the newest cube split fromthe current
// we descend randomly to a leaf instead of just taking a random child because it's possible another thread made more descendants
CubeNode* get_next_cube(CubeNode* current) {
IF_VERBOSE(1, verbose_stream() << "CubeTree: current cube is null: " << (current == nullptr) << "\n");
if (!current) return nullptr;
// must be a leaf
SASSERT(current->is_leaf());
IF_VERBOSE(1, verbose_stream() << "CubeTree: getting next cube from current of size " << current->cube.size() << "\n");
// lambda to find any active leaf in the subtree (explore all branches)
std::function<CubeNode*(CubeNode*)> find_active_leaf;
find_active_leaf = [&](CubeNode* node) -> CubeNode* {
std::function<CubeNode*(CubeNode*)> find_active_leaf = [&](CubeNode* node) -> CubeNode* {
if (!node || !node->active) return nullptr;
if (node->is_leaf()) return node;
for (CubeNode* child : node->children) {
CubeNode* leaf = find_active_leaf(child);
if (leaf) return leaf; // return first found active leaf
if (leaf) return leaf;
}
return nullptr;
};
CubeNode* node = current;
while (node->parent) {
CubeNode* parent = node->parent;
while (node) {
// 1. check if current node itself is active leaf
if (node->active && node->is_leaf()) return node;
// gather active siblings
std::vector<CubeNode*> siblings;
for (CubeNode* s : parent->children) {
if (s != node && s->active)
siblings.push_back(s);
// 2. check active leaf descendants
CubeNode* leaf_descendant = nullptr;
for (CubeNode* child : node->children) {
leaf_descendant = find_active_leaf(child);
if (leaf_descendant) return leaf_descendant;
}
if (!siblings.empty()) {
// try each sibling until we find an active leaf
for (CubeNode* sibling : siblings) {
CubeNode* leaf = find_active_leaf(sibling);
if (leaf) return leaf;
// 3 & 4. check siblings and their active leaf descendants
if (node->parent) {
CubeNode* parent = node->parent;
for (CubeNode* sibling : parent->children) {
if (sibling == node) continue;
// check if sibling itself is an active leaf
if (sibling->active && sibling->is_leaf()) return sibling;
// check for active leaf descendants of sibling
CubeNode* leaf_in_sibling = find_active_leaf(sibling);
if (leaf_in_sibling) return leaf_in_sibling;
}
}
// no active leaf among siblings → climb up
node = parent;
// 5. climb up to parent
node = node->parent;
}
// nothing found
IF_VERBOSE(1, verbose_stream() << "CubeTree: no active cube found\n");
return nullptr;
}
private:
CubeNode* root;
void delete_leaf(CubeNode* node) {
// mark leaf as inactive instead of deleting it
void mark_leaf_inactive(CubeNode* node) {
if (!node || !node->active) return;
// must be a leaf
SASSERT(node->children.empty());
// detach from parent
if (node->parent) {
auto& siblings = node->parent->children;
for (auto it = siblings.begin(); it != siblings.end(); ++it) {
if (*it == node) {
siblings.erase(it);
break;
}
}
}
// just mark inactive
node->active = false;
}
void delete_subtree(CubeNode* node) {
if (!node) return;
for (CubeNode* child : node->children) {
delete_subtree(child);
}
delete node;
}
};

View file

@ -100,13 +100,15 @@ namespace smt {
while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper)
expr_ref_vector cube(m);
CubeNode* cube_node;
LOG_WORKER(1, " Curr cube node is null: " << (m_curr_cube_node == nullptr) << "\n");
if (m_config.m_cubetree) {
cube_node = b.get_cube_from_tree(m_g2l, m_curr_cube_node);
// use std::tie so we don't overshadow cube_node!!!
std::tie(cube_node, cube) = b.get_cube_from_tree(m_g2l, m_curr_cube_node); // cube node is the reference to the node in the tree, tells us how to get the next cube. "cube" is the translated cube we need for the solver
LOG_WORKER(1, " Got cube node from CubeTree. Is null: " << (cube_node == nullptr) << "\n");
m_curr_cube_node = cube_node; // store the current cube so we know how to get the next closest cube from the tree
cube = (expr_ref_vector)(cube_node->cube);
IF_VERBOSE(1, verbose_stream() << " Worker " << id << " got cube of size " << cube.size() << " from CubeTree\n");
}
else {
} else {
cube = b.get_cube(m_g2l);
}
@ -156,6 +158,8 @@ namespace smt {
// should_split tells return_cubes whether to further split the unsolved cube.
b.return_cubes(m_l2g, cube, split_atoms, should_split, cube_hardness);
} else if (m_config.m_cubetree) {
IF_VERBOSE(1, verbose_stream() << " returning undef cube to CubeTree. Cube node is null: " << (cube_node == nullptr) << "\n");
b.return_cubes_tree(m_l2g, cube_node, split_atoms);
} else {
b.return_cubes(m_l2g, cube, split_atoms);
@ -205,6 +209,7 @@ namespace smt {
// prune the tree now that we know the cube is unsat
if (m_config.m_cubetree) {
IF_VERBOSE(1, verbose_stream() << " removing cube node from CubeTree and propagate deletion\n");
b.remove_node_and_propagate(m_curr_cube_node);
}
break;
@ -377,7 +382,7 @@ namespace smt {
return r;
}
CubeNode* parallel::batch_manager::get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube) {
std::pair<CubeNode*, expr_ref_vector> parallel::batch_manager::get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube) {
std::scoped_lock lock(mux);
expr_ref_vector l_cube(g2l.to());
SASSERT(m_config.m_cubetree);
@ -385,24 +390,30 @@ namespace smt {
if (m_cubes_tree.empty()) {
// special initialization: the first cube is emtpy, have the worker work on an empty cube.
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out empty cube.\n");
CubeNode* new_cube_node = new CubeNode(l_cube, nullptr);
expr_ref_vector g_cube(g2l.from());
CubeNode* new_cube_node = new CubeNode(g_cube, nullptr);
m_cubes_tree.add_node(new_cube_node, nullptr);
return new_cube_node; // return empty cube
return {new_cube_node, l_cube}; // return empty cube
} else if (!prev_cube) {
prev_cube = m_cubes_tree.get_root(); // if prev_cube is null, it means that another thread started the tree first. so we also start from the root (i.e. the empty cube)
return {prev_cube, l_cube};
}
// get a cube from the CubeTree
SASSERT(!m_cubes_tree.empty());
CubeNode* next_cube_node = m_cubes_tree.get_next_cube(prev_cube); // get the next cube in the tree closest to the prev cube (i.e. longest common prefix)
expr_ref_vector& next_cube = next_cube_node->cube;
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out cube from CubeTree.\n");
IF_VERBOSE(1, verbose_stream() << "Batch manager giving out cube from CubeTree. Is null: " << (next_cube_node==nullptr) << "\n");
for (auto& e : next_cube) {
for (auto& e : next_cube_node->cube) {
l_cube.push_back(g2l(e));
}
IF_VERBOSE(1, verbose_stream() << " Cube size: " << l_cube.size() << "\n");
next_cube_node->active = false; // mark the cube as inactive (i.e. being processed by a worker)
return next_cube_node;
return {next_cube_node, l_cube};
}
// FOR ALL NON-TREE VERSIONS
@ -452,6 +463,7 @@ namespace smt {
for (auto& e : m_cubes) {
IF_VERBOSE(1, verbose_stream() << "Cube: " << e << "\n");
}
expr_ref_vector l_cube(g2l.to());
for (auto& e : cube) {
l_cube.push_back(g2l(e));
@ -464,6 +476,7 @@ namespace smt {
void parallel::batch_manager::set_sat(ast_translation& l2g, model& m) {
std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting SAT.\n");
if (m_state != state::is_running)
return;
m_state = state::is_sat;
@ -473,6 +486,7 @@ namespace smt {
void parallel::batch_manager::set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core) {
std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNSAT.\n");
if (m_state != state::is_running)
return;
m_state = state::is_unsat;
@ -488,6 +502,7 @@ namespace smt {
void parallel::batch_manager::set_exception(unsigned error_code) {
std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n");
if (m_state != state::is_running)
return;
m_state = state::is_exception_code;
@ -497,6 +512,7 @@ namespace smt {
void parallel::batch_manager::set_exception(std::string const& msg) {
std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception msg: " << msg << ".\n");
if (m_state != state::is_running || m.limit().is_canceled())
return;
m_state = state::is_exception_msg;
@ -766,15 +782,20 @@ namespace smt {
}
void parallel::batch_manager::return_cubes_tree(ast_translation& l2g, CubeNode* cube_node, expr_ref_vector const& A_worker) {
IF_VERBOSE(1, verbose_stream() << " Returning cube to batch manager's cube tree.\n");
expr_ref_vector const& c = cube_node->cube;
IF_VERBOSE(1, verbose_stream() << " Cube node null: " << (cube_node == nullptr) << "\n");
IF_VERBOSE(1, verbose_stream() << " PROCESSING CUBE of size: " << c.size() << "\n");
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
};
// apply the frugal strategy to ALL incoming worker cubes, but save in the PQ data structure for beam search
auto add_split_atom_pq = [&](expr* atom) {
// IF_VERBOSE(1, verbose_stream() << " Adding split atom to PQ: " << mk_bounded_pp(atom, m, 3) << "\n");
auto add_split_atom_tree = [&](expr* atom) {
IF_VERBOSE(1, verbose_stream() << " Adding split atom to tree: " << mk_bounded_pp(atom, m, 3) << "\n");
expr_ref_vector g_cube(l2g.to());
for (auto& atom : c)
g_cube.push_back(l2g(atom));
@ -787,34 +808,32 @@ namespace smt {
expr_ref_vector cube_neg = g_cube;
cube_neg.push_back(m.mk_not(atom));
m_cubes_tree.add_children(cube_node, cube_pos, cube_neg);
// IF_VERBOSE(1, verbose_stream() << " PQ size now: " << m_cubes_pq.size() << ". PQ is empty: " << m_cubes_pq.empty() << "\n");
m_cubes_tree.add_children(cube_node, cube_pos, cube_neg); // default is active
m_stats.m_num_cubes += 2;
m_stats.m_max_cube_depth = std::max(m_stats.m_max_cube_depth, g_cube.size() + 1);
};
std::scoped_lock lock(mux);
expr_ref_vector g_cube(l2g.to());
for (auto& atom : c)
g_cube.push_back(l2g(atom));
if (c.size() >= m_config.m_max_cube_depth) {
// IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
IF_VERBOSE(1, verbose_stream() << " Skipping split of cube at max depth " << m_config.m_max_cube_depth << "\n";);
cube_node->active = true; // mark the cube as active again since we didn't split it
return;
}
// --- Frugal approach: only process NEW worker cubes with NEW atoms ---
for (unsigned i = 0; i < A_worker.size(); ++i) {
IF_VERBOSE(1, verbose_stream() << " Processing worker atom " << mk_bounded_pp(A_worker[i], m, 3) << "\n");
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_VERBOSE(1, verbose_stream() << " splitting worker cubes on new atom for PQ " << mk_bounded_pp(g_atom, m, 3) << "\n");
add_split_atom_pq(g_atom);
add_split_atom_tree(g_atom);
}
}

View file

@ -132,7 +132,7 @@ namespace smt {
// The batch manager returns the next cube to
//
expr_ref_vector get_cube(ast_translation& g2l); // FOR ALL NON-TREE VERSIONS
CubeNode* get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube = nullptr);
std::pair<CubeNode*, expr_ref_vector> get_cube_from_tree(ast_translation& g2l, CubeNode* prev_cube = nullptr);
//
// worker threads return unprocessed cubes to the batch manager together with split literal candidates.
@ -146,6 +146,7 @@ namespace smt {
expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
void remove_node_and_propagate(CubeNode* node) {
std::scoped_lock lock(mux);
SASSERT(m_config.m_cubetree);
CubeNode* last_removed = m_cubes_tree.remove_node_and_propagate(node);
if (last_removed) {
@ -156,6 +157,7 @@ namespace smt {
}
double update_avg_cube_hardness(double hardness) {
std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Cube hardness: " << hardness << ", previous avg: " << m_avg_cube_hardness << ", solved cubes: " << m_solved_cube_count << "\n";);
m_avg_cube_hardness = (m_avg_cube_hardness * m_solved_cube_count + hardness) / (m_solved_cube_count + 1);
m_solved_cube_count++;
@ -212,8 +214,6 @@ namespace smt {
double naive_hardness();
double explicit_hardness(expr_ref_vector const& cube);
double heule_schur_hardness(expr_ref_vector const& cube);
double march_cu_hardness(expr_ref_vector const& cube);
public:
worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
void run();