z3py 为有效的 SMT2 文件引发解析器错误

Question

 1  (set-logic UFLIA)
 2  (set-info :source | Simple list theorem |)
 3  (set-info :smt-lib-version 2.0)
 4  (set-info :category "crafted")
 5  (set-info :status unsat)
 6  (declare-sort List 0)
 7  (declare-sort Elem 0)
 8  (declare-fun cons (Elem List) List)
 9  (declare-fun nil () List)
10  (declare-fun car (List) Elem)
11  (declare-fun cdr (List) List)
12  (declare-fun len (List) Int)
13  (assert (forall ((?x Elem) (?y List)) (= (car (cons ?x ?y)) ?x)))
14  (assert (forall ((?x Elem) (?y List)) (= (cdr (cons ?x ?y)) ?y)))
15  (assert (= (len nil) 0))
16  (assert (forall ((?x Elem) (?y List)) (= (len (cons ?x ?y)) (+ (len ?y) 1))))
17  (declare-fun append (List List) List)
18  (assert (forall ((?y List)) (= (append nil ?y) ?y)))
19  (assert (forall ((?x Elem) (?y1 List) (?y2 List)) (= (append (cons ?x ?y1) ?y2) (cons ?x (append ?y1 ?y2)))))
20  (assert (not (forall ((?x Elem) (?y List)) (= (append (cons ?x nil) ?y) (cons ?x ?y)))))
21  (check-sat)
22  (exit)

对于上述公式，f = z3.parse_smt2_file("UFLIA/misc/list3.smt2") 会导致以下错误。

(error "line 6 column 14: invalid sort declaration, sort already declared/defined")
(error "line 8 column 24: sort constructor expects parameters")
(error "line 9 column 20: sort constructor expects parameters")
(error "line 10 column 18: sort constructor expects parameters")
(error "line 11 column 18: sort constructor expects parameters")
(error "line 12 column 18: sort constructor expects parameters")
(error "line 13 column 31: sort constructor expects parameters")
(error "line 14 column 31: sort constructor expects parameters")
(error "line 15 column 16: unknown constant nil")
(error "line 16 column 31: sort constructor expects parameters")
(error "line 17 column 21: sort constructor expects parameters")
(error "line 18 column 21: sort constructor expects parameters")
(error "line 19 column 32: sort constructor expects parameters")
(error "line 20 column 36: sort constructor expects parameters")

但是使用 z3-4.3.2.bb56885147e4-x64-osx-10.9.2 CLI 处理相同的文件会提供 unsat 结果。

在 Python 中使用 traceback，我发现以下是异常 TypeError: unorderable types: int() < Z3Exception() 的根本原因，根据异常堆栈，似乎错误源于本机 Z3 代码。

知道为什么会发生这种情况以及如何解决这个问题吗？

Answer 1

您必须将“列表”重命名为其他名称。从 API 中，Z3 预加载了“列表”的内置定义。它会忽略逻辑指令，否则会缩小预加载的排序范围。

Answer 2

基于@nikolaj 评论，我使用以下函数通过重命名与使用 Z3 API 时由 Z3 预加载的定义冲突的标识符来转换 SMT2 文件。 [除List外，该函数重命名SMT-LIB公式中常用的标识符。]

import z3
import importlib

def get_formula(src_file_name):
  try:
    f = z3.parse_smt2_file(src_file_name)
    return f
  except z3.Z3Exception as e:
    lines = open(src_file_name, 'rt').readlines()
    tmp1 = ' '.join(lines).replace("max", "c_max")
    tmp1 = tmp1.replace("sin", "c_sin")
    tmp1 = tmp1.replace("cos", "c_cos")
    tmp1 = tmp1.replace("tan", "c_tan")
    tmp1 = tmp1.replace("tanh", "c_tanh")
    tmp1 = tmp1.replace("atan", "c_atan")
    tmp1 = tmp1.replace("min", "c_min")
    tmp1 = tmp1.replace("max", "c_max")
    tmp1 = tmp1.replace("pi", "c_pi")
    tmp1 = tmp1.replace("List", "c_List")
    tmp1 = tmp1.replace("subset", "c_subset")
    tmp1 = tmp1.replace("difference", "c_difference")
    tmp1 = tmp1.replace("union", "c_union")
    tmp1 = tmp1.replace("fp", "c_fp")
    tmp1 = tmp1.replace("repeat", "c_repeat")
    importlib.reload(z3)
    f = z3.parse_smt2_string(tmp1)
    return f

使用此函数，我能够成功解析公式，但退出时程序出现段错误。似乎有一些引用在重新加载 z3 模块后也没有清理。