How to use the pysat.solvers.SolverNames function in pysat

:type clause: iterable(int)
            :type soft: bool
        """

        # first, map external literals to internal literals
        # introduce new variables if necessary
        cl = list(map(lambda l: self._map_extlit(l), clause if not len(clause) == 2 or not type(clause[0]) == list else clause[0]))

        if not soft:
            if not len(clause) == 2 or not type(clause[0]) == list:
                # the clause is hard, and so we simply add it to the SAT oracle
                self.oracle.add_clause(cl)
            else:
                # this should be a native cardinality constraint,
                # which can be used only together with Minicard
                assert self.solver in SolverNames.minicard, \
                        'Only Minicard supports native cardinality constraints.'

                self.oracle.add_atmost(cl, clause[1])
        else:
            self.soft.append(cl)

            # soft clauses should be augmented with a selector
            sel = cl[0]
            if len(cl) > 1 or cl[0] < 0:
                self.topv += 1
                sel = self.topv

                self.oracle.add_clause(cl + [-sel])

            self.sels.append(sel)

...     print(rc2.cost)
                2
        """

        # first, map external literals to internal literals
        # introduce new variables if necessary
        cl = list(map(lambda l: self._map_extlit(l), clause if not len(clause) == 2 or not type(clause[0]) == list else clause[0]))

        if not weight:
            if not len(clause) == 2 or not type(clause[0]) == list:
                # the clause is hard, and so we simply add it to the SAT oracle
                self.oracle.add_clause(cl)
            else:
                # this should be a native cardinality constraint,
                # which can be used only together with Minicard
                assert self.solver in SolverNames.minicard, \
                        'Only Minicard supports native cardinality constraints.'

                self.oracle.add_atmost(cl, clause[1])
        else:
            # soft clauses should be augmented with a selector
            selv = cl[0]  # for a unit clause, no selector is needed

            if len(cl) > 1:
                self.topv += 1
                selv = self.topv

                self.s2cl[selv] = cl[:]
                cl.append(-self.topv)
                self.oracle.add_clause(cl)

            if selv not in self.wght:

def init(self, with_soft=True):
        """
            The method for the SAT oracle initialization. Since the oracle is
            is used non-incrementally, it is reinitialized at every iteration
            of the MaxSAT algorithm (see :func:`reinit`). An input parameter
            ``with_soft`` (``False`` by default) regulates whether or not the
            formula's soft clauses are copied to the oracle.

            :param with_soft: copy formula's soft clauses to the oracle or not
            :type with_soft: bool
        """

        self.oracle = Solver(name=self.solver, bootstrap_with=self.hard, use_timer=True)

        if self.atm1:  # this check is needed at the beggining (before iteration 1)
            assert self.solver in SolverNames.minicard, \
                    'Only Minicard supports native cardinality constraints. Make sure you use the right type of formula.'

            # self.atm1 is not empty only in case of minicard
            for am in self.atm1:
                self.oracle.add_atmost(*am)

        if with_soft:
            for cl, cpy in zip(self.soft, self.scpy):
                if cpy:
                    self.oracle.add_clause(cl)

if opt in ('-c', '--cardenc'):
            cardenc = str(arg)
        elif opt in ('-h', '--help'):
            usage()
            sys.exit(0)
        elif opt in ('-s', '--solver'):
            solver = str(arg)
        elif opt in ('-v', '--verbose'):
            verbose += 1
        else:
            assert False, 'Unhandled option: {0} {1}'.format(opt, arg)

    cardenc = encmap[cardenc]

    # using minicard's native implementation of AtMost1 constraints
    if solver in SolverNames.minicard:
        cardenc = encmap['native']
    else:
        assert cardenc != encmap['native'], 'Only Minicard can handle cardinality constraints natively'

    return solver, cardenc, verbose, args

self.solver = Glucose3(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose4:
                self.solver = Glucose4(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.lingeling:
                self.solver = Lingeling(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplechrono:
                self.solver = MapleChrono(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplecm:
                self.solver = MapleCM(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplesat:
                self.solver = Maplesat(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.minicard:
                self.solver = Minicard(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisat22:
                self.solver = Minisat22(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisatgh:
                self.solver = MinisatGH(bootstrap_with, use_timer)
            else:
                raise(NoSuchSolverError(name))

:raises NoSuchSolverError: if there is no solver matching the given
                name.
        """

        # checking keyword arguments
        kwallowed = set(['incr', 'with_proof'])
        for a in kwargs:
            if a not in kwallowed:
                raise TypeError('Unexpected keyword argument \'{0}\''.format(a))

        if not self.solver:
            name_ = name.lower()
            if name_ in SolverNames.cadical:
                self.solver = Cadical(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose3:
                self.solver = Glucose3(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose4:
                self.solver = Glucose4(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.lingeling:
                self.solver = Lingeling(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplechrono:
                self.solver = MapleChrono(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplecm:
                self.solver = MapleCM(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplesat:
                self.solver = Maplesat(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.minicard:
                self.solver = Minicard(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisat22:
                self.solver = Minisat22(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisatgh:

:param formula: input formula
            :param incr: apply incremental mode of Glucose

            :type formula: :class:`.WCNF`
            :type incr: bool
        """

        # creating a solver object
        self.oracle = Solver(name=self.solver, bootstrap_with=formula.hard,
                incr=incr, use_timer=True)

        # adding native cardinality constraints (if any) as hard clauses
        # this can be done only if the Minicard solver is in use
        # this cannot be done if RC2 is run from the command line
        if isinstance(formula, WCNFPlus) and formula.atms:
            assert self.solver in SolverNames.minicard, \
                    'Only Minicard supports native cardinality constraints. Make sure you use the right type of formula.'

            for atm in formula.atms:
                self.oracle.add_atmost(*atm)

        # adding soft clauses to oracle
        for i, cl in enumerate(formula.soft):
            selv = cl[0]  # if clause is unit, selector variable is its literal

            if len(cl) > 1:
                self.topv += 1
                selv = self.topv

                self.s2cl[selv] = cl[:]
                cl.append(-self.topv)
                self.oracle.add_clause(cl)

if a not in kwallowed:
                raise TypeError('Unexpected keyword argument \'{0}\''.format(a))

        if not self.solver:
            name_ = name.lower()
            if name_ in SolverNames.cadical:
                self.solver = Cadical(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose3:
                self.solver = Glucose3(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose4:
                self.solver = Glucose4(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.lingeling:
                self.solver = Lingeling(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplechrono:
                self.solver = MapleChrono(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplecm:
                self.solver = MapleCM(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplesat:
                self.solver = Maplesat(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.minicard:
                self.solver = Minicard(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisat22:
                self.solver = Minisat22(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisatgh:
                self.solver = MinisatGH(bootstrap_with, use_timer)
            else:
                raise(NoSuchSolverError(name))

if not self.solver:
            name_ = name.lower()
            if name_ in SolverNames.cadical:
                self.solver = Cadical(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose3:
                self.solver = Glucose3(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose4:
                self.solver = Glucose4(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.lingeling:
                self.solver = Lingeling(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplechrono:
                self.solver = MapleChrono(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplecm:
                self.solver = MapleCM(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplesat:
                self.solver = Maplesat(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.minicard:
                self.solver = Minicard(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisat22:
                self.solver = Minisat22(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisatgh:
                self.solver = MinisatGH(bootstrap_with, use_timer)
            else:
                raise(NoSuchSolverError(name))

name_ = name.lower()
            if name_ in SolverNames.cadical:
                self.solver = Cadical(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose3:
                self.solver = Glucose3(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.glucose4:
                self.solver = Glucose4(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.lingeling:
                self.solver = Lingeling(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplechrono:
                self.solver = MapleChrono(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplecm:
                self.solver = MapleCM(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.maplesat:
                self.solver = Maplesat(bootstrap_with, use_timer, **kwargs)
            elif name_ in SolverNames.minicard:
                self.solver = Minicard(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisat22:
                self.solver = Minisat22(bootstrap_with, use_timer)
            elif name_ in SolverNames.minisatgh:
                self.solver = MinisatGH(bootstrap_with, use_timer)
            else:
                raise(NoSuchSolverError(name))