Category
Lean formalization, DRT target(s)
Describe the feature you'd like to request
While we know Symcc will often generate smtlib scripts z3 can't handle (bitvector and set operations), it should ideally be correctly parse any models returned by z3 on a successful query.
We should add copies of symcc-cex-drt.rs and symcc-cex-pbt.rs using z3 instead of cvc5. The targets will need to be updated to ignore expected error from z3 on input that it doesn't support.
There is currently one known z3 model parsing issue cedar-policy/cedar#2415, so the pbt target is expected to fail until that is fixed. We could still add a DRT target before fixing it to test that the Rust and Lean model parsing are equivalent for the z3 models we currently handle.
Describe alternatives you've considered
.
Additional context
No response
Is this something that you'd be interested in working on?
Category
Lean formalization, DRT target(s)
Describe the feature you'd like to request
While we know Symcc will often generate smtlib scripts z3 can't handle (bitvector and set operations), it should ideally be correctly parse any models returned by z3 on a successful query.
We should add copies of symcc-cex-drt.rs and symcc-cex-pbt.rs using z3 instead of cvc5. The targets will need to be updated to ignore expected error from z3 on input that it doesn't support.
There is currently one known z3 model parsing issue cedar-policy/cedar#2415, so the pbt target is expected to fail until that is fixed. We could still add a DRT target before fixing it to test that the Rust and Lean model parsing are equivalent for the z3 models we currently handle.
Describe alternatives you've considered
.
Additional context
No response
Is this something that you'd be interested in working on?