diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-13 16:33:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-13 21:33:07 +0000 |
| commit | 1c0d2738941e948d67c696e0c96e3463da9807d2 (patch) | |
| tree | 31e929bc26f3b01518b339ed0c9bef562bc6983c /src/theory/inference_id.cpp | |
| parent | f7dcb4875bba33b7712732a874581639681926f8 (diff) | |
Add pool instantiation strategy (#6308)
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c1c751800..ceca32a8d 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -174,6 +174,7 @@ const char* toString(InferenceId i) case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI"; case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI"; case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM"; + case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL"; case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG"; case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX"; |