RocketRace / easy_z3

Have you ever thought, "I really need a constraint solver right now" and remembered that the python wrapper for z3 (which is already very easy to use) is not easy enough to use? No? That's fine, I made this anyway.

Metaclasses defining custom namespaces and special syntax, inspect to traverse stack frames and mess with globals, and plenty of glue to patch together some reasonable API to z3.

A metaclass (type inheriting from type) can return any mapping-like object from its __prepare__ method, which will be used while executing the class body to access names within the class scope. For normal classes, this will be a dict. So in the following example, variable access is converted into dictionary access:

In the example, you notice that trying to access variables that aren't defined anywhere will raise a NameError. However, this is only the default behavior of the namespace! You can choose to ignore undefined variables totally when using a custom namespace, as long as you define the __getitem__ and __setitem__ methods used for reading & writing to the namespace. In fact, if the namespace is a subclass of dict, you can define a handy method __missing__ that is called specifically when an unbound name is trying to be accessed!

In this module, the custom namespace (aptly named NameSpace) behaves exactly as dict does, except when unbound value are accessed. (Note: the code is full of jank and inconsistency. Don't be surprised if what I say slightly misrepresents its hackiness.) In those cases, it returns a Variable object.

Leave a Comment