Improve logging & argument no solve

cpmpy/solvers/exact.py

@@ -409,7 +409,7 @@ def transform(self, cpm_expr):
         """
 
         starts = time.time()
-        expr_store = get_store()
+        expr_store = self.expr_store
 
         # apply transformations, then post internally
         # expressions have to be linearized to fit in MIP model. See /transformations/linearize

cpmpy/solvers/gurobi.py

@@ -26,6 +26,8 @@
     ==============
 """
 
+import time
+
 from .solver_interface import SolverInterface, SolverStatus, ExitStatus
 from ..expressions.core import *
 from ..expressions.utils import argvals
@@ -270,18 +272,49 @@ def transform(self, cpm_expr):
 
         :return: list of Expression
         """
+
+        starts = time.time()
+
+        expr_store = self.expr_store
+
+        start = time.time()
+        cpm_cons = toplevel_list(cpm_expr)
+        print(f"gurobi:toplevel_list took {(time.time()-start):.4f} -- {len(cpm_expr)}")
         # apply transformations, then post internally
         # expressions have to be linearized to fit in MIP model. See /transformations/linearize
+        start = time.time()
         cpm_cons = toplevel_list(cpm_expr)
+        print(f"gurobi:toplevel_list took {(time.time()-start):.4f} -- {len(cpm_cons)}")
         supported = {"min", "max", "abs", "alldifferent"} # alldiff has a specialized MIP decomp in linearize
-        cpm_cons = decompose_in_tree(cpm_cons, supported)
-        cpm_cons = flatten_constraint(cpm_cons)  # flat normal form
-        cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']))  # constraints that support reification
-        cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]))  # supports >, <, !=
-        cpm_cons = only_bv_reifies(cpm_cons)
-        cpm_cons = only_implies(cpm_cons)  # anything that can create full reif should go above...
-        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","sub","min","max","mul","abs","pow","div"}))  # the core of the MIP-linearization
-        cpm_cons = only_positive_bv(cpm_cons)  # after linearization, rewrite ~bv into 1-bv
+        start = time.time()
+        cpm_cons = decompose_in_tree(cpm_cons, supported, expr_store=expr_store)
+        print(f"gurobi:decompose_in_tree took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = flatten_constraint(cpm_cons, expr_store=expr_store)  # flat normal form
+        print(f"gurobi:flatten_constraint took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum']), expr_store=expr_store)  # constraints that support reification
+        print(f"gurobi:reify_rewrite took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum", "sub"]), expr_store=expr_store)  # supports >, <, !=
+        print(f"gurobi:only_numexpr_equality took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = only_bv_reifies(cpm_cons, expr_store=expr_store)
+        print(f"gurobi:only_bv_reifies took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = only_implies(cpm_cons, expr_store=expr_store)  # anything that can create full reif should go above...
+        print(f"gurobi:only_implies took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum", "wsum","sub","min","max","mul","abs","pow","div"}), expr_store=expr_store)  # the core of the MIP-linearization
+        print(f"gurobi:linearize_constraint took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+        start = time.time()
+        cpm_cons = only_positive_bv(cpm_cons, expr_store=expr_store)  # after linearization, rewrite ~bv into 1-bv
+        print(f"gurobi:only_positive_bv took {(time.time()-start):.4f} -- {len(cpm_cons)}")
+
+        print(f"gurobi:transformation took {(time.time()-starts):.4f}")
+        print("final size", len(cpm_cons))
+        print("STORE:", len(expr_store.items()))
+
         return cpm_cons
 
     def __add__(self, cpm_expr_orig):

xcsp3/executable/main.py

@@ -205,6 +205,7 @@ class Args:
     intermediate:bool=False
     sat:bool=False
     opt:bool=False
+    solve:bool=True
 
     def __post_init__(self):
         if self.dir is not None:
@@ -229,6 +230,7 @@ def from_cli(args):
             subsolver = args.subsolver if args.subsolver is not None else None,
             time_buffer = args.time_buffer if args.time_buffer is not None else TIME_BUFFER,
             intermediate = args.intermediate if args.intermediate is not None else False,
+            solve = not args.only_transform,
         )
 
     @property
@@ -344,7 +346,7 @@ def gurobi_arguments(args: Args, model:cp.Model):
         "Threads": args.cores,
     }
     if args.intermediate:
-        res |= { "solution_callback": Callback(model, lambda x,_: x.getObjective().getValue()).callback }
+        res |= { "solution_callback": Callback(model, lambda x,_: int(x.getObjective().getValue())).callback }
     return {k:v for (k,v) in res.items() if v is not None}
 
 def solver_arguments(args: Args, model:cp.Model):
@@ -368,6 +370,8 @@ def subsolver_arguments(args: Args, model:cp.Model):
 
 def main():
 
+    start = time.time()
+
     # ------------------------------ Argument parsing ------------------------------ #
 
     parser = argparse.ArgumentParser(
@@ -402,15 +406,16 @@ def main():
     parser.add_argument("--time_buffer", required=False, type=int)
     # If intermediate solutions should be printed (if the solver supports it)
     parser.add_argument("--intermediate", action=argparse.BooleanOptionalAction)
+    # Disable solving, only do transformation
+    parser.add_argument("--only-transform", action=argparse.BooleanOptionalAction)
 
-    # Process cli arguments
-
+    # Process cli arguments 
     args = Args.from_cli(parser.parse_args())
     print_comment(str(args))
 
-    run(args)
+    run(args, start_time=start)
 
-def run(args: Args):
+def run(args: Args, start_time=None):
     import sys, os
 
     # --------------------------- Global Configuration --------------------------- #
@@ -480,17 +485,18 @@ def run(args: Args):
         print_status(ExitStatus.unknown)
         return 
 
-    start = time.time()
-    try:
-        sat = s.solve(
-            time_limit=time_limit,
-            **solver_arguments(args, model)
-        ) 
-        print_comment(f"took {(time.time() - start):.4f} seconds to solve")
-    except MemoryError:
-        print_comment("Ran out of memory when trying to solve.")
-    except GurobiError as e:
-        print_comment("Error from Gurobi: " + str(e))
+    if args.solve:
+        try:
+            start = time.time()
+            sat = s.solve(
+                time_limit=time_limit,
+                **solver_arguments(args, model)
+            ) 
+            print_comment(f"took {(time.time() - start):.4f} seconds to solve")
+        except MemoryError:
+            print_comment("Ran out of memory when trying to solve.")
+        except GurobiError as e:
+            print_comment("Error from Gurobi: " + str(e))
 
 
     # ------------------------------- Print result ------------------------------- #
@@ -507,6 +513,9 @@ def run(args: Args):
         print_status(ExitStatus.unknown)
     else:
         print_status(ExitStatus.unknown)
+
+    if start_time is not None:
+        print_comment(f"Total time taken: {time.time() - start_time}")
 
 
 if __name__ == "__main__":