diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-18 10:06:49 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-18 10:06:49 -0500 |
| commit | 2e02c1c2fb999f2f1cdefe867f843c2c46ad0ef0 (patch) | |
| tree | e9234dd807818316a9029cab5badc62b6874fa67 /src/options/quantifiers_modes.h | |
| parent | 8768c1079798599bbe27b29bc49087d45857a112 (diff) | |
Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes for inst max level.
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 38308c9dc..65445be17 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -153,6 +153,17 @@ enum IteLiftQuantMode { ITE_LIFT_QUANT_MODE_ALL, }; +enum CegqiSingleInvMode { + /** do not use single invocation techniques */ + CEGQI_SI_MODE_NONE, + /** use single invocation techniques */ + CEGQI_SI_MODE_USE, + /** always use single invocation techniques, abort if solution reconstruction will fail */ + CEGQI_SI_MODE_ALL_ABORT, + /** always use single invocation techniques */ + CEGQI_SI_MODE_ALL, +}; + enum SygusInvTemplMode { /** synthesize I( x ) */ SYGUS_INV_TEMPL_MODE_NONE, |