diff options
Diffstat (limited to 'src/options/prop_options.toml')
-rw-r--r-- | src/options/prop_options.toml | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml new file mode 100644 index 000000000..5ad691e62 --- /dev/null +++ b/src/options/prop_options.toml @@ -0,0 +1,84 @@ +id = "PROP" +name = "SAT layer" +header = "options/prop_options.h" + +[[option]] + name = "satRandomFreq" + smt_name = "random-frequency" + category = "regular" + long = "random-freq=P" + type = "double" + default = "0.0" + predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + read_only = true + help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" + +[[option]] + name = "satRandomSeed" + smt_name = "random-seed" + 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" + read_only = true + 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"] + read_only = true + 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" + read_only = true + 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" + read_only = true + help = "instead of solving minisat dumps the asserted clauses in Dimacs format" |