<commit_before>#!/usr/bin/env python3
import argparse
import logging
import tempfile
import helpers.timer as timer

from typing import Iterable

from helpers import automaton2dot
from helpers.main_helper import setup_logging, create_spec_converter_z3
from helpers.python_ext import readfile
from interfaces.expr import Expr, Signal
from module_generation.aiger import lts_to_aiger
from module_generation.dot import lts_to_dot
from parsing.acacia_parser_helper import parse_acacia_and_build_expr
from parsing.tlsf_parser import parse_tlsf_build_expr
from synthesis import model_searcher
from synthesis.encoder_builder import create_encoder
from synthesis.funcs_args_types_names import ARG_MODEL_STATE
from synthesis.smt_logic import UFLIA

CHECK_BOTH, CHECK_REAL, CHECK_UNREAL = 'both', 'real', 'unreal'


def _parse_acacia_spec(spec_file_name:str, ltl3ba)\
        -> (Iterable[Signal], Iterable[Signal], Expr):
    """ :return: (inputs_signals, output_signals, expr) """

    assert spec_file_name.endswith('.ltl'), spec_file_name
    ltl_file_str = readfile(spec_file_name)
    part_file_str = readfile(spec_file_name.replace('.ltl', '.part'))
    return parse_acacia_and_build_expr(ltl_file_str, part_file_str, ltl3ba)


def main(tlsf_file_name,
         output_file_name,
         dot_file_name,
         synthesis_type,
         smt_files_prefix,
         keep_temp_files):

    assert synthesis_type == CHECK_REAL, 'the rest is not impl yet'

    ltl3ba, solver_factory = create_spec_converter_z3(UFLIA(None),  # TODO: use UFLRA
                                                      False,
                                                      False,
                                                      smt_files_prefix,
                                                      not keep_temp_files)

    timer.sec_restart()

    inputs, outputs, expr, is_moore = parse_tlsf_build_expr(tlsf_file_name, ltl3ba)
    logging.info('parsing and building expr took (sec): %i' % timer.sec_restart())

    automaton = ltl3ba.convert(~expr)
    logging.info('automata translation took (sec): %i' % timer.sec_restart())
    logging.debug('automaton (dot) is:\n' + automaton2dot.to_dot(automaton))

    encoder = create_encoder(inputs, outputs,
                             is_moore,
                             automaton,
                             solver_factory.create(), UFLIA(None))

    model = model_searcher.search(1, 24, encoder)  # TODO: guess better min max sizes
    logging.info('model_searcher.search took (sec): %i' %timer.sec_restart())

    is_realizable = model is not None

    logging.info(['unrealizable within the bounds', 'realizable'][is_realizable])

    if is_realizable:
        dot_model_str = lts_to_dot(model, ARG_MODEL_STATE, not is_moore)

        if dot_file_name:
            with open(dot_file_name, 'w') as out:
                out.write(dot_model_str)
                logging.info('{model_type} model is written to {file}'.format(
                             model_type=['Mealy', 'Moore'][is_moore],
                             file=out.name))
        else:
            logging.info(dot_model_str)

        if output_file_name:
            aiger_model_str = lts_to_aiger(model)
            with open(output_file_name, 'w') as out:
                out.write(aiger_model_str)

    return is_realizable


if __name__ == "__main__":
    parser = argparse.ArgumentParser(description='elli trained for syntcomp rally',
                                     formatter_class=argparse.ArgumentDefaultsHelpFormatter)

    parser.add_argument('spec', metavar='spec', type=str,
                        help='tlsf spec file')
    parser.add_argument('-o', '--output', metavar='output', type=str,
                        help='output file for a model in the aiger format')

    parser.add_argument('--check',
                        choices=(CHECK_BOTH, CHECK_REAL, CHECK_UNREAL),
                        default=CHECK_BOTH,
                        help='what type of the check')

    parser.add_argument('--dot', metavar='dot', type=str,
                        help='write the output into a dot graph file')
    parser.add_argument('--tmp', action='store_true', default=False,
                        help='keep temporary smt2 files')
    parser.add_argument('-v', '--verbose', action='count', default=-1,
                        help='verbosity level')

    args = parser.parse_args()
    assert args.check == CHECK_REAL

    setup_logging(args.verbose)
    logging.info(args)

    with tempfile.NamedTemporaryFile(dir='./') as smt_file:
        smt_files_prefix = smt_file.name

    is_realizable = main(args.spec,
                         args.output,
                         args.dot,
                         args.check,
                         smt_files_prefix,
                         args.tmp)

    exit(is_realizable)<commit_msg>zero-real-only<commit_after>#!/usr/bin/env python3
import argparse
import logging
import tempfile
import helpers.timer as timer

from typing import Iterable

from helpers import automaton2dot
from helpers.main_helper import setup_logging, create_spec_converter_z3
from helpers.python_ext import readfile
from interfaces.expr import Expr, Signal
from module_generation.aiger import lts_to_aiger
from module_generation.dot import lts_to_dot
from parsing.acacia_parser_helper import parse_acacia_and_build_expr
from parsing.tlsf_parser import parse_tlsf_build_expr
from synthesis import model_searcher
from synthesis.encoder_builder import create_encoder
from synthesis.funcs_args_types_names import ARG_MODEL_STATE
from synthesis.smt_logic import UFLIA

CHECK_BOTH, CHECK_REAL, CHECK_UNREAL = 'both', 'real', 'unreal'


def _parse_acacia_spec(spec_file_name:str, ltl3ba)\
        -> (Iterable[Signal], Iterable[Signal], Expr):
    """ :return: (inputs_signals, output_signals, expr) """

    assert spec_file_name.endswith('.ltl'), spec_file_name
    ltl_file_str = readfile(spec_file_name)
    part_file_str = readfile(spec_file_name.replace('.ltl', '.part'))
    return parse_acacia_and_build_expr(ltl_file_str, part_file_str, ltl3ba)


def main(tlsf_file_name,
         output_file_name,
         dot_file_name,
         synthesis_type,
         smt_files_prefix,
         keep_temp_files):

    assert synthesis_type == CHECK_REAL, 'the rest is not impl yet'

    ltl3ba, solver_factory = create_spec_converter_z3(UFLIA(None),  # TODO: use UFLRA
                                                      False,
                                                      False,
                                                      smt_files_prefix,
                                                      not keep_temp_files)

    timer.sec_restart()

    inputs, outputs, expr, is_moore = parse_tlsf_build_expr(tlsf_file_name, ltl3ba)
    logging.info('parsing and building expr took (sec): %i' % timer.sec_restart())

    automaton = ltl3ba.convert(~expr)
    logging.info('automata translation took (sec): %i' % timer.sec_restart())
    logging.debug('automaton (dot) is:\n' + automaton2dot.to_dot(automaton))

    encoder = create_encoder(inputs, outputs,
                             is_moore,
                             automaton,
                             solver_factory.create(), UFLIA(None))

    model = model_searcher.search(1, 24, encoder)  # TODO: guess better min max sizes
    logging.info('model_searcher.search took (sec): %i' %timer.sec_restart())

    is_realizable = model is not None

    logging.info(['unrealizable within the bounds', 'realizable'][is_realizable])

    if is_realizable:
        dot_model_str = lts_to_dot(model, ARG_MODEL_STATE, not is_moore)

        if dot_file_name:
            with open(dot_file_name, 'w') as out:
                out.write(dot_model_str)
                logging.info('{model_type} model is written to {file}'.format(
                             model_type=['Mealy', 'Moore'][is_moore],
                             file=out.name))
        else:
            logging.info(dot_model_str)

        aiger_model_str = lts_to_aiger(model)
        if output_file_name:
            with open(output_file_name, 'w') as out:
                out.write(aiger_model_str)
        else:
            print(aiger_model_str)

    return is_realizable


if __name__ == "__main__":
    parser = argparse.ArgumentParser(description='elli trained for syntcomp rally',
                                     formatter_class=argparse.ArgumentDefaultsHelpFormatter)

    parser.add_argument('spec', metavar='spec', type=str,
                        help='tlsf spec file')
    parser.add_argument('-o', '--output', metavar='output', type=str,
                        help='output file for a model in the aiger format (if not given -- print to stdout)')

    parser.add_argument('--check',
                        choices=(CHECK_BOTH, CHECK_REAL, CHECK_UNREAL),
                        default=CHECK_BOTH,
                        help='what type of the check')

    parser.add_argument('--dot', metavar='dot', type=str,
                        help='write the output into a dot graph file')
    parser.add_argument('--tmp', action='store_true', default=False,
                        help='keep temporary smt2 files')
    parser.add_argument('-v', '--verbose', action='count', default=-1,
                        help='verbosity level')

    args = parser.parse_args()
    assert args.check == CHECK_REAL

    setup_logging(args.verbose)
    logging.info(args)

    with tempfile.NamedTemporaryFile(dir='./') as smt_file:
        smt_files_prefix = smt_file.name

    is_realizable = main(args.spec,
                         args.output,
                         args.dot,
                         args.check,
                         smt_files_prefix,
                         args.tmp)

    exit([20, 10][is_realizable])
{'fraction_non_alphanumeric': 0.09046454767726161, 'fraction_numerical': 0.0034637326813365932, 'mean_word_length': 2.290982232651693, 'pattern_counts': {'":': 2, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5171160', 'n_tokens_mistral': 2951, 'n_tokens_neox': 2828, 'n_words': 612}