CODEWITHSUNDEEP
predicatesmt
ndb
ndb

Reputation: 137

How to define a predicate in SMT-LIB

How would I define a predicate such as even: Int -> Bool, which takes an integer and outputs whether it is even or not?

I tried something like

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

I want to know how to declare, for example, that even(2) is true.

Upvotes: 1

Views: 434

Answers (1)

Tim
Tim

Reputation: 1098

There are roughly 3 ways to do this.

  1. You can use the interpreted predicate (_ divisible 2).

    (assert ((_ divisible 2) 6))

    You can use a define-fun to capture even exactly.

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

    Note that this may not be in your logic of choice, say QF_LIA.

  2. You can declare an uninterpreted predicate, and define its semantics pointwise.

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

  3. You can declare an uninterpreted predicate and define its semantics via quantifiers.

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

Upvotes: 5

Related Questions