1

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?

HoaNg
  • 25
  • 2
  • `unknown` would surely be due to the quantifiers. Quantifiers make the logic semi-decidable. `unsat` however, just means that: We can only debug that if you actually post an actual query. As stated, what you posted simply makes `z3` spin forever. – alias Jan 25 '22 at 04:57
  • Instead of declaring `Boolean` as a sort with assumptions, you might want to make it a simple enumeration. That should simplify things to a large extent, and you might have better luck. – alias Jan 25 '22 at 06:29
  • Thanks @alias for the comments, let me work the problem some more and also try with enumeration. – HoaNg Jan 25 '22 at 06:36
  • Sure. Note that you should also directly define your less than function, instead of using axioms. Once you have the enumeration for your Boolean, there’s no reason to make the ordering defined by quantified axioms: it should just be a regular function definition. – alias Jan 25 '22 at 08:27

1 Answers1

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • a question if you don't mind: how would your proposed code be implemented via the Python API, specifically the `declare-datatype` and `define-fun`? (Should I ask this in a separate question?) – Felix Emanuel Feb 18 '22 at 11:04
  • 1
    Yes, you can use the z3py api to add data-type declarations; and the functions you need would be actual Python functions that manipulate those values directly. See the `Datatypes` section in https://ericpony.github.io/z3py-tutorial/advanced-examples.htm for an example. If that doesn't help, feel free to post a new question. – alias Feb 18 '22 at 21:06
  • 1
    Hi @alias, I followed your advice that construct my boolean as enumeration and refine some few other things and my problem seems to be solved for now. Thank you for the thoroughly explanation! I am using transformation tool to translate from a DSL to theory in SMTLib so the user-unfriendliness of the generated theory wasn't one of my concern. Cheers! – HoaNg Mar 04 '22 at 12:15