Are equations with products of uninterpreted functions unsolvable in Z3

Question

The following code

(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns "unknown", even though there is an obvious solution. Eliminating arguments to f and g (effectively making them constants?) results in "sat" with expected assignments. I guess, my question is: what is special about arithmetic with uninterpreted functions?

BTW, replacing * with + also results in "sat", so the issue is not about uninterpreted functions, per se, but about how they are combined.

Additional thoughts

Making the domain (very) finite does not help, e.g.,

(declare-fun f (Bool) Real)
(declare-fun g (Bool) Real)
(declare-const x Bool)
(declare-const y Bool)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns "unknown". This is odd given that f:Bool->Real is essentially just two variables f(False) and f(True) (of course, the solver has to recognize this).

Inability to handle non-linear arithmetic over real-valued uninterpreted functions is a very severe limitation because arrays are implemented as uninterpreted functions. So, for example,

(declare-const a (Array Int Real))
(assert (= (* (select a 1) (select a 1)) 1))
(check-sat)
(get-model)

returns "unknown". In other words, any non-linear algebraic expression on real array elements involving multiplication is unsolvable:'(

Answer 1

It's the non-liearity introduced by the multiplication that makes the problem hard to solve, not the uninterpreted functions. In fact, you can ask the solvers why by using the get-info command:

(set-logic QF_UFNIRA)
(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-info :reason-unknown)

Here're some responses I got from various solvers:

Z3:

(:reason-unknown smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic)))

CVC4:

(:reason-unknown incomplete)

MathSAT:

(error "sat, but with non-linear terms")

So, as the solvers themselves improve and start handling more nonliear arithmetic, you might get models eventually. But, in general, nonlinear problems will always be problematic as they are undecidable when integers are involved. (Since you can code Diophantine equations using non-linear terms.)

See also How does Z3 handle non-linear integer arithmetic? for a relevant discussion from 2012.

Removing uninterpreted functions

Even if you get rid of the uninterpreted functions, you'd still be in the unknown land, so long as you mix Int and Real types and non-linear terms:

(set-logic QF_NIRA)
(declare-const f Real)
(declare-const g Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ (* f g) (to_real (+ x y))) 1.0))
(check-sat)
(get-info :reason-unknown)

Z3 says:

(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")

So, the issue would arise with mixed types and non-linear terms.