在C ++中使用Z3解决表达式变量

Question

如何编写带有2个z3表达式的方程式

z3::exp x;
Z3::exp y;

如何获得z3::exp Z= x+10*y形式的线性方程>

例如，如何使用Z3表达式求解表达式变量，我具有以下方程组：

 x = a+b;
 a = 2*y;
 b = 4*c;
如何获得x =  2*y + 4*c，其中x，y，b和c均为z3表达式

如何写具有2个z3表达式的方程式，例如z3 :: exp x; Z3 :: exp y;如何获得z3 :: exp Z = x + 10 * y形式的线性方程式？如何使用...

Answer 1

类似这样的方法应该起作用：