Commit 920e9ebb authored by Marek Chalupa's avatar Marek Chalupa
Browse files

bself: simplify generating relations 

Do not generate relations for pre-prestates, just check whether the
already generated relations for pre-state hold.
parent 5685f51d

slowbeast/bse/bself.py

+12 −6
Original line number Original line Diff line number Diff line
@@ -116,17 +116,23 @@ def overapprox_state(executor, s, E, target, L): 








def _overapprox_with_assumptions(E, L, S, executor, s, target):

def _overapprox_with_assumptions(E, L, S, executor, s, target):

    """

    Infer a set of relations that hold in S and over-approximate the set

    w.r.t. these relations.

    """

    create_set = executor.create_set

    # precise prestates of this state

    # precise prestates of this state

    prestates = executor._extend_one_step(L, S)

    R0 = set(get_var_relations([S.get_se_state()], prevsafe=target))

    R0 = set(get_var_relations([S.get_se_state()], prevsafe=target))

    if not R0:

        return

    yielded = False

    yielded = False

    prestates = executor._extend_one_step(L, S)

    if prestates:

    if prestates:

        for p in prestates:

        for p in prestates:

            # FIXME: instead of getting relations, we could just check whether the relation

            # check whether the relation from R0 holds in 'p'

            # FIXME: from R0 holds in 'p', it should be better, right?

            # R1 = set(get_var_relations([p], prevsafe=S))

            R1 = set(get_var_relations([p], prevsafe=S))

            P =  create_set(p)

            # For each assumption that we can infer, try to overapproximate the set

            rels =  [r0 for r0 in R0 if not intersection(P, r0).is_empty()]

            rels =  R1.intersection(R0)

            yielded |= bool(rels)

            yielded |= bool(rels)

            yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)

            yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)