wenkokke
commented
1 year ago What is Schmitty?
For the purposes of integrating with agda2hs, we should consider Schmitty as two different projects:
- An embedding of a subset of the SMTLIB language in Agda & tactics to call Z3 and other solvers at compile-time.
- A set of reflection tactics to convert from the types in the standard library to the embedding of SMTLIB.
What solvers does Schmitty support?
Currently, Schmitty has tactics for Z3 and CVC4. Adding bindings for other SMTLIB-compatible solvers is very easy and can be done in only a few lines of code. It's only a matter of crafting the right command-line invocation—the rest is boilerplate. For an example, see Z3.agda.
What theories does Schmitty support?
Currently, Schmitty supports reasoning about naturals, integers, and reals.
- Test_Scripts_Z3_Ints.agda: This test writes an SMTLIB script that uses the theory of integers.
- Test_Reflection_Z3_Ints.agda This tests uses the same theory of integers, but uses the reflection tactics.
Adding support for new theories is possible, but the amount of work will vary with the complexity of the theory. For a theory that is directly supported by SMITLIB, such as integers, you have to specify:
- the sorts, literals, and identifiers the theory adds, and how these render in SMTLIB; and
- the values that may be returned as part of a model, and how these are parsed from SMTLIB.
For a theory that uses some sort of encoding, such as the theory of naturals, you also have to specify that encoding.
Support algebraic datatypes should be fairly simple to add, as it was officially added to SMTLIB in version 2.5. This wouldn't be the same as adding a theory, since datatypes are declared by a declare-datatype statement, which would mean extending the Script type. This should be relatively easy, but may involve some complications depending on how precise you want to be about enforcing that the script type is well-scoped by construction.
How stable is Schmitty?
Schmitty is stable, but there is a pending refactoring to use composible languages following composable-semantics.
Difficulties integrating Schmitty with agda2hs
The major difficulties I foresee is that Schmitty relies on the standard library and agdarsec. I assume agda2hs has its own standard library, which is presumably incompatible with the Agda standard library.
Schmitty's use of the standard library is fairly minimal, and it could probably be rewritten to only use Agda builtin modules.
I believe agdarsec is very tightly coupled with the standard library, so for Schmitty to be portable across different standard libraries we would probably have to:
- abstract over an implementation of parser combinators;
- switch to an implementation of parser combinators that is, itself, portable; or
- bundle a minimal implementation of parser combinators with Schmitty itself.
uhbif19
jespercockx
It would be very useful if one could use Z3 or another SMT solver to automatically dismiss proof obligations for obvious statements. There is already such an integration with Agda: Schmitty (https://github.com/wenkokke/schmitty/). We should check what is needed to integrate Schmitty into an Agda2Hs project and whether we can do anything to make it easier to use (e.g. provide predefined theories for types and functions from the Prelude).