Skip to content

Constraint simplification #162

Description

@CatarinaGamboa

We need to improve the simplification of expressions with various variable instances.
We could try to do something similar to constant propagation, and to flattening variable derivation chains.

For example:
Image
Here I would want the most simplified version to be something like "b >= 100 && b + 100" is not a subtype of Byte(b). Then

We could try using constraint simplification via equivalence analysis, as an algorithm like:

  1. Find equivalences (in variables for this case)
  2. Pick canonical names - use vars from code and not internal vars if possible
  3. Substitute Equivalences - Simplify equivalences, remove duplicate checks
  4. Remove redundancies

In that example:

  1. Equivalences: {b, b_34, b_38}
  2. Use b
#b_39 == #b_38 + 100  →  #b_39 == b + 100
#b_38 == #b_34        →  (redundant, defines equivalence)
#b_34 >= 100b >= 100
b > 0b > 0
#b_34 > 0b > 0  (duplicate)
b == #b_34            →  (redundant, defines equivalence)

simplifies to
#b_39 == b + 100 && b >= 100 && b > 0
4) b > 100 -> b > 0 so we can drop the weaker constraint.

This is open for discussion!

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or requestsimplificationRelated to the simplification of expressions

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions