Skip to content

Commit

Permalink
Add test for FlatZinc JSON output
Browse files Browse the repository at this point in the history
  • Loading branch information
cyderize committed May 14, 2024
1 parent 0b65af0 commit f748de1
Show file tree
Hide file tree
Showing 7 changed files with 201 additions and 8 deletions.
6 changes: 6 additions & 0 deletions changes.rst
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@ MiniZinc Change Log
For detailed bug reports consult the issue tracker at
https://github.com/MiniZinc/libminizinc/issues.

.. _unreleased:

Bug fixes:
^^^^^^^^^^
- Fix specification for constraint items and annotations in FlatZinc JSON.

.. _v2.8.4:

`Version 2.8.4 <https://github.com/MiniZinc/MiniZincIDE/releases/tag/2.8.4>`__
Expand Down
8 changes: 5 additions & 3 deletions tests/conftest.py
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,9 @@ def pytest_addoption(parser):
)


def pytest_collect_file(parent, path):
if path.ext == ".mzn":
return MznFile.from_parent(parent, fspath=path)
def pytest_collect_file(parent, file_path):
if file_path.suffix == ".mzn":
return MznFile.from_parent(parent, path=file_path)


def pytest_html_results_table_header(cells):
Expand Down Expand Up @@ -192,6 +192,8 @@ def solver_allowed(self, solver):
return self.allowed is None or solver in self.allowed

def solver_exists(self, solver):
if solver.endswith(".msc"):
return True
solver_exists = pytest.solver_cache.get(solver, None)
if solver_exists is None:
try:
Expand Down
113 changes: 108 additions & 5 deletions tests/minizinc_testing/spec.py
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,9 @@
from minizinc.helpers import check_result
import pathlib
import re
from json import load, dumps
import jsonschema
import warnings


@yaml.mapping("!Test")
Expand Down Expand Up @@ -50,15 +53,22 @@ def run(self, mzn_file, solver, default_options={}):
try:
model = mzn.Model([file] + extra_files)
model.output_type = Solution
solver = mzn.Solver.lookup(solver)
if solver.endswith(".msc"):
solver = mzn.Solver.load(file.parent.joinpath(solver))
else:
solver = mzn.Solver.lookup(solver)
instance = mzn.Instance(solver, model)
if self.type == "solve":
result = instance.solve(**options)
obtained = Result.from_mzn(result)
elif self.type == "compile":
with instance.flat(**options) as (fzn, ozn, stats):
obtained = FlatZinc.from_mzn(fzn, file.parent)
result = obtained
if solver.inputType == "JSON":
obtained = FlatZincJSON.from_mzn(fzn, file.parent)
result = obtained
else:
obtained = FlatZinc.from_mzn(fzn, file.parent)
result = obtained
elif self.type == "output-model":
with instance.flat(**options) as (fzn, ozn, stats):
obtained = OutputModel.from_mzn(ozn, file.parent)
Expand Down Expand Up @@ -311,7 +321,7 @@ def normalized(self):
lines = [
re.sub(
r"::[^;]*",
ann_sort,
ann_sort,
re.sub(r" +", " ", line),
count=1,
)
Expand Down Expand Up @@ -339,11 +349,104 @@ def from_mzn(fzn, base):
instance.base = base
return instance


def ann_sort(match):
s = match.group(0)
anns = sorted([ann for ann in s.split('::') if ann != ""])
anns = sorted([ann for ann in s.split("::") if ann != ""])
return "::" + "::".join(anns)


@yaml.scalar("!FlatZincJSON")
class FlatZincJSON:
"""
A FlatZinc JSON result, encoded by !FlatZincJSON in YAML.
"""

def __init__(self, path):
self.path = path
self.base = None
self.fzn = None

def check(self, actual):
if not isinstance(actual, FlatZincJSON):
return False

if self.fzn is None:
with open(actual.base.joinpath(self.path), encoding="utf-8") as f:
self.fzn = load(f)

obtained = actual.normalized()

schema_path = (
pathlib.Path(__file__).parent.parent.parent / "docs/en/fznjson.json"
)
if schema_path.exists():
with open(schema_path, encoding="utf-8") as fp:
schema = load(fp)
jsonschema.validate(instance=obtained, schema=schema)
else:
warnings.warn(
"Unable to find FlatZinc JSON schema. Cannot verify validity."
)

return self.normalized() == obtained

def normalized(self):
var_nums = set()
for v in list(self.fzn["variables"].keys()) + list(self.fzn["arrays"].keys()):
m = re.match(r"X_INTRODUCED_(\d+)_", v)
if m is not None:
var_nums.add(int(m.group(1)))
var_map = {
f"X_INTRODUCED_{src}_": f"X_INTRODUCED_{dst}_"
for dst, src in enumerate(sorted(var_nums))
}

def get_ident(obj):
if isinstance(obj, dict):
return obj.get("id")
return obj

def walk(obj, key=None):
if isinstance(obj, dict):
return {walk(k): walk(v, k) for k, v in obj.items()}
if isinstance(obj, list):
items = [walk(v) for v in obj]
if key == "ann":
return sorted(items, key=get_ident)
return items
if isinstance(obj, str):
return var_map.get(obj, obj)
return obj

return walk(self.fzn)

def get_value(self):
if self.fzn is None:
return self.path
return dumps(self.normalized())

@staticmethod
def from_mzn(fzn, base):
"""
Creates a `FlatZinc` object from a `File` returned by `flat()` in the minizinc interface.
Also takes the base path the mzn file was from, so that when loading the expected fzn file
it can be done relative to the mzn path.
"""
with open(fzn.name, encoding="utf-8") as file:
instance = FlatZincJSON(None)
instance.fzn = load(file)
instance.base = base
return instance


def ann_sort(match):
s = match.group(0)
anns = sorted([ann for ann in s.split("::") if ann != ""])
return "::" + "::".join(anns)


@yaml.scalar("!OutputModel")
class OutputModel:
"""
Expand Down
1 change: 1 addition & 0 deletions tests/requirements.txt
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
jsonschema==4.*
PyYAML==6.0.1
pytest==7.*
py==1.11.*
Expand Down
59 changes: 59 additions & 0 deletions tests/spec/unit/fznjson/fznjson-basic.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
{
"variables": {
"x": { "type": "int", "domain": [[1, 3]] },
"y": { "type": "int", "domain": [[1, 3]] },
"b": { "type": "bool", "defined": true },
"X_INTRODUCED_3_": { "type": "bool", "introduced": true, "defined": true }
},
"arrays": {
"X_INTRODUCED_0_": { "a": [1, -1] },
"X_INTRODUCED_1_": { "a": [1, 1] },
"X_INTRODUCED_4_": { "a": ["b"] },
"X_INTRODUCED_5_": { "a": ["x", "y"] }
},
"constraints": [
{ "id": "bool_clause", "args": [["X_INTRODUCED_3_"], ["b"]] },
{
"id": "int_lin_le_reif",
"args": ["X_INTRODUCED_0_", ["x", "y"], -1, "b"],
"defines": "b"
},
{
"id": "int_lin_le_reif",
"args": ["X_INTRODUCED_1_", ["x", "y"], 3, "X_INTRODUCED_3_"],
"defines": "X_INTRODUCED_3_"
}
],
"output": ["x", "y"],
"solve": {
"method": "satisfy",
"ann": [
{
"id": "seq_search",
"args": [
[
{
"id": "int_search",
"args": [
"X_INTRODUCED_5_",
"input_order",
"indomain_min",
"complete"
]
},
{
"id": "bool_search",
"args": [
"X_INTRODUCED_4_",
"input_order",
"indomain_min",
"complete"
]
}
]
]
}
]
},
"version": "1.0"
}
16 changes: 16 additions & 0 deletions tests/spec/unit/fznjson/fznjson-basic.mzn
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
/***
--- !Test
type: compile
solvers: [fznjson.msc]
expected: !FlatZincJSON fznjson-basic.json
***/

var 1..3: x;
var 1..3: y;
var bool: b = x < y;
constraint b -> x + y < 4;

solve :: seq_search([
int_search([x, y], input_order, indomain_min),
bool_search([b], input_order, indomain_min),
]) satisfy;
6 changes: 6 additions & 0 deletions tests/spec/unit/fznjson/fznjson.msc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"id": "org.minizinc.mzn-fzn",
"version": "0.1.0",
"name": "fznjson",
"inputType": "JSON"
}

0 comments on commit f748de1

Please sign in to comment.