z3 - 在 z3 中将值分配给数组的三种方法
问题描述
据我所知,在 z3 中有三种方法可以将值分配给数组。
- 用于
assert
为某些单元格分配值:
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))
z3在添加unsat
约束时返回(assert (= a1 a2))
。
- 用于
as const
首先初始化数组,然后将值分配给特定单元格:
(declare-const a3 (Array Int Int))
(assert
(=
(store ((as const (Array Int Int)) 64) 0 3)
a3
)
)
(declare-const a4 (Array Int Int))
(assert
(=
(store ((as const (Array Int Int)) 64) 0 4)
a4
)
)
添加(assert (= a3 a4))
,我们unsat
再次获得。
- 通过函数定义数组:
(define-const a5 (Array Int Int)
(lambda ((i Int))
(ite (= i 0) 5 64)))
(define-const a6 (Array Int Int)
(lambda ((i Int))
(ite (= i 0) 6 64)))
但是如果我们添加(assert (= a5 a6))
, z3 会返回sat
。为什么?
顺便说一句,有没有(更好的)方法可以将值分配给 z3 中的数组?
解决方案
这是一个错误。看看这个问题。
推荐阅读
- c# - 如何从 C# 中支持 ONVIF 的 VMS 和记录器获取 RTSP url
- python - Python:如何处理子类中的类型提示?
- c++ - 无法在#include 的 Visual Studio 中链接“GLFW”
- x86 - 如果汇编代码跳转到包含错误指令的地址会发生什么?
- embedded - esp32 中的以下错误是什么意思?
- ssas - SSAS:使用当前用户对 SQL 数据库进行 DirectQuery
- node.js - 将 Node.js API 连接到 Microsoft Azure / Azure CLI 上的虚拟机
- google-cloud-platform - 为什么 smtp 的 wordpress 给我不同的错误?
- api - Instagram 使用哪个 API 调用来获取主页帖子提要?
- ruby-on-rails - 使用连接的太阳黑子搜索关联