diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-02 21:04:49 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-02 21:04:49 -0600 |
| commit | b72de87fb2804325137352ce79a6044d1b805576 (patch) | |
| tree | 5b08037711382c26e52de705038a9756c2160b46 /src/options/quantifiers_modes.h | |
| parent | 1b24f3f0fd5fdd4163a46689949fa8a5c60f3322 (diff) | |
Option to use sampling for CEGIS (#1555)
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 6274269ce..91fab54ff 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -216,6 +216,16 @@ enum CegqiSingleInvMode { CEGQI_SI_MODE_ALL, }; +enum CegisSampleMode +{ + /** do not use samples for CEGIS */ + CEGIS_SAMPLE_NONE, + /** use samples for CEGIS */ + CEGIS_SAMPLE_USE, + /** trust samples for CEGQI */ + CEGIS_SAMPLE_TRUST, +}; + enum SygusInvTemplMode { /** synthesize I( x ) */ SYGUS_INV_TEMPL_MODE_NONE, |