id     = "DECISION"
name   = "Decision Heuristics"

[[option]]
  name       = "decisionMode"
  alias      = ["decision-mode"]
  category   = "regular"
  long       = "decision=MODE"
  type       = "DecisionMode"
  default    = "INTERNAL"
  predicates = ["setDecisionModeStopOnly"]
  help       = "choose decision mode, see --decision=help"
  help_mode  = "Decision modes."
[[option.mode.INTERNAL]]
  name = "internal"
  help = "Use the internal decision heuristics of the SAT solver."
[[option.mode.JUSTIFICATION]]
  name = "justification"
  help = "An ATGP-inspired justification heuristic."
[[option.mode.JUSTIFICATION_OLD]]
  name = "justification-old"
  help = "Older implementation of an ATGP-inspired justification heuristic."
[[option.mode.RELEVANCY]]
  name = "justification-stoponly"
  help = "Use the justification heuristic only to stop early, not for decisions."

[[option]]
  name       = "decisionStopOnly"
  category   = "undocumented"
  type       = "bool"

[[option]]
  name       = "decisionThreshold"
  category   = "expert"
  long       = "decision-threshold=N"
  type       = "cvc5::decision::DecisionWeight"
  default    = "0"
  includes   = ["options/decision_weight.h"]
  help       = "ignore all nodes greater than threshold in first attempt to pick decision"

[[option]]
  name       = "decisionUseWeight"
  category   = "expert"
  long       = "decision-use-weight"
  type       = "bool"
  default    = "false"
  help       = "use the weight nodes (locally, by looking at children) to direct recursive search"


[[option]]
  name       = "decisionRandomWeight"
  category   = "expert"
  long       = "decision-random-weight=N"
  type       = "int"
  default    = "0"
  help       = "assign random weights to nodes between 0 and N-1 (0: disable)"

[[option]]
  name       = "decisionWeightInternal"
  category   = "expert"
  long       = "decision-weight-internal=HOW"
  type       = "DecisionWeightInternal"
  default    = "OFF"
  help       = "compute weights of internal nodes using children: off, max, sum, usr1"
  help_mode  = "Decision weight internal mode."
[[option.mode.OFF]]
  name = "off"
[[option.mode.MAX]]
  name = "max"
[[option.mode.SUM]]
  name = "sum"
[[option.mode.USR1]]
  name = "usr1"

[[option]]
  name       = "jhSkolemMode"
  category   = "expert"
  long       = "jh-skolem=MODE"
  type       = "JutificationSkolemMode"
  default    = "FIRST"
  help       = "policy for when to satisfy skolem definitions in justification heuristic"
  help_mode  = "Policy for when to satisfy skolem definitions in justification heuristic"
[[option.mode.FIRST]]
  name = "first"
  help = "satisfy pending relevant skolem definitions before input assertions"
[[option.mode.LAST]]
  name = "last"
  help = "satisfy pending relevant skolem definitions after input assertions"

[[option]]
  name       = "jhRlvOrder"
  category   = "expert"
  long       = "jh-rlv-order"
  type       = "bool"
  default    = "true"
  help       = "maintain activity-based ordering for decision justification heuristic"

[[option]]
  name       = "jhSkolemRlvMode"
  category   = "expert"
  long       = "jh-skolem-rlv=MODE"
  type       = "JutificationSkolemRlvMode"
  default    = "ASSERT"
  help       = "policy for when to consider skolem definitions relevant in justification heuristic"
  help_mode  = "Policy for when to consider skolem definitions relevant in justification heuristic"
[[option.mode.ASSERT]]
  name = "assert"
  help = "skolems are relevant when they occur in an asserted literal"
[[option.mode.ALWAYS]]
  name = "always"
  help = "skolems are always relevant"