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

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

…it compiles but segfaults immediately so it needs a lot of debugging

…and active status. other things are still wrong

…tead marks all such 'removed' nodes as inactive

… only working in the frontier determined by their split atoms, and only overlapping frontiers once they've exhausted their own

…not crash. also fix a couple of things in get_next_cube. also, setting k=1 for split atoms might be better, not sure

…ier when we just started a new frontier (like if we're at the empty cube at the root)

…g new frontier nodes. i think it works now?? it's still not as fast as I would want

also, there are a lot of messy debug prints i will need to remove

…ies are UNSAT, the entire formula is UNSAT

… is found closed by a thread, and finally multiple threads can work on the same cube if it's the only active leaf

…e ugly 'frontier' logic is now gone