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")
会导致以下错误。z3py针对有效的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同一文件提供不饱和度的结果。
在Python中使用traceback
,我发现以下是异常的根本原因TypeError: unorderable types: int() < Z3Exception()
根据异常堆栈,似乎错误源于原生Z3代码。
任何想法为什么会发生这种情况,以及如何解决这个问题?
根据您的评论,我试着在使用Z3解析之前转换公式:1)加载公式。 2)如果失败,则搜索/替换某些定义(例如列表)并重新加载公式。有趣的是,重新加载结果公式仍然导致解析器错误,并且没有关于错误位置的信息。 我想知道是否有从先前的分析尝试z3py饼干屑,混乱后来的解析尝试。如果是这样,在同一过程中重置z3py的最佳方法是什么? (我尝试过使用上下文,但没有成功。) – 2014-11-05 06:59:06
我试着给'z3._main_ctx'分配一个新的上下文,并且在退出这个过程时崩溃了这个过程。同样,我尝试通过'importlib.reload(z3)'重新加载z3模块,并在退出进程时导致段错误。任何想法如何重置z3py? – 2014-11-05 18:38:27