Groups
Sign in
Groups
pySMT
Conversations
About
Send feedback
Help
pySMT
Contact owners and managers
1–24 of 24
Mark all as read
Report group
0 selected
marco...@gmail.com
Jun 24
pySMT 0.9.6: CVC5 and upgraded solvers
pySMT 0.9.6 is out! What's Changed: Fixed issue #613 by @mikand in #710 - Thanks @ekiwi for
unread,
pySMT 0.9.6: CVC5 and upgraded solvers
pySMT 0.9.6 is out! What's Changed: Fixed issue #613 by @mikand in #710 - Thanks @ekiwi for
Jun 24
jian cao
,
Andrea Micheli
2
Jan 24
How to solve both real and integer problems simultaneously?
Hello Jian, sorry for the late reply. Pysmt is strict about typing, you cannot compare an integaer
unread,
How to solve both real and integer problems simultaneously?
Hello Jian, sorry for the late reply. Pysmt is strict about typing, you cannot compare an integaer
Jan 24
Michele Lombardi
,
Andrea Micheli
4
7/15/21
Time limit?
Did you also experience problems with the `Portfolio` meta-solver [1]? There, we use the normal `
unread,
Time limit?
Did you also experience problems with the `Portfolio` meta-solver [1]? There, we use the normal `
7/15/21
Ipsita Koley
,
Andrea Micheli
2
8/30/19
z3py issue
Dear Ipsita, this seems a problem with z3py, not pysmt (http://pysmt.org). Anyhow, it's hard to
unread,
z3py issue
Dear Ipsita, this seems a problem with z3py, not pysmt (http://pysmt.org). Anyhow, it's hard to
8/30/19
Sree Harsha
, …
Marco Gario
6
3/18/19
How to solve this error?
ITS WORKING IN LINUX On Saturday, March 16, 2019 at 9:36:46 PM UTC-5, Rocky wrote: getting an error
unread,
How to solve this error?
ITS WORKING IN LINUX On Saturday, March 16, 2019 at 9:36:46 PM UTC-5, Rocky wrote: getting an error
3/18/19
Marco Gario
1/27/19
Announcement
pySMT 0.8.0: Better Install and Great Community
pySMT 0.8.0 is out! This release is way overdue and contains a lot of improvements collected over the
unread,
Announcement
pySMT 0.8.0: Better Install and Great Community
pySMT 0.8.0 is out! This release is way overdue and contains a lot of improvements collected over the
1/27/19
sy...@mics.snu.ac.kr
,
Andrea Micheli
5
10/22/18
How to write a function in PySMT?
Yes I understood. It helps a lot. Thanks 2018년 10월 22일 (월) 오후 5:26, Andrea Micheli <micheli.andrea
unread,
How to write a function in PySMT?
Yes I understood. It helps a lot. Thanks 2018년 10월 22일 (월) 오후 5:26, Andrea Micheli <micheli.andrea
10/22/18
Marco Gario
6/30/18
RFC: Python 2 deprecation
If you are using python 2 with pySMT, please take a look at issue 504 [1] and leave a comment. Thanks
unread,
RFC: Python 2 deprecation
If you are using python 2 with pySMT, please take a look at issue 504 [1] and leave a comment. Thanks
6/30/18
Marco Gario
5/29/18
pySMT 0.7.5: Strings and Cython Parser
pySMT 0.7.5 is out! This release includes several bugfixes and updates, and it provides initial
unread,
pySMT 0.7.5: Strings and Cython Parser
pySMT 0.7.5 is out! This release includes several bugfixes and updates, and it provides initial
5/29/18
Sanjai Narain
,
Marco Gario
3
3/20/18
Obtaining a conjunctive normal form of a PySMT formula
Can you provide more information on what are you trying to accomplish? Of the solutions I mentioned
unread,
Obtaining a conjunctive normal form of a PySMT formula
Can you provide more information on what are you trying to accomplish? Of the solutions I mentioned
3/20/18
Sanjai Narain
,
Andrea Micheli
3
2/12/18
Multiplication question
Thanks, Andrea. That worked. BTW, Z3Py is forgiving of this. -- Sanjai On Monday, February 12, 2018
unread,
Multiplication question
Thanks, Andrea. That worked. BTW, Z3Py is forgiving of this. -- Sanjai On Monday, February 12, 2018
2/12/18
陳宏毅
,
Marco Gario
3
9/16/17
Will it matter anything if "The logic QF_BV is not reducible to any SMTLib2 standard logic"
I cannot reproduce. If you could share the formula (in smt format or the code to generate it) that
unread,
Will it matter anything if "The logic QF_BV is not reducible to any SMTLib2 standard logic"
I cannot reproduce. If you could share the formula (in smt format or the code to generate it) that
9/16/17
陳宏毅
,
Andrea Micheli
2
8/31/17
The bit-width transformation of bit vectors
Hi! in SMT the width of each BV variable must be fixed, there is no way to dynamically extend it to
unread,
The bit-width transformation of bit vectors
Hi! in SMT the width of each BV variable must be fixed, there is no way to dynamically extend it to
8/31/17
陳宏毅
,
Andrea Micheli
4
8/30/17
Matrix Computation by bitvectors
I have tried BV(int(Mat[i][j]), 8) Then this works. 陳宏毅於 2017年8月28日星期一 UTC+2上午11時14分22秒寫道: Dear
unread,
Matrix Computation by bitvectors
I have tried BV(int(Mat[i][j]), 8) Then this works. 陳宏毅於 2017年8月28日星期一 UTC+2上午11時14分22秒寫道: Dear
8/30/17
Marco Gario
8/12/17
Announcement
pySMT 0.7.0: Class Based Walkers and Sorts
pySMT 0.7.0 is out! This release changes and simplifies the way we construct walkers by defining the
unread,
Announcement
pySMT 0.7.0: Class Based Walkers and Sorts
pySMT 0.7.0 is out! This release changes and simplifies the way we construct walkers by defining the
8/12/17
Filipe Pereira
,
Andrea Micheli
4
7/25/17
Solver instalation problems
Glad it worked! Best, Andrea On Tue, Jul 25, 2017 at 5:04 PM, Filipe Pereira <filipe.pereira.1995@
unread,
Solver instalation problems
Glad it worked! Best, Andrea On Tue, Jul 25, 2017 at 5:04 PM, Filipe Pereira <filipe.pereira.1995@
7/25/17
averm...@gmail.com
,
Marco Gario
4
7/22/17
pysmt-install --cvc4 not working
Hi, The following line looks suspicious: "configure: WARNING: could not figure out which toolset
unread,
pysmt-install --cvc4 not working
Hi, The following line looks suspicious: "configure: WARNING: could not figure out which toolset
7/22/17
Matthias Heinzmann
,
Andrea Micheli
2
6/27/17
timing in pySMT
For some reason, this is a re-post of an old discussion. See https://groups.google.com/d/msgid/pysmt/
unread,
timing in pySMT
For some reason, this is a re-post of an old discussion. See https://groups.google.com/d/msgid/pysmt/
6/27/17
Matthias Heinzmann
, …
Andrea Micheli
3
4/24/17
timing in pySMT
Just a follow up on Marco's answer. Keep in mind that creating a new solver in pysmt is not like
unread,
timing in pySMT
Just a follow up on Marco's answer. Keep in mind that creating a new solver in pysmt is not like
4/24/17
Ming Yang Koh
,
Andrea Micheli
3
3/23/17
how to duplicate solvers in pysmt for divergent incremental solving?
hello Andrea! that helps! thank you! On Monday, 20 March 2017 17:09:49 UTC+8, Andrea Micheli wrote:
unread,
how to duplicate solvers in pysmt for divergent incremental solving?
hello Andrea! that helps! thank you! On Monday, 20 March 2017 17:09:49 UTC+8, Andrea Micheli wrote:
3/23/17
Marco Gario
12/3/16
Announcement
pySMT 0.6.1: Portfolio and Coverage
pySMT 0.6.1 is out! For this release we have been working hard to improve the quality of the codebase
unread,
Announcement
pySMT 0.6.1: Portfolio and Coverage
pySMT 0.6.1 is out! For this release we have been working hard to improve the quality of the codebase
12/3/16
Marco Gario
10/9/16
Announcement
pySMT 0.6.0: GMPY2 and Goodbye Recursion
pySMT 0.6.0 is out! This is a quite big release with a few backwards incompatible changes. The most
unread,
Announcement
pySMT 0.6.0: GMPY2 and Goodbye Recursion
pySMT 0.6.0 is out! This is a quite big release with a few backwards incompatible changes. The most
10/9/16
Marco Gario
10/6/16
Announcement
Hacktoberfest 2016
Dear all, pySMT is participating in the Hacktoberfest 2016! By opening 4 Pull-Requests on your
unread,
Announcement
Hacktoberfest 2016
Dear all, pySMT is participating in the Hacktoberfest 2016! By opening 4 Pull-Requests on your
10/6/16
Marco Gario
8/17/16
pySMT 0.5.1: NIRA and Python 3.5
pySMT 0.5.1 is out! The highlights for this version are the support for Non-Linear Arithmetic and
unread,
pySMT 0.5.1: NIRA and Python 3.5
pySMT 0.5.1 is out! The highlights for this version are the support for Non-Linear Arithmetic and
8/17/16