(self)
return self._stored_solver
Creates or gets a Claripy solver, based on the state options.
Creates or gets a Claripy solver, based on the state options.
Creates or gets a Claripy solver based on the state options .
def _solver(self):
        """
        Creates or gets a Claripy solver, based on the state options.
        """
        if self._stored_solver is not None:
            return self._stored_solver

        track = o.CONSTRAINT_TRACKING_IN_SOLVER in self.state.options
        approximate_first = o.APPROXIMATE_FIRST in self.state.options

        if o.STRINGS_ANALYSIS in self.state.options:
            if 'smtlib_cvc4' in backend_manager.backends._backends_by_name:
                our_backend = backend_manager.backends.smtlib_cvc4
            elif 'smtlib_z3' in backend_manager.backends._backends_by_name:
                our_backend = backend_manager.backends.smtlib_z3
            elif 'smtlib_abc' in backend_manager.backends._backends_by_name:
                our_backend = backend_manager.backends.smtlib_abc
            else:
                l.error("Cannot find a suitable string solver. Please ensure you have installed a string solver that "
                        "angr supports, and have imported the corresponding solver backend in claripy. You can try "
                        "adding \"from claripy.backends.backend_smtlib_solvers import *\" at the beginning of your "
                        "script.")
                raise ValueError("Cannot find a suitable string solver")
            if o.COMPOSITE_SOLVER in self.state.options:
                self._stored_solver = claripy.SolverComposite(
                    template_solver_string=claripy.SolverCompositeChild(backend=our_backend, track=track)
                )
        elif o.ABSTRACT_SOLVER in self.state.options:
            self._stored_solver = claripy.SolverVSA()
        elif o.SYMBOLIC in self.state.options and o.REPLACEMENT_SOLVER in self.state.options:
            self._stored_solver = claripy.SolverReplacement(auto_replace=False)
        elif o.SYMBOLIC in self.state.options and o.CACHELESS_SOLVER in self.state.options:
            self._stored_solver = claripy.SolverCacheless(track=track)
        elif o.SYMBOLIC in self.state.options and o.COMPOSITE_SOLVER in self.state.options:
            self._stored_solver = claripy.SolverComposite(track=track)
        elif o.SYMBOLIC in self.state.options and any(opt in self.state.options for opt in o.approximation):
            self._stored_solver = claripy.SolverHybrid(track=track, approximate_first=approximate_first)
        elif o.HYBRID_SOLVER in self.state.options:
            self._stored_solver = claripy.SolverHybrid(track=track, approximate_first=approximate_first)
        elif o.SYMBOLIC in self.state.options:
            self._stored_solver = claripy.Solver(track=track)
        else:
            self._stored_solver = claripy.SolverConcrete()

        return self._stored_solver
def _solver ( self ) : if self . _stored_solver is not None : return self . _stored_solver track = o . CONSTRAINT_TRACKING_IN_SOLVER in self . state . options approximate_first = o . APPROXIMATE_FIRST in self . state . options if o . STRINGS_ANALYSIS in self . state . options : if 'smtlib_cvc4' in backend_manager . backends . _backends_by_name : our_backend = backend_manager . backends . smtlib_cvc4 elif 'smtlib_z3' in backend_manager . backends . _backends_by_name : our_backend = backend_manager . backends . smtlib_z3 elif 'smtlib_abc' in backend_manager . backends . _backends_by_name : our_backend = backend_manager . backends . smtlib_abc else : l . error ( "Cannot find a suitable string solver. Please ensure you have installed a string solver that " "angr supports, and have imported the corresponding solver backend in claripy. You can try " "adding \"from claripy.backends.backend_smtlib_solvers import *\" at the beginning of your " "script." ) raise ValueError ( "Cannot find a suitable string solver" ) if o . COMPOSITE_SOLVER in self . state . options : self . _stored_solver = claripy . SolverComposite ( template_solver_string = claripy . SolverCompositeChild ( backend = our_backend , track = track ) ) elif o . ABSTRACT_SOLVER in self . state . options : self . _stored_solver = claripy . SolverVSA ( ) elif o . SYMBOLIC in self . state . options and o . REPLACEMENT_SOLVER in self . state . options : self . _stored_solver = claripy . SolverReplacement ( auto_replace = False ) elif o . SYMBOLIC in self . state . options and o . CACHELESS_SOLVER in self . state . options : self . _stored_solver = claripy . SolverCacheless ( track = track ) elif o . SYMBOLIC in self . state . options and o . COMPOSITE_SOLVER in self . state . options : self . _stored_solver = claripy . SolverComposite ( track = track ) elif o . SYMBOLIC in self . state . options and any ( opt in self . state . options for opt in o . approximation ) : self . _stored_solver = claripy . SolverHybrid ( track = track , approximate_first = approximate_first ) elif o . HYBRID_SOLVER in self . state . options : self . _stored_solver = claripy . SolverHybrid ( track = track , approximate_first = approximate_first ) elif o . SYMBOLIC in self . state . options : self . _stored_solver = claripy . Solver ( track = track ) else : self . _stored_solver = claripy . SolverConcrete ( ) return self . _stored_solver