has anyone used Z3?

[Chris Smith]

I just learned about Z3 which is something that could help with the SymPy assumption system or solving relational system (perhaps multivariate) as someone was trying to do here. It has an MIT license.

/c

[SHUBHAM JHA]

Hello Chris,

Z3 is a powerful SMT solver by Microsoft and also has a Python wrapper that is used here. As suggested by Aaron here, I have proposed an SMT solver in my GSoC project which will be based on open source projects like Z3. I have already started looking into it and would love to implement such in SymPy.

Regards,

Shubham

On Mon, May 6, 2019 at 11:02 AM Chris Smith <smi...@gmail.com> wrote:

I just learned about Z3 which is something that could help with the SymPy assumption system or solving relational system (perhaps multivariate) as someone was trying to do here. It has an MIT license.

/c

--
You received this message because you are subscribed to the Google Groups "sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email to sympy+un...@googlegroups.com.
To post to this group, send email to sy...@googlegroups.com.
Visit this group at https://groups.google.com/group/sympy.
To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/57c11b15-e7e3-44f1-bcab-2e90aa1ff83b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Aaron Meurer]

I have used Z3 a bit. As Shubham noted, I think an SMT solver is what
is needed to push the assumptions system to the next level. The satask
solver is already somewhat a SMT system, but because it has
performance issues because in part because it is not a true SMT solver
(it doesn't incorporate the theories into the solver itself).

It may also be interesting to play with using Z3 as an optional
backend to SymPy.

Aaron Meurer

> To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CAE4GFin7GNCV3NcrxzabDMP%2BD25ZMkDzhjCJJjAq1KMjVTE9TA%40mail.gmail.com.

[Chris Smith]

I just happened across another constraint solving option: python-constraint

The Python constraint module offers solvers for Constraint Solving Problems (CSPs) over finite domains in simple and pure Python. CSP is class of problems which may be represented in terms of variables (a, b, ...), domains (a in [1, 2, 3], ...), and constraints (a < b, ...).

On Monday, May 6, 2019 at 12:35:45 PM UTC-5, Aaron Meurer wrote:

I have used Z3 a bit. As Shubham noted, I think an SMT solver is what
is needed to push the assumptions system to the next level. The satask
solver is already somewhat a SMT system, but because it has
performance issues because in part because it is not a true SMT solver
(it doesn't incorporate the theories into the solver itself).

It may also be interesting to play with using Z3 as an optional
backend to SymPy.

Aaron Meurer

On Mon, May 6, 2019 at 7:11 AM SHUBHAM JHA <skjh...@gmail.com> wrote:
>
> Hello Chris,
>
> Z3 is a powerful SMT solver by Microsoft and also has a Python wrapper that is used here. As suggested by Aaron here, I have proposed an SMT solver in my GSoC project which will be based on open source projects like Z3. I have already started looking into it and would love to implement such in SymPy.
>
> Regards,
> Shubham
>
> On Mon, May 6, 2019 at 11:02 AM Chris Smith <smi...@gmail.com> wrote:
>>
>> I just learned about Z3 which is something that could help with the SymPy assumption system or solving relational system (perhaps multivariate) as someone was trying to do here. It has an MIT license.
>>
>> /c
>>
>> --
>> You received this message because you are subscribed to the Google Groups "sympy" group.

>> To unsubscribe from this group and stop receiving emails from it, send an email to sy...@googlegroups.com.

>> To post to this group, send email to sy...@googlegroups.com.
>> Visit this group at https://groups.google.com/group/sympy.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/57c11b15-e7e3-44f1-bcab-2e90aa1ff83b%40googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "sympy" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to sy...@googlegroups.com.