CODEWITHSUNDEEP
z3smtz3py
z3_test
z3_test

Reputation: 19

How to convert Z3Py code to C# code (Z3, SAT)

in past i write some Z3Py code that i want now convert to C# .NetCore. I check many examples but i have some problems :-)

I have defined function with name MyFun, that accept parameter and return variable based on value. Simple example:

H0 = BitVec('H0', 8)
H1 = BitVec('H1', 8)
H2 = BitVec('H2', 8)
H3 = BitVec('H3', 8)
I1 = BitVec('I1', 8)
T1 = BitVec('T1', 8)

def MyFun(N):
  return z3.If(N == 0x00, H0,
         z3.If(N == 0x01, H1,
         z3.If(N == 0x02, H2, H3)))

s.add(T1 == z3.If(MyFun(I1) == 0x33, 0x11, 0x12) )

I have problem with "function definition" and also problem with "z3.If". I think MkFuncDecl is for something else. Maybe solution is create normal C# Function with classic C# If and then directly call it? I think it must be somehow defined inside Z3... (due speed, Z3 <-> C#) Or maybe it was working also with the same way inside Z3Py (Python function with, Python If wrapper)?

Upvotes: 0

Views: 375

Answers (1)

alias
alias

Reputation: 30428

It would be a regular C# function, but calling Z3's If, not C#'s If. Essentially you're building the abstract-syntax-tree for the expression, it just happens to be in C# as opposed to Python. Otherwise, it's the same.

Upvotes: 2

Related Questions