簡化使用C++ API

Question

Z3表達我有這樣的表達

z3::expr expr = (exists ((flag Bool)) 
       (exists ((w Int)) 
       (exists ((i Int)) 
        (exists ((counter Int)) 
         (and (= i (+ x y z)) 
          flag 
          (not (= i 0)) 
          (= i counter) 
          (not (= w counter)) 
          (>= i 1) 
          (= w 0))))))) 

我使用C++ API做量詞消除和簡化。

z3::goal g(ctx); 
g.add(expr); 
z3::apply_result result = (qe & simplify & propagate_ineqs)(g); 

我已經定義了策略。

我想要得到這樣的結果：

(or (>= (+ x y z) 1) 
    (<= (+ x y z) -1)) 

，但我得到這個輸出，我的應用程序是適當的：

(let ((a!1 (or (<= (+ (* (- 1) x) 
          (* (- 1) y) 
          (* (- 1) z)) 
         (- 1)) 
        (<= (+ x y z) (- 1))))) 
     (and (or (<= (+ x y z) (- 1)) 
       (>= (+ x y z) 1)) 
      a!1 
      (>= (+ x y z) 1))) 

我應該用什麼戰術，使其工作，因爲我想要的嗎？

Answer 1

我解決了這個問題，通過設置下的這些選項，定義目標之前：

ctx.set(":pp-min-alias-size", 1000000); 
ctx.set(":pp-max-depth", 1000000); 

它並沒有簡化，因爲我想要的，但去掉了「讓」 s以及總比沒有好！