Fixpoint3.Phase.Simplifier
Definitions
def simplifyProgram(program: RamProgram): RamProgram
SourceOptimize and simplify stmt by deleting redundant code and reordering code.
Examples of redundancy include x[i] == x[i].
Reordering means (0, 1) ∉ Path ∧ x[1] = y[0] would be swapped x[1] = y[0] ∧ (0, 1) ∉ Path.
A simple static analysis also reveals that the following join-loop is redundant
in stratum j if C is computed in stratum i and i < j:
`
search x ∈ B do
search y ∈ ΔC do
if (x[0] == y[0] ∧ (x[0]) ∉ A ∧ (x[0]) ∉ R) then
project (x[0]) into ΔR'
end
end
end
`
The returned RAM program is always the same size or smaller.
def simplifyStmt(stmt: RamStmt, nonEmpty: Set[RelSym], predicates: Predicates): RamStmt
SourceSimplifies stmt by removing redundant code.
nonEmpty is the set of RelSym whose relation is non-empty.
Predicates is a structure for interacting with predicate symbols.