我可以在另一個SMT表達式中使用SMT程序的結果嗎？

Question

我想在另一個模型中使用一個模型的輸出（在我的情況下坐下來和不滿足）。在這裏，模型是對一組邏輯公式中涉及的常量（本例中爲Z3表達式）的令人滿意的分配。我的目標可以簡要解釋如下。

我的問題可以詳細描述如下：我有一個形式化的問題P，一組邏輯公式（表達式）對應一些約束（C）。在這些表達式中，一個（例如，Ai> 0）是我的目標。執行模型/形式化P返回sat，如果所有的約束都是可滿足的。請注意，Ai = 0始終是可能的。 現在，我想找到一組特定變量對應的約束（C），確保Ai> 0（對於任何i）是不可能的。 目前，我正在通過編寫一個程序（使用C＃）來開發一個基於DFS的約束搜索算法（即約束值），並通過「push /流行」。雖然我試圖讓搜索更好，但這對我沒有多大幫助。對於較大的問題規模而言效率很低。如果我能夠用P來創建另一個SMT程序（模型）來搜索這樣一個可滿足的集合，那將是非常好的。

問題P（短SMT LIB 2版原問題）目前形式化如下：

(declare-fun th1() Real) 
(declare-fun th2() Real) 
(declare-fun th3() Real) 
(declare-fun th4() Real) 
(declare-fun th5() Real) 

(declare-fun l1() Real) 
(declare-fun l2() Real) 
(declare-fun l3() Real) 
(declare-fun l4() Real) 
(declare-fun l5() Real) 
(declare-fun l6() Real) 
(declare-fun l7() Real) 

(declare-fun p1() Real) 
(declare-fun p2() Real) 
(declare-fun p3() Real) 
(declare-fun p4() Real) 
(declare-fun p5() Real) 

(declare-fun sl1() Int) 
(declare-fun sl2() Int) 
(declare-fun sl3() Int) 
(declare-fun sl4() Int) 
(declare-fun sl5() Int) 
(declare-fun sl6() Int) 
(declare-fun sl7() Int) 

(declare-fun sp1() Int) 
(declare-fun sp2() Int) 
(declare-fun sp3() Int) 
(declare-fun sp4() Int) 
(declare-fun sp5() Int) 

(declare-fun a1() Int) 
(declare-fun a2() Int) 
(declare-fun a3() Int) 
(declare-fun a4() Int) 
(declare-fun a5() Int) 

(declare-fun na() Int) 
(declare-fun ns() Int) 
(declare-fun attack() Bool) 

;;;; System 
(assert (and  (= l1 (* (- th2 th1) 17.0)) 
     (= l2 (* (- th5 th1) 4.5)) 
     (= l3 (* (- th3 th2) 5.05)) 
     (= l4 (* (- th4 th2) 5.65)) 
     (= l5 (* (- th5 th2) 5.75)) 
     (= l6 (* (- th4 th3) 5.85)) 
     (= l7 (* (- th5 th4) 23.75))   

     (= p1 (+ l1 l2)) 
     (= p2 (+ l1 l3 l4 l5)) 
     (= p3 (+ l3 l6)) 
     (= p4 (+ l4 l6 l7)) 
     (= p5 (+ l2 l5 l7)) 
     ) 
) 

;;;; Secured measurements 
(assert (and (or (= sl1 0) (= sl1 1)) 
     (or (= sl2 0) (= sl2 1)) 
     (or (= sl3 0) (= sl3 1)) 
     (or (= sl4 0) (= sl4 1)) 
     (or (= sl5 0) (= sl5 1)) 
     (or (= sl6 0) (= sl6 1)) 
     (or (= sl7 0) (= sl7 1)) 

     (or (= sp1 0) (= sp1 1)) 
     (or (= sp2 0) (= sp2 1)) 
     (or (= sp3 0) (= sp3 1)) 
     (or (= sp4 0) (= sp4 1)) 
     (or (= sp5 0) (= sp5 1))   
     ) 
)   

(assert (and (=> (not (= l1 0.0)) (= sl1 0)) 
     (=> (not (= l2 0.0)) (= sl2 0)) 
     (=> (not (= l3 0.0)) (= sl3 0)) 
     (=> (not (= l4 0.0)) (= sl4 0)) 
     (=> (not (= l5 0.0)) (= sl5 0)) 
     (=> (not (= l6 0.0)) (= sl6 0)) 
     (=> (not (= l7 0.0)) (= sl7 0))  

     (=> (not (= p1 0.0)) (= sp1 0)) 
     (=> (not (= p2 0.0)) (= sp2 0)) 
     (=> (not (= p3 0.0)) (= sp3 0)) 
     (=> (not (= p4 0.0)) (= sp4 0)) 
     (=> (not (= p5 0.0)) (= sp5 0))   
    ) 
) 

(assert (and (= sl1 1) (= sl2 1))) 

;;;; Attacks 
(assert (and (or (= a1 0) (= a1 1)) 
     (or (= a2 0) (= a2 1)) 
     (or (= a3 0) (= a3 1)) 
     (or (= a4 0) (= a4 1)) 
     (or (= a5 0) (= a5 1))  
    ) 
) 

(assert (and 
     (= (not (= th1 0.0)) (= a1 1)) 
     (= (not (= th2 0.0)) (= a2 1)) 
     (= (not (= th3 0.0)) (= a3 1)) 
     (= (not (= th4 0.0)) (= a4 1)) 
     (= (not (= th5 0.0)) (= a5 1))  
    ) 
) 

(assert (= th1 0.0)) // Base condition 
(assert (= na (+ a1 a2 a3 a4 a5))) 
(assert (=> attack (> na 1))) 


;;;; Check for satisfiable model 

(assert attack) 

(check-sat) 
(get-model) 
(exit) 

我想合成的安全措施（即，找到「SL」的分配和「SP」而言），這樣就沒有攻擊（即NA爲0）給定的約束，例如，如下：

(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5))) 
(assert (<= ns 4)) 

在這種情況下，斷言（即「（斷言（和（= sl11）（= sl21）））'）將被評論。目前，我開發了一個C＃程序，它分配'sl'和'sp'，聲明它們類似於（assert（和（= sl1 1）（= sl2 1）...））''，並執行給定的程序看看是否有任何可能的攻擊。當程序返回不成功時，我就完成了（即na> 1是不可能的）。有沒有辦法只用SMT（Z3）解決問題？

Answer 1

如果我理解正確，那麼您正在尋找（通用）量化。請原諒我的僞符號，但您是否在尋找一個令人滿意的賦值給下面的自由變量（config_params）？

config_constraints(config_params) -> forall attack_params: not attack_constraints(attack_params, config_params) 

其中()表示法僅指示約束依賴於哪個變量（集合）。我非常肯定.Net API支持量詞，因爲它們在Java API中。

Answer 2

感謝您解決問題。如果我已經理解了這些事情，則可以使用Z3執行搜索sli和spj的值，但無法僅使用SMT-LIB執行此操作，您需要使用API​​。我們的想法是從一個使用模型（滿意的分配）坐在檢查，這是未來的檢查約束，因爲這些答案詳細解釋：

Z3: finding all satisfying models

Z3: Check if model is unique

(Z3Py) checking all solutions for equation

這是你的例如Python的API中的編碼（z3py鏈路：http://rise4fun.com/Z3Py/KHzm）：

s = Solver() 

th1, th2, th3, th4, th5 = Reals('th1 th2 th3 th4 th5') 
th = { 'th1' : th1, 'th2' : th2, 'th3' : th3, 'th4' : th4, 'th5' : th5} 
l1, l2, l3, l4, l5, l6, l7 = Reals('l1 l2 l3 l4 l5 l6 l7') 
l = { 'l1' : l1, 'l2' : l2, 'l3' : l3, 'l4' : l4, 'l5' : l5, 'l6' : l6, 'l7' : l7 } 
p1, p2, p3, p4, p5 = Reals('p1 p2 p3 p4 p5') 
p = { 'p1' : p1, 'p2' : p2, 'p3' : p3, 'p4' : p4, 'p5' : p5 } 
sl1, sl2, sl3, sl4, sl5, sl6, sl7 = Ints('sl1 sl2 sl3 sl4 sl5 sl6 sl7') 
sl = { 'sl1' : sl1, 'sl2' : sl2, 'sl3' : sl3, 'sl4' : sl4, 'sl5' : sl5, 'sl6' : sl6, 'sl7' : sl7 } 
sp1, sp2, sp3, sp4, sp5 = Ints('sp1 sp2 sp3 sp4 sp5') 
sp = { 'sp1' : sp1, 'sp2' : sp2, 'sp3' : sp3, 'sp4' : sp4, 'sp5' : sp5 } 
a1, a2, a3, a4, a5 = Ints('a1 a2 a3 a4 a5') 
a = { 'a1' : a1, 'a2' : a2, 'a3' : a3, 'a4' : a4, 'a5' : a5 } 
na, ns = Ints('na ns') 
attack = Bool('attack') 
n = { 'na' : na, 'ns' : ns, 'attack' : attack} 
dict_decl = dict(th.items() + l.items() + p.items() + sl.items() + sp.items() + a.items() + n.items()) 

assertions = [] 
assertions.append(parse_smt2_string('(assert (and  (= l1 (* (- th2 th1) 17.0)) (= l2 (* (- th5 th1) 4.5)) (= l3 (* (- th3 th2) 5.05)) (= l4 (* (- th4 th2) 5.65)) (= l5 (* (- th5 th2) 5.75)) (= l6 (* (- th4 th3) 5.85)) (= l7 (* (- th5 th4) 23.75)) (= p1 (+ l1 l2)) (= p2 (+ l1 l3 l4 l5)) (= p3 (+ l3 l6)) (= p4 (+ l4 l6 l7)) (= p5 (+ l2 l5 l7))))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (and (or (= sl1 0) (= sl1 1)) (or (= sl2 0) (= sl2 1)) (or (= sl3 0) (= sl3 1)) (or (= sl4 0) (= sl4 1)) (or (= sl5 0) (= sl5 1)) (or (= sl6 0) (= sl6 1)) (or (= sl7 0) (= sl7 1)) (or (= sp1 0) (= sp1 1)) (or (= sp2 0) (= sp2 1)) (or (= sp3 0) (= sp3 1)) (or (= sp4 0) (= sp4 1)) (or (= sp5 0) (= sp5 1))  ))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (and (=> (not (= l1 0.0)) (= sl1 0)) (=> (not (= l2 0.0)) (= sl2 0)) (=> (not (= l3 0.0)) (= sl3 0)) (=> (not (= l4 0.0)) (= sl4 0)) (=> (not (= l5 0.0)) (= sl5 0)) (=> (not (= l6 0.0)) (= sl6 0)) (=> (not (= l7 0.0)) (= sl7 0))  (=> (not (= p1 0.0)) (= sp1 0)) (=> (not (= p2 0.0)) (= sp2 0)) (=> (not (= p3 0.0)) (= sp3 0)) (=> (not (= p4 0.0)) (= sp4 0)) (=> (not (= p5 0.0)) (= sp5 0))   ))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (and (or (= a1 0) (= a1 1))(or (= a2 0) (= a2 1))(or (= a3 0) (= a3 1))(or (= a4 0) (= a4 1))(or (= a5 0) (= a5 1))  ))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (and (= (not (= th1 0.0)) (= a1 1))(= (not (= th2 0.0)) (= a2 1))(= (not (= th3 0.0)) (= a3 1))(= (not (= th4 0.0)) (= a4 1))(= (not (= th5 0.0)) (= a5 1))  ))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (<= ns 4))', decls=dict_decl)) 
#assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl)) # commented as suggested 
assertions.append(parse_smt2_string('(assert (= th1 0.0))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (= na (+ a1 a2 a3 a4 a5)))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert (=> attack (> na 1)))', decls=dict_decl)) 
assertions.append(parse_smt2_string('(assert attack)', decls=dict_decl)) 

print assertions 

s.add(assertions) 

synthesized = [] 

iters = 0 
while s.check() == sat: 
    print "Iteration " + str(iters) 
    print s.model() 
    avoid = [] 
    # key step: add constraint to prevent any values assigned (if possible) to constants from being equal to their satisfying assignments (models) in this sat iteration 
    for sli in sl.values(): 
    avoid.append(sli != s.model()[sli]) 
    for spi in sp.values(): 
    avoid.append(spi != s.model()[spi]) 
    s.add(Or(avoid)) 
    # end key step 
    synthesized.append(avoid) 
    print avoid 
    iters = iters + 1 
    # unless you know how to guarantee termination (e.g., there is a constraint ensuring the slis and spis take values in finite sets) 
    if iters >= 1000: 
    break 

print "Done" 
print synthesized # all the constraints 

對於所有常量和數字的道歉，我只是使用了SMT-LIB腳本的最快翻譯，但最終變得相當麻煩，我會在任何地方使用迭代器。這產生在sli和spj常數以下限制：

[[sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0]]