CODEWITHSUNDEEP
z3
user2158237
user2158237

Reputation: 43

Simplifying uninterpreted functions in Z3

Is there any way to apply simplifications to uninterpreted functions defined in z3, rather than the goals and subgoals ?

I have the following z3 code :

(declare-fun f (Bool Bool) Bool)
(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)
(get-model)

And I get the following output:

sat
(model 
(define-fun b1!1 () Bool
  false)
(define-fun b2!0 () Bool
  false)
(define-fun k!7 ((x!1 Bool)) Bool
  false)
(define-fun f!8 ((x!1 Bool) (x!2 Bool)) Bool
  (ite (and (= x!1 false) (= x!2 true)) true
  false))
(define-fun k!6 ((x!1 Bool)) Bool
  (ite (= x!1 false) false
  true))
(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (f!8 (k!7 x!1) (k!6 x!2)))
)

It turns out that by applying rewrite rules to the definition of f, we can get that f is equal to the second argument (x!2) by the following derivation:

(f!8 (k!7 x!1) (k!6 x!2))
= (f!8 false (k!6 x!2))
= (f!8 false x!2)
=(x!2)

Is there any way to get z3 to produce the following definition automatically ?

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (x!2))

Thanks for your help. Regards, Oswaldo.

Upvotes: 4

Views: 533

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

One option is to ask Z3 to evaluate the expression (f x y) where x and y are fresh Boolean constants. The eval command will evaluated (f x y) in the current model, and will produce y in your example. Here is the complete example (also available online here): 

(declare-fun f (Bool Bool) Bool)

; x and y are free Boolean constants that will be used to create the expression (f x y)
(declare-const x Bool)
(declare-const y Bool)

(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)

(eval (f x y))

Upvotes: 4

Related Questions