z3:科学表示法的集合逻辑意外行为

Question

当我用以下代码调用z3时

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

然后，我得到了预期的(和right)的答案：

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

但有时我需要解决更复杂的问题，需要指定一个逻辑来获得正确的结果，比如AUFNIRA (它支持整数/实和线性/非线性算法)。

但是，这些特定的逻辑都不支持我在这里使用的科学表示法()，我在这里输入了像(* -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运算符^并返回正确的解决方案，但是如果我试图指定任何逻辑，则会返回此错误。

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

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

BOOL，LIA，上帝军，NIA，NRA，QF_LRA，QF_NIA，QF_NRA，QF_UFLIA，QF_UFLRA，QF_UFNIA，QF_UFNRA，UFLIRA，UF上帝军，UFNIA，AUFNIRA

(是的，即使是无关紧要的)，但他们似乎都不支持电力运营商。这怎麽可能？

谢谢

Answer 1

SMT-LIB逻辑在smtlib.org中指定.power操作符不是任何SMT-LIB逻辑的一部分，因此解析器拒绝这些操作符。指定SMT逻辑时的期望是，求解程序根据所支持的片段进行操作。对于运算符(例如^)，除非第二个参数是非负整数，否则不存在一般决策过程。