關於Z3中未解釋函數的表示

我有一個簡單的問題。我寫了一個簡單的程序（使用Z3 NET API），並得到如下輸出。關於Z3中未解釋函數的表示

計劃（部分）：

 Sort[] domain = new Sort[3]; 
     domain[0] = intT; 
     domain[1] = intT;   
     domain[2] = intT; 
     FPolicy = z3.MkFuncDecl("FPolicy", domain, boolT);  

     Term[] args = new Term[3]; 
     args[0] = z3.MkNumeral(0, intT); 
     args[1] = z3.MkNumeral(1, intT); 
     args[2] = z3.MkNumeral(30, intT); 
     z3.AssertCnstr(z3.MkApp(FPolicy, args)); 

     args[1] = z3.MkNumeral(2, intT); 
     args[2] = z3.MkNumeral(20, intT); 
     z3.AssertCnstr(z3.MkApp(FPolicy, args));

輸出：

FPolicy -> { 
    0 1 30 -> true 
    0 2 20 -> true  
    else -> true 
}

我想知道我可以做的「其他 - >真」爲假（即「其他 - >假」）。

來源

2012-01-04 Ashiq

對於量詞免費的問題，Z3（3.2）看到更好的解決方案將會爲else選擇更經常在range發生的值。這裏的range是指Z3分配給特定有限輸入值集合的有限的一組值。在我們的示例中，只有true發生在range中。因此，true被選爲else的值。

對於無量詞自由（無陣列）問題，如果不使用選項:model-compact true，那麼else的值無關緊要。也就是說，如果公式F可以滿足，Z3將產生一個型號M。然後，如果我們更改M中的任何else的值，則生成的模型M’仍然是F的模型。因此，你可以忽略else，或者假設它是你想要的，如果輸入公式F是免費量化的，F不使用數組理論，並且不使用:model-compact true。此屬性基於Z3中當前實施的算法，並且這可能在未來發生變化。相比之下，由mhs提供的解決方案不受Z3實施方式變化的影響。在他的編碼中，任何SMT求解器（成功生成一個模型）都必須使用false作爲函數的值，在量詞前面未指定的每個點中。

另一種選擇是使用default運算符，並使用數組對您的問題進行編碼。當使用default運算符時，我們應該將數組視爲成對:(實際數組，默認值）。此默認值用於在模型構建過程中提供else值。 Z3還有幾個內建公理可以將缺省值傳播到：store和map運算符。這是你的問題使用這種方法編碼：

(set-option :produce-models true) 
(declare-const FPolicy (Array Int Int Int Bool)) 

(assert (select FPolicy 0 1 30)) 
(assert (select FPolicy 0 2 20)) 
(assert (not (default FPolicy))) 

(check-sat) 
(get-model)

來源

2012-01-05 18:23:44

這是我希望的一種更好的解決方案。但是，使用陣列理論是否存在任何（可能的）缺點？ – 2012-01-06 07:35:49

主要缺點是性能。即使我們只使用'select'和'default'，也會有開銷。也就是說，如果我們不*使用陣列理論的'store'，'map'和'const'運算符。例如，所有函數應用程序都會有一個額外的參數。用於檢測一致條件的散列表將會變得更大。 – 2012-01-06 18:12:15

以下情況如何（RiSE4fun link）？

(set-option :MBQI true) 

(declare-fun FPolicy (Int Int Int) Bool) 

(assert (forall ((x1 Int) (x2 Int) (x3 Int)) (! 
    (implies 
    (not 
     (or 
     (and (= x1 0) (= x2 1) (= x3 30)) 
     (and (= x1 0) (= x2 2) (= x3 20)))) 
     (= (FPolicy x1 x2 x3) false)) 
    :pattern (FPolicy x1 x2 x3)))) 

(assert (FPolicy 0 1 30)) 
(assert (FPolicy 0 2 20)) 

(check-sat) 
(get-model)

我可以看到的好處是，你可以改變它使得FPolicy（0 1 30）==虛假不接觸FORALL約束。明顯的缺點是你基本上必須提及所有參數元組兩次，而且創建的模型相當複雜。

我很期待:-)

來源

2012-01-05 08:54:36

關於Z3中未解釋函數的表示

回答

相關問題