具有数组数据类型的z3建模图

如何解决具有数组数据类型的z3建模图

我试图在z3中为有向图建模，但是我陷入了困境。我在这里向图添加了一个公理，因为边的存在意味着它连接的节点的存在。但是，仅此一项就导致不满意

GraphSort = Datatype('GraphSort')
GraphSort.declare('Graph',('V',ArraySort(IntSort(),BoolSort())),('E',BoolSort()))),)
GraphSort = GraphSort.create()
V = GraphSort.V
E = GraphSort.E

G = Const('G',GraphSort)
n,m = Consts('n m',IntSort())
Graph_axioms = [
    ForAll([G,n,m],Implies(E(G)[n][m],And(V(G)[n],V(G)[m]))),]

s = Solver()
s.add(Graph_axioms)

我正在尝试为图建模，以使V(G)[n]暗示存在节点n，而E(G)[n][m]暗示存在从n到{{1}的边}。有人对这里出什么问题有任何提示吗？甚至更好的是，在z3中建模图表的任何一般技巧？

编辑：

有了alias的解释，我想出了以下稍微有些棘手的解决方案：

m

解决方法

您的模型为unsat，因为数据类型是自由生成的。这是一个常见的误解：创建数据类型并声明一个公理时，您不将z3限制为仅考虑那些满足该公理的模型。相反，您要说的是检查此数据类型的所有实例是否符合公理。这显然是不正确的，因此是unsat。这类似于说：

a = Int("a")
s.add(ForAll([a],a > 0))

由于同样的原因，它也是unsat；但希望更容易理解原因。另请参阅以下答案以解释“自由生成”的含义：https://stackoverflow.com/a/60998125/936310

要为诸如此类的图建模，您应仅在图节点的单个实例上声明这些公理，而不应对广义/量化公理进行陈述。与其断言这个公理，不如将重点放在您要建模的其他方面。由于您并未真正提供要解决的问题的更多详细信息，因此很难进一步提出意见。