我有一个代码z3
,旨在解决布尔公式的优化问题
(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000)
(declare-const a0 Int) (assert (= a0 2))
(declare-const b0 Int) (assert (= b0 2))
(declare-const c0 Int) (assert (= c0 (- 99999)))
(declare-const d0 Int) (assert (= d0 99999))
(declare-const e0 Int) (assert (= e0 49))
(declare-const f0 Int) (assert (= f0 49))
(declare-const a1 Int) (assert (= a1 3))
(declare-const b1 Int) (assert (= b1 3))
(declare-const c1 Int) (assert (= c1 (- 99999)))
(declare-const d1 Int) (assert (= d1 99999))
(declare-const e1 Int) (assert (= e1 48))
(declare-const f1 Int) (assert (= f1 49))
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(define-fun max ((x Int) (y Int)) Int
(ite (>= x y) x y))
(define-fun min ((x Int) (y Int)) Int
(ite (< x y) x y))
(define-fun goal ((c Int) (d Int) (e Int) (f Int)) Int
(* (- d c) (- f e)))
(define-fun sat ((c Int) (d Int) (e Int) (f Int)) Bool
(and (and (>= d c) (>= f e))
(forall ((x Int)) (=> (and (<= a0 x) (<= x b0))
(> (max c (+ x e)) (min d (+ x f)))))))
(assert (and (sat c d e f)
(forall ((cp Int) (dp Int) (ep Int) (fp Int)) (=> (sat cp dp ep fp)
(>= (goal c d e f) (goal cp dp ep fp))))))
(check-sat)
我猜是因为量词和含义,这段代码成本很高。当我在线测试时,它给了我2个警告,最终结果是unknown
:
failed to find a pattern for quantifier (quantifier id: k!33)
using non nested arith. pattern (quantifier id: k!48), the weight was increased to 1000000000 (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>). timeout`.
谁能告诉我这两个警告是否会避免获得良好的结果?有什么办法可以优化这段代码使其运行吗?