Невозможно создать абстрактную операцию сложения для GADT в Z3 - PullRequest
Новая
       7

Невозможно создать абстрактную операцию сложения для GADT в Z3

0 голосов
/ 08 февраля 2019

Проблема

Я работаю со следующими Datatype определениями в Z3.Моя цель состоит в том, чтобы существенно «перегрузить» оператор сложения.Я попробовал следующий трюк, используя 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".

1 Ответ

0 голосов
/ 09 февраля 2019

Система 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)))

(обратите внимание на круглые скобки.)

...