#!/usr/bin/env python
import logging
l = logging.getLogger("claripy.frontends.constrained_frontend")
from ..frontend import Frontend
[docs]class ConstrainedFrontend(Frontend): # pylint:disable=abstract-method
[docs] def __init__(self):
Frontend.__init__(self)
self.constraints = []
self.variables = set()
self._finalized = False
def _blank_copy(self, c):
super()._blank_copy(c)
c.constraints = []
c.variables = set()
c._finalized = False
def _copy(self, c):
super()._copy(c)
c.constraints = list(self.constraints)
c.variables = set(self.variables)
# finalize both
self.finalize()
c.finalize()
#
# Serialization support
#
def __getstate__(self):
return self.constraints, self.variables, self._finalized, super().__getstate__()
def __setstate__(self, s):
self.constraints, self.variables, self._finalized, base_state = s
super().__setstate__(base_state)
#
# Constraint management
#
[docs] def independent_constraints(self):
return self._split_constraints(self.constraints)
#
# Serialization and such.
#
[docs] def downsize(self):
Frontend.downsize(self)
#
# Merging and splitting
#
[docs] def finalize(self):
self._finalized = True
[docs] def merge(self, others, merge_conditions, common_ancestor=None):
if common_ancestor is None:
merged = self.blank_copy()
options = []
for s, v in zip([self] + others, merge_conditions):
options.append(And(*([v] + s.constraints)))
merged.add([Or(*options)])
else:
merged = common_ancestor.branch()
merged.add([Or(*merge_conditions)])
return False, merged
[docs] def combine(self, others):
combined = self.blank_copy()
combined.add(self.constraints) # pylint:disable=E1101
for o in others:
combined.add(o.constraints)
return combined
[docs] def split(self):
results = []
l.debug("Splitting!")
for variables, c_list in self.independent_constraints():
l.debug("... got %d constraints with %d variables", len(c_list), len(variables))
s = self.blank_copy()
s.add(c_list)
results.append(s)
return results
#
# Light functionality
#
[docs] def add(self, constraints):
self.constraints += constraints
for c in constraints:
self.variables.update(c.variables)
return constraints
[docs] def simplify(self):
to_simplify = [
c
for c in self.constraints
if not any(isinstance(a, SimplificationAvoidanceAnnotation) for a in c.annotations)
]
no_simplify = [
c for c in self.constraints if any(isinstance(a, SimplificationAvoidanceAnnotation) for a in c.annotations)
]
if len(to_simplify) == 0:
return self.constraints
simplified = simplify(And(*to_simplify)).split(["And"]) # pylint:disable=no-member
self.constraints = no_simplify + simplified
return self.constraints
#
# Stuff that should be implemented by subclasses
#
[docs] def check_satisfiability(self, extra_constraints=(), exact=None):
raise NotImplementedError("check_satisfiable() is not implemented")
[docs] def satisfiable(self, extra_constraints=(), exact=None):
raise NotImplementedError("satisfiable() is not implemented")
[docs] def batch_eval(self, exprs, n, extra_constraints=(), exact=None):
raise NotImplementedError("batch_eval() is not implemented")
[docs] def eval(self, e, n, extra_constraints=(), exact=None):
raise NotImplementedError("eval() is not implemented")
[docs] def min(self, e, extra_constraints=(), signed=False, exact=None):
raise NotImplementedError("min() is not implemented")
[docs] def max(self, e, extra_constraints=(), signed=False, exact=None):
raise NotImplementedError("max() is not implemented")
[docs] def solution(self, e, v, extra_constraints=(), exact=None):
raise NotImplementedError("solution() is not implemented")
[docs] def is_true(self, e, extra_constraints=(), exact=None):
raise NotImplementedError("is_true() is not implemented")
[docs] def is_false(self, e, extra_constraints=(), exact=None):
raise NotImplementedError("is_false() is not implemented")
from ..ast.base import simplify
from ..ast.bool import And, Or
from ..annotation import SimplificationAvoidanceAnnotation