遍歷C/C++中的Z3_ast樹

簡而言之，我需要能夠遍歷Z3_ast樹並訪問與其節點相關的數據。似乎無法找到有關如何做到這一點的任何文檔/示例。任何指針都會有幫助。遍歷C/C++中的Z3_ast樹

最後，我需要解析smt2lib類型公式到Z3中，使一些變量爲常量替換，然後在與另一個不相關的SMT Sovler兼容的數據結構中重現該公式（具體而言，我沒有認爲關於mistral的細節對於這個問題很重要，但有趣的是，它沒有命令行界面，我可以給它提供文本公式，它只是一個C API）。我已經想到要生成公式的格式，我需要遍歷Z3_ast樹並以所需格式重構公式。我似乎無法找到任何證明如何做到這一點的文檔/示例。任何指針都會有幫助。

來源

2012-09-19 Garvit Juniwal

考慮使用定義在z3++.h處的C++輔助類。 Z3發行版還包含使用這些類的示例。這是一個遍歷Z3表達式的小代碼片段。如果你的公式不包含量詞，那麼你甚至不需要處理is_quantifier()和is_var()分支。

void visit(expr const & e) { 
    if (e.is_app()) { 
     unsigned num = e.num_args(); 
     for (unsigned i = 0; i < num; i++) { 
      visit(e.arg(i)); 
     } 
     // do something 
     // Example: print the visited expression 
     func_decl f = e.decl(); 
     std::cout << "application of " << f.name() << ": " << e << "\n"; 
    } 
    else if (e.is_quantifier()) { 
     visit(e.body()); 
     // do something 
    } 
    else { 
     assert(e.is_var()); 
     // do something 
    } 
} 

void tst_visit() { 
    std::cout << "visit example\n"; 
    context c; 

    expr x = c.int_const("x"); 
    expr y = c.int_const("y"); 
    expr z = c.int_const("z"); 
    expr f = x*x - y*y >= 0; 

    visit(f); 
}

來源

2012-09-19 20:02:41

遍歷C/C++中的Z3_ast樹

回答

相關問題