CODEWITHSUNDEEP
z3
rem
rem

Reputation: 893

Uninterpreted int Constants in z3

Is it possible to treat int constants as uninterpreted in z3? For example, treat tuple(project(t, 0), project(t, 1)) = t as tuple(project(t, left), project(t, right)) = t. Context: my equations are essentially in QF_UF, but because they contain int constants I'm forced to use a logic with integer arithmetic which leads to nontermination sometimes.

Upvotes: 0

Views: 152

Answers (1)

alias
alias

Reputation: 30525

You can declare Int to be an uninterpreted sort, so long as you set the logic to be something that doesn't define it already:

(set-logic QF_UF)

(declare-sort Int 0)
(declare-fun f ((Int)) Int)

(declare-fun i () Int)
(assert (distinct (f i) (f i)))
(check-sat)

z3 says:

unsat

If you add:

(assert (= (f 2) 2))

then you get:

(error "line 8 column 15: Sort mismatch at argument #1 for function (declare-fun f (Int) Int) supplied sort is Int")

which avoids confusions. (Though the error message is rather confusing to read!)

If you set your logic to be:

(set-logic QF_LIA)

then z3 says:

(error "line 3 column 18: sort already defined Int")

so, that works out as well. See Section 4.2.3 of the SMTLib specification for details.

Hope that helps!

Upvotes: 0

Related Questions