From d78143a7ab8e6b7df9f924cfe914edf4dc8080ce Mon Sep 17 00:00:00 2001
From: Thomas Paviot <tpaviot@gmail.com>
Date: Mon, 8 Jan 2024 12:09:58 +0100
Subject: [PATCH] Improve unsatisfied result report

---
 processscheduler/solver.py | 34 ++++++++++++++++++++--------------
 1 file changed, 20 insertions(+), 14 deletions(-)

diff --git a/processscheduler/solver.py b/processscheduler/solver.py
index a1f037c1..a694eacf 100644
--- a/processscheduler/solver.py
+++ b/processscheduler/solver.py
@@ -26,6 +26,12 @@
 
 import z3
 
+# use rich print if available
+try:
+    from rich import print
+except ImportError:
+    pass
+
 from pydantic import Field, PositiveFloat, Extra, ConfigDict
 
 from processscheduler.base import BaseModelWithJson
@@ -47,7 +53,6 @@
     clean_buffer_states,
 )
 
-
 #
 # Solver class definition
 #
@@ -101,7 +106,7 @@ def __init__(self, **data) -> None:
         super().__init__(**data)
         self._objective = None  # the list of all objectives defined in this problem
         self._current_solution = None  # no solution until the problem is solved
-        self._map_boolrefs_to_geometric_constraints = {}
+        self._map_boolrefs_to_constraints = {}
         self._initialized = False
 
         if self.debug:
@@ -390,7 +395,7 @@ def append_z3_assertion(self, assts, higher_constraint_name=None) -> bool:
                 # if the higher_contraint_name is defined, fill in the map_boolrefs_to_geometric_constraints dict
                 # to track the constraint that causes the conflict
                 if higher_constraint_name is not None:
-                    self._map_boolrefs_to_geometric_constraints[
+                    self._map_boolrefs_to_constraints[
                         asst_identifier
                     ] = higher_constraint_name
         else:
@@ -644,24 +649,25 @@ def solve(self) -> Union[bool, SchedulingSolution]:
                     unknown_asst_origins = []
                     for asst in unsat_core:
                         # look for an entry in the map dict
-                        if f"{asst}" in self._map_boolrefs_to_geometric_constraints:
-                            constraint = self._map_boolrefs_to_geometric_constraints[
+                        if f"{asst}" in self._map_boolrefs_to_constraints:
+                            constraint_name = self._map_boolrefs_to_constraints[
                                 f"{asst}"
                             ]
-                            conflicting_contraits.append(constraint)
+                            conflicting_contraits.append(self.problem.constraints[constraint_name])
                         else:
                             unknown_asst_origins.append(f"{asst}")
                     print(
-                        f"\tUnsatisfied assertions - conflict between {len(conflicting_contraits)} constraints:"
+                        f"\tUnsatisfied constraints - conflict between {len(conflicting_contraits)} constraints:"
                     )
                     for c in conflicting_contraits:
-                        print(f"\t\t-> {c}")
-                    print(
-                        f"\tUnknown assertion origins ({len(unknown_asst_origins)} conflicts):"
-                    )
-                    for a in unknown_asst_origins:
-                        print(f"\t\t-> {a}")
-                    # look the entry
+                        print("\t -> ", end="")
+                        print(c)
+                        print("====")
+                    #print(
+                    #    f"\tUnknown assertion origins ({len(unknown_asst_origins)} conflicts):"
+                    #)
+                    #for a in unknown_asst_origins:
+                    #    print(f"\t\t-> {a}")
                 return False
 
             if sat_result == z3.unknown: