Z3, создайте структуру данных / класс, используя тип данных - PullRequest
Новая
       10

Z3, создайте структуру данных / класс, используя тип данных

0 голосов
/ 28 января 2020

Возможно, создайте структуру данных, которая будет содержать ту же информацию, что и следующий класс Python. 

class Variable:
    def __init__(self):
        self.name = "v1"  #str
        self.size = 10    #int
        self.initialized = True    #bool

Имеют три разных поля разных типов.

Если бы поля были одного типа, например "str", я мог бы просто использовать z3.Array('a', StringSort(), StringSort()). Вид использования это как отображение.

Что мне делать в случае полей другого типа, как показано в коде python?

Я изучил Datatype и прочитал пример из руководства по z3py о том, как они создали List. Однако я не мог полностью понять, что именно происходит. Я думаю, что термины, используемые в документации по z3, немного отличаются от тех, которые обычно используются в языках программирования ОО, таких как Java, Python? У меня действительно тяжелые времена, чтобы набрать asp некоторые термины и примеры ...

*** Более сложная часть, как вы храните переменные такого типа в массиве z3? Например, я хочу найти индекс объекта Variable в массиве, который имеет размер> 10, используя решение с ограничением z3.

Ответы [ 2 ]

1 голос
/ 28 января 2020

Тип данных - это структура, которая может иметь несколько конструкторов: например, дерево (лист или ветвь), или список (ноль, или минусы), или любая другая, как правило, древовидная структура.

Из вашего описания видно, что на самом деле вам нужен не тип данных, а прямое значение записи. (Терминология сбивает с толку. То, что ОО люди называют типом данных, в большинстве случаев является просто структурой / записью, а то, что функциональное программирование или SMT-люди называют типом данных, является чем-то гораздо более богатым, поскольку многие конструкторы рекурсивны, как список. Это неудачно, но то, что вы изучаете однажды и легко запоминается.)

Очевидно, что не один размер подходит всем; и описание вашего вопроса довольно расплывчато. Но я предполагаю, что вы хотите представить какое-то понятие Variable, которое имеет ассоциированное фиксированное имя, размер и какое-то инициализированное поле. Вам нужен просто класс Python, где вы можете полагаться на гибкую типизацию, чтобы использовать ее как конкретные переменные или как символические c переменные, которыми z3 может манипулировать. Исходя из этого, я был бы склонен закодировать вашу проблему следующим образом: 

from z3 import *

class Variable:
    def __init__(self, nm):
        self.name        = nm
        self.size        = Int(nm + '_size')
        self.initialized = Bool(nm + '_initialized')

    def __str__(self):
        return "<Name: %s, Size: %s, Initialized: %s>" % (self.name, self.size, self.initialized)

# Helper function to grab a variable from a z3 model
def getVar(m, v):
    var             = Variable(v.name)
    var.size        = m[v.size]
    var.initialized = m[v.initialized]
    return var

# Declare a few vars
myVar1 = Variable('myVar1')
myVar2 = Variable('myVar2')

# Add some constraints
s = Solver()

s.add(myVar1.size == 12)
s.add(myVar2.initialized == True);
s.add(myVar1.size > myVar2.size)
s.add(myVar1.initialized == Not(myVar2.initialized))

# Get a satisfying model
if s.check() == sat:
    m = s.model()
    print getVar(m, myVar1)
    print getVar(m, myVar2)

Я использую класс Variable для представления как обычного значения, как в Python, так и того, что может хранить размер символов c (через Int(nm + '_size')) и инициализированную информацию символов c (через Bool(nm + '_initialized')). Синтаксис может показаться немного запутанным, но если вы go через программу, я уверен, вы увидите лог c. Функция getVar является помощником для получения значения одной из этих переменных после вызова check для доступа к значениям модели.

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

$ python a.py
<Name: myVar1, Size: 12, Initialized: False>
<Name: myVar2, Size: 11, Initialized: True>

, которая дает мне хорошую модель, которая удовлетворяет всем указанным мною ограничениям.

Надеюсь, это поможет!

0 голосов
/ 28 января 2020

Я нахожусь в такой же ситуации, как и вы, но я постараюсь ответить на ваш вопрос как можно лучше.

I could just use z3.Array('a', StringSort(), StringSort()). What do I do in this kind of situation?

Да, вы должны реализовать его, но помните что массив в Z3 (и в SMT) имеет неограниченный размер, если вы хотите фиксированный массив, вы можете это сделать: 

vec = IntVector('vec', 10)

Уважайте ваш другой вопрос, я был в аналогичной ситуации с вами, потому что у меня был много трудностей с пониманием правильно Z3. Я адаптирую Список, как будто вы работаете в Haskell (для большей ясности) 

def funList(sort):
    List = Datatype('List')
    #Constructor insert: (Int, List) -> List
    List.declare('insert', ('head', sort), ('tail', List)) 
    List.declare('nil') #declaración de nil, así permito la opción de tener una lista vacía
    return List.create() #creo la lista
...