diff options
Diffstat (limited to 'src/theory/inference_id.h')
| -rw-r--r-- | src/theory/inference_id.h | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 884a7c428..8a787ca2d 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -169,6 +169,35 @@ enum class InferenceId DATATYPES_HEIGHT_ZERO, // ---------------------------------- end datatypes theory + //-------------------------------------- quantifiers theory + // skolemization + QUANTIFIERS_SKOLEMIZE, + // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent + QUANTIFIERS_REDUCE_ALPHA_EQ, + //-------------------- counterexample-guided instantiation + // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose + // counterexample literal is G1. + QUANTIFIERS_CEGQI_CEX_DEP, + // 0 < delta + QUANTIFIERS_CEGQI_VTS_LB_DELTA, + // delta < c, for positive c + QUANTIFIERS_CEGQI_VTS_UB_DELTA, + // infinity > c + QUANTIFIERS_CEGQI_VTS_LB_INF, + //-------------------- sygus solver + // preprocessing a sygus conjecture based on quantifier elimination, of the + // form Q <=> Q_preprocessed + QUANTIFIERS_SYGUS_QE_PREPROC, + // G or ~G where G is the active guard for a sygus enumerator + QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT, + // manual exclusion of a current solution + QUANTIFIERS_SYGUS_EXCLUDE_CURRENT, + // manual exclusion of a current solution for sygus-stream + QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT, + // ~Q where Q is a PBE conjecture with conflicting examples + QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA, + //-------------------------------------- end quantifiers theory + // ---------------------------------- sep theory // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w SEP_PTO_NEG_PROP, |