阵列和数据类型在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

回答

相关问题