Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clean up Symbolic #42

Open
CactusWin opened this issue Aug 23, 2022 · 2 comments
Open

Clean up Symbolic #42

CactusWin opened this issue Aug 23, 2022 · 2 comments
Assignees

Comments

@CactusWin
Copy link
Collaborator

CactusWin commented Aug 23, 2022

Main components of Symbolic

  • Expression
  • Interpreter
  • Eliminator
  • Normalization
  • Interval

Expression

  • Make sure the ordering of the functions are the same within the classes
  • Are the specific error classes still necessary? Can we reuse the ones that python already has? Should we add an error message to these classes if we want to keep them?

Interpreter

Evaluates and simplifies the function

  • Should we rename this to evaluator? I think the naming is a little confusing, since the word "interpreter" has difference meanings

Eliminator

Eliminates the quantifier expression

  • Add doc string to explain what is happening (move the doc string from normalizer into eliminator)

Normalization

Rename GeneralNormalizer and QuantifierFreeNormalizer

  • GeneralNormalizer currently pushes the integral down into the leaves of a piecewise function. This does it lazily (and we also have another normalizer called LazyNormalizer. It also does not push down the add.

  • QuantifierFreeNormalizer does it eagerly. It pushes down the add and the integral, and you have to renormalize after you normalize the leaf/ subsection of the tree

  • Delete LazyNormalizer

Interval

[max(lower_bounds), min(upper_bound)] => Also need to normalize the interval => min and max is technically also a piecewise

  • Refine Intervals
  • Combine in MagicInterval into the normal Interval class

Docstring

Some docstrings are outdated

  • Add docstrings for EquivalenceClass and OrderedZ3Expression in z3_expression

Profiler

  • Look into python profiling tools

Typing

  • Think of names to help with docstrings => min max aren't integrable fast

Linting

  • Lint all the files for clean code
@CactusWin CactusWin self-assigned this Aug 23, 2022
@CactusWin
Copy link
Collaborator Author

@hsiang-wu and I went through the code for future steps I should take after he leaves

@CactusWin
Copy link
Collaborator Author

CactusWin commented Aug 26, 2022

Expression clean up: #43
Interpreter clean up: #49

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant