陣列和數據類型在Z3py

我實際使用Z3py調度解決問題，我想代表2個處理器系統中的不同執行時間4個過程必須做到的。陣列和數據類型在Z3py

我的實際數據是：方法1：在0到達和執行4種方法2的時間：到達在1和執行3個工序3的時間：到達在第3和執行5種方法4的時間：到達在1和2

實際上，我試圖同時在相同的時間子分解每個代表每個過程的執行時間，所以我的數據類型是這樣的：

Pn = Datatype('Pn') 
Pn.declare('1') 
Pn.declare('2') 
Pn.declare('3') 
Pn.declare('4') 
Pt = Datatype('Pt') 
Pt.declare('1') 
Pt.declare('2') 
Pt.declare('3') 
Pt.declare('4') 
Pt.declare('5') 
Process = Datatype('Process') 
Process.declare('cons' , ('name',Pn) , ('time', Pt)) 
Process.declare('idle')

其中PN和PT的進程名和過程的一部分（1過程中4個部分，...）

但現在我不知道我可以代表我的處理器加3分的規則，我需要：唯一性（每個子流程必須做且只有1個被時間只有1個處理器）檢查到來（它到達之前的過程的第一部分不能被處理）和順序（一個過程的每一部分必須在先例之後處理）所以我想使用數組來表示我的2個處理器的用這種聲明：

P = Array('P', IntSort() , Process)

但是，當我試圖執行它，我得到了一個錯誤信息說：

Traceback (most recent call last): 
    File "C:\Users\Alexis\Desktop\test.py", line 16, in <module> 
    P = Array('P', IntSort() , Process) 
    File "src/api/python\z3.py", line 3887, in Array 
    File "src/api/python\z3.py", line 3873, in ArraySort 
    File "src/api/python\z3.py", line 56, in _z3_assert 
Z3Exception: 'Z3 sort expected'

，知道我不知道該怎麼處理呢？我必須建立一個新的數據類型和計算方式來增加我的規則？或者是有辦法的數據類型添加到陣列這將讓我創建的規則是這樣的：

unicity = ForAll([x,y] , (Implies(x!=y,P[x]!=P[y])))

在此先感謝

來源

2013-05-16 a.fossart

有使用數據類型從Python API的教程。到教程的鏈接是： http://rise4fun.com/Z3Py/tutorialcontent/advanced#h22 它顯示瞭如何創建列表數據類型，並使用「創建（）」方法來實例化從聲明數據類型時所使用的對象中的對象排序。對於你的例子，只需要在你想使用聲明類型的地方添加對「create（）」的調用即可。請參閱：http://rise4fun.com/Z3Py/rQ7t

關於您正在研究的案例研究的其餘部分：您肯定可以使用量詞和數組來表示constrsaints。你也可以考慮更有效的編碼：

而不是使用數組，使用函數聲明。所以P將被聲明爲一元函數： P =函數（'P'，IntSort（），Process.create（））。
對小型有限域問題使用量詞可能比益處更多的開銷。將約束直接記爲有限連接節省了可能重複實例化量詞的開銷。也就是說，一些量化的公理也可以被優化。 Z3自動編譯形式的公理：的ForAll（！[X，Y]，蘊涵（X = Y，P（X）= P（Y）））轉換成形式的FORALL一個公理（[X]，PINV（ P（x））== x），其中「Pinv」是一個新鮮的函數。新公理仍然強制P是內射的，但僅需要線性數量的實例，對於某個項't'，P（t）的出現次數是線性的。

玩得開心！

來源

2013-05-16 16:26:51

謝謝，它幫助我繼續（我沒有看到教程中的create（）方法...）但是現在我被卡住了，因爲當我嘗試獲得具有唯一性的模型時（我將其調整爲2數組）我只獲得所有索引我們得到空閒的數組...（0->空閒，否則 - >空閒），我不知道如何改變...所以我還有很長的路要走^ ^ –

陣列和數據類型在Z3py

回答

相關問題