सी/सी ++

Question

में Z3_ast पेड़ ट्रैवर्सिंग संक्षेप में, मुझे Z3_ast पेड़ को पार करने और अपने नोड्स से जुड़े डेटा तक पहुंचने में सक्षम होना चाहिए। ऐसा करने के तरीके पर कोई दस्तावेज़ीकरण/उदाहरण नहीं मिल रहा है। कोई संकेतक सहायक होगा।

लंबाई में, मुझे z3 में smt2lib प्रकार के सूत्रों को पार्स करने की आवश्यकता है, कुछ परिवर्तनीय निरंतर प्रतिस्थापन करें और फिर डेटा संरचना में सूत्र को पुन: उत्पन्न करें जो किसी अन्य असंबंधित एसएमटी सॉवलर के साथ संगत है (विशिष्ट होने के लिए गलत है, मैं नहीं करता इस सवाल के लिए गलत के बारे में विवरण महत्वपूर्ण हैं लेकिन मज़ेदार रूप से पर्याप्त है कि इसमें कमांड लाइन इंटरफ़ेस नहीं है जहां मैं इसे टेक्स्ट फॉर्मूला खिला सकता हूं। इसमें केवल एक सीपीआई है)। मैंने पाया है कि गलत तरीके से प्रारूप में सूत्र उत्पन्न करने के लिए, मुझे Z3_ast पेड़ को पार करने और वांछित प्रारूप में सूत्र का पुनर्निर्माण करने की आवश्यकता होगी। मुझे ऐसा कोई प्रलेखन/उदाहरण नहीं मिल रहा है जो यह दर्शाता है कि यह कैसे करें। कोई संकेतक सहायक होगा।

Answer 1

z3++.h पर परिभाषित सी ++ सहायक कक्षाओं का उपयोग करने पर विचार करें। 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); 
}