5
के लिए पैटर्न खोजने में विफल रहा मुझे निम्न सरल SMT-LIB प्रोग्राम में दिखाए गए एक समस्या मिलती है।Z3 में चेतावनी संदेश के पीछे क्या कारण है: "क्वांटिफ़ायर (क्वांटिफ़ायर आईडी: के! 18)"
श्रीमती मसलन कोड:
WARNING: failed to find a pattern for quantifier (quantifier id: k!18)
sat
........
........
मैं चेतावनी संदेश के बारे में सोच रहा हूँ:
(declare-fun isDigit (Int) Bool)
(assert (forall ((x Int))
(=> (isDigit x)
(and (>= x 0) (< x 10))
)
)
)
(assert (forall ((x Int))
(=> (and (>= x 12) (< x 15))
(exists ((y Int))
(and (>= y 1) (< y 6)
(isHost (- x y))
)
)
)
)
)
(check-sat)
(get-model)
यह निम्न चेतावनी देता है। मुझे पता है कि मुझे कुछ याद आ रही है, लेकिन मैं समझ नहीं पा रहा हूं। क्या कोई इस मुद्दे में मेरी मदद कर सकता है?