diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-11 02:44:30 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 08:44:30 +0000 |
| commit | 223155cfb300458f534f4be6b88e5fdc17b0ff14 (patch) | |
| tree | ea6eb835057de2c1705020ef5e4f8b1c18a1b6e8 /src/theory/inference_id.cpp | |
| parent | e348f20c62bd55993d675ba4994d7aa6322b7b2f (diff) | |
Direct lemmas and inference ids for sygus extension (#5960)
This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 3db147a16..7acf2e861 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -101,6 +101,27 @@ const char* toString(InferenceId i) case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE"; case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS"; case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO"; + case InferenceId::DATATYPES_SYGUS_SYM_BREAK: + return "DATATYPES_SYGUS_SYM_BREAK"; + case InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK: + return "DATATYPES_SYGUS_CDEP_SYM_BREAK"; + case InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK: + return "DATATYPES_SYGUS_ENUM_SYM_BREAK"; + case InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK: + return "DATATYPES_SYGUS_SIMPLE_SYM_BREAK"; + case InferenceId::DATATYPES_SYGUS_FAIR_SIZE: + return "DATATYPES_SYGUS_FAIR_SIZE"; + case InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT: + return "DATATYPES_SYGUS_FAIR_SIZE_CONFLICT"; + case InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC: + return "DATATYPES_SYGUS_VAR_AGNOSTIC"; + case InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION: + return "DATATYPES_SYGUS_SIZE_CORRECTION"; + case InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION: + return "DATATYPES_SYGUS_VALUE_CORRECTION"; + case InferenceId::DATATYPES_SYGUS_MT_BOUND: + return "DATATYPES_SYGUS_MT_BOUND"; + case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS"; case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; |