kdrag.theories.real.sympy.solve

kdrag.theories.real.sympy.solve(constrs: list[BoolRef], vs: list[ExprRef]) → list[dict[ExprRef, ExprRef]]

>>> x,y,z = smt.Reals("x y z")
>>> solve([x + y == 1, x - z == 2], [x, y, z])
[{x: z + 2, y: -z - 1}]
>>> solve([real.cos(x) == 3], [x]) # Note that does not return all possible solutions.
[{x: 2*pi - acos(3)}, {x: acos(3)}]

Parameters:

• constrs (list[BoolRef])

• vs (list[ExprRef])

Return type:

list[dict[ExprRef, ExprRef]]