решение бескванторной VC с использованием z3

Я читал эту исследовательскую работу: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.9467&rep=rep1&type=pdf

Таким образом, вкратце, они преобразуют квантифицированные рупорные предложения в рупорные предложения без кванторов путем создания экземпляров (через E-сопоставление), и результирующие условия проверки (VC) приведены на рис. 6 документа.

Насколько я понимаю, в документе предлагается передать результирующие виртуальные каналы, показанные на рис. 6, в любой решатель SMT, поскольку виртуальные каналы теперь не имеют кванторов и могут быть решены любым решателем SMT. (Пожалуйста, поправьте меня, если я ошибаюсь.)

Итак, продолжая понимать это, я попробовал кодировать VC Рис. 6 с помощью z3py.

Изменить: Моя цель - найти решение для VC на рис. 6. Что я должен добавить в качестве возвращаемого типа инварианта P, который должен выводиться z3? Есть ли лучший способ сделать это с помощью z3? Спасибо за уделенное время!

Вот код:

    from z3 import *
    Z = IntSort()
    B = BoolSort()

    k0, k1, k2, N1, N2 = Ints('k0, k1, k2, N1, N2')
    i0, i1, i2 = Ints('i0, i1, i2')

    P = Function('P', B, Z)

    a0 = Array('a0', Z, B)
    a1 = Array('a1', Z, B)
    a2 = Array('a2', Z, B)


    prove(And(Implies(i0 == 0, P( Select(a0,k0), i0) ), 
          Implies(And(P(Select(a1, k1),i1), i1<N1), P(Select(Store(a1, i1, 0)), i1+1) ),
          Implies(And(P(Select(a2,k2), i2), not(i2<N2)), Implies(0<=k2<=N2, a2[k2]) )))

z3 z3py quantifiers first-order-logic hoare-logic
person user8616916    schedule 20.10.2020    source источник
comment
Function('P', B, Z) - функция от B до Z; в объявлении отсутствует второй аргумент или тип возвращаемого значения.   -  person Christoph Wintersteiger    schedule 20.10.2020
comment
Правда! Я пропустил возвращаемый тип. Согласно исследовательской статье, на которую я ссылался в вопросе, это инвариант, который должен быть выведен. Я не совсем уверен, как это будет выведено решателем, как это упоминается в статье, и каков тип возвращаемого значения инварианта.   -  person user8616916    schedule 20.10.2020

Ответы (1)


arrow_upward
1
arrow_downward

У вас есть ряд проблем с кодированием в вашем коде z3Py. Вот его перекодировка, которая, по крайней мере, проходит через z3 без каких-либо ошибок:

from z3 import *

Z = IntSort()
B = BoolSort()

k0, k1, k2, N1, N2 = Ints("k0 k1 k2 N1 N2")
i0, i1, i2 = Ints("i0 i1 i2")

P = Function('P', B, Z, B)

a0 = Array('a0', Z, B)
a1 = Array('a1', Z, B)
a2 = Array('a2', Z, B)

s = Solver()
s.add(Implies(i0 == 0, P(Select(a0, k0), i0)))

s.add(Implies(And(P(Select(a1,k1),i1), i1<N1), P(Select(Store(a1, i1, False), k1), i1+1)))

s.add(Implies(And(P(Select(a2,k2),i2), Not(i2<N2)), Implies(And(0<=k2, k2<=N2), a2[k2])))

print(s.sexpr())
print(s.check())

Некоторые исправления я внес в ваш код:

  • Функция P является предикатом, поэтому ее окончательный тип - bool. Исправьте это, сказав P = Function('P', B, Z, B)

  • Обозначение A <= B <= C, хотя вы можете написать его на z3Py, не означает то, что вы думаете. Вам нужно разбить его на две части и использовать союз.

  • Лучше разделить ограничения на несколько строк, чтобы их было легче отлаживать.

  • Логическое отрицание Not, а не not

и т.д. Пока z3 выдает sat на этом; но я не совсем уверен, правильный ли это перевод из статьи. (В частности, обозначение a1[i1 ← 0][k1] или последовательность импликаций A -> B -> C должны быть правильно переведены. Кажется, вы полностью упускаете C часть этой последовательности импликаций. Я не изучал этот документ, поэтому я не уверен, что они должны означать.)

Итак, кодировка, которую я дал выше, хотя и проходит через z3, определенно не соответствует условиям в статье. Но, надеюсь, это поможет вам начать.

person alias    schedule 20.10.2020
comment
Спасибо за ответ. Мне было интересно, могу ли я отфильтровать VC из самого z3. Возможно ли использование каких-либо опций в z3? - person user8616916; 20.10.2020
comment
Кроме того, не могли бы вы рассказать, почему вы пришли к выводу, что P является предикатом и возвращает bool? - person user8616916; 20.10.2020
comment
Инвариант по определению является предикатом, т. Е. Принимает некоторые аргументы и производит логическое значение. (Вы также можете увидеть это по тому, как записываются VC, результаты P используются в логических контекстах.) Следовательно, результат bool. - person alias; 20.10.2020
comment
Не уверен, что вы имеете в виду, говоря «Если бы я мог отфильтровать VC из самого z3». Эта проблема, похоже, пытается синтезировать инвариант P, поэтому вы можете просто распечатать модель, которая должна иметь предложения, определяющие, как P должен себя вести. Вы можете увидеть присвоение ему, выполнив print(s.model()). - person alias; 20.10.2020