consider z3 implementation of ASP concretizer

[cosmicexplorer]

We would like to determine whether z3 can be used in the place of clingo for the new concretizer implemented in #19501.

Rationale

• z3 is more widely used, and may be more performant (this needs to be verified).
• Initially, we thought z3 would be easier to bootstrap. But as per the discussion in vendor libstdc++ and clingo for bootstrapping from source in arcane environments #20123 and the changes in clean up how spack builds clingo #20159, it seems like clingo will also bootstrap successfully. But we need to verify that either will build and run on all of spack's supported platforms.

Description

• Implement a z3 solver which produces similar output to Experimental ASP-based concretizer #19501 (currently in https://github.com/spack/spack/tree/z3-concretizer).
• If we can validate in CI that clingo builds in a 2.6, C++11-only environment, we can close this issue.

[cosmicexplorer]

We are pretty sure this is a reasonable thing to do, so closing this issue.