id     = "PROP"
name   = "SAT Layer"

[[option]]
  name       = "satRandomFreq"
  alias      = ["random-frequency"]
  category   = "regular"
  long       = "random-freq=P"
  type       = "double"
  default    = "0.0"
  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
  help       = "sets the frequency of random decisions in the sat solver (P=0.0 by default)"

[[option]]
  name       = "satRandomSeed"
  category   = "regular"
  long       = "random-seed=S"
  type       = "uint32_t"
  default    = "0"
  help       = "sets the random seed for the sat solver"

[[option]]
  name       = "satVarDecay"
  category   = "regular"
  type       = "double"
  default    = "0.95"
  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
  help       = "variable activity decay factor for Minisat"

[[option]]
  name       = "satClauseDecay"
  category   = "regular"
  type       = "double"
  default    = "0.999"
  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
  help       = "clause activity decay factor for Minisat"

[[option]]
  name       = "satRestartFirst"
  category   = "regular"
  long       = "restart-int-base=N"
  type       = "unsigned"
  default    = "25"
  help       = "sets the base restart interval for the sat solver (N=25 by default)"

[[option]]
  name       = "satRestartInc"
  category   = "regular"
  long       = "restart-int-inc=F"
  type       = "double"
  default    = "3.0"
  predicates = ["doubleGreaterOrEqual0"]
  help       = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"

[[option]]
  name       = "sat_refine_conflicts"
  category   = "regular"
  long       = "refine-conflicts"
  type       = "bool"
  default    = "false"
  help       = "refine theory conflict clauses (default false)"

[[option]]
  name       = "minisatUseElim"
  category   = "regular"
  long       = "minisat-elimination"
  type       = "bool"
  default    = "true"
  help       = "use Minisat elimination"

[[option]]
  name       = "minisatDumpDimacs"
  category   = "regular"
  long       = "minisat-dump-dimacs"
  type       = "bool"
  default    = "false"
  help       = "instead of solving minisat dumps the asserted clauses in Dimacs format"