无法为Z3中的GADT创建抽象加法运算 [英] Cannot create abstract addition operation for GADT in Z3

问题描述

问题

我在Z3中使用以下Datatype定义。我的目标是从本质上"重载"加法操作符。我使用ForAll尝试了以下技巧，但Z3似乎认为它无效。

问题

这是怎么回事？为什么这不起作用？

代码

import pytest
from z3 import Datatype, IntSort, Solver, Ints

def test_stackoverflow():
    FooBar = Datatype('FooBar')
    FooBar.declare('foo', ('unfoo', IntSort()))
    FooBar.declare('bar', ('unbar', FooBar))
    FooBar.declare('plus', ('left', FooBar), ('right', FooBar))
    FooBar = FooBar.create()

    foo = FooBar.foo
    unfoo = FooBar.unfoo
    bar = FooBar.bar
    unbar = FooBar.unbar
    plus = FooBar.plus

    solver = Solver()
    x, y = Ints('x y')
    solver.add(ForAll[x, y], plus(foo(x), foo(y)) == foo(x + y))
    assert str(solver) == "sat"

这不会通过，因为结果是"unsat"。

推荐答案

系统是unsat，因为您实际上是说：

  forall x, y => foo (x+y) = plus (foo x, foo y)

这显然是错误的，因为foo和plus是您的数据类型的两个不同的构造函数，因此无论您传递什么，它们永远不会相等。请注意，数据类型是自由生成的：每个构造函数定义不同的值。

我怀疑您想说的是plus生成了一些类似"数字"的东西，使得foo (x+y) = plus (foo x, foo y)成立。如果是这种情况，则不要使plus成为构造函数。相反，使其成为接受FooBar并产生Int的未解释函数；并适当地断言上面的内容。在SMTLib表示法中，它如下所示：

(declare-datatypes ((FooBar 0)) (((foo (unfoo Int)) (bar (unbar FooBar)))))
(declare-fun plus (FooBar FooBar) Int)
(assert (forall ((x Int) (y Int)) (= (plus (foo x) (foo y)) (unfoo (foo (+ x y))))))
(check-sat)
(get-model)

唉，虽然这是非常好的编码，但Z3只是在它上面吃午饭：

$ z3 -v:3 a.smt2
... many lines of verbose output showing quantifier instantiation ...

在这种情况下，电子匹配引擎很难找到模型。当然，如果您有额外的约束，您可能会得到一个有用的结果，或者您可以尝试使用模式来帮助Z3。但是，根据我的经验，所有这些都不会真正起作用，因为量词只会让问题对于当前的SMT解决技术来说太难了。

Nb.你的程序中有一个小的打字错误，倒数第二行应该是：

    solver.add(ForAll([x, y], plus(foo(x), foo(y)) == foo(x + y)))

(请注意括号)

这篇关于无法为Z3中的GADT创建抽象加法运算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！