Support mixing low-level and high-level SMT APIs

[rbtying]

Since not all of the functions are supported in the high-level API (e.g. bvsgt for bitvectors), would it be possible to allow exposing those by having the low-level AST be usable mixed with the high-level API?

[oeb25]

Yeah I think this would be a good thing to allow for! I, however, want to be careful what is exposed, since I'd like the smtlib crate to be "type safe", which is to say, all code that passes the Rust type checker should also pass the smtlib type checker. Allowing arbitrary smtlib construction would make this guarantee hard to enforce. But some middle ground or escape hatch would be great!

Currently we have Term as the untyped core AST building block, and all typed wrappers such as Real, Int, Bool have Into<Term> and From<Term>, so one can go back and forth between the typed and untyped. It is not particularly ergonomic however, and constructing applications can be done with Term::Application but that isn't that great either.

I'd like to attempt to have as many of the smtlib API's exposed in the high-level crate, and minimize the need for interacting with the low-level crate. Something along the lines of "anytime the low-level API is needed, it should be considered a bug in the high-level API." I don't know how realistic this is as a rule, but I'd like to try and see how far we can push it. In that spirit, feel free to open more issues about specific API's that are missing! I've gone ahead and added a few more bitvector API's as a starting point.

[rbtying]

Yup, this makes sense.

Out of curiosity, how are you thinking about contributions to this library? I came across it due to wanting to use Z3 in Advent of Code and ran into some issues, but I don’t mind trying to fix them myself.

[oeb25]

Oh I'd be more than happy to receive PR's!

And in general if you find any annoyances feel free to open issues, even for the smallest thing; could prevent future users from hitting them again. I know I found a few when I did Advent of Code, as well 😉