1

Why is z3 unable to sat check the following?

(declare-fun f (Int) Int)
(assert (forall ((a Int) (b Int)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))
(check-sat)
(get-model)

I would expect a result along the lines of f(x) = x, however z3 seems to consume an increasing amount of ram, and never find a solution. Is this something uninterpreted functions are not intended for?

I've tried using reals and adding an additional function which I expect is the same as f, like so:

(declare-fun f (Real) Real)
(declare-fun g (Real) Real)
(assert (forall ((a Real)) (= (g a) a)))
(assert (forall ((a Real) (b Real)) (= (+ (f a) (f b) ) (f (+ a b)))))
(assert (= (f 1) 1))


(check-sat)
(get-model)
1

Well, it's not simple at all. Quantifiers are hard, and as you suspected, SMT solvers are not a good choice for reasoning with them. In your particular case, the model finder would have to find a very specific kind of function that has that property, and that is well beyond capabilities of current SMT solving technology; and honestly the focus.

Having said that, you can look into quantifier patterns: You can help the e-matching engine in certain cases to solve such problems, but it's definitely not the right technology. See here: https://rise4fun.com/z3/tutorialcontent/guide#h28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.