檢查一個公式是否是Z3Py中的一個術語

在Z3Py中，我需要使用標準語法term := const | var | f(t1,...,tn)來檢查某些術語是否是一個術語。我寫了下面的函數來確定，但我的方法來檢查是否n元函數似乎不是最佳。檢查一個公式是否是Z3Py中的一個術語

有沒有更好的方法來做到這一點？這些效用函數is_term,is_atom,is_literal等將被包括在Z3中是有用的。我會把它們在contrib部分

CONNECTIVE_OPS = [Z3_OP_NOT,Z3_OP_AND,Z3_OP_OR,Z3_OP_IMPLIES,Z3_OP_IFF,Z3_OP_ITE] 
REL_OPS = [Z3_OP_EQ,Z3_OP_LE,Z3_OP_LT,Z3_OP_GE,Z3_OP_GT] 

def is_term(a): 
    """ 
    term := const | var | f(t1,...,tn) 
    """ 
    if is_const(a): 
     return True 
    else: 
     r = (is_app(a) and \ 
       a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \ 
       all(is_term(c) for c in a.children())) 
     return r

來源

2013-01-03 Vu Nguyen

功能是合理的，幾點意見：

這取決於你的意思是在你規範「變種」是什麼。 Z3具有de-Brujin指數的變量。在z3py「is_var（a）」中有一個函數來檢查「a」是否是一個變量索引。
還有另一個布爾連接Z3_OP_XOR。
還有其他的關係操作，比如比較位向量的操作。這取決於您的意圖和代碼的用法，但您可以選擇檢查類型的表達式是否爲布爾型，以及是否確保未解釋頭部函數符號。（a）被定義爲返回is_app（a）和a.num_args（）== 0.所以is_const實際上是由默認情況處理的。
Z3由於簡化，解析或其他轉換而創建的表達式可能具有許多共享的子表達式。因此，直接遞歸下降可以在表達式的DAG大小中佔用指數時間。您可以通過維護已訪問節點的散列表來處理此問題。從Python中，您可以使用Z3_get_ast_id檢索表達式的唯一編號並將其保存在一個集合中。只要術語不被垃圾收集，標識符就是唯一的，所以你應該只保留這樣的一個局部變量。

所以，沿着線的東西：

def get_expr_id(e): 
    return Z3_get_ast_id(e.ctx.ref(), e.ast) 

def is_term_aux(a, seen): 
    if get_expr_id(a) in seen: 
     return True 
    else: 
     seen[get_expr_id(a)] = True 
     r = (is_app(a) and \ 
      a.decl().kind() not in CONNECTIVE_OPS + REL_OPS and \ 
      all(is_term_aux(c, seen) for c in a.children())) 
     return r 

def is_term(a): 
    return is_term_aux(a, {})

來源

2013-01-03 16:10:47

的「教科書」在一階邏輯中使用術語，原子的定義和文字不能直接應用到Z3表達式。在Z3中，我們允許表達式如f(And(a, b)) > 0和f(ForAll([x], g(x) == 0))，其中f是從布爾到Integer的函數。這種擴展不會增加表達能力，但在編寫問題時它們非常方便。 SMT 2.0標準還允許「術語」if-then-else表達式。這是另一個功能，可以讓我們在「條款」中嵌入「公式」。例如：g(If(And(a, b), 1, 0))。

當實現操作Z3表達式的過程時，我們有時需要區分佈爾表達式和非布爾表達式。在這種情況下，「term」只是一個沒有布爾類型的表達式。

def is_term(a): 
    return not is_bool(a)

在其他情況下，我們要處理以特殊方式布爾連接詞（And，Or，...）。例如，我們正在定義一個CNF翻譯器。在這種情況下，我們將「atom」定義爲任何不是量詞的布爾表達式，是一個（自由）變量或不是布爾連接詞之一的應用程序。

def is_atom(a): 
    return is_bool(a) and (is_var(a) or (is_app(a) and a.decl().kind() not in CONNECTIVE_OPS))

後，我們定義一個原子，文字可以被定義爲：

def is_literal(a): 
    return is_atom(a) or (is_not(a) and is_atom(a.arg(0)))

下面是一個說明這些功能的示例（在rise4fun也可在線）：

x = Int('x') 
p, q = Bools('p q') 
f = Function('f', IntSort(), BoolSort()) 
g = Function('g', IntSort(), IntSort()) 
print is_literal(Not(x > 0))  
print is_literal(f(x)) 
print is_atom(Not(x > 0)) 
print is_atom(f(x)) 
print is_atom(x) 
print is_term(f(x)) 
print is_term(g(x)) 
print is_term(x) 
print is_term(Var(1, IntSort()))

來源

2013-01-03 16:22:23

檢查一個公式是否是Z3Py中的一個術語

回答

相關問題