如何在 SMT-LIB 中定义谓词

Question

如何定义一个谓词，例如even: Int -> Bool，它接受一个整数并输出它是否是偶数？

我尝试了类似的东西

(set-logic AUFNIRA)
(declare-fun even (Int) Bool)

我想知道如何声明，例如，even(2) 是真的。

Answer 1

大约有 3 种方法可以做到这一点。

1. 您可以使用解释谓词(_ divisible 2)。

   (assert ((_ divisible 2) 6))
   

   您可以使用define-fun 来精确捕捉。

   (define-fun even ((x Int)) Bool ((_ divisible 2) x))
   

   请注意，这可能不在您选择的逻辑范围内，例如 QF_LIA。

2. 您可以声明一个未解释的谓词，并定义 它的语义逐点。

   (declare-fun even (Int) Bool)
   (assert (even 2))
   (assert (not (even 3)))
   

3. 您可以声明一个未解释的谓词并定义 它的语义通过量词。

   (declare-fun even (Int) Bool)
   (assert (forall ((x Int)) (= (even x) (exists ((y Int)) (= x (* 2 y))))))