Marco Gario

Not in the short term, but we would be happy to shepherd a patch in this direction. When you say enum/datatypes do you mean the SMTLIB dataypes or something else?...

Upgrade of installer and wrapper in #514 . TODO: - Support for Quantified BV - Support for unsat core (solving under assumption) - Support for incremental interface

See WIP branch btor/quantifiers_and_unsat_core - Incremental Interface: - Implemented pop and push - **TODO**: `reset_assertions`, does not seem to be a corresponding method in Boolector. Might implement as a series...

Improved option-handling is part of PR #338 .

This is the syntax for the enums (#187). Note that our main concern there was how to encode/decode this information, since we assumed that the solver did not have a...

The following is the suggested syntax for arity 0. For higher arity or recursive types, this syntax might not work. Examples are welcome ```lisp (declare-datatypes ( (Color 0) ) (...

Yes, thanks for the link. I think I need to see some more "application" oriented examples: How would you expect to operate on datatypes? What are typical things you want...

> The syntax of creating a floating-point constant node. How is this done in SMT-LIB? How is this done in z3? These are typically things we look at to make...

Support for Z3 depends on newer versions of Z3 than the one we are currently using. Also, there are some open issues: https://github.com/Z3Prover/z3/issues/1219

Splitting this long-standing PR into a first part for the Theory and CVC4 support (#458). Leaving this open to track Z3 status. Currently, the Z3 bug was fixed, but the...