Z3

Question

में बाध्य चर के अनुक्रमण को समझना मैं समझने की कोशिश कर रहा हूं कि z3 में बाध्य चर कैसे अनुक्रमित हैं। यहां z3py और इसी आउटपुट में एक स्निपेट में। (http://rise4fun.com/Z3Py/plVw1)

x, y = Ints('x y') 
f1 = ForAll(x, And(x == 0, Exists(y, x == y))) 
f2 = ForAll(x, Exists(y, And(x == 0, x == y))) 
print f1.body() 
print f2.body() 

आउटपुट:।

ν0 = 0 ∧ (∃y : ν1 = y) 
y : ν1 = 0 ∧ ν1 = y 

f1 में, क्यों एक ही बाध्य चर x अलग सूचकांक है (0 और 1)। अगर मैं f1 संशोधित करता हूं और Exists निकालता हूं, तो x में एक ही अनुक्रमणिका (0) है।

मैं एक FOL सूत्र स्केला में एक डीएसएल कि मैं z3 को भेजना चाहते हैं में प्रतिनिधित्व किया है:

कारण मैं अनुक्रमण तंत्र को समझने के लिए चाहते हैं। अब ScalaZ3 में mkBound एपीआई है जो index और sort तर्कों के रूप में बाध्य चर बनाने के लिए है। मुझे यकीन नहीं है कि मुझे index तर्क में किस मूल्य को पास करना चाहिए। तो, मुझे पता है कि निम्नलिखित चाहते हैं: यदि मैं दो सूत्र phi1 और अधिकतम बाध्य चर अनुक्रमित n1 और n2 साथ phi2, क्या ForAll(x, And(phi1, phi2))

इसके अलावा में x के सूचकांक हो जाएगा

, वहाँ एक रास्ता है अनुक्रमित रूप में सभी चर दिखाने के लिए? f1.body() मुझे अनुक्रमित रूप में x दिखाता है और y नहीं। (मुझे लगता है कि कारण यह है कि y अभी भी f1.body() में बाध्य है)

Answer 1

Z3 डी ब्रुज़न इंडेक्स का उपयोग करके बाध्य चर को एन्कोड करता है। http://en.wikipedia.org/wiki/De_Bruijn_index टिप्पणी: निम्नलिखित विकिपीडिया लेख में विस्तार से डे Bruijn सूचकांकों का वर्णन सूचकांक ऊपर लेख में जेड 3 में, वे 0.

पर शुरू आपके दूसरे प्रश्न के बारे में, 1 से शुरू करें, तो आप जेड 3 सुंदर बदल सकते हैं मुद्रक। जेड 3 वितरण में पायथन एपीआई का स्रोत कोड शामिल है। सुंदर प्रिंटर फ़ाइल python\z3printer.py में लागू किया गया है। तुम बस विधि को बदलने के लिए की जरूरत है: आप HTML सुंदर प्रिंटर को फिर से परिभाषित करना चाहते हैं

def pp_var(self, a, d, xs): 
    idx = z3.get_var_index(a) 
    return seq1('Var', (to_format(idx),)) 

साथ

def pp_var(self, a, d, xs): 
    idx = z3.get_var_index(a) 
    sz = len(xs) 
    if idx >= sz: 
     return seq1('Var', (to_format(idx),)) 
    else: 
     return to_format(xs[sz - idx - 1]) 

, आप भी बदलना चाहिए।

def pp_var(self, a, d, xs): 
    idx = z3.get_var_index(a) 
    sz = len(xs) 
    if idx >= sz: 
     # 957 is the greek letter nu 
     return to_format('&#957;<sub>%s</sub>' % idx, 1) 
    else: 
     return to_format(xs[sz - idx - 1]) 

def pp_var(self, a, d, xs): 
    idx = z3.get_var_index(a) 
    return to_format('&#957;<sub>%s</sub>' % idx, 1) 

साथ