CODEWITHSUNDEEP
python-3.xz3solver
Jocelyn
Jocelyn

Reputation: 45

How to declare variables with unique name in python?

A program receives a map vars, which maps the name and type of variables in pathCons. Now, I want to solve this path_cons, I designed the following parse() function to try to implement it. However, to make solver identify all variables in path_cons, I have to first declare them. But their names are recorded into a variable, so how do I implement my goal?

def parse(vars, pathCons):
    for var in list(vars.keys()):
       if vars[var] == "uint":
           ???(should be name of var) = BitVec(var, 256)
       elif vars[x] == "bool":
           ??? = Bool(var)
   solver.add(eval(path_cons))

I thought of an idea that I randomly generate a unique name for each variable and then replace them with the new names in path_cons. But similarly, the generated name is also a value that cannot be as a name of variables.

For example,

vars = {"length":"int", "balance":"uint", "day":"uint", "flag":"bool"}
pathcons = "length>9, ULT(day, 10), UGE(balance + day, 100), flag == true"

Now I receive these two variables, and I want to solve pathcons.

Upvotes: 0

Views: 324

Answers (1)

alias
alias

Reputation: 30525

It's hard to understand what you're trying to achieve here. Stack-overflow works the best if you post code that people can run and see the issue you're running into.

But it seems to me that you want to create a bunch of z3 names corresponding to some notion of variables you have. To do so, simply create an array of them and use it accordingly. I'd do:

from z3 import *

progVars = {"length":"int", "balance":"uint", "day":"uint", "flag":"bool"}

def mkVar(var):
    if progVars[var] == "uint":
        return BitVec(var, 256)
    elif progVars[var] == "bool":
        return Bool(var)
    elif progVars[var] == "int":
        return Int(var)
    else:
        raise Exception("Don't know how to handle %s" % progVars[var])

z3Vars = [{"progVar": v, "z3Var": mkVar(v)} for v in progVars.keys()]

print(z3Vars)

This prints:

[{'progVar': 'length', 'z3Var': length}, {'progVar': 'balance', 'z3Var': balance}, {'progVar': 'flag', 'z3Var': flag}, {'progVar': 'day', 'z3Var': day}]

Notice how our dictionary is now indexed by your "program keys", and for each we store the created z3 variable in the z3Var field. Those will be true symbolic values that you can later manipulate with z3, add to the solver with constraints etc.

Upvotes: 1

Related Questions