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 <[email protected]> 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 <[email protected]> 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 [email protected]. >> To post to this group, send email to [email protected]. >> 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 [email protected]. > To post to this group, send email to [email protected]. > 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/CAE4GFin7GNCV3NcrxzabDMP%2BD25ZMkDzhjCJJjAq1KMjVTE9TA%40mail.gmail.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 [email protected]. To post to this group, send email to [email protected]. 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/CAKgW%3D6KBoK2BuBa0JmpBoXKZG%3D9V0%3DnNv39MvTDedQo4Ds_QOQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
