在Z3及Z3 Python中实现统计指定b值对应数对数量的函数

我拥有一组有限的(int a, int b)类型数对，数对的具体值已明确存在于知识库中，可通过有限域上完全定义的函数(int a, int b) -> bool exists来表示。希望实现一个签名为(int b) -> int count的函数f，用于统计数对中第二个成员为指定b值的数对数量。例如给定数对：
(0, 0)
(0, 1)
(1, 1)
(1, 2)
(2, 1)
则f(0) = 1、f(1) = 3、f(2) = 1。以下是具体实现方法：

Z3 语言实现 #

1. 定义数对存在性函数 #

先声明判断数对是否存在的函数，再用断言枚举所有有效数对，同时限定不存在其他未枚举的数对：

; 定义存在性函数：is_pair_exists(a, b) 返回该数对是否存在
(declare-fun is_pair_exists (Int Int) Bool)

; 枚举所有有效数对
(assert (is_pair_exists 0 0))
(assert (is_pair_exists 0 1))
(assert (is_pair_exists 1 1))
(assert (is_pair_exists 1 2))
(assert (is_pair_exists 2 1))

; 断言仅存在上述枚举的数对
(assert (forall ((a Int) (b Int))
  (=> (is_pair_exists a b)
      (or (and (= a 0) (= b 0))
          (and (= a 0) (= b 1))
          (and (= a 1) (= b 1))
          (and (= a 1) (= b 2))
          (and (= a 2) (= b 1))))))

2. 定义统计函数f(b) #

遍历所有可能的a值，累加满足is_pair_exists(a, b)的次数：

; 定义统计函数f(b)
(declare-fun f (Int) Int)

(assert (forall ((b Int))
  (= (f b)
     (+ (ite (is_pair_exists 0 b) 1 0)
        (ite (is_pair_exists 1 b) 1 0)
        (ite (is_pair_exists 2 b) 1 0)))))

3. 验证函数正确性 #

通过反证法验证指定b值的统计结果：

; 验证f(0)=1
(assert (not (= (f 0) 1)))
(check-sat) ; 返回unsat，说明f(0)=1成立

(reset-assertions)
; 验证f(1)=3
(assert (not (= (f 1) 3)))
(check-sat) ; 返回unsat，说明f(1)=3成立

(reset-assertions)
; 验证f(2)=1
(assert (not (= (f 2) 1)))
(check-sat) ; 返回unsat，说明f(2)=1成立

Z3 Python 实现 #

1. 初始化环境并定义存在性函数 #

from z3 import *

# 创建求解器实例
s = Solver()

# 定义存在性函数：is_pair_exists(a, b)
a = Int('a')
b = Int('b')
is_pair_exists = Function('is_pair_exists', IntSort(), IntSort(), BoolSort())

# 枚举所有有效数对
pairs = [(0,0), (0,1), (1,1), (1,2), (2,1)]
for p in pairs:
    s.add(is_pair_exists(p[0], p[1]) == True)

# 断言仅存在上述枚举的数对
all_valid_pairs = Or([And(a == p[0], b == p[1]) for p in pairs])
s.add(ForAll([a, b], Implies(is_pair_exists(a, b), all_valid_pairs)))

2. 定义统计函数f(b) #

提取所有可能的a值，通过累加存在性判断结果实现统计：

# 定义统计函数f(b)
f = Function('f', IntSort(), IntSort())

# 获取所有出现过的a值（去重）
possible_a_values = list({p[0] for p in pairs})

# 构建f(b)的定义
f_def = ForAll([b], f(b) == Sum([If(is_pair_exists(a_val, b), 1, 0) for a_val in possible_a_values]))
s.add(f_def)

3. 验证并查询结果 #

# 验证f(0)=1
s.push()
s.add(f(0) != 1)
print("f(0)=1 是否成立:", s.check() == unsat)  # 输出True

# 验证f(1)=3
s.pop()
s.push()
s.add(f(1) != 3)
print("f(1)=3 是否成立:", s.check() == unsat)  # 输出True

# 验证f(2)=1
s.pop()
s.push()
s.add(f(2) != 1)
print("f(2)=1 是否成立:", s.check() == unsat)  # 输出True

# 直接查询f(1)的具体值
s.pop()
count = Int('count')
s.add(f(1) == count)
s.check()
print("f(1)的统计结果:", s.model()[count])  # 输出3

内容的提问来源于stack exchange，提问作者nickt