Various utilities (in particular, OrderedSet)

class Semantics(value)[source]

Semantics for inductive definitions


String constants

NOT_SATISFIABLE = 'Not satisfiable.'

Module that monkey-patches json module when it’s imported so JSONEncoder.default() automatically checks for a special “to_json()” method and uses it to encode the object if found.

exception IDPZ3Error[source]

raised whenever an error occurs in the conversion from AST to Z3

class OrderedSet(els=[])[source]

a list of expressions without duplicates (first-in is selected)


Initialize self. See help(type(self)) for accurate signature.

pop(k[, d])v, remove specified key and return the corresponding value.[source]

If key is not found, d is returned if given, otherwise KeyError is raised