diff options
Diffstat (limited to 'src/smt/options')
| -rw-r--r-- | src/smt/options | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/smt/options b/src/smt/options index d2455b520..6b9944cdd 100644 --- a/src/smt/options +++ b/src/smt/options @@ -42,18 +42,31 @@ common-option interactive interactive-mode --interactive bool :read-write option doITESimp --ite-simp bool :read-write turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) +option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false + do the ite simplification pass again if repeating simplification + +option simplifyWithCareEnabled --simp-with-care bool :default false :read-write + enables simplifyWithCare in ite simplificiation + +option compressItes --simp-ite-compress bool :default false :read-write + enables compressing ites after ite simplification + option unconstrainedSimp --unconstrained-simp bool :default false :read-write turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) option repeatSimp --repeat-simp bool :read-write make multiple passes with nonclausal simplifier +option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288 + post ite compression enables zombie removal while the number of nodes is above this threshold + option sortInference --sort-inference bool :read-write :default false calculate sort inference of input problem, convert the input based on monotonic sorts common-option incrementalSolving incremental -i --incremental bool enable incremental solving + option abstractValues abstract-values --abstract-values bool :default false in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard option modelUninterpDtEnum --model-u-dt-enum bool :default false |