<jupyter_start><jupyter_text>Translate `dzn` to `smt2` for OptiMathSAT  Check Versions of Tools<jupyter_code>import os
import subprocess

my_env = os.environ.copy()
output = subprocess.check_output(f'''/home/{my_env['USER']}/optimathsat/bin/optimathsat -version''',
                                 shell=True, universal_newlines=True)
output
output = subprocess.check_output(f'''/home/{my_env['USER']}/minizinc/build/minizinc --version''',
                                 shell=True, universal_newlines=True)
output<jupyter_output><empty_output><jupyter_text>First generate the FlatZinc files using the MiniZinc tool. Make sure that a `smt2` folder is located inside `./minizinc/share/minizinc/`. Else, to enable OptiMathSAT's support for global constraints download the [smt2.tar.gz](http://optimathsat.disi.unitn.it/data/smt2.tar.gz) package and unpack it there using```zshtar xf smt2.tar.gz $MINIZINC_PATH/share/minizinc/```If next output shows a list of `.mzn` files, then this dependency is satified.<jupyter_code>output = subprocess.check_output(f'''ls -la /home/{my_env['USER']}/minizinc/share/minizinc/smt2/''',
                                 shell=True, universal_newlines=True)
print(output)<jupyter_output>total 292
drwxr-xr-x  2 jov<NAME> 4096 Jan 15  2018 .
drwxr-xr-x 11 jovyan jovyan 4096 Jul 11 12:34 ..
-rw-r--r--  1 <NAME>  328 Nov 13  2017 alldifferent_except_0.mzn
-rw-r--r--  1 <NAME>  382 Nov 13  2017 all_different_int.mzn
-rw-r--r--  1 <NAME>  396 Nov 13  2017 all_different_set.mzn
-rw-r--r--  1 <NAME>  270 Nov 13  2017 all_disjoint.mzn
-rw-r--r--  1 <NAME>  150 Nov 14  2017 all_equal_int.mzn
-rw-r--r--  1 <NAME>  164 Nov 13  2017 all_equal_set.mzn
-rw-r--r--  1 <NAME>  351 Nov 13  2017 among.mzn
-rw-r--r--  1 <NAME>  305 Nov  8  2017 arg_max_float.mzn
-rw-r--r--  1 <NAME>  291 Nov  8  2017 arg_max_int.mzn
-rw-r--r--  1 <NAME>  306 Nov  8  2017 arg_min_float.mzn
-rw-r--r--  1 <NAME>  291 Nov  8  2017 arg_min_int.mzn
-rw-r--r--  1 <NAME>  480 Nov 13  2017 at_least_int.mzn
-rw-r--r--  1 <NAME>  506 Nov 14  2017 at_least_set.mzn
-rw-r--r--  1 <NAME>  340 Nov 13  2017 at_most1.mzn
-[...]<jupyter_text>Transform `dzn` to `fzn` Using a Model `mzn` Then transform the desired `.dzn` files to `.fzn` using a `Mz.mzn` MiniZinc model. First list all `dzn` files contained in the `dzn_path` that should get processed.<jupyter_code>import os

dzn_files = []
dzn_path = f'''/home/{my_env['USER']}/data/dzn/'''

for filename in os.listdir(dzn_path):
    if filename.endswith(".dzn"):
        dzn_files.append(filename)
len(dzn_files)<jupyter_output><empty_output><jupyter_text>Model $Mz_1$<jupyter_code>import sys

fzn_path = f'''/home/{my_env['USER']}/data/fzn/smt2/Mz1-noAbs/'''
minizinc_base_cmd = f'''/home/{my_env['USER']}/minizinc/build/minizinc \
    -Werror \
    --compile --solver org.minizinc.mzn-fzn \
    --search-dir /home/{my_env['USER']}/minizinc/share/minizinc/smt2/ \
    /home/{my_env['USER']}/models/mzn/Mz1-noAbs.mzn '''
translate_count = 0
for dzn in dzn_files:
    translate_count += 1
    minizinc_transform_cmd = minizinc_base_cmd + dzn_path + dzn \
        + ' --output-to-file ' + fzn_path + dzn.replace('.', '-') + '.fzn'
    print(f'''\r({translate_count}/{len(dzn_files)}) Translating {dzn_path + dzn} to {fzn_path + dzn.replace('.', '-')}.fzn''', end='')
    sys.stdout.flush()
    subprocess.check_output(minizinc_transform_cmd, shell=True, 
                                     universal_newlines=True)<jupyter_output>(278/278) Translating /home/jovyan/data/dzn/R028.dzn to /home/jovyan/data/fzn/smt2/Mz1-noAbs/R028-dzn.fzn<jupyter_text>Model $Mz_2$<jupyter_code>import sys

fzn_path = f'''/home/{my_env['USER']}/data/fzn/smt2/Mz2-noAbs/'''
minizinc_base_cmd = f'''/home/{my_env['USER']}/minizinc/build/minizinc \
    -Werror \
    --compile --solver org.minizinc.mzn-fzn \
    --search-dir /home/{my_env['USER']}/minizinc/share/minizinc/smt2/ \
    /home/{my_env['USER']}/models/mzn/Mz2-noAbs.mzn '''
translate_count = 0
for dzn in dzn_files:
    translate_count += 1
    minizinc_transform_cmd = minizinc_base_cmd + dzn_path + dzn \
        + ' --output-to-file ' + fzn_path + dzn.replace('.', '-') + '.fzn'
    print(f'''\r({translate_count}/{len(dzn_files)}) Translating {dzn_path + dzn} to {fzn_path + dzn.replace('.', '-')}.fzn''', end='')
    sys.stdout.flush()
    subprocess.check_output(minizinc_transform_cmd, shell=True, 
                                     universal_newlines=True)<jupyter_output>(278/278) Translating /home/jovyan/data/dzn/R028.dzn to /home/jovyan/data/fzn/smt2/Mz2-noAbs/R028-dzn.fzn<jupyter_text>Translate `fzn` to `smt2` The generated `.fzn` files can be used to generate a `.smt2` files using the `fzn2smt2.py` script from this [project](https://github.com/PatrickTrentin88/fzn2omt).**NOTE**: Files `R001` (no cables) and `R002` (one one-sided cable) throw an error while translating.  $Mz_1$<jupyter_code>import os

fzn_files = []
fzn_path = f'''/home/{my_env['USER']}/data/fzn/smt2/Mz1-noAbs/'''

for filename in os.listdir(fzn_path):
    if filename.endswith(".fzn"):
        fzn_files.append(filename)
len(fzn_files)
smt2_path = f'''/home/{my_env['USER']}/data/smt2/optimathsat/Mz1-noAbs/'''
fzn2smt2_base_cmd = f'''/home/{my_env['USER']}/fzn2omt/bin/fzn2optimathsat.py '''
translate_count = 0
my_env = os.environ.copy()
my_env['PATH'] = f'''/home/{my_env['USER']}/optimathsat/bin/:{my_env['PATH']}'''
for fzn in fzn_files:
    translate_count += 1
    fzn2smt2_transform_cmd = fzn2smt2_base_cmd + fzn_path + fzn \
            + ' --smt2 ' + smt2_path + fzn.replace('.', '-') + '.smt2'
    print(f'''\r({translate_count}/{len(fzn_files)}) Translating {fzn_path + fzn} to {smt2_path + fzn.replace('.', '-')}.smt2''', end='')
    try:
        output = subprocess.check_output(fzn2smt2_transform_cmd, shell=True, env=my_env,
                                     universal_newlines=True, stderr=subprocess.STDOUT)
    except Exception as e:
        output = str(e.output)
    print(f'''\r{output}''', end='')
    sys.stdout.flush()<jupyter_output>Traceback (most recent call last):/data/fzn/smt2/Mz1-noAbs/R001-dzn.fzn to /home/jovyan/data/smt2/optimathsat/Mz1-noAbs/R001-dzn-fzn.smt2
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 360, in <module>
    main()
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 356, in main
    optimathsat(config, solver_config)
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 42, in optimathsat
    optimathsat_compile(config, solver_config)
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 110, in optimathsat_compile
    result = subprocess.run(args, capture_output=True, text=True, check=True)
  File "/srv/conda/envs/notebook/lib/python3.7/subprocess.py", line 512, in run
    output=stdout, stderr=stderr)
subprocess.CalledProcessError: Command '['optimathsat', '-input=fzn', '/home/jovyan/data/fzn/smt2/Mz1-noAbs/R001-dzn.fzn', '-debug.api_call_trace=1', '-debug.api_call_trace_dump_config=False', '-debug.api_call_trace_filename=/home/jovyan/data/smt2/optimathsat/[...]<jupyter_text>$Mz_2$<jupyter_code>import os

fzn_files = []
fzn_path = f'''/home/{my_env['USER']}/data/fzn/smt2/Mz2-noAbs/'''

for filename in os.listdir(fzn_path):
    if filename.endswith(".fzn"):
        fzn_files.append(filename)
len(fzn_files)
smt2_path = f'''/home/{my_env['USER']}/data/smt2/optimathsat/Mz2-noAbs/'''
fzn2smt2_base_cmd = f'''/home/{my_env['USER']}/fzn2omt/bin/fzn2optimathsat.py '''
translate_count = 0
my_env = os.environ.copy()
my_env['PATH'] = f'''/home/{my_env['USER']}/optimathsat/bin/:{my_env['PATH']}'''
for fzn in fzn_files:
    translate_count += 1
    fzn2smt2_transform_cmd = fzn2smt2_base_cmd + fzn_path + fzn \
            + ' --smt2 ' + smt2_path + fzn.replace('.', '-') + '.smt2'
    print(f'''\r({translate_count}/{len(fzn_files)}) Translating {fzn_path + fzn} to {smt2_path + fzn.replace('.', '-')}.smt2''', end='')
    try:
        output = subprocess.check_output(fzn2smt2_transform_cmd, shell=True, env=my_env,
                                     universal_newlines=True, stderr=subprocess.STDOUT)
    except Exception as e:
        output = str(e.output)
    print(f'''\r{output}''', end='')
    sys.stdout.flush()<jupyter_output>Traceback (most recent call last):/data/fzn/smt2/Mz2-noAbs/R001-dzn.fzn to /home/jovyan/data/smt2/optimathsat/Mz2-noAbs/R001-dzn-fzn.smt2
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 360, in <module>
    main()
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 356, in main
    optimathsat(config, solver_config)
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 42, in optimathsat
    optimathsat_compile(config, solver_config)
  File "/home/jovyan/fzn2omt/bin/fzn2optimathsat.py", line 110, in optimathsat_compile
    result = subprocess.run(args, capture_output=True, text=True, check=True)
  File "/srv/conda/envs/notebook/lib/python3.7/subprocess.py", line 512, in run
    output=stdout, stderr=stderr)
subprocess.CalledProcessError: Command '['optimathsat', '-input=fzn', '/home/jovyan/data/fzn/smt2/Mz2-noAbs/R001-dzn.fzn', '-debug.api_call_trace=1', '-debug.api_call_trace_dump_config=False', '-debug.api_call_trace_filename=/home/jovyan/data/smt2/optimathsat/[...]<jupyter_text>Test Generated `smt2` Files Using `OptiMathSAT`This shoud generate the `smt2` file without any error. If this was the case then `OptiMathSAT` can be called on a file by running```zshoptimathsat output/A004-dzn-smt2-fzn.smt2 ```yielding something similar to```zsh                                                     sat(objectives (obj 88))(error "model generation not enabled")unsupported```  Test with `smt2` from $Mz_1$<jupyter_code>try:
    result = subprocess.check_output(
        f'''/home/{my_env['USER']}/optimathsat/bin/optimathsat \
        /home/{my_env['USER']}/data/smt2/optimathsat/Mz1-noAbs/A004-dzn-fzn.smt2''',
        shell=True, universal_newlines=True)
except Exception as e:
    result = str(e.output)
print(result)<jupyter_output>sat

(objectives
 (obj 88)
)
(error "model generation not enabled")
unsupported<jupyter_text>Test with `smt2` from $Mz_2$<jupyter_code>result = subprocess.check_output(
    f'''/home/{my_env['USER']}/optimathsat/bin/optimathsat \
    /home/{my_env['USER']}/data/smt2/optimathsat/Mz2-noAbs/A004-dzn-fzn.smt2''',
    shell=True, universal_newlines=True)
print(result)<jupyter_output>sat

(objectives
 (obj 88)
)
(error "model generation not enabled")
unsupported<jupyter_text>Adjust `smt2` Files According to Chapter 5.2 in PaperContrary to the `z3` version we're dropping the settings and the optimization function for OptiMathSAT `smt2` files, as those are set by the [OMT Python Timeout Wrapper](https://github.com/kw90/omt_python_timeout_wrapper).- Add lower and upper bounds for the decision variable `pfc`- Add number of cavities as comments for later solution extraction (workaround)<jupyter_code>import os
import re

def adjust_smt2_file(smt2_path: str, file: str, write_path: str):

    with open(smt2_path+'/'+file, 'r+') as myfile:
        data = "".join(line for line in myfile)

    filename = os.path.splitext(file)[0]

    newFile = open(os.path.join(write_path, filename +'.smt2'),"w+")
    newFile.write(data)
    newFile.close()

    openFile = open(os.path.join(write_path, filename +'.smt2'))
    data = openFile.readlines()
    additionalLines = data[-6:]
    data = data[:-6]
    openFile.close()

    newFile = open(os.path.join(write_path, filename +'.smt2'),"w+")
    newFile.writelines([item for item in data])
    newFile.close()

    with open(os.path.join(write_path, filename +'.smt2'),"r") as myfile:
        data = "".join(line for line in myfile)
    newFile = open(os.path.join(write_path, filename +'.smt2'),"w+")
    matches = re.findall(r'\(define-fun .\d\d \(\) Int (\d+)\)', data)
    try:
        cavity_count = int(matches[0])
        newFile.write(f''';; k={cavity_count}\n''')
        newFile.write(f''';; Extract pfc from\n''')
        for i in range(0,cavity_count):
            newFile.write(f''';; X_INTRODUCED_{str(i)}_\n''')
        newFile.write(data)
        for i in range(1,cavity_count+1):
            lb = f'''(define-fun lbound{str(i)} () Bool (> X_INTRODUCED_{str(i-1)}_ 0))\n'''
            ub = f'''(define-fun ubound{str(i)} () Bool (<= X_INTRODUCED_{str(i-1)}_ {str(cavity_count)}))\n'''
            assertLb = f'''(assert lbound{str(i)})\n'''
            assertUb = f'''(assert ubound{str(i)})\n'''

            newFile.write(lb)
            newFile.write(ub)
            newFile.write(assertLb)
            newFile.write(assertUb)
    except:
        print(f'''\nCheck {filename} for completeness - data missing?''')

    newFile.close()<jupyter_output><empty_output><jupyter_text>$Mz_1$<jupyter_code>import os

smt2_files = []
smt2_path = f'''/home/{my_env['USER']}/data/smt2/optimathsat/Mz1-noAbs'''

for filename in os.listdir(smt2_path):
    if filename.endswith(".smt2"):
        smt2_files.append(filename)
len(smt2_files)
fix_count = 0
for smt2 in smt2_files:
    fix_count += 1
    print(f'''\r{fix_count}/{len(smt2_files)} Fixing file {smt2}''', end='')
    adjust_smt2_file(smt2_path=smt2_path, file=smt2, write_path=f'''{smt2_path}''')
    sys.stdout.flush()<jupyter_output>49/278 Fixing file R002-dzn-fzn.smt2
Check R002-dzn-fzn for completeness - data missing?
150/278 Fixing file R001-dzn-fzn.smt2
Check R001-dzn-fzn for completeness - data missing?
278/278 Fixing file R166-dzn-fzn.smt2<jupyter_text>$Mz_2$<jupyter_code>import os

smt2_files = []
smt2_path = f'''/home/{my_env['USER']}/data/smt2/optimathsat/Mz2-noAbs'''

for filename in os.listdir(smt2_path):
    if filename.endswith(".smt2"):
        smt2_files.append(filename)
len(smt2_files)
fix_count = 0
for smt2 in smt2_files:
    fix_count += 1
    print(f'''\r{fix_count}/{len(smt2_files)} Fixing file {smt2}''', end='')
    adjust_smt2_file(smt2_path=smt2_path, file=smt2, write_path=f'''{smt2_path}''')
    sys.stdout.flush()<jupyter_output>49/278 Fixing file R002-dzn-fzn.smt2
Check R002-dzn-fzn for completeness - data missing?
150/278 Fixing file R001-dzn-fzn.smt2
Check R001-dzn-fzn for completeness - data missing?
278/278 Fixing file R166-dzn-fzn.smt2
{'fraction_non_alphanumeric': 0.16208597603946442, 'fraction_numerical': 0.036575052854122624, 'mean_word_length': 3.815405497115711, 'pattern_counts': {'":': 0, '<': 58, '<?xml version=': 0, '>': 58, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '12', 'dir': 'jupyter-structured-clean-dedup', 'id': '582767', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 5923, 'n_tokens_neox': 5604, 'n_words': 988, 'path': 'translation_toolchain/scripts/TranslateDZN2SMT2_OptiMathSAT.ipynb', 'repo_name': 'kw90/ctw_translation_toolchain', 'size': '14292'}