Status
A discussion of what theories are supported in Smtlink and what we
intend to support in the future.
SMT solvers
Currently only Z3 is supported.
Theories
Currently Smtlink supports:
- Basic types: booleanp, integerp, real,
rationalp, real/rationalp and symbolp
- FTY types generated using: defprod, deflist,
defalist and defoption
- Basic functions: binary-+, binary-*, unary-/, unary--, equal, <, implies, if, not, and lambda
- Functions associated with FTY types:
- defprod: recognizer, fixer, constructor, and field accessors.
- deflist: recognizer, fixer, cons, car, cdr
and consp.
- defalist: recognizer, fixer, acons, and assoc-equal
- defoption: recognizer, fixer, constructor, and field-accessor.
Wishlist
- Using ACL2::meta-extract capability introduced in year 2017 Workshop for
fully verifying several of the verified clause-processors in the architecture.
This will improve performance.
- Develop type inference engine to remove the burden on the user for
providing type information.
- Generate ACL2 evaluatable counter-examples.
- Adding support for SMT-LIB.
- Build a computed hint for Smtlink so that it's automatically fired on goals
that seems likely to be solved by Smtlink, possibly recognizing induction
steps.
- Do proof reconstruction for the trusted clause-processor so that ACL2
doesn't have to trust an external procedure.
