2

g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) を使用して式を満たす A、B、C、D の値を見つけようとしますsolve(g) 。これには多くの可能な解決策があります.1つはA=1,B=-1,C=D=0Z3がこれを行うことができないようです（solve(g)終了しません）.

Z3 はこの種の非線形 (しかし単純な) 式を実行できますか? おそらく、これに対していくつかのQE戦略または何かを指定できますか？

4

1 に答える 1

4

Z3 has a quantifier elimination tactic. We can enable it by creating a solver using:

s = Then('qe', 'smt').solver()

This command will create a solver that first applies quantifier elimination and then invokes a SMT solver. However, Z3 has very limited support for quantifier elimination of nonlinear formulas. Your examples is nonlinear because it contains: A * i + B * j + C * k + D <= 0. So, the qe tactic will not be able to eliminate the quantifier.

It would be great if you could implement better QE support for nonlinear arithmetic.

于 2013-02-19T02:08:07.957 に答える