5
मैं क्यूएफबीवी सूत्रों पर जेड 3 का उपयोग कर रहा हूं। मैं सोच रहा था कि क्या Z3 एसएटी सॉल्वर जैसे सूत्रों पर वृद्धिशील रूप से काम कर सकता है, बूलियन क्लॉज पर। असल में मुझे निम्न लूप को लागू करने का एक तरीका चाहिए:क्या Z3 incremental मोड में काम कर सकता है?
F = initial QFBV formula
while(F is unsat) {
F := F Union {some additional QFBV formula based on unsat core}
}
क्या Z3 सीखा जानकारी बनाए रखता है? क्या मैं z3 incrementally उपयोग कर सकते हैं?
धन्यवाद।