Marco Gario

I think the environment does not have an object to encapsulate user preferences at the moment. **Actions**: 1. Create an Options object in the environment to keep user preferences 2....

See #211 . This has been open for a while :( Ideally, the Printers check against annotations for each expression that they are writing. Unfortunately, annotations must be within the...

I can help with this (if it is still of interest). We are preparing the new release of pySMT (0.7.0) and afterwards, we would like to better understand possible use-cases...

We recently released [pySMT 0.7.0](https://github.com/pysmt/pysmt/releases/tag/v0.7.0) ! I am working on the next release (that will include the theory of Strings) but I would like to start working on this in...

I looked closer into this and looked into a couple of approaches. In particular, I was attempting to implement a PySMTSolver class that would be equivalent to Z3Solver and CVC4Solver...

https://github.com/programa-stic/barf-project/compare/master...marcogario:intro_pysmt?expand=1 I made an example of how the testcases in test_smtsolver.py would be converted after the introduction of pySMT. There are two points that I would like your opinion on:...

In pySMT we distinguish between expressions and the solver being used to reason on the expression. These are two distinct concepts that can live independently of each other. In many...

> I'll restore CVC4 then, but maybe we can exclude it from CI? Thanks, this would be my preference too.

Can you confirm that there is no solving involved here? When you say model you mean the formula/problem, right? How big is the final SMT file? It sounds that what...

As long as the python bindings for the solver can be found by the python interpreter that is running pysmt, then you should be able to use solvers installed by...