Describe the improvement you'd like to request
The LocalSolver implementation in cedar-policy-symcc/src/symcc/solver.rs extracts solver models by looking for a specific text shape "(\n<the actual model>\n)\n".
A more robust implementation could instead parse the S-expression returned by the solver.
Reusing the implementation in decoder.rs would also make it easier to have a single implementation of what the solver output is expected to be.
Describe alternatives you've considered
Leave the lightweight implementation in place, since only CVC5 models that follow this convention are supported.
Additional context
No response
Is this something that you'd be interested in working on?
Describe the improvement you'd like to request
The
LocalSolverimplementation incedar-policy-symcc/src/symcc/solver.rsextracts solver models by looking for a specific text shape"(\n<the actual model>\n)\n".A more robust implementation could instead parse the S-expression returned by the solver.
Reusing the implementation in
decoder.rswould also make it easier to have a single implementation of what the solver output is expected to be.Describe alternatives you've considered
Leave the lightweight implementation in place, since only CVC5 models that follow this convention are supported.
Additional context
No response
Is this something that you'd be interested in working on?