CODEWITHSUNDEEP
pythonz3z3py
Julia
Julia

Reputation: 81

Defining Functions in Z3Py that return true for some inputs and false for others

I am trying to define a function that will return true if two objects are connected and false otherwise. In the example (cf. picture), where node a is connected to node b and c but there is no connection between b and c I want the function to behave like that:

connected(a, b) = true
connected(a, c) = true
connected(b, c) = false

So my question can be divided in two sub-questions:

a) How would i define such a function generally with the python api of Z3 (z3py), considering, that i would provide all possible assignments for the function upfront.

b) is it possible to define a funciton in a way, that I only provide the cases, where the function evaluates to true (i.e. only for the connected nodes) and then say somehow, that this function should evaluate to false in all other cases.

enter image description here

Upvotes: 1

Views: 152

Answers (2)

Behrouz Talebi
Behrouz Talebi

Reputation: 21

alias is right, you can simply declare the signature of the function and the implementation as you please. In other words, the evaluation of the function is up to you to assert.

Upvotes: 0

alias
alias

Reputation: 30525

Sure:

from z3 import *

Object, (a, b, c) = EnumSort('Object', ('a', 'b', 'c'))

connections = [(a, b), (a, c)]

def isConnected(x, y):
    return Or([And(x == i, y == j) for (i, j) in connections])

s = Solver()
s.add(isConnected(a, b))
s.add(isConnected(a, c))
print(s.check())

s.add(isConnected(b, c))
print(s.check())

The first print will say sat, and the second will say unsat, since b and c are not connected.

You can easily generalize this to any number of objects. Or even do things like:

s = Solver()
p = Const('p', Object)
q = Const('q', Object)
s.add(isConnected(p, q))
print(s.check())
print(s.model())

which will print:

sat
[q = b, p = a]

but note that this assignment will never contain the pair b, c as requested.

Upvotes: 1

Related Questions