Skip to content

implement domain propagation #1

@giucamp

Description

@giucamp
  • Domains
  • Domain Propagation
  • Constant propagation

Domains
A (scalar) range is composed by a lower bound, an upper bound, and two flags specifying whether bounds are inclusive or not.
Invariant: ranges are always canonicalized, that is: lower bound <= upper bound.

A domain is a union of ranges, stored in a vector.
Invariant: domains are always canonicalized, that is ranges are sorted and cannot overlap.

example of domain:
real x where 1 < x <= 2 || 4 <= x < 7
(two separated finite ranges)

real x where -inf <= x < 0 || 0 < x= < inf
(all numbers but 0)

Both Range and Domain should support

  • domain-domain and scalar-domain union (with the operator |)
  • domain-domain and scalar-domain intersection (with the operator &)
  • bound transformation (a functor that is applied to all bounds)
  • explicit cast to bool that returns whether the source is the empty set

Domain Propagation
An expression can have a domain. All the scalars of the expression lie in the domain (in miu6 this is a corollary)

Every operator defines its way to compute a domain based on the domains of operands. For example:

corollary: Domain(x + y where 0 <= x <= 1 && 0 <= y <= 1) == (0 <= x + y <= 2)

the operator Domain returns the domain as bool expression.

Constant propagation
Operators can exploit the range of operands during constant propagation. For example :
x < 0 where x > 6
evaluates to:
false

Operators may trigger a panic whenever the range of an operand includes singularities.
For example:
Log(real x) where x > -1
should panic.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions