Z3py: how to make constraints on "else" value in function output
I have outputted the function using z3py as follows
f = Function('f',IntSort(),IntSort(),IntSort())
After the approval of a set of restrictions, such as:
s.add(f(a1,b1)==c1)
s.add(f(a2,b2)==c2)
s.add(f(a3,b3)==c3)...
The function is output as
[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> 2]
How can I bind the else value to a fixed number? To print output f would be
[(a1,b1) -> c1, (a2,b2) -> c2, (a3,b3) -> c3, ..., else -> some number that I assert]
Edit:
from z3 import * s = Solver() k = Int('k') f = Function('f',IntSort(),IntSort()) s.add(And(f(1)==1,f(2)==2)) list1 = [] list1.append(k!=1) list1.append(k!=2) s.add(ForAll(k,Implies(And(list1),f(k)==5))) print s.check() print s.model()
Output signal
sat
[f = [1 -> 1, 2 -> 2, else -> 5]]
This seems to work great for this simple case.
However, when input for function 'f' is not specified in constraints. The exit may be strange. for example
from z3 import * s = Solver() f = Function('f',IntSort(),IntSort(),IntSort()) i = Int('i') j = Int('j') k = Int('k') l = Int('l') s.add(i>=0,i<5) s.add(j>=0,j<5) s.add(And(f(j,1)==i,f(i,2)==j)) list1 = [] list1.append(And(k==1,l==j)) list1.append(And(k==2,l==i)) s.add(ForAll([k,l],Implies(Not(Or(list1)),f(l,k)==5))) print s.check() print s.model()
Output signal
[i = 0,
k!6 = 0,
j = 3,
k!12 = 6,
f = [else -> f!15(k!13(Var(0)), k!14(Var(1)))],
f!15 = [(3, 1) -> 0, (0, 2) -> 3, else -> 5],
k!13 = [0 -> 0, 3 -> 3, else -> 6],
k!14 = [2 -> 2, 1 -> 1, else -> 0]]
Then it is difficult to interpret the output of f.
source to share
This is a great question and a very informed analysis. Yes, you can control the default values using quantifiers. The Z3 will have no choice but to agree. However, the coding of the models is based on how the quantifier instantiator is (see "Full Quantifier Creation" by Yeting Ge and Leonardo de Moura). Z3 does not beta abbreviate expressions in models and leaves them to applications to perform beta repairs if needed. You can have a beta Z3 with the addition of else branches by connecting your arguments to function parameters (use the substitution routines provided by the API) and then call the model evaluator to reduce the resulting expression relative to the model.
source to share