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

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

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

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

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

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

…ext. add some debug prints

…ing strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel?

…hase of the greedy cubing, and the frugal fallback

Signed-off-by: Lev Nachmanson <[email protected]>

…rallel-solving

…rallel-solving

…rugal at all (eliminate the incorrect/wasteful step by processing current batch first)

…tch manager. needs some reworking/debug still

…ng shared lits