Handle KeyboardInterupt to terminate

dtree_synth.py

@@ -177,6 +177,9 @@ def main():
                 result.append({"part": part,
                                "status": "not found",
                                "result": ret})
+        except KeyboardInterrupt:
+            print("User pressed Ctrl+C. Skip all remaining partition.")
+            break  # NOTE finally block is executed before break
         except Exception as e:
             result.append({"part": part,
                            "status": "exception",

dtree_teacher_gem_stanley.py

@@ -140,9 +140,10 @@ class DTreeGEMStanleyGurobiTeacher(GEMStanleyGurobiTeacher):
                 else:
                     # raise RuntimeError(f"Only found spurious cexs {cex_list} for the conjunct {conjunct}.")
                     pass
-
             elif self._gp_model.status == gp.GRB.INFEASIBLE:
                 continue
+            elif self._gp_model.status == gp.GRB.INTERRUPTED:
+                raise KeyboardInterrupt
             else:
                 return z3.unknown
         print("Done")