尝试rise4fun / z3 / tutorial / strategies中的示例

Question

来自rise4ful-site的一些示例：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a Int)        ;  this is added

(assert (= a 3 ))            ; this is added:  a := 3
(assert (< 0 x  10))         ; rewritten, but same constraint
(assert (< 0 y  10))
(assert (< 0 z  10))

(assert (= (+ (* 3 y) (* 2 x)) z))        ; plain function from rise4fun
;(assert (= (+ (* a y) (* 2 x)) z))       ; here literal 3 is replaced by a

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                       normalize-bounds
                       lia2pb
                       pb2bv
                       bit-blast
                       sat))
(get-model)
(get-info :version)

当我注释rise4fun中的普通函数并取消注释我的函数时，求解器将无法生成结果并返回'unknown‘(已尝试使用4.8.0)。求解器或某个预处理器是否足够聪明，可以看到'a‘只是一个固定值为3的常量？

Answer 1

没错，simplify策略不够智能，无法传播值，因为它通常代价太高。但是，ctx-simplify或propagate-values可以完成这项工作。例如：

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                       propagate-values
                       normalize-bounds
                       lia2pb
                       pb2bv
                       bit-blast
                       sat))