Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 29 additions & 25 deletions dace/sdfg/performance_evaluation/assumptions.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@
import sympy as sp
from typing import Dict

from dace.symbolic import symbol


class UnionFind:
"""
Expand Down Expand Up @@ -112,7 +114,9 @@ def propagate_assumptions(x, y, condensed_assumptions):
condensed_assumptions[y] = Assumptions()
assum_y = condensed_assumptions[y]
for e in assum_x.equal:
if e is not sp.Symbol(y):
# Skip a self-reference (the symbol named ``y`` itself); compare by name because DaCe
# symbols, unlike sympy symbols, are not interned, so an ``is`` check would never match.
if not (isinstance(e, sp.Symbol) and e.name == y):
assum_y.add_equal(e)
for g in assum_x.greater:
assum_y.add_greater(g)
Expand Down Expand Up @@ -150,7 +154,7 @@ def propagate_assumptions_equal_symbols(condensed_assumptions):
for other in condensed_assumptions[sym].equal:
if isinstance(other, sp.Symbol):
propagate_assumptions(sym, uf.find(sym), condensed_assumptions)
equality_subs1.update({sym: sp.Symbol(uf.find(sym))})
equality_subs1.update({sym: symbol(uf.find(sym))})

equality_subs2 = {}
# In a second step, each symbol gets replaced with its equal number (if present)
Expand Down Expand Up @@ -221,37 +225,37 @@ def parse_assumptions(assumptions, array_symbols):
condensed_assumptions: Dict[str, Assumptions] = {}
for a in assumptions:
if '==' in a:
symbol, rhs = a.split('==')
if symbol not in condensed_assumptions:
condensed_assumptions[symbol] = Assumptions()
lhs, rhs = a.split('==')
if lhs not in condensed_assumptions:
condensed_assumptions[lhs] = Assumptions()
try:
condensed_assumptions[symbol].add_equal(int(rhs))
condensed_assumptions[lhs].add_equal(int(rhs))
except ValueError:
condensed_assumptions[symbol].add_equal(sp.Symbol(rhs))
condensed_assumptions[lhs].add_equal(symbol(rhs))
elif '>' in a:
symbol, rhs = a.split('>')
if symbol not in condensed_assumptions:
condensed_assumptions[symbol] = Assumptions()
lhs, rhs = a.split('>')
if lhs not in condensed_assumptions:
condensed_assumptions[lhs] = Assumptions()
try:
condensed_assumptions[symbol].add_greater(int(rhs))
condensed_assumptions[lhs].add_greater(int(rhs))
except ValueError:
condensed_assumptions[symbol].add_greater(sp.Symbol(rhs))
condensed_assumptions[lhs].add_greater(symbol(rhs))
# add the opposite, i.e. for x>y, we add y<x
if rhs not in condensed_assumptions:
condensed_assumptions[rhs] = Assumptions()
condensed_assumptions[rhs].add_lesser(sp.Symbol(symbol))
condensed_assumptions[rhs].add_lesser(symbol(lhs))
elif '<' in a:
symbol, rhs = a.split('<')
if symbol not in condensed_assumptions:
condensed_assumptions[symbol] = Assumptions()
lhs, rhs = a.split('<')
if lhs not in condensed_assumptions:
condensed_assumptions[lhs] = Assumptions()
try:
condensed_assumptions[symbol].add_lesser(int(rhs))
condensed_assumptions[lhs].add_lesser(int(rhs))
except ValueError:
condensed_assumptions[symbol].add_lesser(sp.Symbol(rhs))
condensed_assumptions[lhs].add_lesser(symbol(rhs))
# add the opposite, i.e. for x<y, we add y>x
if rhs not in condensed_assumptions:
condensed_assumptions[rhs] = Assumptions()
condensed_assumptions[rhs].add_greater(sp.Symbol(symbol))
condensed_assumptions[rhs].add_greater(symbol(lhs))

# Handle equal assumptions.
equality_subs = propagate_assumptions_equal_symbols(condensed_assumptions)
Expand All @@ -272,14 +276,14 @@ def parse_assumptions(assumptions, array_symbols):
for sym, assum in condensed_assumptions.items():
i = 0
for g in assum.greater:
replacement_symbol = sp.Symbol(f'_p_{sym}', positive=True, integer=True)
all_subs[i][0].update({sp.Symbol(sym): replacement_symbol + g})
all_subs[i][1].update({replacement_symbol: sp.Symbol(sym) - g})
replacement_symbol = symbol(f'_p_{sym}', nonnegative=True)
all_subs[i][0].update({symbol(sym): replacement_symbol + g})
all_subs[i][1].update({replacement_symbol: symbol(sym) - g})
i += 1
for l in assum.lesser:
replacement_symbol = sp.Symbol(f'_n_{sym}', negative=True, integer=True)
all_subs[i][0].update({sp.Symbol(sym): replacement_symbol + l})
all_subs[i][1].update({replacement_symbol: sp.Symbol(sym) - l})
replacement_symbol = symbol(f'_n_{sym}', negative=True)
all_subs[i][0].update({symbol(sym): replacement_symbol + l})
all_subs[i][1].update({replacement_symbol: symbol(sym) - l})
i += 1

return equality_subs, all_subs
Loading