<commit_before>#
# This file is part of pySMT.
#
#   Copyright 2014 <NAME> and <NAME>
#
#   Licensed under the Apache License, Version 2.0 (the "License");
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#       http://www.apache.org/licenses/LICENSE-2.0
#
#   Unless required by applicable law or agreed to in writing, software
#   distributed under the License is distributed on an "AS IS" BASIS,
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#   limitations under the License.
#
"""Factories are used to build new Solvers or Quantifier Eliminators
without the need of specifying them. For example, the user can simply
require a Solver that is able to deal with quantified theories, and
the factory will return one such solver among the available ones.
This makes it possible to write algorithms that do not depend on a
particular solver.
"""

from functools import partial
from six import iteritems

from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
                              NoLogicAvailableError)
from pysmt.logics import QF_UFLIRA, LRA
from pysmt.logics import AUTO as AUTO_LOGIC
from pysmt.logics import most_generic_logic, get_closer_logic
from pysmt.oracles import get_logic

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'picosat', 'bdd']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
DEFAULT_LOGIC = QF_UFLIRA
DEFAULT_QE_LOGIC = LRA

class Factory(object):

    def __init__(self, environment,
                 solver_preference_list=None,
                 qelim_preference_list=None):
        self.environment = environment
        self._all_solvers = None
        self._all_unsat_core_solvers = None
        self._all_qelims = None
        self._generic_solvers = {}

        if solver_preference_list is None:
            solver_preference_list = DEFAULT_SOLVER_PREFERENCE_LIST
        self.solver_preference_list = solver_preference_list

        if qelim_preference_list is None:
            qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
        self.qelim_preference_list = qelim_preference_list
        self._default_logic = DEFAULT_LOGIC
        self._default_qe_logic = DEFAULT_QE_LOGIC

        self._get_available_solvers()
        self._get_available_qe()


    def get_solver(self, quantified=False, name=None, logic=None):
        assert quantified is False or logic is None, \
            "Cannot specify both quantified and logic."

        if quantified is True:
            logic = self.default_logic.get_quantified_version

        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_solvers,
                                  solver_type="Solver",
                                  preference_list=self.solver_preference_list,
                                  default_logic=self.default_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic,
                           user_options={"generate_models" : True})


    def get_unsat_core_solver(self, quantified=False, name=None,
                              logic=None, unsat_cores_mode="all"):
        assert quantified is False or logic is None, \
            "Cannot specify both quantified and logic."

        if quantified is True:
            logic = self.default_logic.get_quantified_version

        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_unsat_core_solvers,
                                  solver_type="Solver supporting Unsat Cores",
                                  preference_list=self.solver_preference_list,
                                  default_logic=self.default_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic,
                           user_options={"generate_models" : True,
                                         "unsat_cores_mode" : unsat_cores_mode})


    def get_quantifier_eliminator(self, name=None, logic=None):
        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_qelims,
                                  solver_type="Quantifier Eliminator",
                                  preference_list=self.qelim_preference_list,
                                  default_logic=self.default_qe_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic)


    def _get_solver_class(self, solver_list, solver_type, preference_list,
                          default_logic, name=None, logic=None):
        if len(solver_list) == 0:
            raise NoSolverAvailableError("No %s is available" % solver_type)

        if name is not None:
            if name not in solver_list:
                raise NoSolverAvailableError("%s '%s' is not available" % \
                                             (solver_type, name))

            if logic is not None and \
               name not in self._filter_solvers(solver_list, logic=logic):
                raise NoSolverAvailableError("%s '%s' does not support logic %s"%
                                             (solver_type, name, logic))

            SolverClass = solver_list[name]
            try:
                logic = most_generic_logic(SolverClass.LOGICS)
            except NoLogicAvailableError:
                logic = SolverClass.LOGICS[0]

            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)

            return SolverClass, closer_logic

        if logic is None:
            logic = default_logic

        solvers = self._filter_solvers(solver_list, logic=logic)

        if solvers is not None and len(solvers) > 0:
            # Pick the first solver based on preference list
            SolverClass = self._pick_favorite(preference_list, solver_list, solvers)
            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
            return SolverClass, closer_logic

        else:
            raise NoSolverAvailableError("No %s is available for logic %s" %
                                         (solver_type, logic))
<commit_msg>Added support for using default logic if the solver (or quantifier eliminator) does not have a most generic logic<commit_after>#
# This file is part of pySMT.
#
#   Copyright 2014 <NAME> and <NAME>
#
#   Licensed under the Apache License, Version 2.0 (the "License");
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#       http://www.apache.org/licenses/LICENSE-2.0
#
#   Unless required by applicable law or agreed to in writing, software
#   distributed under the License is distributed on an "AS IS" BASIS,
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#   limitations under the License.
#
"""Factories are used to build new Solvers or Quantifier Eliminators
without the need of specifying them. For example, the user can simply
require a Solver that is able to deal with quantified theories, and
the factory will return one such solver among the available ones.
This makes it possible to write algorithms that do not depend on a
particular solver.
"""

from functools import partial
from six import iteritems

from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
                              NoLogicAvailableError)
from pysmt.logics import QF_UFLIRA, LRA
from pysmt.logics import AUTO as AUTO_LOGIC
from pysmt.logics import most_generic_logic, get_closer_logic
from pysmt.oracles import get_logic

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'picosat', 'bdd']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
DEFAULT_LOGIC = QF_UFLIRA
DEFAULT_QE_LOGIC = LRA

class Factory(object):

    def __init__(self, environment,
                 solver_preference_list=None,
                 qelim_preference_list=None):
        self.environment = environment
        self._all_solvers = None
        self._all_unsat_core_solvers = None
        self._all_qelims = None
        self._generic_solvers = {}

        if solver_preference_list is None:
            solver_preference_list = DEFAULT_SOLVER_PREFERENCE_LIST
        self.solver_preference_list = solver_preference_list

        if qelim_preference_list is None:
            qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
        self.qelim_preference_list = qelim_preference_list
        self._default_logic = DEFAULT_LOGIC
        self._default_qe_logic = DEFAULT_QE_LOGIC

        self._get_available_solvers()
        self._get_available_qe()


    def get_solver(self, quantified=False, name=None, logic=None):
        assert quantified is False or logic is None, \
            "Cannot specify both quantified and logic."

        if quantified is True:
            logic = self.default_logic.get_quantified_version

        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_solvers,
                                  solver_type="Solver",
                                  preference_list=self.solver_preference_list,
                                  default_logic=self.default_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic,
                           user_options={"generate_models" : True})


    def get_unsat_core_solver(self, quantified=False, name=None,
                              logic=None, unsat_cores_mode="all"):
        assert quantified is False or logic is None, \
            "Cannot specify both quantified and logic."

        if quantified is True:
            logic = self.default_logic.get_quantified_version

        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_unsat_core_solvers,
                                  solver_type="Solver supporting Unsat Cores",
                                  preference_list=self.solver_preference_list,
                                  default_logic=self.default_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic,
                           user_options={"generate_models" : True,
                                         "unsat_cores_mode" : unsat_cores_mode})


    def get_quantifier_eliminator(self, name=None, logic=None):
        SolverClass, closer_logic = \
           self._get_solver_class(solver_list=self._all_qelims,
                                  solver_type="Quantifier Eliminator",
                                  preference_list=self.qelim_preference_list,
                                  default_logic=self.default_qe_logic,
                                  name=name,
                                  logic=logic)

        return SolverClass(environment=self.environment,
                           logic=closer_logic)


    def _get_solver_class(self, solver_list, solver_type, preference_list,
                          default_logic, name=None, logic=None):
        if len(solver_list) == 0:
            raise NoSolverAvailableError("No %s is available" % solver_type)

        if name is not None:
            if name not in solver_list:
                raise NoSolverAvailableError("%s '%s' is not available" % \
                                             (solver_type, name))

            if logic is not None and \
               name not in self._filter_solvers(solver_list, logic=logic):
                raise NoSolverAvailableError("%s '%s' does not support logic %s"%
                                             (solver_type, name, logic))

            SolverClass = solver_list[name]
            if logic is None:
                try:
                    logic = most_generic_logic(SolverClass.LOGICS)
                except NoLogicAvailableError:
                    if default_logic in SolverClass.LOGICS:
                        logic = default_logic
                    else:
                        raise NoLogicAvailableError("Cannot automatically select a logic")

            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)

            return SolverClass, closer_logic

        if logic is None:
            logic = default_logic

        solvers = self._filter_solvers(solver_list, logic=logic)

        if solvers is not None and len(solvers) > 0:
            # Pick the first solver based on preference list
            SolverClass = self._pick_favorite(preference_list, solver_list, solvers)
            closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
            return SolverClass, closer_logic

        else:
            raise NoSolverAvailableError("No %s is available for logic %s" %
                                         (solver_type, logic))

{'fraction_non_alphanumeric': 0.061127242945424765, 'fraction_numerical': 0.0020102747375474648, 'mean_word_length': 1.9928698752228164, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 46, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7510182', 'n_tokens_mistral': 3721, 'n_tokens_neox': 3504, 'n_words': 943}