z3py針對有效的SMT2文件拋出分析器錯誤

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代碼。

任何想法爲什麼會發生這種情況，以及如何解決這個問題？

來源

2014-11-04 Venkatesh-Prasad Ranganath

您必須將「List」重命名爲其他名稱。從API中，Z3預加載「List」的內置定義。它會忽略邏輯指令，否則會縮小預加載的排序。

來源

2014-11-04 10:46:56

根據您的評論，我試着在使用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

基於@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

使用此功能，我能夠成功解析公式，但退出時程序SEG-故障。看起來有些引用在重新加載z3模塊後仍未清理。

來源

2014-11-05 01:51:40

來自2014年11月7日的最新Z3套件修復了這個問題！ – 2014-11-08 00:13:14

z3py針對有效的SMT2文件拋出分析器錯誤

回答

相關問題