1from . import frontend_mixins
2from . import frontends
3from . import backends
4
5class Solver(
6    frontend_mixins.ConstraintFixerMixin,
7    frontend_mixins.ConcreteHandlerMixin,
8    frontend_mixins.EagerResolutionMixin,
9    frontend_mixins.ConstraintFilterMixin,
10    frontend_mixins.ConstraintDeduplicatorMixin,
11    frontend_mixins.SimplifySkipperMixin,
12    frontend_mixins.SatCacheMixin,
13    frontend_mixins.ModelCacheMixin,
14    frontend_mixins.ConstraintExpansionMixin,
15    frontend_mixins.SimplifyHelperMixin,
16    frontends.FullFrontend
17):
18    def __init__(self, backend=backends.z3, **kwargs):
19        super(Solver, self).__init__(backend, **kwargs)
20
21class SolverCacheless(
22    frontend_mixins.ConstraintFixerMixin,
23    frontend_mixins.ConcreteHandlerMixin,
24    frontend_mixins.EagerResolutionMixin,
25    frontend_mixins.ConstraintFilterMixin,
26    frontend_mixins.ConstraintDeduplicatorMixin,
27    frontend_mixins.SimplifySkipperMixin,
28    frontends.FullFrontend
29):
30    def __init__(self, backend=backends.z3, **kwargs):
31        super(SolverCacheless, self).__init__(backend, **kwargs)
32
33class SolverReplacement(
34    frontend_mixins.ConstraintFixerMixin,
35    frontend_mixins.ConcreteHandlerMixin,
36    frontend_mixins.ConstraintDeduplicatorMixin,
37    frontends.ReplacementFrontend
38):
39    def __init__(self, actual_frontend=None, **kwargs):
40        actual_frontend = Solver() if actual_frontend is None else actual_frontend
41        super(SolverReplacement, self).__init__(actual_frontend, **kwargs)
42
43class SolverHybrid(
44    frontend_mixins.ConstraintFixerMixin,
45    frontend_mixins.ConcreteHandlerMixin,
46    frontend_mixins.EagerResolutionMixin,
47    frontend_mixins.ConstraintFilterMixin,
48    frontend_mixins.ConstraintDeduplicatorMixin,
49    frontend_mixins.SimplifySkipperMixin,
50    # TODO: frontend_mixins.ConstraintExpansionMixin,
51    frontends.HybridFrontend
52):
53    def __init__(
54        self, exact_frontend=None, approximate_frontend=None,
55        complex_auto_replace=True, replace_constraints=True,
56        track=False, approximate_first=False,
57        **kwargs
58    ):
59        exact_frontend = Solver(track=track) if exact_frontend is None else exact_frontend
60        approximate_frontend = SolverReplacement(
61            actual_frontend=SolverVSA(),
62            complex_auto_replace=complex_auto_replace, replace_constraints=replace_constraints,
63        ) if approximate_frontend is None else approximate_frontend
64        super(SolverHybrid, self).__init__(
65            exact_frontend, approximate_frontend, approximate_first=approximate_first, **kwargs
66        )
67
68class SolverVSA(
69    frontend_mixins.ConstraintFixerMixin,
70    frontend_mixins.ConcreteHandlerMixin,
71    frontend_mixins.ConstraintFilterMixin,
72    frontends.LightFrontend
73):
74    def __init__(self, **kwargs):
75        super(SolverVSA, self).__init__(backends.vsa, **kwargs)
76
77class SolverConcrete(
78    frontend_mixins.ConstraintFixerMixin,
79    frontend_mixins.ConcreteHandlerMixin,
80    frontend_mixins.ConstraintFilterMixin,
81    frontends.LightFrontend
82):
83    def __init__(self, **kwargs):
84        super(SolverConcrete, self).__init__(backends.concrete, **kwargs)
85
86class SolverStrings(
87    # TODO: Figure ot if we need to use all these mixins
88    frontend_mixins.ConstraintFixerMixin,
89    frontend_mixins.ConcreteHandlerMixin,
90    frontend_mixins.ConstraintFilterMixin,
91    frontend_mixins.ConstraintDeduplicatorMixin,
92    frontend_mixins.EagerResolutionMixin,
93    frontend_mixins.EvalStringsToASTsMixin,
94    frontend_mixins.SMTLibScriptDumperMixin,
95    frontends.FullFrontend,
96):
97    def __init__(self, backend, *args, **kwargs):
98        super(SolverStrings, self).__init__(backend, *args, **kwargs)
99
100#
101# Composite solving
102#
103
104class SolverCompositeChild(
105    frontend_mixins.ConstraintDeduplicatorMixin,
106    frontend_mixins.SatCacheMixin,
107    frontend_mixins.SimplifySkipperMixin,
108    frontend_mixins.ModelCacheMixin,
109    frontends.FullFrontend
110):
111    def __init__(self, backend=backends.z3, **kwargs):
112        super(SolverCompositeChild, self).__init__(backend, **kwargs)
113
114    def __repr__(self):
115        return "<SolverCompositeChild with %d variables>" % len(self.variables)
116
117class SolverComposite(
118    frontend_mixins.ConstraintFixerMixin,
119    frontend_mixins.ConcreteHandlerMixin,
120    frontend_mixins.EagerResolutionMixin,
121    frontend_mixins.ConstraintFilterMixin,
122    frontend_mixins.ConstraintDeduplicatorMixin,
123    frontend_mixins.SatCacheMixin,
124    frontend_mixins.SimplifySkipperMixin,
125    frontend_mixins.SimplifyHelperMixin,
126    frontend_mixins.ConstraintExpansionMixin,
127    frontend_mixins.CompositedCacheMixin,
128    frontends.CompositeFrontend
129):
130    def __init__(self, template_solver=None, track=False, template_solver_string=None, **kwargs):
131        template_solver = SolverCompositeChild(track=track) if template_solver is None else template_solver
132        template_solver_string = SolverCompositeChild(track=track, backend=backends.z3) if \
133            template_solver_string is None else template_solver_string
134        super(SolverComposite, self).__init__(template_solver, template_solver_string, track=track, **kwargs)
135
136    def __repr__(self):
137        return "<SolverComposite %x, %d children>" % (id(self), len(self._solver_list))
138