Skip to content

Commit

Permalink
Move _split_constraints utility method to ConstrainedFrontend where i…
Browse files Browse the repository at this point in the history
…t is used (#465)

* Move _split_constraints utility method to ConstrainedFrontend where it is used

* Improve lint
  • Loading branch information
twizmwazin authored Sep 2, 2024
1 parent 29b31e9 commit 837b904
Show file tree
Hide file tree
Showing 3 changed files with 55 additions and 53 deletions.
50 changes: 0 additions & 50 deletions claripy/frontend.py
Original file line number Diff line number Diff line change
Expand Up @@ -240,53 +240,3 @@ def _concrete_value(self, e): # pylint:disable=no-self-use

def _concrete_constraint(self, e): # pylint:disable=no-self-use
return self._concrete_value(e)

def _constraint_filter(self, c): # pylint:disable=no-self-use
return c

@staticmethod
def _split_constraints(constraints, concrete=True):
"""
Returns independent constraints, split from this Frontend's `constraints`.
"""

splitted = []
for i in constraints:
splitted.extend(i.split(["And"]))

l.debug("... splitted of size %d", len(splitted))

concrete_constraints = []
variable_connections = {}
constraint_connections = {}
for n, s in enumerate(splitted):
l.debug("... processing constraint with %d variables", len(s.variables))

connected_variables = set(s.variables)
connected_constraints = {n}

if len(connected_variables) == 0:
concrete_constraints.append(s)

for v in s.variables:
if v in variable_connections:
connected_variables |= variable_connections[v]
if v in constraint_connections:
connected_constraints |= constraint_connections[v]

for v in connected_variables:
variable_connections[v] = connected_variables
constraint_connections[v] = connected_constraints

unique_constraint_sets = set()
for v in variable_connections:
unique_constraint_sets.add((frozenset(variable_connections[v]), frozenset(constraint_connections[v])))

results = []
for v, c_indexes in unique_constraint_sets:
results.append((set(v), [splitted[c] for c in c_indexes]))

if concrete and len(concrete_constraints) > 0:
results.append(({"CONCRETE"}, concrete_constraints))

return results
3 changes: 1 addition & 2 deletions claripy/frontend_mixins/constraint_filter_mixin.py
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,7 @@ def _constraint_filter(self, constraints):
if len(constraints) == 0:
return constraints

filtered = super()._constraint_filter(constraints)
ccs = [self._concrete_constraint(c) for c in filtered]
ccs = [self._concrete_constraint(c) for c in constraints]
if False in ccs:
raise UnsatError("Constraints contain False.")
return tuple((o if n is None else o) for o, n in zip(constraints, ccs, strict=False) if n is not True)
Expand Down
55 changes: 54 additions & 1 deletion claripy/frontends/constrained_frontend.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,9 @@
l = logging.getLogger("claripy.frontends.constrained_frontend")


class ConstrainedFrontend(Frontend): # pylint:disable=abstract-method
class ConstrainedFrontend(Frontend):
"""ConstrainedFrontend is a base class for all frontends that support constraints."""

def __init__(self):
Frontend.__init__(self)
self.constraints = []
Expand Down Expand Up @@ -153,3 +155,54 @@ def is_true(self, e, extra_constraints=(), exact=None):

def is_false(self, e, extra_constraints=(), exact=None):
raise NotImplementedError("is_false() is not implemented")

#
# Some utility functions
#

@staticmethod
def _split_constraints(constraints, concrete=True):
"""
Returns independent constraints, split from this Frontend's `constraints`.
"""

splitted = []
for i in constraints:
splitted.extend(i.split(["And"]))

l.debug("... splitted of size %d", len(splitted))

concrete_constraints = []
variable_connections = {}
constraint_connections = {}
for n, s in enumerate(splitted):
l.debug("... processing constraint with %d variables", len(s.variables))

connected_variables = set(s.variables)
connected_constraints = {n}

if len(connected_variables) == 0:
concrete_constraints.append(s)

for v in s.variables:
if v in variable_connections:
connected_variables |= variable_connections[v]
if v in constraint_connections:
connected_constraints |= constraint_connections[v]

for v in connected_variables:
variable_connections[v] = connected_variables
constraint_connections[v] = connected_constraints

unique_constraint_sets = set()
for v, c in variable_connections.items():
unique_constraint_sets.add((frozenset(c), frozenset(constraint_connections[v])))

results = []
for v, c_indexes in unique_constraint_sets:
results.append((set(v), [splitted[c] for c in c_indexes]))

if concrete and len(concrete_constraints) > 0:
results.append(({"CONCRETE"}, concrete_constraints))

return results

0 comments on commit 837b904

Please sign in to comment.