<commit_before>from interfaces.parser_expr import QuantifiedSignal
from synthesis.func_description import FuncDescription


def build_signals_values(signals, label) -> (dict, list):
    for s in signals: #TODO: remove after debug
        assert isinstance(s, QuantifiedSignal)

    value_by_signal = dict()
    free_values = []

    for s in signals:
        if s in label:
            value_by_signal[s] = str(label[s]).lower()
        else:
            value = '?{0}'.format(str(s)).lower() #TODO: hack: we str(signal)
            value_by_signal[s] = value
            free_values.append(value)

    return value_by_signal, free_values


def get_bits_definition(arg_prefix, nof_bits):
    args = list(map(lambda i: arg_prefix+str(i), range(nof_bits)))
    args_defs = list(map(lambda a: (a, 'Bool'), args))
    return args, args_defs


def make_check_sat():
    return "(check-sat)"


def make_get_model():
    return "(get-model)"


def make_exit():
    return "(exit)"


def make_set_logic(logic):
    return ';(set-logic {0})\n'.format(logic.smt_name)


def make_headers():
    #TODO: ask stackoverflow about other speed upers
    #ematching slows down if forall quantifier is present
    return '(set-option :produce-models true)\n(set-option :EMATCHING false)\n'


#TODO: no need of constraints for input values
def declare_bool_const(const_name, value):
    smt = ['(declare-const {0} Bool)\n'.format(const_name),
           '(assert (= {0} {1}))\n'.format(const_name, str(value).lower())]
    return ''.join(smt)


def get_output_name(output):
    return 'fo_' + str(output)


def declare_output(output, sys_state_type):
    return declare_fun(get_output_name(output), [sys_state_type], "Bool")


def declare_counters(logic, sys_state_type, spec_state_type):
    smt_lines = [
        declare_fun("lambda_B", [spec_state_type, sys_state_type], "Bool"),
        declare_fun("lambda_sharp", [spec_state_type, sys_state_type], logic.counters_type(4))]

    return '\n'.join(smt_lines)


def get_valued_var_name(var, value):
    return '{0}{1}'.format('i_' if value else 'i_not_', var)


def declare_inputs(inputs):
    smt_str = ''
    for input_var in inputs:
        for value in [False, True]:
            smt_str += declare_bool_const(get_valued_var_name(input_var, value), value)

    smt_str += '\n'
    return smt_str


def declare_enum(enum_name, values):
    smt_str = '(declare-datatypes () (({0} {1})))'.format(enum_name,
        ' '.join(values))
    return smt_str

#def declare_enum_as_int_consts(names):
#    smt_lines = StrAwareList()
#    for crt_val, n in enumerate(names):
#        smt_lines += '(declare-const {name} Int)'.format(
#            name = n)
#
#        smt_lines += '(assert (= {name} {value}))'.format(
#            name=n,
#            value=crt_val)
#
#    return '\n'.join(smt_lines)
#
#
#def declare_enum_as_bv_consts(names):
#    smt_lines = StrAwareList()
#
#    width = int(max(int(math.ceil(math.log(len(names), 2))), 1))
#    for crt_val, n in enumerate(names):
#        smt_lines += '(declare-const {name} {type})'.format(
#            name = n,
#            type = '(_ bv {width})'.format(width = width))
#
#        smt_lines += '(assert (= {name} {value}))'.format(
#            name=n,
#            value='(_ bv{width} {value})'.format(width=width, value = crt_val))
#
#    return '\n'.join(smt_lines)


def tuple_type(name, component_types):
    args = ' '.join(component_types)
    return '({name} {args})'.format_map({'name':name, 'args':args})


def declare_tuple(name, component_types, getter_prefix):
    """ This implementation is Z3 specific """

    ctor_args = ' '.join(map(lambda i: 'arg'+str(i), range(len(component_types))))
    components_def = ' '.join(map(lambda i,t: '({get}{i} {t})'.format_map({'i':i,
                                                                           't':t,
                                                                           'get':getter_prefix}),
                                  enumerate(component_types)))

    smt_str = """
    (declare-datatypes ({args})
    ( ({name} (mk-pair {components_def})) )
    )
    """.format_map({'args':ctor_args, 'name':name, 'components_def':components_def})

    return smt_str


def call_func_raw(func_name, args):
    smt_str = '(' + func_name + ' '
    for arg in args:
        smt_str += str(arg) + ' '
    if len(args):
        smt_str = smt_str[:-1]
    smt_str += ')'
    return smt_str


def call_func(func_desc:FuncDescription, func_args_dict:dict):
    return call_func_raw(func_desc.name, func_desc.get_args_list(func_args_dict))


def make_assert(formula):
    smt_str = '(assert ' + formula + ')\n'
    return smt_str


def comment(comment):
    smt_str = '; ' + str(comment)
    return smt_str


def declare_fun(name, input_types, out_type):
    input_types = list(input_types)
    smt_str = '(declare-fun '
    smt_str += name + ' ('

    for var in input_types:
        smt_str += var + ' '
    if len(input_types):
        smt_str = smt_str[:-1]

    smt_str += ') ' + out_type + ')\n'
    return smt_str


def declare_sort(name, num_param):
    smt_str = '(declare-sort '
    smt_str += name + ' ' + str(num_param) + ')\n'
    return smt_str


def op_implies(arg1, arg2):
    smt_str = '(=> ' + arg1 + ' ' + arg2 + ')'
    return smt_str


def eq(arg1, arg2): #is equal to
    smt_str = '(= ' + arg1 + ' ' + arg2 + ')'
    return smt_str


def gt(arg1, arg2, logic):
    return '({0} {1} {2})'.format(logic.gt, arg1, arg2)


def ge(arg1, arg2, logic):
    return '({0} {1} {2})'.format(logic.ge, arg1, arg2)
<commit_msg>eq -> op_eq<commit_after>from interfaces.parser_expr import QuantifiedSignal
from synthesis.func_description import FuncDescription


def build_signals_values(signals, label) -> (dict, list):
    for s in signals: #TODO: remove after debug
        assert isinstance(s, QuantifiedSignal)

    value_by_signal = dict()
    free_values = []

    for s in signals:
        if s in label:
            value_by_signal[s] = str(label[s]).lower()
        else:
            value = '?{0}'.format(str(s)).lower() #TODO: hack: we str(signal)
            value_by_signal[s] = value
            free_values.append(value)

    return value_by_signal, free_values


def get_bits_definition(arg_prefix, nof_bits):
    args = list(map(lambda i: arg_prefix+str(i), range(nof_bits)))
    args_defs = list(map(lambda a: (a, 'Bool'), args))
    return args, args_defs


def make_check_sat():
    return "(check-sat)"


def make_get_model():
    return "(get-model)"


def make_exit():
    return "(exit)"


def make_set_logic(logic):
    return ';(set-logic {0})\n'.format(logic.smt_name)


def make_headers():
    #TODO: ask stackoverflow about other speed upers
    #ematching slows down if forall quantifier is present
    return '(set-option :produce-models true)\n(set-option :EMATCHING false)\n'


#TODO: no need of constraints for input values
def declare_bool_const(const_name, value):
    smt = ['(declare-const {0} Bool)\n'.format(const_name),
           '(assert (= {0} {1}))\n'.format(const_name, str(value).lower())]
    return ''.join(smt)


def get_output_name(output):
    return 'fo_' + str(output)


def declare_output(output, sys_state_type):
    return declare_fun(get_output_name(output), [sys_state_type], "Bool")


def declare_counters(logic, sys_state_type, spec_state_type):
    smt_lines = [
        declare_fun("lambda_B", [spec_state_type, sys_state_type], "Bool"),
        declare_fun("lambda_sharp", [spec_state_type, sys_state_type], logic.counters_type(4))]

    return '\n'.join(smt_lines)


def get_valued_var_name(var, value):
    return '{0}{1}'.format('i_' if value else 'i_not_', var)


def declare_inputs(inputs):
    smt_str = ''
    for input_var in inputs:
        for value in [False, True]:
            smt_str += declare_bool_const(get_valued_var_name(input_var, value), value)

    smt_str += '\n'
    return smt_str


def declare_enum(enum_name, values):
    smt_str = '(declare-datatypes () (({0} {1})))'.format(enum_name,
        ' '.join(values))
    return smt_str

#def declare_enum_as_int_consts(names):
#    smt_lines = StrAwareList()
#    for crt_val, n in enumerate(names):
#        smt_lines += '(declare-const {name} Int)'.format(
#            name = n)
#
#        smt_lines += '(assert (= {name} {value}))'.format(
#            name=n,
#            value=crt_val)
#
#    return '\n'.join(smt_lines)
#
#
#def declare_enum_as_bv_consts(names):
#    smt_lines = StrAwareList()
#
#    width = int(max(int(math.ceil(math.log(len(names), 2))), 1))
#    for crt_val, n in enumerate(names):
#        smt_lines += '(declare-const {name} {type})'.format(
#            name = n,
#            type = '(_ bv {width})'.format(width = width))
#
#        smt_lines += '(assert (= {name} {value}))'.format(
#            name=n,
#            value='(_ bv{width} {value})'.format(width=width, value = crt_val))
#
#    return '\n'.join(smt_lines)


def tuple_type(name, component_types):
    args = ' '.join(component_types)
    return '({name} {args})'.format_map({'name':name, 'args':args})


def declare_tuple(name, component_types, getter_prefix):
    """ This implementation is Z3 specific """

    ctor_args = ' '.join(map(lambda i: 'arg'+str(i), range(len(component_types))))
    components_def = ' '.join(map(lambda i,t: '({get}{i} {t})'.format_map({'i':i,
                                                                           't':t,
                                                                           'get':getter_prefix}),
                                  enumerate(component_types)))

    smt_str = """
    (declare-datatypes ({args})
    ( ({name} (mk-pair {components_def})) )
    )
    """.format_map({'args':ctor_args, 'name':name, 'components_def':components_def})

    return smt_str


def call_func_raw(func_name, args):
    smt_str = '(' + func_name + ' '
    for arg in args:
        smt_str += str(arg) + ' '
    if len(args):
        smt_str = smt_str[:-1]
    smt_str += ')'
    return smt_str


def call_func(func_desc:FuncDescription, func_args_dict:dict):
    return call_func_raw(func_desc.name, func_desc.get_args_list(func_args_dict))


def make_assert(formula):
    smt_str = '(assert ' + formula + ')\n'
    return smt_str


def comment(comment):
    smt_str = '; ' + str(comment)
    return smt_str


def declare_fun(name, input_types, out_type):
    input_types = list(input_types)
    smt_str = '(declare-fun '
    smt_str += name + ' ('

    for var in input_types:
        smt_str += var + ' '
    if len(input_types):
        smt_str = smt_str[:-1]

    smt_str += ') ' + out_type + ')\n'
    return smt_str


def declare_sort(name, num_param):
    smt_str = '(declare-sort '
    smt_str += name + ' ' + str(num_param) + ')\n'
    return smt_str


def op_implies(arg1, arg2):
    smt_str = '(=> ' + arg1 + ' ' + arg2 + ')'
    return smt_str


def op_eq(arg1, arg2):
    smt_str = '(= ' + arg1 + ' ' + arg2 + ')'
    return smt_str


def gt(arg1, arg2, logic):
    return '({0} {1} {2})'.format(logic.gt, arg1, arg2)


def ge(arg1, arg2, logic):
    return '({0} {1} {2})'.format(logic.ge, arg1, arg2)

{'fraction_non_alphanumeric': 0.15306671449067433, 'fraction_numerical': 0.00663558106169297, 'mean_word_length': 2.9591764288249913, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3598625', 'n_tokens_mistral': 4079, 'n_tokens_neox': 3942, 'n_words': 814}