Создание переменных, пар и наборов в Z3Py - PullRequest
Новая
       13

Создание переменных, пар и наборов в Z3Py

0 голосов
/ 12 января 2019

это вопрос из трех частей об использовании Python API для Z3 (Z3Py).

  1. Я думал, что знаю разницу между константой и переменной, но, очевидно, нет. Я думал, что смогу объявить сортировку и создать переменную такого рода следующим образом: 

    Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Node('n1') # c.f. x = Int('x')

    Но python выдает исключение, говорящее, что вы не можете "вызвать Node". Единственное, что, кажется, работает - это объявить n1 константой 

    Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)

    но я озадачен этим, поскольку я думаю, что a1, a2, a3 - это константы. Возможно, n1 является символической константой, но как бы я объявил фактическую переменную?

  2. Как создать постоянный набор? Я попытался начать с пустого набора и добавить к нему, но это не работает 

    Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
nodes = EmptySet(Node)
SetAdd(nodes, a1) #<-- want to create a set {a1}
solve([IsMember(n1,nodes)])

    Но это не работает, Z3 не возвращает решения. С другой стороны, заменив 3-ю строку на 

    nodes = Const('nodes',SetSort(Node))

    теперь слишком разрешительный, что позволяет Z3 интерпретировать узлы как любой набор узлов, необходимый для удовлетворения формулы. Как мне создать только набор {a1}?

  3. Есть ли простой способ создания пар, кроме необходимости проходить через объявление типа данных, которое кажется немного громоздким? например, 

    Edge = Datatype('Edge')
Edge.declare('pr', ('fst', Node), ('snd',Node))
Edge.create()
edge1 = Edge.pr(a1,a2)

1 Ответ

0 голосов
/ 12 января 2019

Объявление Enums

Const - это правильный способ заявить, как вы узнали. Это немного вводит в заблуждение, но именно так создаются все символические переменные. Например, вы можете сказать: 

 a = Const('a', IntSort())

и это было бы эквивалентно высказыванию 

a = Int('a')

Просто последний выглядит лучше, но на самом деле это просто функция, определенная людьми из z3, которая делает то, что делает первый. Если вам нравится этот синтаксис, вы можете сделать следующее: 

NodeSort, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])

def Node(nm):
    return Const(nm, NodeSort)

Теперь вы можете сказать: 

 n1 = Node ('n1')

это то, что вы намеревались, я полагаю.

Вставка в наборы

Вы на правильном пути; но имейте в виду, что функция SetAdd не изменяет установленный аргумент. Это просто создает новый. Итак, просто дайте ему имя и используйте его так: 

emptyNodes = EmptySet(Node)
myNodes = SetAdd(emptyNodes, a1)
solve([IsMember(n1,myNodes)])

Или вы можете просто заменить: 

mySet = SetAdd(SetAdd(EmptySet(Node), a1), a2)

, который создаст набор {a1, a2}.

Как правило, API старается быть всегда функциональным, то есть без разрушительных обновлений существующих переменных, но вместо этого вы создаете новые значения из старых.

Работа с парами

Это единственный способ. Но ничто не мешает вам определить свои собственные функции для упрощения этой задачи, как мы это делали с функцией Node в первой части. В конце концов, z3py - это, по сути, библиотека Python, и люди из z3 проделали большую работу, чтобы сделать его лучше, но у вас также есть все возможности Python, чтобы упростить вашу жизнь. Фактически, многие другие интерфейсы к z3 из других языков (Scala, Haskell, O'Caml и т. Д.) Как раз и делают это, чтобы значительно упростить работу с API, используя функции соответствующих им основных языков.

...