CODEWITHSUNDEEP
z3relationsmtsat-solvers
Fathiyeh
Fathiyeh

Reputation: 31

Can we define relations in Z3?

I am new to z3 SMT solver. I need to define a relation, instead of a function. I mean a function that can return more than one value. I looked up the tutorial, and couldn't find anything. I appreciate if you can help me in this regard.

Thanks a lo.

Upvotes: 2

Views: 976

Answers (3)

OrenIshShalom
OrenIshShalom

Reputation: 7162

I think the following example is probably what you look for:

(define-fun sqrt ((a Int) (b Int)) Bool
    (= (* b b) a)
)
(declare-const a  Int)
(declare-const b1 Int)
(declare-const b2 Int)
(assert (sqrt a b1))
(assert (sqrt a b2))
(assert (not (= b1 b2)))
(check-sat)
(get-model)

And when I call z3 I get:

$ z3 -smt2 rel.smt
sat
(model 
  (define-fun b2 () Int
    2)
  (define-fun a () Int
    4)
  (define-fun b1 () Int
    (- 2))
)

The sqrt relation is simply a set of ordered pairs: {(a,b) | a == b*b}. and both (4,2) and (4,-2) belong to this relation. In SMT phrasing, this means that both sqrt(4,2) and sqrt(4,-2) are true. This corresponds to your question's phrasing where 4 can have multiple values. Unfortunately, other answers like the one that uses foo do not really handle relations but rather ask the solver to choose between two functions.

Upvotes: 0

alias
alias

Reputation: 30525

In a sense, SMT "naturally" supports relational programming. You can simply disjunct the possible values for an argument, and thus achieve the desired result. Something like:

(declare-fun foo ((Int)) Int)
(assert (or (= (foo 3) 4) (= (foo 3) 5)))
(check-sat)
(eval (foo 3))   ; might produce 4 of 5
(assert (distinct (foo 3) 4))
(check-sat)
(eval (foo 3))   ; will produce 5
(assert (distinct (foo 3) 5))
(check-sat)      ; will declare unsat

Here're you're saying foo when applied to 3, can produce 4 or 5. And then you can assert "further" facts to constrain the space as needed; or leave it free. You can use this trick to essentially model foo as a relation; making the SMT-solver to behave as a relational-programming-language..

Of course, how you really want to go about modeling relations really depends on the problem at hand. The above may not be the best choice for your problem.

Upvotes: 1

Kyle Jones
Kyle Jones

Reputation: 5532

Use one of the logics that supports the ArrayEx theory, which provides the Array sort and associated functions for manipulating arrays. You can then have your functions return array values which can contain arbitrarily many Ints or Bools or whatever.

This SMT tutorial is a good resource that gathers many SMT details into one place.

Upvotes: 1

Related Questions