<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.
#
from __future__ import absolute_import

from pysmt.exceptions import SolverAPINotFound

try:
    import z3
except ImportError:
    raise SolverAPINotFound

from six.moves import xrange

import pysmt.typing as types
from pysmt.solvers.solver import (IncrementalTrackingSolver, UnsatCoreSolver,
                                  Model, Converter)
from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
from pysmt.solvers.qelim import QuantifierEliminator
from pysmt.solvers.interpolation import Interpolator

from pysmt.walkers import DagWalker
from pysmt.exceptions import (SolverReturnedUnknownResultError,
                              SolverNotConfiguredForUnsatCoresError,
                              SolverStatusError,
                              ConvertExpressionError,
                              UndefinedSymbolError)
from pysmt.decorators import clear_pending_pop, catch_conversion_error
from pysmt.logics import LRA, LIA, QF_UFLIA, QF_UFLRA, PYSMT_LOGICS
from pysmt.oracles import get_logic
from pysmt.constants import Fraction, Numeral, is_pysmt_integer, to_python_integer


# patch z3api
z3.is_ite = lambda x: z3.is_app_of(x, z3.Z3_OP_ITE)
z3.is_implies = lambda x: z3.is_app_of(x, z3.Z3_OP_IMPLIES)
z3.is_function = lambda x: z3.is_app_of(x, z3.Z3_OP_UNINTERPRETED)
z3.is_iff = lambda x: z3.is_app_of(x, z3.Z3_OP_IFF)
z3.is_uminus = lambda x: z3.is_app_of(x, z3.Z3_OP_UMINUS)
z3.is_xor = lambda x: z3.is_app_of(x, z3.Z3_OP_XOR)

z3.is_bv_and = lambda x: z3.is_app_of(x, z3.Z3_OP_BAND)
z3.is_bv_or = lambda x: z3.is_app_of(x, z3.Z3_OP_BOR)
z3.is_bv_xor = lambda x: z3.is_app_of(x, z3.Z3_OP_BXOR)
z3.is_bv_neg = lambda x: z3.is_app_of(x, z3.Z3_OP_BNEG)
z3.is_bv_not = lambda x: z3.is_app_of(x, z3.Z3_OP_BNOT)
z3.is_bv_concat = lambda x: z3.is_app_of(x, z3.Z3_OP_CONCAT)
z3.is_bv_slt = lambda x: z3.is_app_of(x, z3.Z3_OP_SLT)
z3.is_bv_sleq = lambda x: z3.is_app_of(x, z3.Z3_OP_SLEQ)
z3.is_bv_ult = lambda x: z3.is_app_of(x, z3.Z3_OP_ULT)
z3.is_bv_uleq = lambda x: z3.is_app_of(x, z3.Z3_OP_ULEQ)
z3.is_bv_sgt = lambda x: z3.is_app_of(x, z3.Z3_OP_SGT)
z3.is_bv_sgeq = lambda x: z3.is_app_of(x, z3.Z3_OP_SGEQ)
z3.is_bv_ugt = lambda x: z3.is_app_of(x, z3.Z3_OP_UGT)
z3.is_bv_ugeq = lambda x: z3.is_app_of(x, z3.Z3_OP_UGEQ)
z3.is_bv_extract = lambda x: z3.is_app_of(x, z3.Z3_OP_EXTRACT)
z3.is_bv_add = lambda x: z3.is_app_of(x, z3.Z3_OP_BADD)
z3.is_bv_mul = lambda x: z3.is_app_of(x, z3.Z3_OP_BMUL)
z3.is_bv_udiv = lambda x: z3.is_app_of(x, z3.Z3_OP_BUDIV)
z3.is_bv_sdiv = lambda x: z3.is_app_of(x, z3.Z3_OP_BSDIV)
z3.is_bv_urem = lambda x: z3.is_app_of(x, z3.Z3_OP_BUREM)
z3.is_bv_srem = lambda x: z3.is_app_of(x, z3.Z3_OP_BSREM)
z3.is_bv_lshl = lambda x: z3.is_app_of(x, z3.Z3_OP_BSHL)
z3.is_bv_lshr = lambda x: z3.is_app_of(x, z3.Z3_OP_BLSHR)
z3.is_bv_ashr = lambda x: z3.is_app_of(x, z3.Z3_OP_BASHR)
z3.is_bv_sub = lambda x: z3.is_app_of(x, z3.Z3_OP_BSUB)
z3.is_bv_rol = lambda x: z3.is_app_of(x, z3.Z3_OP_ROTATE_LEFT)
z3.is_bv_ror = lambda x: z3.is_app_of(x, z3.Z3_OP_ROTATE_RIGHT)
z3.is_bv_ext_rol = lambda x: z3.is_app_of(x, z3.Z3_OP_EXT_ROTATE_LEFT)
z3.is_bv_ext_ror = lambda x: z3.is_app_of(x, z3.Z3_OP_EXT_ROTATE_RIGHT)
z3.is_bv_zext = lambda x: z3.is_app_of(x, z3.Z3_OP_ZERO_EXT)
z3.is_bv_sext = lambda x: z3.is_app_of(x, z3.Z3_OP_SIGN_EXT)
z3.is_power = lambda x: z3.is_app_of(x, z3.Z3_OP_POWER)
z3.is_array_select = lambda x: z3.is_app_of(x, z3.Z3_OP_SELECT)
z3.is_array_store = lambda x: z3.is_app_of(x, z3.Z3_OP_STORE)
z3.is_const_array = lambda x: z3.is_app_of(x, z3.Z3_OP_CONST_ARRAY)

z3.get_payload = lambda node,i : z3.Z3_get_decl_int_parameter(node.ctx.ref(),
                                                              node.decl().ast, i)
#z3.AlgebraicNumRef.__hash__ = z3.AlgebraicNumRef.hash
#z3.is_root_obj = lambda node: str(node.decl()) == "RootObject"


class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)

def askey(n):
    assert isinstance(n, z3.AstRef)
    return AstRefKey(n)



class Z3Model(Model):

    def __init__(self, environment, z3_model):
        Model.__init__(self, environment)
        self.z3_model = z3_model
        self.converter = Z3Converter(environment)

    def get_value(self, formula, model_completion=True):
        titem = self.converter.convert(formula)
        z3_res = self.z3_model.eval(titem, model_completion=model_completion)
        return self.converter.back(z3_res, model=self.z3_model)

    def iterator_over(self, language):
        for x in language:<commit_msg>Z3: Remove unused z3.is_* functions<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.
#
from __future__ import absolute_import

from pysmt.exceptions import SolverAPINotFound

try:
    import z3
except ImportError:
    raise SolverAPINotFound

from six.moves import xrange

import pysmt.typing as types
from pysmt.solvers.solver import (IncrementalTrackingSolver, UnsatCoreSolver,
                                  Model, Converter)
from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
from pysmt.solvers.qelim import QuantifierEliminator
from pysmt.solvers.interpolation import Interpolator

from pysmt.walkers import DagWalker
from pysmt.exceptions import (SolverReturnedUnknownResultError,
                              SolverNotConfiguredForUnsatCoresError,
                              SolverStatusError,
                              ConvertExpressionError,
                              UndefinedSymbolError)
from pysmt.decorators import clear_pending_pop, catch_conversion_error
from pysmt.logics import LRA, LIA, QF_UFLIA, QF_UFLRA, PYSMT_LOGICS
from pysmt.oracles import get_logic
from pysmt.constants import Fraction, Numeral, is_pysmt_integer, to_python_integer


# patch z3api
z3.is_ite = lambda x: z3.is_app_of(x, z3.Z3_OP_ITE)
z3.is_function = lambda x: z3.is_app_of(x, z3.Z3_OP_UNINTERPRETED)
z3.is_array_store = lambda x: z3.is_app_of(x, z3.Z3_OP_STORE)
z3.get_payload = lambda node,i : z3.Z3_get_decl_int_parameter(node.ctx.ref(),
                                                              node.decl().ast, i)

class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)

def askey(n):
    assert isinstance(n, z3.AstRef)
    return AstRefKey(n)



class Z3Model(Model):

    def __init__(self, environment, z3_model):
        Model.__init__(self, environment)
        self.z3_model = z3_model
        self.converter = Z3Converter(environment)

    def get_value(self, formula, model_completion=True):
        titem = self.converter.convert(formula)
        z3_res = self.z3_model.eval(titem, model_completion=model_completion)
        return self.converter.back(z3_res, model=self.z3_model)

    def iterator_over(self, language):
        for x in language:
{'fraction_non_alphanumeric': 0.09150006132711885, 'fraction_numerical': 0.027842511958788178, 'mean_word_length': 3.5680672268907565, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1958235', 'n_tokens_mistral': 3330, 'n_tokens_neox': 3253, 'n_words': 692}