My Example: system of equations
Pseudo-Code Constraint Base
a = b+c
∧ e = a*c
∧ a = +2 ; some replaceable concrete values
∧ c = +18
Solution
b = -16
∧ e = -32
The Information I Want
In a system of equations, I want to get the following knowledge:
Abstract formulas which I can use to compute the variable values (the solution) from the given values (in the constraint base).
(Like in high school where the teacher don't just wanted the see the result, but also such an transformated abstract formula.)
Formulas Like ...
b = a-c ; is an equivalent transformation from `a = b+c`
∧ e = (a-c)*c ; is an term replacement `b → a-c` of `e = a*c`
My Question
How can I use Z3Py retrieve this information from a Z3 constraint system of equations?
Thanks. - If anything's unclear, please comment concerning what's wrong.
Z3 is not the ideal tool for extracting this kind of information.
Internally, it has modules (e.g., Gaussian elimination, Groebner Basis) that may be useful for implementing this kind of functionality for particular cases, but they are not exposed in the Z3 API.
The Z3 source code is available online.
The problem you described is interesting, but it is also non trivial. In general, the input is not just a set of equations. Moreover, even if we have only equations, but they are nonlinear, then it may not be possible to get a "solved" form like the one described in your question. In the nonlinear case, we may put the equations in triangular form, but that is it. Another issue is that even when the number of solutions is finite, it is not unique like in the linear case.
Moreover, in general, the solution of a nonlinear set of equations can't be expressed using radicals. Internally, Z3 uses real algebraic numbers for representing the solution.
