时间戳

首页 > 解决方案 > Z3型号的桌子

z3 - Z3型号的桌子

问题描述

我试图让我的头脑围绕 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 ""))) 
)

我不认为我的输入模型是完美的，然后我不知道如何对约束建模(int)table.Rows[0]["name"]，即命名单元格包含一个int值。

所以我的问题是如何对此建模以及如何处理从这些用代码编写的更复杂的代码约束到 Z3 约束（即类型映射）的转换。并回答基本问题，例如

如果你能推荐任何论文、帖子或项目，那就太棒了:)

谢谢，

卡雷尔

标签： z3solver

解决方案

在项目的帮助下，我能够想出一个解决方案

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()))

求解器正在解决的问题是在名称为 的列中找到一个值大于 5DataTable的单个。DataRowValue

结果模型是

{
   "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也会有所不同（但可能会有一个技巧来概括它）。

推荐阅读