2016-05-18 52 views
1

C++ APIを使用して、指定されたシンボリック変数の最適化を得るにはどうすればよいですかSymVar_0最大化/最小化Z3 SMT C++ API

私はthis postを見ましたが、それを使用する方法についてはっきりしません。

(set-logic QF_AUFBV)(declare-fun SymVar_0() (_ BitVec 32))(declare-fun SymVar_1() (_ BitVec 8))(declare-fun SymVar_2() (_ BitVec 8))(declare-fun SymVar_3() (_ BitVec 8))(declare-fun SymVar_4() (_ BitVec 8))(declare-fun SymVar_5() (_ BitVec 8))(declare-fun SymVar_6() (_ BitVec 8))(declare-fun SymVar_7() (_ BitVec 8))(declare-fun SymVar_8() (_ BitVec 8))(declare-fun SymVar_9() (_ BitVec 8))(declare-fun SymVar_10() (_ BitVec 8))(declare-fun SymVar_11() (_ BitVec 8))(declare-fun SymVar_12() (_ BitVec 8))(declare-fun SymVar_13() (_ BitVec 8))(declare-fun SymVar_14() (_ BitVec 8))(declare-fun SymVar_15() (_ BitVec 8))(declare-fun SymVar_16() (_ BitVec 8))(declare-fun SymVar_17() (_ BitVec 8))(assert (= (ite (= ((_ extract 0 0) (ite (= ((_ extract 31 0) (bvsub (concat ((_ extract 7 0) ((_ extract 31 24) SymVar_0)) ((_ extract 7 0) ((_ extract 23 16) SymVar_0)) ((_ extract 7 0) ((_ extract 15 8) SymVar_0)) ((_ extract 7 0) ((_ extract 7 0) SymVar_0))) ((_ sign_extend 0) (_ bv2 32)))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1)) (_ bv4198495 32) (_ bv4198490 32)) (_ bv4198495 32)))(assert (bvsge SymVar_0 (_ bv1 32)))(minimize SymVar_0) 

これまでの数式を最適化します。

おかげ

答えて

3

Z3が付属してC++の例もopt_exampleを参照して、最適化のためにそれを使用する方法の例が含まれています。

関連する問題