最大化/最小化 Z3 SMT C++ API

Question

如何使用 C++ API 对给定的符号变量 SymVar_0 进行优化？

我见过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)

看看我要优化之前的公式。

谢谢

Answer 1

Z3 附带的 C++ 示例还包含如何使用它进行优化的示例，请参阅opt_example。