不能创建在Z3的GADT抽象的加法运算

Question

问题

我在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"

这不通过的结果是“不饱和度”。

Answer 1

该系统是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)))

（注意括号内。）