new tactic: partition

Mar 1, 2016 at 12:43 PM
I should like to suggest a new tactic that partitions a given SMT-problem (CSP) into minimal independent components.

The partition algorithm works on the primal constraint graph.
(1) If two variables appear together in a constraint, they end up in the same CSP-component.
(2) A constraint that has a variable in one of the CSP-components, ends up in that component.

The partition tactic should be a splitting tactic like split-clause. The constraints in each component should be combined into a separate goal.

A tactical such as then could be used to serially solve each of the component-CSPs.

A tactic such as par-then could be used to solve the component-CSPs in parallel.
It would be very useful if one could limit the number of threads used by par-then.
Mar 1, 2016 at 12:46 PM
This dicussion board is not in use anymore as Z3 has moved to GitHub. For this kind of request, please submit a new issue in our issue tracker.