slothy-optimizer / slothy

Assembly super-optimization via constraint solving
https://slothy-optimizer.github.io/slothy/
Other
167 stars 10 forks source link

Add config obective_lower_bound #93

Closed mkannwischer closed 1 month ago

mkannwischer commented 1 month ago

Sometimes one already knows a lower bound for an objective (spills, stalls) and searching longer is a waste of compute. This PR adds an option to SLOTHY to provide that lower bound at which SLOTHY stops optimizing.

Usage example (for spill code generation):

        slothy.config.objective_lower_bound = 7
        slothy.config.inputs_are_outputs = True
        slothy.config.constraints.functional_only = True
        slothy.config.constraints.allow_spills = True
        slothy.config.constraints.minimize_spills = True
        slothy.config.constraints.allow_reordering = False
        slothy.optimize(start="layer1234_start", end="layer1234_end")

It also fixes a small error in core.py line 3259 that lead to the following error:

Traceback (most recent call last):
  File "/home/mjk/git/pqmx/slothy/example.py", line 2405, in <module>
    main()
  File "/home/mjk/git/pqmx/slothy/example.py", line 2399, in main
    run_example(e, debug=args.debug, dry_run=args.dry_run,
  File "/home/mjk/git/pqmx/slothy/example.py", line 2395, in run_example
    ex.run(**kwargs)
  File "/home/mjk/git/pqmx/slothy/example.py", line 163, in run
    self.core(slothy, *self.extra_args)
  File "/home/mjk/git/pqmx/slothy/example.py", line 1919, in core
    slothy.optimize(start="layer1234_start", end="layer1234_end")
  File "/home/mjk/git/pqmx/slothy/slothy/core/slothy.py", line 261, in optimize
    early, core, late, num_exceptional = Heuristics.periodic(body, logger, c)
                                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mjk/git/pqmx/slothy/slothy/core/heuristics.py", line 325, in periodic
    res = Heuristics.linear( body, logger=logger, conf=conf)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mjk/git/pqmx/slothy/slothy/core/heuristics.py", line 402, in linear
    return Heuristics.optimize_binsearch(body,logger.getChild("slothy"), conf)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mjk/git/pqmx/slothy/slothy/core/heuristics.py", line 137, in optimize_binsearch
    return Heuristics.optimize_binsearch_external(source, logger, conf,
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/mjk/git/pqmx/slothy/slothy/core/heuristics.py", line 181, in optimize_binsearch_external
    if not core.optimize(source):
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/mjk/git/pqmx/slothy/slothy/core/core.py", line 1470, in optimize
    self._add_objective()
  File "/home/mjk/git/pqmx/slothy/slothy/core/core.py", line 3292, in _add_objective
    self._model.cp_model.Minimize(cp_model.LinearExpr.Sum(minlist))
  File "/home/mjk/git/pqmx/slothy/venv/lib/python3.12/site-packages/ortools/sat/python/cp_model.py", line 2377, in Minimize
    self._SetObjective(obj, minimize=True)
  File "/home/mjk/git/pqmx/slothy/venv/lib/python3.12/site-packages/ortools/sat/python/cp_model.py", line 2373, in _SetObjective
    raise TypeError("TypeError: " + str(obj) + " is not a valid objective")
TypeError: TypeError: [(0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1), (0..1)] is not a valid objective