z3：科学记数法的集合逻辑意外行为

Question

当我使用以下代码调用 z3 时

    (declare-const x Real)
    (assert (> x (* -1.79769 (^ 10.0 308.0))))
    (check-sat)
    (get-model)

然后我得到以下，预期（和正确）答案：

    sat
    (model 
      (define-fun x () Real
        (+ 1.0 (* (- (/ 179769.0 100000.0)) (^ 10.0 308.0))))
    )

但有时我需要解决更复杂的问题，我需要指定逻辑以获得正确的结果，例如 AUFNIRA（支持 integer/real 和 linear/non-linear 算术） .

但是none这些特定的逻辑支持科学记数法的表示，我在这里使用的是输入值，如(* -1.7 (^ 10.0 308.0))（在常用科学记数法中正好代表-1.7e308）。

特别是，如果我只是添加一个 set-logic 命令获取下面的代码

    (set-logic AUFNIRA)
    (declare-const x Real)
    (assert (> x (* -1.79769 (^ 10.0 308.0))))
    (check-sat)
    (get-model)

然后我得到以下错误

    (error "line 3 column 38: unknown function/constant ^")
    sat
    (model 
    )

（注意空模型）。

我的问题是：如果不指定逻辑，求解器怎么可能支持 power 运算符 ^ 和 returns 正确的解决方案，但是如果我尝试指定 any 逻辑，则会返回此错误？

我的意思是，如果它在没有指定逻辑的情况下起作用，则意味着某些逻辑必须包含它，对吗？如果是，哪个逻辑包含此运算符？

根据this question我已经尝试了以下所有逻辑：

BOOL、LIA、LRA、NIA、NRA、QF_LRA、QF_NIA、QF_NRA、QF_UFLIA、QF_UFLRA、QF_UFNIA , QF_UFNRA, UFLIRA, UFLRA, UFNIA, AUFNIRA

（是的，即使是无关紧要的那个）但其中 none 似乎支持幂运算符。这怎么可能？

谢谢

Answer 1

SMT-LIB 逻辑在smtlib.org 中指定。电力运营商不是任何 SMT-LIB 逻辑的一部分，因此解析器拒绝此类运算符。指定 SMT-LIB 逻辑时的期望是求解器根据支持的片段运行。对于诸如 ^ 之类的运算符，除非第二个参数是非负整数，否则没有通用的决策过程。

z3: set-logic unexpected behavior for scientific notation