使用 Z3 求解器获取表达式
Get expression using Z3 solver
我是 Z3 求解器和 SMTLib2 的新手。我想获得约束中每个变量的表达式。假设，我有这个程序。
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))
使用get-value，我可以获得满足所有约束的z的值。但是，我怎样才能得到 z 的表达式呢？类似于 z=y+11。
我发现使用 simplify，我可以简化约束，但无论如何都可以为约束中的每个变量获取表达式。
Z3 是第一个也是最重要的 SMT 求解器；它解决存在性问题，即它只会表明存在一个解决方案，它不会计算所有解决方案的封闭形式。
就是说，有一些方法至少可以获得该形式的某些结果，例如通过上述的简化，或者如果逻辑允许的话可能通过量词消除（例如参见 [=10= ]).
如果需要多个但可能不是所有模型，请查看 Z3: finding all satisfying models 并搜索多个其他类似标题的问题。
我是 Z3 求解器和 SMTLib2 的新手。我想获得约束中每个变量的表达式。假设，我有这个程序。
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))
使用get-value，我可以获得满足所有约束的z的值。但是，我怎样才能得到 z 的表达式呢？类似于 z=y+11。
我发现使用 simplify，我可以简化约束，但无论如何都可以为约束中的每个变量获取表达式。
Z3 是第一个也是最重要的 SMT 求解器；它解决存在性问题，即它只会表明存在一个解决方案，它不会计算所有解决方案的封闭形式。
就是说，有一些方法至少可以获得该形式的某些结果，例如通过上述的简化，或者如果逻辑允许的话可能通过量词消除（例如参见 [=10= ]).
如果需要多个但可能不是所有模型，请查看 Z3: finding all satisfying models 并搜索多个其他类似标题的问题。