CODEWITHSUNDEEP
z3smtz3py
nnarek
nnarek

Reputation: 13

how to define SolveIfOnly function in z3?

I want to define SolveIfOnly function in z3 so that it will accept equation and will return its solution if there are only one solution otherwise it should return null

I have defined it so, but it does not work. I know that I can write python function which will create new instance of Solver,find solution and return it. But I want to have z3 function and be able to use it inside z3 expressions

from z3 import *

SortToFind = IntSort()

R = Datatype("Result")
R.declare("nil")
R.declare("res", ("val", SortToFind))
R = R.create()

SolveIfOnly = Function('SolveIfOnly', ArraySort(SortToFind,BoolSort()),   R)
n = FreshConst(SortToFind)
m = FreshConst(SortToFind)
cond = FreshConst(ArraySort(SortToFind,BoolSort()))
s = Solver()
s.add(ForAll([n,cond], If(And(cond[n],Not(Exists([m],And(cond[m],n!=m)))) , SolveIfOnly(cond)==R.res(n), SolveIfOnly(cond)==R.nil)))

equation = Array("equation",SortToFind,BoolSort())
n = FreshConst(SortToFind)
s.add(ForAll([n],equation[n]==(n-1==0))) 

# s.add(SolveIfOnly(equation)!=R.nil) # returns unsat 
# s.add(SolveIfOnly(equation)==R.nil) # returns unsat
# s.add(R.val(SolveIfOnly(equation))==1) # returns unknown 

s.check()

Upvotes: 0

Views: 44

Answers (0)

Related Questions