Модель Z3 для стола - PullRequest
Новая
       11

Модель Z3 для стола

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

Я пытаюсь разобраться с Z3.Хотя я понимаю основные принципы и примеры решения основных проблем.

Я создаю символический инструмент динамического выполнения и использую Z3 в качестве решателя.В тестируемой программе-примере есть условие table.Rows.Count == 1, которое я успешно перевел вручную в модель Z3 с решением: 

(declare-datatypes () ((Type (Char) (Decimal) (String) (Bool) (Int))))
(declare-datatypes (T S) ((Column (mkcol (first T) (second S)))))
(declare-datatypes () ((Row (Array (String (Column Type String))))))
(declare-datatypes () ((Table (Array (Int (Row))))))
(declare-const a Int)
(declare-const row Row)
(declare-const column (Column String String))
(declare-const c Row)
(declare-const x Int)
(declare-const table Table)
(declare-const table.Rows (List Row))
(declare-const list2 (List Row))
(assert (not (= table.Rows nil))) ; an actual instance (not null)
(assert (= (head table.Rows) row)) ; firt row

(check-sat)
(get-model)

И решение 

sat 
(model 
  (define-fun table.Rows () (List Row) 
    (insert (Array (mkcol String "")) nil)) 
  (define-fun row () Row 
    (Array (mkcol String ""))) 
)

Iне думаю, что моя входная модель идеальна, и тогда я не знаю, как смоделировать ограничение (int)table.Rows[0]["name"], то есть именованная ячейка содержит значение int.

Таким образом, мой вопрос заключается в том, как смоделировать это и как приблизить такие переводы из этих более сложных ограничений кода, записанных в коде, к ограничениям Z3 (т. Е. Сопоставление типов).И отвечая на основные вопросы, такие как

  • Должно ли свойство Rows быть смоделировано как (declare-const table.Rows (List Row)) для переменной table?
  • Или свойство Rows должно быть смоделировано с использованием пользовательскогоsort?
  • Должен ли также быть объявлен Count или он может быть "пропущен" несколькими head и tail утверждениями?

Если вы можете порекомендовать любую бумагуили пост или проект, это было бы здорово:)

Спасибо,

Карел

1 Ответ

0 голосов
/ 20 марта 2019

С помощью проекта я смог найти решение 

from model import *
from z3 import *

import yaml
import pprint
import inspect
import linecache
import timeit
import itertools

classes_yaml = """
-
  name: DataColumn
  attribute: [{name: Value, type: Integer}]
- 
  name: DataTable
  reference: [
    {name: Rows, type: DataRowCollection}
  ]
-
  name: DataRow
  reference: [
    {name: Columns, type: DataColumn, multiple: true}
  ]
-
  name: DataRowCollection
  reference: [
    {name: Row, type: DataRow, multiple: true}
  ]
"""

classes = yaml.load(classes_yaml)
DataColumn, DataTable, DataRow, DataRowCollection = load_all_classes(classes)

dc = DefineObject('col1', DataColumn)

drc = DefineObject('drc', DataRowCollection)
dt = DefineObject('dt', DataTable).force_value('Rows', drc)
dr1 = DefineObject('dr1', DataRow)
dr2 = DefineObject('dr2', DataRow)
dr3 = DefineObject('dr3', DataRow)

generate_meta_constraints()
generate_config_constraints()

solver = Optimize()
solver = Solver()
solver.add(*get_all_meta_facts())
solver.add(*get_all_config_facts())

solver.add(dt.isinstance(DataTable))
solver.add(dt['Rows'] == drc)
solver.add(drc['Row'].count() == 1)
solver.add(dc['Value'] > 5);
solver.add(dr1['Columns'].count() == 1)

print(solver)
print(solver.check())
print(cast_all_objects(solver.model()))

Проблема, которую решает решатель, - найти DataTable с одним DataRow, который имеет значениебольше 5 в столбце с именем Value.

Результирующая модель: 

{
   "dt":{
      "name": "dt", "type": "DataTable", "alive": True,
      "Rows": "drc"
   },
   "dr1":{
      "name": "dr1", "type": "DataRow", "alive": True,
      "Columns":[
         "col1"
      ]
   },
   "col1": {
      "name": "col1", "type":"DataColumn", "alive": True,
      "Value":6
   },
   "dr3": {
      "name": "dr3", "type": "DataRow", "alive": True, 
      "Columns": []
   },
   "dr2": {
      "name": "dr2", "type": "DataRow", "alive": True, 
      "Columns": []
   },
   "drc": {
      "name": "drc", "type": "DataRowCollection", "alive": True,
      "Row": [
         "dr2"
      ]
   }
}

Это не универсальное решение, и класс предположений необходимо пересоздавать каждый раз, когда ограничение кода отличается, то есть предположения и инициализации будут разными дляЗадача «2 строки с двумя различными таблицами значений».Кроме того, определения классов для DataRow также будут отличаться (но может быть хитрость, как немного обобщить это).

...