Skip to content

Clean up Symbolic #42

@CactusWin

Description

@CactusWin

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

Metadata

Metadata

Assignees

Labels

No labels
No labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions