Z3Py: Parsing expressions using eval or z3.parse_smt2_string

Question

I am writing a python program that amongst other things has to convert large propositional formulae into z3 instances. For example the formula f that can be created by my program via

a = my_atomic_proposition("a") # Bool
b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42
c = my_atomic_proposition("c") # Bool
f = my_and(a, my_or(b, my_not(c)))

should be converted into the z3 instance g that is

a = z3.Bool("a")
b = z3.Real("b")
c = z3.Bool("c")
g = z3.And(a, z3.Or(b >= 42, z3.Not(c)))

Please keep in mind that I am talking about formulae containing mostly over 100 terms.

Following the post Z3 with string expressions I first tried to build my own parser (Option 1 suggested by Leornardo de Moura in the post) which simply went recursively through all of my formula's operands and built up the z3 instance on the way. This option was quite slow so I instead tried recursively building up strings which was much faster and then calling eval on them (Option 3 described in the post from above). This solution was much faster, however, did not work whenever my formulae became too big (a MemoryError was thrown).

So now I am about to try the third Option: Using z3.parse_smt2_string to create the z3 instance from a string (not the one that I used above with eval, it has to have different syntax). I would proceed somehow similar as it is done in Z3_parse_smtlib_string usage issues. However, I would like to know if I might run into similar memory issues using z3.parse_smt2_string as I did with eval? Since then I would probably look for another way before putting too much effort into this.

Also, if anybody has another (hopefully even smarter idea) on how I could achieve my goal I would be glad for any comment. Thank you for help!

EDIT - Example for MemoryError:

I will exemplify one case where a MemoryError is thrown: Let's assume I have the following formula as a string:

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,z3.Or(a___40,z3.And(True,z3.Or(a___41,z3.And(True,z3.Or(a___42,z3.And(True,z3.Or(a___43,z3.And(True,z3.Or(a___44,z3.And(True,z3.Or(a___45,z3.And(True,z3.Or(a___46,z3.And(True,z3.Or(a___47,z3.And(True,z3.Or(a___48,z3.And(True,z3.Or(a___49,z3.And(True,a___50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'

and the following list of strings that represent the variables of f:

variables = ['a___2', 'a___31', 'a___34', 'a___46', 'a___29', 'a___12', 'a___9', 'a___32', 'a___41', 'a___24', 'a___38', 'a___23', 'a___19', 'a___50', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___45', 'a___10', 'a___39', 'a___43', 'a___22', 'a___27', 'a___7', 'a___49', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___44', 'a___11', 'a___14', 'a___30', 'a___42', 'a___47', 'a___8', 'a___26', 'a___48', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']

then I use eval in the following way:

# Declare z3 variables for all strings in my list 'variables'
for x in variables:
    globals()[x] = z3.Bool(x)
# Create z3 object from string 'f'
z3f = eval(f)

and receive the error:

---------------------------------------------------------------------------
MemoryError                               Traceback (most recent call last)
<ipython-input-71-b7421db475e5> in <module>()
      3     globals()[x] = z3.Bool(x)
      4 # Create z3 object from string 'f'
----> 5 z3f = eval(f)

MemoryError:

For a similar but shorter f the code from above works fine. For example for:

f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,a___40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'
variables = ['a___2', 'a___31', 'a___34', 'a___29', 'a___12', 'a___9', 'a___32', 'a___24', 'a___38', 'a___23', 'a___19', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___10', 'a___39', 'a___22', 'a___27', 'a___7', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___11', 'a___14', 'a___30', 'a___8', 'a___26', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']

I receive:

z3f = Or(a___0,
And(True,
   Or(a___1,
      And(True,
          Or(a___2,
             And(True,
                 Or(a___3,
                    And(True,
                        Or(a___4,
                           And(True,
                               Or(a___5,
                                  And(True,
                                    Or(a___6,
                                    And(True,
                                    Or(a___7,
                                    And(True,
                                    Or(a___8,
                                    And(True,
                                    Or(a___9,
                                    And(True,
                                    Or(..., ...)))))))))))))))))))))

This question is very hard to answer without seeing the actual formulas you're trying to parse. Without that, I'd say you'd probably see similar issues with parse_smt2_string. However, since you get a MemoryError, the actual problem may be on the Python side of things just as well (Z3 never raises this type of exception by itself). — Christoph Wintersteiger
@ChristophWintersteiger I added an example for an actual formula I am trying to parse where a MemoryError is thrown. It might very well be the case that this is a problem of Python itself... — ec-m

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2017-01-05T15:04:37

Thanks for adding the example ec-m!

This is in fact a problem on the Python side of things. Python limits the stack for eval(...) very conservatively, apparently it can only handle 35 scopes in some versions (as claimed in Parser crashes for deeply nested list displays). A similar problem exists with deeply nested lambdas (see Python: nested lambdas — s_push: parser stack overflow Memory Error).

It will definitely be possible to avoid this type of problem by switching to Z3's parse_smt2_string, which allows much larger stacks.

Z3Py: Parsing expressions using eval or z3.parse_smt2_string

1 Answers