सरलीकृत होने से समाधान को रोकें

Question

मैं समाधान को let कथनों का उपयोग करके सरलीकरण के बिना z3 से वापस प्राप्त करना चाहता हूं।

उदाहरण के लिए अगर मैं निम्नलिखित दे:

(declare-const x Int) 
    (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
      (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
             (and (<= (- 4 x.1) 0) 
              (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0)))) 

मैं वापस के रूप में समाधान मिल:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13))) 
       (<= x 11)))) 
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1)) 

वहाँ एक रास्ता जेड 3 बताने के लिए एक लेट बयान में कुछ जटिल भाव को निकालने के लिए नहीं है ? परिणाम के विश्लेषण के लिए मेरे लिए आसान होगा अगर मुझे जवाब देने के बिना जवाब मिल जाए।

Answer 1

हम let रों

(set-option :pp-min-alias-size 1000000) 
(set-option :pp-max-depth  1000000) 

किसी भी बड़ी संख्या का उपयोग कर चाल करना होगा से जेड 3 सुंदर प्रिंटर को रोकने के लिए निम्न विकल्प सेट कर सकते हैं।

हमें यह ध्यान रखना होगा कि कुछ सूत्रों को प्रदर्शित करने के लिए संभव नहीं हो सकता है जिनमें बहुत से साझा उप-अभिव्यक्तियां होती हैं जब हम let से बचते हैं। आंतरिक रूप से, Z3 सूत्रों को पेड़ों के बजाय डीएजी के रूप में संग्रहीत करता है। अगर हम let एस का उपयोग नहीं करते हैं, तो ऐसे सूत्रों का सुंदर प्रिंट उनके आंतरिक प्रतिनिधित्व से तेजी से बड़ा हो सकता है। इसलिए, हमें उपरोक्त विकल्पों का दुरुपयोग नहीं करना चाहिए।

Answer 2

मैं z3-4.5.0 का उपयोग कर रहा हूं और ऐसा लगता है कि विकल्पों के नाम थोड़ा बदल गए हैं। यदि pp-max-depth आपके लिए काम नहीं किया है, तो pp.max_depth और pp.min_alias_size आज़माएं।

मैं जावा एपीआई का उपयोग कर रहा हूँ और मेरे साथ काम किया निम्नलिखित

com.microsoft.z3.Global.setParameter("pp.min_alias_size", "1000000"); 
com.microsoft.z3.Global.setParameter("pp.max_depth", "1000000");