Marco Gario
Marco Gario
SMT-LIB 2.6 introduces datatypes and the match operator. As a first implementation, I would focus only on non-recursive datatypes. Datatypes: - Extend the Type system to include datatypes - Define...
When writing ``1 + x`` python tries the ``__radd_`` operator, and here we can perform the casting of left operand. Some right-hand operators are currently not implemented in Fnode. These...
https://github.com/SRI-CSL/yices2/releases/tag/Yices-2.6.0
We have a concept of Array constant, and we have a way to manipulate it after reading a model etc. However, the simplifier does not seem to be using it....
Many changes with boolector 3, including licensing, source repo, and support for quantified bv. https://github.com/boolector/boolector
In many cases we need to encode an SMT formula `f` into an equisatisfiable one `g`. Currently, pySMT has no way of doing this systematically. This issue is for discussing...
Support for Strings Theory #245 - For now the only solver supporting this is CVC4
This issue is to keep track of the status of support of Microsoft Windows (win from now on). Each solver should be tested on win and, if it works, the...
This issue is to keep track of the status of support of OSX. Each solver should be tested on OSX and, if it works, the installer (pysmt-install) should be able...
Coverage report [1] shows that we are not testing the smtlibscript with any incremental problem (use of push-pop). It should be reasonably straight forward to address this, and add a...