Solver: Implement sympy Simplifier

[bliutech]

We will be benchmarking two potential ways to simplify boolean statements for our solver. This next technique leverages the symbolic algebra library, sympy. The goal of this issue is to write an optimization pass for our solver to leverage which uses the sympy backend.

Action Items

• Create a file called solver/passes/sympy_pass.py. Follow the format shown in template_pass.py as this is the required format for our solver module.
• Write a visitor called SympyMappingVisitor whose job is to visit all nodes and when a Var is reached, the goal is to initialize a sympy.Symbol object which represents the Boolean symbol and add it to a dict[str, sympy.Symbol]. This will allow us to quickly reference the same boolean objects / symbols when we translate the AST into a sympy equation. This should inherit from the Visitor class. A similar example is shown in the template_pass.py file. For example, a mapping of A | B will have { "A" : Symbol("A"), "B" : Symbol("B") }.
• Write a visitor called TranslateToSympy which converts the AST to a sympy data structure. The goal of this is to represent the AST in a data structure that can be simplified by the sympy backend. For example, for A | B the data structure will be Or(Symbol("A"), Symbol("B"). There are a few ways to do it but one way is to inherit from RetVisitor and override all methods on the visitor to return part of the data structure. The visitVarRet should use the dictionary / mapping we created from the SympyMappingVisitor since we want to reuse the same instance of a variable rather than create a new instance every time. One quick note is that for identifying the And or Or, you may need to use isinstance Python function to see the the Expr node is an instance of an AndExpr or an OrExpr when trying to translate this inside the visit function for VarExpr. An example of on to use `RetVisitor is shown in this example pass.
• After building the equation, call the simplify_logic equation from the sympy library. There are some parameters you can play around with on this library so if you have time, try and see if we can maybe optimize further. An example of how to call this library is shown here.
• Get the string representation of the simplified boolean expression and use the Parser to build this back into an AST to be returned.

Here is the general flow of our pass.

# SympyMappingVisitor produces a mapping of the string representation of `Var`s to the `sympy.Symbol` instances
# TranslateToSympy produces the sympy representation of the boolean expression
# `simplify_logic` is called on the boolean expression to produced the simplified output.
# pass the string representation of the simplified output back into the `Parser` so we can return the simplified AST.

Resources

• https://github.com/sympy/sympy
• https://docs.sympy.org/latest/tutorials/intro-tutorial/simplification.html
• https://docs.sympy.org/latest/modules/logic.html

Check out example_pass.py. Some of the code structures are similar to what we are tackling here.

[bliutech]

As a quick aside, sympy looks like it uses SOP or POS as a strategy for simplification and picks the best one. There are some potential optimizations we can look into while simplifying to see if we can potentially take advantage of "don't cares" somewhere here.

https://docs.sympy.org/latest/modules/logic.html#simplification-and-equivalence-testing