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

…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

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