Skip to content

module cvc5ml

solverpy_learn.builder.cvc5ml

Cvc5ML

Bases: AutoTuner

AutoTuner that trains an ML-enhanced cvc5 strategy: apply/template produce an -ml-suffixed sid pointing at the trained model.

Source code in packages/solverpy-learn/src/solverpy_learn/builder/cvc5ml.py
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
class Cvc5ML(AutoTuner):
   """
   [`AutoTuner`][solverpy_learn.builder.autotuner.AutoTuner] that trains an
   ML-enhanced cvc5 strategy: `apply`/`template` produce an `-ml`-suffixed
   sid pointing at the trained model.
   """

   def __init__(
      self,
      setup: Setup,
      tuneargs: (dict[str, Any] | None) = None,
   ):
      AutoTuner.__init__(
         self,
         setup,
         tuneargs,
      )

   def template(self, sid : str) -> str:
      "`sid` must be base strategy without parameters"
      if sid.endswith("-ml"):
         logger.debug(f"strategy {sid} already ml-enhanced")
         return sid
      sidml = f"{sid}-ml"
      if os.path.exists(sids.path(sidml)):
         logger.debug(f"ml strategy {sidml} already exists")
         return sidml
      dbpath = bids.dbpath(NAME)
      mod = f"{dbpath}/@@@model:default@@@/model.lgb"
      strat = sids.load(sid).rstrip()
      strat = self.mlstrat(strat, mod)
      sids.save(sidml, strat)
      logger.debug(
         f"created parametric ml strategy {sidml} inherited from {sid}:\n{strat}"
      )
      return sidml

   def mlstrat(self, strat: str, model: str) -> str:
      adds = "\n".join([
         f"--ml-engine",
         f"--ml-model={model}",
         f"--ml-usage=@@@usage:1.0@@@",
         f"--ml-fallback=@@@fallback:0@@@",
         f"--ml-selector=@@@sel:orig@@@",
         f"--ml-selector-value=@@@val:0.5@@@",
      ])
      return f"{strat}\n{adds}"

   def apply(self, sid: str, model: str) -> list[str]:
      (base, args) = sids.split(sid)
      tpl = self.template(base)
      sidml = sids.fmt(tpl, dict(args, model=model))
      logger.debug(f"new strategy: {sidml}")
      return [sidml]

template(sid: str) -> str

sid must be base strategy without parameters

Source code in packages/solverpy-learn/src/solverpy_learn/builder/cvc5ml.py
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
def template(self, sid : str) -> str:
   "`sid` must be base strategy without parameters"
   if sid.endswith("-ml"):
      logger.debug(f"strategy {sid} already ml-enhanced")
      return sid
   sidml = f"{sid}-ml"
   if os.path.exists(sids.path(sidml)):
      logger.debug(f"ml strategy {sidml} already exists")
      return sidml
   dbpath = bids.dbpath(NAME)
   mod = f"{dbpath}/@@@model:default@@@/model.lgb"
   strat = sids.load(sid).rstrip()
   strat = self.mlstrat(strat, mod)
   sids.save(sidml, strat)
   logger.debug(
      f"created parametric ml strategy {sidml} inherited from {sid}:\n{strat}"
   )
   return sidml