z3：表達式與先驗函數從z3py到smt-lib2的轉換

據我所知，由於z3無法識別超越函數，所以在使用下面的代碼進行轉換時拋出錯誤。z3：表達式與先驗函數從z3py到smt-lib2的轉換

def convertor(f, status="unknown", name="benchmark", logic=""): 
    v = (Ast * 0)() 
    if isinstance(f, Solver): 
    a = f.assertions() 
    if len(a) == 0: 
     f = BoolVal(True) 
    else: 
     f = And(*a) 
    return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast()) 


pi, EI, kA , kB, N = Reals('pi EI kA kB N') 

s= Solver() 
s.add(pi == 3.1415926525) 
s.add(EI == 175.2481) 
s.add(kA>= 0) 
s.add(kA<= 100) 
s.add(kB>= 0) 
s.add(kB<= 100) 
s.add(N>= 100) 
s.add(N<= 200)

請更改輸入文件「beamfinv3.bch」的路徑，這可以在這裏找到：link

continue_read=False 
input_file = open('/home/mani/downloads/new_z3/beamfinv3.bch', 'r') 
for line in input_file: 
    if line.strip()=="Constraints": 
     continue_read=True 
     continue 
    if line.strip()=="end": 
     continue_read=False 
    if continue_read==True: 
     parts = line.split(';') 
     if (parts[0]!="end"):    
     #print parts[0] 
     s.add(eval(parts[0])) 

input_file.close() 
file=open('cyber.smt2','w')  
result=convertor(s, logic="None") 
file.write (result)

錯誤：

File "<string>", line 1, in <module> 
NameError: name 'sin' is not defined

任何出路？或幫助？

謝謝。

來源

2015-10-05 Rauf

此問題的核心是eval嘗試執行Python腳本，即在parts[0]內發生的所有函數都必須具有相同名稱的相應Python函數，而三角函數不是這樣（函數既不在Python API也不在C API，前者基於後者）。現在，您可以嘗試自己添加這些函數，也許可以使用基於parse_smt2_string的實現，或者也可以將Python字符串替換爲SMT2字符串。

Z3可以表示包含三角函數的表達式，但是當邏輯被設置爲某些東西時它會拒絕這樣做;見arith_decl_plugin。我不太瞭解Python，但它可能必須是None而不是""。

儘管Z3可以表示這些表達式，但它可能不是很好解決它們。請參閱Can Z3 handle sinusoidal and exponential functions，Z3 supports for nonlinear arithmetics和Z3 Performance with Non-Linear Arithmetic中的限制意見。

來源

2015-10-05 19:52:29

謝謝，但仍然不起作用，拋出相同的錯誤。 – Rauf

你還嘗試過什麼，以及你在餵食哪個表情？ –

我試圖更改「」無/無/「無」等我不完全知道如何：https://github.com/Z3Prover/z3/blob/master/src/ast/arith_decl_plugin.cpp#L550 工程，但如果三角函數被定義，那麼它不應該拋出任何錯誤，它應該承認「罪」。我餵它的表情非常大。 – Rauf

z3：表達式與先驗函數從z3py到smt-lib2的轉換

回答

相關問題