<commit_before>import logging
l = logging.getLogger("claripy.backends.backend_z3")

solve_count = 0
cache_count = 0

from decimal import Decimal
import weakref

# import and set up Z3
import os
import z3
if "Z3PATH" in os.environ:
    z3_path = os.environ["Z3PATH"]
elif "VIRTUAL_ENV" in os.environ:
    virtual_env = os.environ["VIRTUAL_ENV"]
    z3_path = virtual_env + "/lib/"
else:
    z3_path = "/opt/python/lib/"
if not '.so' in z3_path and not '.dll' in z3_path:
    z3_path += 'libz3.so'
z3.init(z3_path)
supports_fp = hasattr(z3, 'fpEQ')

from .solver_backend import SolverBackend

#pylint:disable=unidiomatic-typecheck

#import threading
#import functools
#z3_lock = threading.RLock()
#def synchronized(f):
#    @functools.wraps(f)
#    def synced(self, *args, **kwargs):
#        if not (self._background_solve or (self._background_solve is None and self._claripy.parallel)):
#            return f(self, *args, **kwargs)
#
#        try:
#            #while not z3_lock.acquire(blocking=False): print "ACQUIRING...",__import__('time').sleep(1)
#            z3_lock.acquire()
#            return f(self, *args, **kwargs)
#        finally:
#            z3_lock.release()
#    return synced

def condom(f):
    def z3_condom(*args, **kwargs):
        '''
        The Z3 condom intersects Z3Exceptions and throws a ClaripyZ3Error instead.
        '''
        try:
            return f(*args, **kwargs)
        except z3.Z3Exception as ze:
            raise ClaripyZ3Error("Z3Exception: %s" % ze)
    return z3_condom

class BackendZ3(SolverBackend):
    _split_on = { 'And', 'Or' }

    def __init__(self):
        SolverBackend.__init__(self)
        self._ast_cache = weakref.WeakValueDictionary()
        self._var_cache = weakref.WeakKeyDictionary()
        self._sym_cache = weakref.WeakKeyDictionary()
        self._simplification_cache_key = weakref.WeakKeyDictionary()
        self._simplification_cache_val = weakref.WeakValueDictionary()
        self._enable_simplification_cache = False

        # and the operations
        all_ops = backend_fp_operations | backend_operations if supports_fp else backend_operations
        for o in all_ops - {'Reverse', 'fpToSBV', 'fpToUBV'}:
            self._op_raw[o] = getattr(z3, o)

        self._op_raw['Reverse'] = self.reverse
        self._op_raw['Identical'] = self.identical
        self._op_raw['I'] = lambda thing: thing
        self._op_raw['fpToSBV'] = self.fpToSBV
        self._op_raw['fpToUBV'] = self.fpToUBV

    def downsize(self):<commit_msg>solve the stupid int/long issue in z3<commit_after>import sys
import logging
l = logging.getLogger("claripy.backends.backend_z3")

solve_count = 0
cache_count = 0

from decimal import Decimal
import weakref

# import and set up Z3
import os
import z3
if "Z3PATH" in os.environ:
    z3_path = os.environ["Z3PATH"]
elif "VIRTUAL_ENV" in os.environ:
    virtual_env = os.environ["VIRTUAL_ENV"]
    z3_path = virtual_env + "/lib/"
else:
    z3_path = "/opt/python/lib/"
if not '.so' in z3_path and not '.dll' in z3_path:
    z3_path += 'libz3.so'
z3.init(z3_path)
supports_fp = hasattr(z3, 'fpEQ')

from .solver_backend import SolverBackend

#pylint:disable=unidiomatic-typecheck

#import threading
#import functools
#z3_lock = threading.RLock()
#def synchronized(f):
#    @functools.wraps(f)
#    def synced(self, *args, **kwargs):
#        if not (self._background_solve or (self._background_solve is None and self._claripy.parallel)):
#            return f(self, *args, **kwargs)
#
#        try:
#            #while not z3_lock.acquire(blocking=False): print "ACQUIRING...",__import__('time').sleep(1)
#            z3_lock.acquire()
#            return f(self, *args, **kwargs)
#        finally:
#            z3_lock.release()
#    return synced

def condom(f):
    def z3_condom(*args, **kwargs):
        '''
        The Z3 condom intersects Z3Exceptions and throws a ClaripyZ3Error instead.
        '''
        try:
            args = tuple((int(a) if type(a) is long and a < sys.maxint else a) for a in args)
            return f(*args, **kwargs)
        except z3.Z3Exception as ze:
            raise ClaripyZ3Error("Z3Exception: %s" % ze)
    return z3_condom

class BackendZ3(SolverBackend):
    _split_on = { 'And', 'Or' }

    def __init__(self):
        SolverBackend.__init__(self)
        self._ast_cache = weakref.WeakValueDictionary()
        self._var_cache = weakref.WeakKeyDictionary()
        self._sym_cache = weakref.WeakKeyDictionary()
        self._simplification_cache_key = weakref.WeakKeyDictionary()
        self._simplification_cache_val = weakref.WeakValueDictionary()
        self._enable_simplification_cache = False

        # and the operations
        all_ops = backend_fp_operations | backend_operations if supports_fp else backend_operations
        for o in all_ops - {'Reverse', 'fpToSBV', 'fpToUBV'}:
            self._op_raw[o] = getattr(z3, o)

        self._op_raw['Reverse'] = self.reverse
        self._op_raw['Identical'] = self.identical
        self._op_raw['I'] = lambda thing: thing
        self._op_raw['fpToSBV'] = self.fpToSBV
        self._op_raw['fpToUBV'] = self.fpToUBV

    def downsize(self):
{'fraction_non_alphanumeric': 0.11694094869312681, 'fraction_numerical': 0.01297192642787996, 'mean_word_length': 3.0296411856474257, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4714073', 'n_tokens_mistral': 1802, 'n_tokens_neox': 1773, 'n_words': 394}