CODEWITHSUNDEEP
sortingz3z3pytheorem-proving
user3723800
user3723800

Reputation: 145

use of sort in Z3

Can somebody help to know how to use "for all" correctly in Z3, Ive been looking in the documentation but I couldnt find information. What I am trying to do is

within "foo" I need say in Z3 something to the equivalent of

"let (u,r) be runnable(t) in { (assert ((u,r) is in users) (assert (r,t) is in roles)) }"

What I don't know is how to take the first element in runnable to assert that is in users, and then the second element to assert that is in roles.

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) Bool)

(assert (forall (t Task)) (foo))

(check-sat) (get-model)

Upvotes: 1

Views: 2243

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

This example is not well-formed SMT2, functions can not return multiple objects. The Z3 Guide for examples of how to use datatypes as well as quantifiers.

Upvotes: 1

Related Questions