我已阅读“Sriram Sankaranarayanan、Henny B. Sipma 和 Zohar Mann”的论文“基于约束的线性关系分析”，通过在具有未知系数的给定模板不等式中应用 Farkas 引理来检查抽象解释产生的不动点方程，它计算对系数值的约束，以便将任何解代回模板中产生有效的不变关系。
我遵循了示例 1（在那张纸上）
Let V = {x, y}和L = { 0 }. 考虑如下所示的过渡系统。每个转换都模拟一个并发过程，它会自动更新变量 x、y。
Θ = (x = 0 ∧ y = 0)
T = {τ1 , τ2 }
τ1 = <l0 , l0 , [x' = x + 2y ∧ y' = 1 − y]>
τ2 = <l0, l0 , [x' = x + 1 ∧ y' = y + 2]>
我通过使用 Farkas 引理（该纸上的示例 2）以及连续（通过转换 τ1 和 τ2）对 Initiation 进行了编码。
作者说：
Π我们用变量固定一个线性转移系统{x1 , . . . , xn }，统称为 x。假设系统具有单个位置以简化演示。位置的模板断言是α(c) = c1 x1 + · · · + cn xn + d ≥ 0. 系数变量{c1 , . . . , cn , d}统称为c。系统的转换是{τ1 , . . . , τm }，其中τi : , , ρi。初始条件用 Θ 表示。示例 1 中的系统将用作运行示例来说明所提出的想法。
我已经达到了通过将每个转换的启动和连续获得的约束结合起来获得的总体约束（该论文上的示例 4）。
在那一点上，我想可以通过将所有这些编码到像Z3. 事实上，我是通过将线性算术直接编码为Z3：
(define-sort MyType () Int)
(declare-const myzero MyType)
(declare-const mi1 MyType)
(declare-const mi2 MyType)
(declare-const c1 MyType)
(declare-const c2 MyType)
(declare-const d MyType)
(assert (= myzero 0))
;initiation
(assert (>= d 0) )
;transition 1
(assert (and
(= (- (* mi1 c1) c1) 0)
(= (- (+ (* mi1 c2) c2) (* 2 c1) ) 0)
(<= (- (- (* mi1 d) d) c2) 0)
(>= mi1 0)
))
;transition 2
(assert (and
(= (- (* mi2 c1) c1) 0)
(= (- (* mi2 c2) c2) 0)
(<= (- (- (- (* mi2 d) d) c1) (* 2 c2) ) 0)
(>= mi2 0)
))
(check-sat)
(get-model)
我想一旦我没有l0通过c1, c2, ...,cn找出位置处的任何归纳不变量d作为单个（o范围）值，我就做得不好。
Z3 对所有系数的回答为零：
sat
(model
(define-fun mi2 () Int 0)
(define-fun c2 () Int 0)
(define-fun mi1 () Int 0)
(define-fun c1 () Int 0)
(define-fun d () Int 4)
(define-fun myzero () Int 0)
)
我试图找到相关的例子，但直到现在还没有运气。