Improve compatibility with CP-SAT via configurable model export

example.py

@@ -88,7 +88,7 @@ def __init__(self, infile, name=None, funcname=None, suffix="opt",
     def core(self, slothy):
         slothy.optimize()
 
-    def run(self, debug=False, dry_run=False, silent=False, timeout=0):
+    def run(self, debug=False, log_model=False, dry_run=False, silent=False, timeout=0):
 
         if dry_run is True:
             annotation = " (dry run only)"
@@ -140,6 +140,9 @@ def run(self, debug=False, dry_run=False, silent=False, timeout=0):
             slothy.config.constraints.allow_renaming = False
             slothy.config.variable_size = True
 
+        if log_model is True:
+            slothy.config.log_model = f"{self.name}_model.txt"
+
         # On Apple M1, we must not use x18
         if "m1" in target_label_dict[self.target]:
             self.target_reserved = ["x18"]
@@ -1066,6 +1069,8 @@ def __init__(self, var="", arch=AArch64_Neon, target=Target_CortexA55):
     def core(self, slothy):
         slothy.config.sw_pipelining.enabled = True
         slothy.config.inputs_are_outputs = True
+        slothy.config.constraints.stalls_first_attempt = 160
+        slothy.config.constraints.stalls_minimum_attempt = 160
         slothy.config.sw_pipelining.minimize_overlapping = False
         slothy.config.sw_pipelining.optimize_preamble = False
         slothy.config.sw_pipelining.optimize_postamble = False
@@ -1329,6 +1334,7 @@ def main():
                  ntt_dilithium_123_456_78(False, target=Target_CortexM85r1),
                  ntt_dilithium_123_456_78(True, target=Target_CortexM85r1),
                  # Cortex-A55
+                 ntt_dilithium_45678(),
                  ntt_dilithium_123_45678(),
                  ntt_dilithium_123_45678(var="w_scalar"),
                  ntt_dilithium_123_45678(var="manual_st4"),
@@ -1377,6 +1383,7 @@ def main():
     parser.add_argument("--silent", default=False, action="store_true")
     parser.add_argument("--iterations", type=int, default=1)
     parser.add_argument("--timeout", type=int, default=0)
+    parser.add_argument("--log-model", default=False, action="store_true")
 
     args = parser.parse_args()
     if args.examples != "all":
@@ -1398,7 +1405,7 @@ def run_example(name, **kwargs):
     for e in todo:
         for _ in range(iterations):
             run_example(e, debug=args.debug, dry_run=args.dry_run,
-                        silent=args.silent, timeout=args.timeout)
+                        silent=args.silent, log_model=args.log_model, timeout=args.timeout)
 
 if __name__ == "__main__":
     main()

slothy/core/config.py

@@ -1052,6 +1052,8 @@ def __init__(self, Arch, Target):
 
         self.solver_random_seed = 42
 
+        # TODO: Document log_dir and log_model
+        self.log_model = None
         self.log_dir = "logs/"
         if not os.path.exists(self.log_dir):
             os.makedirs(self.log_dir)

slothy/core/core.py

@@ -1191,7 +1191,7 @@ def optimize(self, source, prefix_len=0, suffix_len=0, log_model=None, retry=Fal
         # - Objective
         self._add_objective()
         # - Export (optional)
-        self._export_model(log_model)
+        self._export_model()
 
         self._result = Result(self.config)
 
@@ -2926,11 +2926,12 @@ def _AddHint(self,var,val): # pylint:disable=invalid-name
     def _AddNoOverlap(self,interval_list): # pylint:disable=invalid-name
         return self._model.cp_model.AddNoOverlap(interval_list)
 
-    def _export_model(self, log_model):
-        if log_model is None:
+    def _export_model(self):
+        if self.config.log_model is None:
             return
-        self.logger.info("Writing model to %s...", log_model)
-        assert self._model.cp_model.ExportToFile(self.config.log_dir + "/" + log_model)
+        log_file = self.config.log_dir + "/" + self.config.log_model
+        self.logger.info("Writing model to %s ...", log_file)
+        assert self._model.cp_model.ExportToFile(log_file)
 
     def _solve(self):