CODEWITHSUNDEEP
z3datalog
jnfoster
jnfoster

Reputation: 31

Z3 muZ + uninterpreted functions?

Are uninterpreted functions supported in muZ?

I'd like to do something like the following:

(declare-fun f (Int) Int)
(declare-rel r (Int))
(declare-var X Int)
(rule (=> (= (f X) X) (r X)))
(query (r X)
:default-relation smt_relation2
:engine datalog
:print-answer true)

but it seems that I need to supply a definition for f as Z3 returns the following output:

% z3 -smt2 test.z3
error "query failed: Uninterpreted 'f' in r(#0) :- 
(= (f (:var 0)) (:var 0)).
")
unknown

I think I can get away with modeling my functions as relations, but wanted to see if there is another workaround...

Thanks!

-N

Upvotes: 2

Views: 389

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 21

Uninterpreted functions are not supported. In some cases it will work with arrays instead, but the handling of arrays is ad hoc (there is no generalization step in the pdr engine). You probably also want to use the pdr engine for such problems.

Upvotes: 2

Related Questions