Zapobieganie upraszczaniu rozwiązania

Question

Chcę, aby rozwiązanie wróciło z Z3 bez uproszczeń za pomocą instrukcji let.

Na przykład jeśli dam następujące:

(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)))) 

wrócę rozwiązania jak:

(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)) 

Czy istnieje sposób, aby powiedzieć Z3 nie wyodrębnić kilka złożonych wyrażeń w oświadczeniu let ? Łatwiej będzie mi przeanalizować wynik, jeśli otrzymam odpowiedź bez deklaracji.

Answer 1

Możemy ustawić następujące opcje, aby zapobiec ładną drukarkę Z3 z użyciem let s

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

Wszelkie dużą liczbę rade.

Musimy pamiętać, że wyświetlanie niektórych formuł zawierających wiele współdzielonych wyrażeń podrzędnych może być niewykonalne, gdy unikniemy let s. Wewnętrznie Z3 przechowuje formuły jako DAG zamiast Drzew. Jeśli nie używamy let s, ładny wydruk takich wzorów może być wykładniczo większy niż ich wewnętrzna reprezentacja. Dlatego nie powinniśmy nadużywać powyższych opcji.

Answer 2

Używam z3-4.5.0 i wygląda na to, że nazwy opcji nieco się zmieniły. Jeśli pp-max-depth nie działa, spróbuj pp.max_depth i pp.min_alias_size.

Używam API Javy oraz następujące pracował ze mną

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