<commit_before>from __future__ import absolute_import

from rpython.rlib.rfloat import float_as_rbigint_ratio

from topaz.coerce import Coerce
from topaz.module import Module, ModuleDef, ClassDef
from topaz.objects.objectobject import W_RootObject, W_Object
from topaz.utils import rz3


class W_Z3Object(W_RootObject):
    _attrs_ = ["ctx", "solver", "enabled_constraints", "is_solved"]
    _immutable_fields_ = ["ctx", "solver"]
    classdef = ClassDef("Z3", W_Object.classdef, filepath=__file__)

    def __init__(self):
        cfg = rz3.z3_mk_config()
        rz3.z3_set_param_value(cfg, "MODEL", "true")
        ctx = rz3.z3_mk_context(cfg)
        rz3.z3_del_config(cfg)
        solver = rz3.z3_mk_solver(ctx)
        rz3.z3_solver_inc_ref(ctx, solver)
        self.ctx = ctx
        self.solver = solver
        self.enabled_constraints = []
        self.is_solved = False

    def getsingletonclass(self, space):
        raise space.error(space.w_TypeError, "can't define singleton")

    def find_instance_var(self, space, name):
        return space.w_nil

    def set_instance_var(self, space, name, w_value):
        raise space.error(space.w_TypeError, "can't add instance variables")

    @classdef.setup_class
    def setup_class(cls, space, w_cls):
        w_ptr_cls = space.getclassfor(W_Z3Ptr)
        space.set_const(w_cls, w_ptr_cls.name, w_ptr_cls)

    def make_variable(self, space, w_object, ctx, ty):
        # XXX: This should somehow also set the initial value
        id = space.int_w(space.send(w_object, space.newsymbol("object_id")))
        sym = rz3.z3_mk_int_symbol(ctx, id)
        return W_Z3Ptr(self, rz3.z3_mk_const(ctx, sym, ty))

    def assert_ptr(self, space, w_pointer):
        if not isinstance(w_pointer, W_Z3Ptr):
            raise space.error(
                space.w_TypeError,
                "expected %s, got %s" % (space.getclassfor(W_Z3Ptr).name, space.getclass(w_pointer).name)<commit_msg>cannot rely on object_id for symbols, avoid clashes using a running id<commit_after>from __future__ import absolute_import

from rpython.rlib.rfloat import float_as_rbigint_ratio

from topaz.coerce import Coerce
from topaz.module import Module, ModuleDef, ClassDef
from topaz.objects.objectobject import W_RootObject, W_Object
from topaz.utils import rz3


class W_Z3Object(W_RootObject):
    _attrs_ = ["ctx", "solver", "enabled_constraints", "is_solved"]
    _immutable_fields_ = ["ctx", "solver"]
    classdef = ClassDef("Z3", W_Object.classdef, filepath=__file__)

    def __init__(self):
        cfg = rz3.z3_mk_config()
        rz3.z3_set_param_value(cfg, "MODEL", "true")
        ctx = rz3.z3_mk_context(cfg)
        rz3.z3_del_config(cfg)
        solver = rz3.z3_mk_solver(ctx)
        rz3.z3_solver_inc_ref(ctx, solver)
        self.ctx = ctx
        self.solver = solver
        self.enabled_constraints = []
        self.is_solved = False
        self.next_id = 0

    def getsingletonclass(self, space):
        raise space.error(space.w_TypeError, "can't define singleton")

    def find_instance_var(self, space, name):
        return space.w_nil

    def set_instance_var(self, space, name, w_value):
        raise space.error(space.w_TypeError, "can't add instance variables")

    @classdef.setup_class
    def setup_class(cls, space, w_cls):
        w_ptr_cls = space.getclassfor(W_Z3Ptr)
        space.set_const(w_cls, w_ptr_cls.name, w_ptr_cls)

    def make_variable(self, space, w_object, ctx, ty):
        # XXX: This should somehow also set the initial value
        sym = rz3.z3_mk_int_symbol(ctx, self.next_id)
        self.next_id += 1
        return W_Z3Ptr(self, rz3.z3_mk_const(ctx, sym, ty))

    def assert_ptr(self, space, w_pointer):
        if not isinstance(w_pointer, W_Z3Ptr):
            raise space.error(
                space.w_TypeError,
                "expected %s, got %s" % (space.getclassfor(W_Z3Ptr).name, space.getclass(w_pointer).name)
{'fraction_non_alphanumeric': 0.10124650216229968, 'fraction_numerical': 0.012210633426609005, 'mean_word_length': 3.24622030237581, 'pattern_counts': {'":': 0, '<': 3, '<?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': '2728894', 'n_tokens_mistral': 1409, 'n_tokens_neox': 1365, 'n_words': 291}