diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-25 10:10:47 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-25 10:10:47 -0600 |
| commit | a1135ca591276f6d02b3632bc77a3934ded2d2af (patch) | |
| tree | fa45a24bc072970abd71f59967a4dd759d2be0d2 /src/options/quantifiers_modes.h | |
| parent | bab37658aa27ee455e3928c66db49c1bb3224e3b (diff) | |
Minor improvement to partial qe. Add options for representative selection in FMF.
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 7395a9a30..8aa3756cc 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -172,6 +172,14 @@ enum QuantDSplitMode { QUANT_DSPLIT_MODE_AGG, }; +enum QuantRepMode { + /** let equality engine choose representatives */ + QUANT_REP_MODE_EE, + /** default, choose representatives that appear first */ + QUANT_REP_MODE_FIRST, + /** choose representatives that have minimal depth */ + QUANT_REP_MODE_DEPTH, +}; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ |