…#7743

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

…pressions

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

axioms for len(substr(...)) escaped due to nested rewriting

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.

Signed-off-by: Nikolaj Bjorner <[email protected]>

add pre-processing simplification

fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.

…digm, need to debug as I am getting segfault still

…rallel-solving

…rallel-solving

…can. the PQ implementation backend still remains in case we want to switch back

…rallel-solving

…stalled (Z3Prover#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.

Signed-off-by: Nikolaj Bjorner <[email protected]>

…e 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

…rallel-solving

… still naive!

…ven if we don't split it further

…sted)

…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

… march, need to re-examine/debug/evaluate

…head.cpp implementations. they seem to be buggy, need to revisit. also set up experimental params for running on polytest

…lved but others remain