Source code for minizinc.result

#  This Source Code Form is subject to the terms of the Mozilla Public
#  License, v. 2.0. If a copy of the MPL was not distributed with this
#  file, You can obtain one at http://mozilla.org/MPL/2.0/.

import re
from dataclasses import dataclass
from datetime import timedelta
from enum import Enum, auto
from json import loads
from typing import Any, Dict, List, Optional, Tuple, Type, Union

from .json import MZNJSONDecoder
from .model import Method

StatisticsType = Union[float, int, str, timedelta]

StdStatisticTypes = {
    # Number of search nodes
    "nodes": int,
    # Number of leaf nodes that were failed
    "failures": int,
    # Number of times the solver restarted the search
    "restarts": int,
    # Number of variables
    "variables": int,
    # Number of integer variables created by the solver
    "intVariables": int,
    # Number of Boolean variables created by the solver
    "boolVariables": int,
    # Number of floating point variables created by the solver
    "floatVariables": int,
    # Number of set variables created by the solver
    "setVariables": int,
    # Number of propagators created by the solver
    "propagators": int,
    # Number of propagator invocations
    "propagations": int,
    # Peak depth of search tree
    "peakDepth": int,
    # Number of nogoods created
    "nogoods": int,
    # Number of backjumps
    "backjumps": int,
    # Peak memory (in Mbytes)
    "peakMem": float,
    # Initialisation time
    "initTime": timedelta,
    # Solving time
    "solveTime": timedelta,
    # Flattening time
    "flatTime": timedelta,
    # Number of paths generated
    "paths": int,
    # Number of Boolean variables in the flat model
    "flatBoolVars": int,
    # Number of floating point variables in the flat model
    "flatFloatVars": int,
    # Number of integer variables in the flat model
    "flatIntVars": int,
    # Number of set variables in the flat model
    "flatSetVars": int,
    # Number of Boolean constraints in the flat model
    "flatBoolConstraints": int,
    # Number of floating point constraints in the flat model
    "flatFloatConstraints": int,
    # Number of integer constraints in the flat model
    "flatIntConstraints": int,
    # Number of set constraints in the flat model
    "flatSetConstraints": int,
    # Optimisation method in the Flat Model
    "method": str,
    # Number of reified constraints evaluated during flattening
    "evaluatedReifiedConstraints": int,
    # Number of half-reified constraints evaluated during flattening
    "evaluatedHalfReifiedConstraints": int,
    # Number of implications removed through chain compression
    "eliminatedImplications": int,
    # Number of linear constraints removed through chain compression
    "eliminatedLinearConstraints": int,
}


def set_stat(stats: Dict[str, StatisticsType], name: str, value: str):
    """Set statistical value in the result object.

    Set solving statiscal value within the result object. This value is
    converted from string to the appropriate type as suggested by the
    statistical documentation in MiniZinc. Timing statistics, expressed through
    floating point numbers in MiniZinc, will be converted to timedelta objects.

    Args:
        stats: The dictionary to be extended with the new statistical value
        name: The name under which the statistical value will be stored.
        value: The value for the statistical value to be converted and stored.

    """
    value = value.strip('"')
    tt = StdStatisticTypes.get(name, None)
    if tt is None and ("time" in name or "Time" in name):
        tt = timedelta
    try:
        if tt is timedelta:
            time_us = int(float(value) * 1000000)
            stats[name] = timedelta(microseconds=time_us)
        elif tt is not None:
            stats[name] = tt(value)
        else:
            try:
                stats[name] = int(value)
            except ValueError:
                stats[name] = float(value)
    except ValueError:
        stats[name] = value


[docs]class Status(Enum): """Enumeration to represent the status of the solving process. Attributes: ERROR: An error occurred during the solving process. UNKNOWN: No solutions have been found and search has terminated without exploring the whole search space. UNBOUNDED: The objective of the optimisation problem is unbounded. UNSATISFIABLE: No solutions have been found and the whole search space was explored. SATISFIED: A solution was found, but possibly not the whole search space was explored. ALL_SOLUTIONS: All solutions in the search space have been found. OPTIMAL_SOLUTION: A solution has been found that is optimal according to the objective. """ ERROR = auto() UNKNOWN = auto() UNBOUNDED = auto() UNSATISFIABLE = auto() SATISFIED = auto() ALL_SOLUTIONS = auto() OPTIMAL_SOLUTION = auto() @classmethod def from_output(cls, output: bytes, method: Method): """Determines the solving status from the output of a MiniZinc process Determines the solving status according to the standard status output strings defined by MiniZinc. The output of the MiniZinc will be scanned in a defined order to best determine the status of the solving process. UNKNOWN will be returned if no status can be determined. Args: output (bytes): the standard output of a MiniZinc process. method (Method): the objective method used in the optimisation problem. Returns: Optional[Status]: Status that could be determined from the output. """ s = None if b"=====ERROR=====" in output: s = cls.ERROR elif b"=====UNKNOWN=====" in output: s = cls.UNKNOWN elif b"=====UNSATISFIABLE=====" in output: s = cls.UNSATISFIABLE elif ( b"=====UNSATorUNBOUNDED=====" in output or b"=====UNBOUNDED=====" in output ): s = cls.UNBOUNDED elif method is Method.SATISFY: if b"==========" in output: s = cls.ALL_SOLUTIONS elif b"----------" in output: s = cls.SATISFIED else: if b"==========" in output: s = cls.OPTIMAL_SOLUTION elif b"----------" in output: s = cls.SATISFIED return s @classmethod def from_str(cls, status: str): s = None if status == "ERROR": s = cls.ERROR elif status == "UNKNOWN": s = cls.UNKNOWN elif status == "UNBOUNDED" or status == "UNSAT_OR_UNBOUNDED": s = cls.UNBOUNDED elif status == "UNSATISFIABLE": s = cls.UNSATISFIABLE elif status == "SATISFIED": s = cls.SATISFIED elif status == "ALL_SOLUTIONS": s = cls.ALL_SOLUTIONS elif status == "OPTIMAL_SOLUTION": s = cls.OPTIMAL_SOLUTION return s def __str__(self): return self.name
[docs] def has_solution(self) -> bool: """Returns true if the status suggest that a solution has been found.""" if self in [self.SATISFIED, self.ALL_SOLUTIONS, self.OPTIMAL_SOLUTION]: return True return False
[docs]@dataclass class Result: """Representation of a MiniZinc solution in Python Attributes: status (Status): The solving status of the MiniZinc instance solution (Any): Variable assignments made to form the solution statistics (Dict[str, Union[float, int, timedelta]]): Statistical information generated during the search for the Solution """ status: Status solution: Any statistics: Dict[str, Union[float, int, timedelta]] @property def objective(self) -> Optional[Union[int, float]]: """Returns objective of the solution Returns the objective of the solution when possible. If no solutions have been found or the problem did not have an objective, then None is returned instead. Returns: Optional[Union[int, float]]: best objective found or None """ if self.solution is not None: if isinstance(self.solution, list): return getattr(self.solution[-1], "objective", None) else: return getattr(self.solution, "objective", None) else: return None
[docs] def __getitem__(self, key): """Retrieves solution or a member of a solution. Overrides the default implementation of item access (obj[key]) to retrieve a solution object or member of a solution from the result object. - If the Result object does not contain any solutions, then a KeyError will always be raised. - If the Result object contains a single solutions, then the names of a variable can be used in this method to retrieve its value in the solution. - If the Result object contains multiple solutions, then a single integer can be used to retrieve the solution object or a tuple of an integer and the name of a variable can be used to retrieve the value of that variable in the numbered solution object. Args: key: solution number or name of the solution member. Returns: Solution object or the value of the member in the solution. Raises: KeyError: No solution was found, solution number is out of range, or no solution member with this name exists. """ try: if self.solution is not None: if isinstance(self.solution, list): if isinstance(key, tuple): return getattr(self.solution.__getitem__(key[0]), key[1]) else: return self.solution.__getitem__(key) else: return getattr(self.solution, key) else: raise KeyError except AttributeError: raise KeyError
[docs] def __len__(self): """Returns the number of solutions included in the Result object Returns: int: number of solution that can be accessed """ if self.solution is None: return 0 elif isinstance(self.solution, list): return len(self.solution) else: return 1
def __str__(self): return str(self.solution)
def parse_solution( raw: bytes, output_type: Type, enum_map: Optional[Dict[str, Enum]] = None, renames: Optional[List[Tuple[str, str]]] = None, ) -> Tuple[Optional[Any], Dict]: """Parses a solution from the output of a MiniZinc process. Parses the MiniZinc output between solution separators. The solution is expected to be formatted according to the MiniZinc JSON standards. Statistical information can be included in the output in accordance with the MiniZinc statistics standard. Statistics will be parsed and retyped according to the types given in StatisticTypes. Statistics will be parsed even if no solution is found. Args: raw (bytes): The output on stdout for one solution of the process solving the MiniZinc instance. output_type (Type): The type used for every solution enum_map (Optional[Dict[str, Enum]]): A map to map enumeration identifiers to the internal values used in Python ranames (Optional[List[Tuple[str, str]]]): A list of keys to be renamed from the raw solution to the solution object input Returns: Tuple[Optional[Dict], Dict]: A tuple containing the parsed solution assignments and the parsed statistics. """ if enum_map is None: enum_map = {} if renames is None: renames = [] # Parse statistics statistics: Dict[str, StatisticsType] = {} matches = re.findall(rb"%%%mzn-stat:? (\w*)=([^\r\n]*)", raw) for m in matches: set_stat(statistics, m[0].decode(), m[1].decode()) match = re.search(rb"% time elapsed: (\d+.\d+) s", raw) if match: time_us = int(float(match[1]) * 1000000) statistics["time"] = timedelta(microseconds=time_us) # Parse solution solution = None raw = re.sub( rb"^-{10}|={5}(ERROR|UNKNOWN|UNSATISFIABLE|UNSATorUNBOUNDED|UNBOUNDED|)?={5}", b"", raw, flags=re.MULTILINE, ) raw = re.sub(rb"^\w*%.*\n?", b"", raw, flags=re.MULTILINE) if b"{" in raw: tmp = loads(raw, enum_map=enum_map, cls=MZNJSONDecoder) if "_objective" in tmp: tmp["objective"] = tmp.pop("_objective") if "_output" in tmp: tmp["_output_item"] = tmp.pop("_output") for before, after in renames: tmp[after] = tmp.pop(before) solution = output_type(**tmp) return solution, statistics