首页 文章

如何在SMT-LIB中定义谓词

提问于
浏览 次
0

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

我试过类似的东西

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

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

predicate smt

1 回答

  • 3

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

    (assert ((_ divisible 2) 6))

    你可以使用define-fun来捕捉甚至是准确的 .

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

    请注意，这可能不是您选择的逻辑，比如QF_LIA .

    • 您可以声明未解释的谓词，并逐点定义其语义 .
    (declare-fun even (Int) Bool)
(assert (even 2))
(assert (not (even 3)))
    • 您可以声明未解释的谓词并通过量词定义其语义 .
    (declare-fun even (Int) Bool)
(assert (forall ((x Int)) (= (even x) (exists ((y Int)) (= x (* 2 y))))))
    回复于

相关问题