diff options
Diffstat (limited to 'src/options/quantifiers_modes.h')
| -rw-r--r-- | src/options/quantifiers_modes.h | 33 |
1 files changed, 31 insertions, 2 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a949b97be..afb54002c 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -208,12 +208,41 @@ enum CegqiSingleInvMode { 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, }; +/** Solution reconstruction modes for single invocation conjectures + * + * These modes indicate the policy when CVC4 solves a synthesis conjecture using + * single invocation techniques for a sygus problem with a user-specified + * grammar. + */ +enum CegqiSingleInvRconsMode +{ + /** + * Do not try to reconstruct solutions to single invocation conjectures. With + * this mode, solutions produced by CVC4 may violate grammar restrictions. + */ + CEGQI_SI_RCONS_MODE_NONE, + /** + * Try to reconstruct solution to single invocation conjectures in an + * incomplete (fail fast) way. + */ + CEGQI_SI_RCONS_MODE_TRY, + /** + * Reconstruct solutions to single invocation conjectures, but fail if we + * reach an upper limit on number of iterations in the enumeration + */ + CEGQI_SI_RCONS_MODE_ALL_LIMIT, + /** + * Reconstruct solutions to single invocation conjectures. This method + * relies on an expensive enumeration technique which only terminates when + * we succesfully reconstruct the solution, although it may not terminate. + */ + CEGQI_SI_RCONS_MODE_ALL, +}; + enum CegisSampleMode { /** do not use samples for CEGIS */ |