diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-01 10:07:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-01 10:07:39 -0500 |
| commit | bdf46b42d6bd66121a5b5175a81408cd64d7ecfa (patch) | |
| tree | 2aae6c707375616964afd88437be3b48f1dbe45a /src/theory/incomplete_id.h | |
| parent | d288f52dd82fe6590950758289e86ebcb039350d (diff) | |
Add option to limit the number of instantiation rounds (#6818)
This adds an option to limit the number of instantiation rounds used by quantifiers engine.
This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.
This PR also makes minor improvements to the quantifier utility infrastructure.
Diffstat (limited to 'src/theory/incomplete_id.h')
| -rw-r--r-- | src/theory/incomplete_id.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index c166d0c0a..951c2a94f 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -42,6 +42,8 @@ enum class IncompleteId QUANTIFIERS_FMF, // incomplete due to explicitly recorded instantiations QUANTIFIERS_RECORDED_INST, + // incomplete due to limited number of allowed instantiation rounds + QUANTIFIERS_MAX_INST_ROUNDS, // incomplete due to separation logic SEP, // relations were used in combination with set cardinality constraints |