<commit_before>#!/usr/bin/python
# -*- coding: utf-8 -*-

import logging
import z3

import c_info
import err

logger = logging.getLogger(__name__)

INT_SIZE = c_info.sizeof_int()  # bytes
BYTE = 8  # bits
INT_SIZE_BITS = INT_SIZE * BYTE
HEX_BASE = 16
BIN_BASE = 2
REAL2FLOAT_PRECISION = 6


def smt_solver_factory(solver_name):
    if solver_name == 'z3':
        return Z()
    else:
        raise err.Fatal('solver name not recognized: {}'.format(solver_name))


class Solver(object):

    pass


class Z(Solver):

    def __init__(self):

        # self.solver = z3.Solver()

        self.TRUE = z3.BoolVal(True)
        self.FALSE = z3.BoolVal(False)

        return

    def And(self, *args):
        return z3.And(*args)

    def ArraySort(self, *args):
        return z3.ArraySort(*args)

    def BitVecSort(self, *args):
        return z3.BitVecSort(*args)

    def Function(self, *args):
        return z3.Function(*args)

    def Array(self, *args):
        return z3.Array(*args)

    def smt2_2_constraints(self, s, decls):
        return z3.parse_smt2_string(s, decls=decls)

    def SAT(self, c):
        s = z3.Solver()
        s.add(c)
        return s.check() == z3.sat

    def equal(self, x, val):
        cons_list = []
        if isinstance(x, z3.ExprRef):
            if x.sort() == z3.ArraySort(z3.BitVecSort(32), z3.BitVecSort(8)):
                for i in range(len(val)):
                    c_equal = z3.Concat(x[INT_SIZE * i + 3], x[INT_SIZE * i + 2],
                                        x[INT_SIZE * i + 1], x[INT_SIZE * i + 0]) \
                        == val[i]
                    cons_list.append(c_equal)
            elif x.sort() == z3.RealSort():
                c_equal = x == val
                cons_list.append(c_equal)
            else:
                raise err.Fatal('unhandled sort x: {}'.format(x.sort()))
        elif isinstance(x, list):
            cons_list = map((lambda x, c: x == c), x, val)
        else:
            raise err.Fatal('unhandled type: {}'.format(type(x)))
        # loop sentinel
        if cons_list == []:
            cons_list = True
        return z3.And(cons_list)

    def RealVector(self, s_str, length):
        return z3.RealVector(s_str, length)

    def IntVector(self, s_str, length):
        return z3.IntVector(s_str, length)

    def BitVecArray(self, s_str):
        return z3.Array(s_str, z3.BitVecSort(32), z3.BitVecSort(8))

    # TODO: depends on interval constraints api...is this ok?
    def ic2smt(self, ic, x):
        cons_list = []
        if isinstance(x, z3.ExprRef):
            if x.sort() == z3.ArraySort(z3.BitVecSort(32), z3.BitVecSort(8)):
                for i in range(ic.dim):
                    c_upper_bound = z3.Concat(x[INT_SIZE * i + 3],
                                              x[INT_SIZE * i + 2],
                                              x[INT_SIZE * i + 1],
                                              x[INT_SIZE * i + 0]) \
                                    <= ic.h[i]
                    c_lower_bound = z3.Concat(x[INT_SIZE * i + 3],
                                              x[INT_SIZE * i + 2],
                                              x[INT_SIZE * i + 1],
                                              x[INT_SIZE * i + 0]) \
                                    >= ic.l[i]
                    cons_list.append(c_upper_bound)
                    cons_list.append(c_lower_bound)
            else:
                raise err.Fatal('unknown sort: {}'.format(x.sort()))
        elif isinstance(x, list):
            cons_list = map((lambda x, c: x <= c), x, ic.h)\
                      + map((lambda x, c: x >= c), x, ic.l)
        else:
            raise err.Fatal('unhandled type: {}'.format(type(x)))
        return z3.And(cons_list)

    # TODO: fix the function call!
    def substitute(
            self,
            C,
            v,
            v_,
            ):
        return z3.substitute(C, (v, v_))

    def simplify(self, *args):
        return z3.simplify(*args)

    def solver(self):
        return z3.Solver()

    def sample_bvArray(
            self,
            surface,
            num_points,
            outputVarList,
            var2dim_dict,
            var2sample_list,<commit_msg>upto date with svn version<commit_after>#!/usr/bin/python
# -*- coding: utf-8 -*-

import logging
import z3

import c_info
import err

logger = logging.getLogger(__name__)

INT_SIZE = c_info.sizeof_int()  # bytes
BYTE = 8  # bits
INT_SIZE_BITS = INT_SIZE * BYTE
HEX_BASE = 16
BIN_BASE = 2
REAL2FLOAT_PRECISION = 6


def smt_solver_factory(solver_name):
    if solver_name == 'z3':
        return Z()
    else:
        raise err.Fatal('solver name not recognized: {}'.format(solver_name))


class Solver(object):

    pass


class Z(Solver):

    def __init__(self):

        # self.solver = z3.Solver()

        self.TRUE = z3.BoolVal(True)
        self.FALSE = z3.BoolVal(False)

        return

    def And(self, *args):
        return z3.And(*args)

    def ArraySort(self, *args):
        return z3.ArraySort(*args)

    def BitVecSort(self, *args):
        return z3.BitVecSort(*args)

    def Function(self, *args):
        return z3.Function(*args)

    def Array(self, *args):
        return z3.Array(*args)

    def smt2_2_constraints(self, s, decls):
        return z3.parse_smt2_string(s, decls=decls)

    def SAT(self, c):
        s = z3.Solver()
        s.add(c)
        return s.check() == z3.sat

    def equal(self, x, val):
        cons_list = []
        if isinstance(x, z3.ExprRef):
            if x.sort() == z3.ArraySort(z3.BitVecSort(32), z3.BitVecSort(8)):
                for i in range(len(val)):
                    c_equal = z3.Concat(x[INT_SIZE * i + 3], x[INT_SIZE * i + 2],
                                        x[INT_SIZE * i + 1], x[INT_SIZE * i + 0]) \
                        == val[i]
                    cons_list.append(c_equal)
            elif x.sort() == z3.RealSort():
                c_equal = x == val
                cons_list.append(c_equal)
            else:
                raise err.Fatal('unhandled sort x: {}'.format(x.sort()))
        elif isinstance(x, list):
            cons_list = map((lambda x, c: x == c), x, val)
        else:
            raise err.Fatal('unhandled type: {}'.format(type(x)))
        # loop sentinel
        if cons_list == []:
            cons_list = True
        return z3.And(cons_list)

    def RealVector(self, s_str, length):
        return z3.RealVector(s_str, length)

    def IntVector(self, s_str, length):
        return z3.IntVector(s_str, length)

    def BitVecArray(self, s_str):
        return z3.Array(s_str, z3.BitVecSort(32), z3.BitVecSort(8))

    # TODO: depends on interval constraints api...is this ok?
    def ic2smt(self, ic, x):
        cons_list = []
        if isinstance(x, z3.ExprRef):
            if x.sort() == z3.ArraySort(z3.BitVecSort(32), z3.BitVecSort(8)):
                for i in range(ic.dim):
                    c_upper_bound = z3.Concat(x[INT_SIZE * i + 3],
                                              x[INT_SIZE * i + 2],
                                              x[INT_SIZE * i + 1],
                                              x[INT_SIZE * i + 0]) \
                                    <= ic.h[i]
                    c_lower_bound = z3.Concat(x[INT_SIZE * i + 3],
                                              x[INT_SIZE * i + 2],
                                              x[INT_SIZE * i + 1],
                                              x[INT_SIZE * i + 0]) \
                                    >= ic.l[i]
                    cons_list.append(c_upper_bound)
                    cons_list.append(c_lower_bound)
            else:
                raise err.Fatal('unknown sort: {}'.format(x.sort()))
        elif isinstance(x, list):
            cons_list = map((lambda x, c: x <= c), x, ic.h)\
                      + map((lambda x, c: x >= c), x, ic.l)
        else:
            raise err.Fatal('unhandled type: {}'.format(type(x)))
#         # Loop Sentinel
#         if cons_list == []:
#             cons_list = True
        return z3.And(cons_list)

    # TODO: fix the function call!
    def substitute(
            self,
            C,
            v,
            v_,
            ):
        return z3.substitute(C, (v, v_))

    def simplify(self, *args):
        return z3.simplify(*args)

    def solver(self):
        return z3.Solver()

    def sample_bvArray(
            self,
            surface,
            num_points,
            outputVarList,
            var2dim_dict,
            var2sample_list,
{'fraction_non_alphanumeric': 0.12247269346967232, 'fraction_numerical': 0.01603532419242389, 'mean_word_length': 1.438243626062323, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6045201', 'n_tokens_mistral': 2830, 'n_tokens_neox': 2677, 'n_words': 613}