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")
会导致以下错误。在
但是用z3-4.3.2.bb56885147e4-x64-osx-10.9.2cli处理同一个文件会产生不sat的结果。在
{{Z3>源于下面的异常{Z3>源于本机代码。在
你知道为什么会发生这种情况吗?怎么解决?在
你必须将“列表”重命名为其他名称。从API中,Z3预加载“List”的内置定义。它忽略逻辑指令,否则会缩小预加载的sort。在
基于@nikolaj注释,我使用下面的函数通过重命名标识符来转换SMT2文件,这些标识符在使用z3api时与Z3预先加载的定义冲突。[除了
List
,函数重命名SMT-LIB公式中常用的标识符。]有了这个函数,我能够成功地解析公式,但程序seg在退出时出错。似乎有一些引用即使在重新加载z3模块之后也没有被清除。在
相关问题 更多 >
编程相关推荐