CODEWITHSUNDEEP
typeswrapperz3parametric-polymorphism
Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

Sort-parametric wrapper functions

Assuming the use of several built-in and user defined Z3 sorts, e.g. Int, Bool, S1, S2, ..., is there a way of writing a generic sort-wrapping and -unwrapping function that kind of casts from sort A to sort B and back? For example

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(WRAP[S1] b) ; Expression is of sort S1
(WRAP[S1] c) ; Expression is of sort S1
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int

I currently cover each case manually, e.g.

(declare-fun $boolToInt (Bool) Int)
(declare-fun $intToBool (Int) Bool)

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

(assert (forall ((x Bool))
  (= x ($intToBool($boolToInt x)))))

Such wrappers could be created automatically from a given set of sorts, but I would prefer a generic solution of possible.

Upvotes: 1

Views: 192

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

You can use datatypes to encode "union types". Here is an example:

(declare-sort S1)
(declare-sort S2)

(declare-datatypes () ((S1-S2-Int (WRAP-S1 (S1-Value S1))
                                  (WRAP-S2 (S2-Value S2))
                                  (WRAP-Int (Int-Value Int)))))

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(simplify (WRAP-S1 a))
(simplify (= (WRAP-S1 a) (WRAP-Int 10)))
(simplify (S1-Value (WRAP-S1 a)))
(simplify (is-WRAP-S2 (WRAP-S1 a)))
(simplify (is-WRAP-S1 (WRAP-S1 a)))
(simplify (is-WRAP-Int (WRAP-Int c)))
(simplify (S1-Value (WRAP-S2 b)))

You can find more information about datatypes in the Z3 guide. The datatype S1-S2-Int has three constructors: WRAP-S1, WRAP-S2 and WRAP-Int. Z3 automatically generates the recognizer predicates: is-WRAP-S1, is-WRAP-S2 and is-WRAP-Int. The accessors S1-Value, S2-Value and Int-Value are used to "deconstruct" a S1-S2-Int value. For example, for all a, (S1-Value (WRAP-S1 a)) = a. The value of (S1-Value (WRAP-S2 b)) is underspecified. In this case, Z3 treats S1-Value as a uninterpreted function.

BTW, the axiom 

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

is equivalent to false. It is essentially trying to inject the integers into the Booleans.

Upvotes: 3

Related Questions