Z3;使用 if-then-else 进行简化

【问题标题】：Z3; Simplify with if-then-elseZ3;使用 if-then-else 进行简化
【发布时间】：2020-07-30 02:00:57
【问题描述】：

有没有办法将下面的表达式简化为“6

(declare-fun var () Int)
(simplify
    (exists ((bx Int))
        (and
        (exists ((byX Int))
          (ite (> bx 5) (= byX 0) (&& (> bx 2) (= byX (+ byX 4)))))
        (= bx (+ var 1))
        (> var 6)
        )
      )
  :push_ite_arith true
  :pull_cheap_ite true
  :ite_extra_rules true
)
      
(assert
    (not
      (iff 
        (exists ((bx Int))
            (and
            (exists ((by Int))
              (ite (> bx 5) (= by 0) (&& (> bx 2) (= by (+ by 4)))))
            (= bx (+ var 1))
            (> var 6)
            )
          )
        (< 6 var)
      )
    )
)
(check-sat)

【问题讨论】：

标签： z3

【解决方案1】：

一般不会，不会。

Z3 的简化和您认为的“简单”通常不一样，它或多或少像一个黑匣子一样工作。它不会像您从符号数学包或类似程序中获得的那样产生输出：简化更倾向于使输入“更简单”以进一步求解；不是为了“将它呈现给用户”的目的。

您可以在 stack-overflow 上找到许多类似的问题，请参阅：https://stackoverflow.com/search?q=%5Bz3%5D+simplify，尤其是来自 Leo 的这个答案：simplification in Z3

【讨论】：