मैं यह समझने की कोशिश कर रहा हूं कि C ++ API का उपयोग करके Z3 के ऑप्टिमाइज़ वर्ग के लिए टाइमआउट कैसे सेट किया जाए।
यह मेरा कोड है:
context c;
optimize opt(c);
z3::params par(c);
par.set("timeout", 1000);
opt.set(par);
लेकिन मुझे "अज्ञात पैरामीटर" टाइमआउट "" अपवाद मिलता हैलाइन ऑप्ट.सेट (बराबर) पर। क्या ऑप्टिमाइज़ क्लास के लिए टाइमआउट सेट करना संभव है (टाइमआउट के बाद, मैं सबसे अच्छा समाधान प्राप्त करना चाहता हूं)?
धन्यवाद!
उत्तर:
जवाब के लिए 0 № 1मुझे पता है कि यह एक पुराना प्रश्न है, लेकिन अगर किसी को अभी भी उत्तर की तलाश है, तो आपको इसकी आवश्यकता है:
Z3_global_param_set ("टाइमआउट", टाइमआउट);
और आपके टाइमआउट को सी स्ट्रिंग के रूप में दिया जाना चाहिए।