以下代码
(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)
返回“未知”，即使有一个明显的解决方案。消除 f 和 g 的参数（有效地使它们成为常量？）导致具有预期分配的“sat”。我想，我的问题是：具有未解释函数的算术有什么特别之处？
顺便说一句，用 + 替换 * 也会导致“sat”，因此问题本身不在于未解释的函数，而在于它们如何组合。
其他想法
使域（非常）有限没有帮助，例如，
(declare-fun f (Bool) Real)
(declare-fun g (Bool) Real)
(declare-const x Bool)
(declare-const y Bool)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)
返回“未知”。这很奇怪，因为 f:Bool->Real 本质上只是两个变量 f(False) 和 f(True)（当然，求解器必须认识到这一点）。
无法处理实值未解释函数的非线性算术是一个非常严重的限制，因为数组是作为未解释函数实现的。所以，例如，
(declare-const a (Array Int Real))
(assert (= (* (select a 1) (select a 1)) 1))
(check-sat)
(get-model)
返回“未知”。换句话说，任何涉及乘法的实数数组元素上的非线性代数表达式都是不可解的:'(
正是乘法引入的非线性使问题难以解决，而不是未解释的函数。实际上，您可以使用以下get-info命令询问求解器原因：
(set-logic QF_UFNIRA)
(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-info :reason-unknown)
以下是我从各种求解器那里得到的一些回复：
Z3：
(:reason-unknown smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic)))
CVC4：
(:reason-unknown incomplete)
数学SAT：
(error "sat, but with non-linear terms")
因此，随着求解器自身的改进并开始处理更多的非线性算术，您最终可能会获得模型。但是，一般来说，非线性问题总是有问题的，因为它们在涉及整数时是不可判定的。（因为您可以使用非线性项对丢番图方程进行编码。）
另请参阅Z3 如何处理非线性整数算术？2012 年的相关讨论。
即使你摆脱了未解释的函数，你仍然会在unknown土地上，只要你混合Int和Real类型和非线性术语：
(set-logic QF_NIRA)
(declare-const f Real)
(declare-const g Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ (* f g) (to_real (+ x y))) 1.0))
(check-sat)
(get-info :reason-unknown)
Z3 说：
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")
因此，混合类型和非线性项会出现问题。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句