A set of benchmarks to compare a new prototype MiniZinc implementation
dekker.one
1#!/usr/bin/env python3
2import minizinc
3import sys
4import os
5import re
6import time
7import subprocess
8from pathlib import Path
9
10MZNCC = "/Users/jdek0001/Dropbox/development/minizinc.byte/build/Release/mzncc"
11MZNASM = "/Users/jdek0001/Dropbox/development/minizinc.byte/build/Release/mznasm"
12
13# Instances Selection (File location)
14if len(sys.argv) < 4:
15 print("Usage: test_solve.py <solver/library> <output_var> <model> <data_file>?")
16 exit(1)
17
18solver = sys.argv[1]
19outputvar = sys.argv[2]
20model = Path(sys.argv[3])
21data = None
22if len(sys.argv) > 4:
23 data = Path(sys.argv[4])
24
25# Extend model with `output_this`
26model_bin = model.read_bytes()
27model_bin += bytes(f"constraint output_this({outputvar});", encoding='utf8')
28Path("_temp.mzn").write_bytes(model_bin)
29
30# Compile model using MZNCC
31os.system(f"{MZNCC} -G{solver} _temp.mzn > _temp.uzn")
32
33# Flatten/Run model using MZNASM
34cmd = [
35 MZNASM,
36 "--solver",
37 solver,
38 "-t",
39 str(20000),
40 "-f",
41 "_temp.uzn",
42]
43if data:
44 cmd.append(data)
45output = subprocess.run(cmd, capture_output=True,)
46if output.stderr:
47 print(f"mznasm stderr:\n {output.stderr.decode('utf-8')}")
48if b"=====ERROR=====" in output.stdout:
49 print("=====ERROR=====")
50 exit(1)
51elif b"=====UNKNOWN=====" in output.stdout:
52 print("=====UNKNOWN=====")
53 exit(1)
54elif b"=====UNSATISFIABLE=====" in output.stdout:
55 print("=====UNSATISFIABLE=====")
56 exit(1)
57elif (b"=====UNSATorUNBOUNDED=====" in output.stdout or b"=====UNBOUNDED=====" in output.stdout):
58 print("=====UNSATISFIABLE=====")
59 exit(1)
60
61filtered = re.sub(
62 rb"^-{10}|={5}(ERROR|UNKNOWN|UNSATISFIABLE|UNSATorUNBOUNDED|UNBOUNDED|)?={5}",
63 b"",
64 output.stdout,
65 flags=re.MULTILINE,
66)
67filtered = re.sub(rb"^\w*%.*\n?", b"", filtered, flags=re.MULTILINE)
68
69if output.returncode != 0:
70 print(
71 f"mznasm ({cmd}) ERROR {output.returncode}: \n{str(output.stderr)}\n",
72 file=sys.stderr,
73 )
74 exit(1)
75
76gecode = minizinc.Solver.lookup("gecode")
77check_inst = minizinc.Instance(gecode)
78check_inst.add_file(model)
79if data:
80 check_inst.add_file(data, parse_data=False)
81
82check_inst.add_string(f"constraint {outputvar} = {filtered.decode('utf-8')};")
83
84sol = check_inst.solve()
85print(f"Status: {sol.status}")
86print(sol)