将变量约束到数组中

如果不知道你想做什么,很难在这里提出好的建议。但是,也许你不需要 sqrt ?如果你想要的只是一个完美正方形的数字,那么你可以换一种方式:

(declare-fun sqrtx () Int)
(declare-fun x     () Int)

; this will make sure x is a perfect square:
(assert (and (>= sqrtx 0) (= x (* sqrtx sqrtx))))

; make it interesting:
(assert (> x 10))

(check-sat)
(get-value (x sqrtx))

印刷品:

sat
((x 16)
 (sqrtx 4))

本质上,对于您想要的每个“完美的正方形”,您可以声明一个幽灵变量并断言所需的关系。

请注意,这会导致非线性(因为您要将两个符号值相乘),因此解算器可能难以处理所有约束。但是,如果不知道你到底在做什么,我认为这是最简单的方法来拥有完美的平方和推理。