Z3ソルバー差ロジックのpython API

Question

私はpythonでこのような何かをしようとしてきた：私は、ソルバー（solver.set('smt.arith.solver', 1)）のためにそれを行うことができました

(set-option :smt.arith.solver 1) 
(declare-const x Int) 
(declare-const y Int) 
(assert (>= 10 x)) 
(assert (>= x (+ y 7))) 
(maximize (+ x y)) 
(check-sat) 

、しかしでそれを行うことはできませんクラスを最適化する。 Pythonで上記のようなことを書くことは可能ですか？

また、通常の整数リニアプログラムを取得した場合、差分ロジックに設定されたソルバーはエラーをスローしますか？

Answer 1

ロジックを記述するための標準的な方法は、あなたがSolverFor（）の工場を使用して、ソルバーのインスタンスを作成するときに、ロジックのSMT-LIBの名前を提供することである（https://z3prover.github.io/api/html/z3.htmlを参照）

設定する必要はありませんロジックがZ3を動作させるためには、ロジックについて心配することなく、問題の作業バージョンに到達する価値があるかもしれません。