A three-valued boolean logic with Z3 solver

Question

I have been trying to define a three-valued propositional logic and reason about it using Z3 SMT Solver. To be more precise, I have define a sort Boolean with three values: TRUE, FALSE and NULL with some assertions.

(declare-sort Boolean 0)       ;I declare a sort Boolean
(declare-const TRUE Boolean)   ;I define three constants
(declare-const TRUE Boolean)
(declare-const FALSE Boolean)
(declare-const NULL Boolean)

(assert (distinct TRUE FALSE)) ;I define the meaning of these constants
(assert (distinct TRUE NULL))
(assert (distinct FALSE NULL))

(assert (forall ((b Boolean))
    (or (= b TRUE)
        (= b FALSE)
        (= b NULL))))

Next, let's say I am defining an the semantics of >= operator of integer under this logic, assuming that an integer can be NULL.

(declare-const nullInt Int)
(declare-fun >=_B (Int Int) Boolean)

(assert (forall ((i1 Int) (i2 Int))
    (= (= TRUE (>=_B i1 i2))
       (and (distinct i1 nullInt)
            (distinct i2 nullInt)
            (>= i1 i2)))))

(assert (forall ((i1 Int) (i2 Int))
    (= (= FALSE (>=_B i1 i2))
       (and (distinct i1 nullInt)
            (distinct i2 nullInt)
            (not (>= i1 i2))))))

(assert (forall ((i Int))
    (= NULL (>=_B i nullInt))))

(assert (forall ((i Int))
    (= NULL (>=_B nullInt i))))

Finally, with the above definitions, I use the >=_B function in my assertions but keep getting unexpected UNSAT or unknown. I would like to know what makes the theory falls into the undecidable area. Is it because of the Boolean sort I made? or Is it because of the assertions in which I quantify over the infinite set of Int?

Answer 1

I think you're complicating the modeling by using quantifiers and uninterpreted sorts. Simply make your boolean an enumeration and define your predicate accordingly:

(declare-datatype Boolean ((TRUE) (FALSE) (NULL)))

(declare-const nullInt Int)

(define-fun >=_B ((i1 Int) (i2 Int)) Boolean
    (ite (or (= i1 nullInt) (= i2 nullInt)) NULL (ite (>= i1 i2) TRUE FALSE)))

(check-sat)
(get-model)

This produces:

sat
(
  (define-fun nullInt () Int
    0)
)

Arbitrarily picking nullInt as 0. Now you can build your other operations on top of this and model whatever aspects of your 3-valued logic you want.

Two notes:

• I've written the most "obvious" definition of >=_B I can think of, though you should check to make sure this matches your intuition.

• It's odd to have nullInt as an uninterpreted constant. What you really want is probably "extended" integers. i.e., integers and a new value null-int. What you modeled however, does not do that. But you can do the same trick with a declare-datatype and make the type of extended integers and define >=_B accordingly. I'd use a type of the form:

(declare-datatype NullableInt ((NullInt) (RegInt (getRegInt Int))))

and then define all your operations on this type. Of course, this is more hairy, since you have to lift all your arithmetic operations (i.e., +, -, * etc.) as well.

Final note: while SMTLib is lingua-franca for SMT solvers, it's not the most human readable/writable. If you're experimenting, I'd recommend using a higher-level interface, such as one from Python/Haskell etc., that can get rid of most of the noise.