[Features] Does Z3 contains a configuration that let the program control the constraint priority

[yjg66]

Dear authors,

Recently, we have a scenario, hope the z3 solves the constraints (CDCL algorithm) based on our attached constraints orders. I am not sure Z3 contains these features?

Unsat core does not match our requirements, as we want to diagnosis the root cause as the constraint attached orders.

[NikolajBjorner]

CDCL dynamically adjusts ordering based on search traversal. There isn't a configuration to control ordering. You can try to incrementally add constraints and use multiple calls to find the shortest prefix of a set of constraints that are unsatisfiable, and then configure core minimization to obtain minimal cores or roll your own core minimization algorithm based on priorities if that is what you want.

[yjg66]

Thanks！