From c6210af1db67701495efa263207b91064a3bcd0b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 18 Feb 2021 01:21:38 -0600 Subject: [PATCH] Document UF inferences (#5917) Document UF entries of InferenceId enum. --- src/theory/inference_id.h | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index bb69f5d7f..2ce1a4634 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -411,17 +411,38 @@ enum class InferenceId // Clause from the uf symmetry breaker UF_BREAK_SYMMETRY, + //-------------------------------------- begin cardinality extension to UF + // The inferences below are described in Reynolds' thesis 2013. + // conflict of the form (card_T n) => (not (distinct t1 ... tn)) UF_CARD_CLIQUE, + // conflict of the form (not (card_T1 n1)) ^ ... (not (card_Tk nk)) ^ (card n) + // where n1 + ... + nk >= n, where (card n) is a combined cardinality + // constraint. UF_CARD_COMBINED, + // (not (card_T n)) => (distinct t1 ... tn) UF_CARD_ENFORCE_NEGATIVE, + // used to make the index terms in cardinality constraints equal UF_CARD_EQUIV, + // conflict of the form (not (card_T1 n)) ^ (card_T2 m) where the cardinality + // of T2 can be assumed to be without loss of generality larger than T1 due to + // monotonicity reasoning (Claessen et al 2011). UF_CARD_MONOTONE_COMBINED, + // conflict of the form (not (card_T n)) ^ (card_T m) where n>m UF_CARD_SIMPLE_CONFLICT, + // equality split requested by cardinality solver + // (or (= t1 t2) (not (= t1 t2)) + // to satisfy the cardinality constraints on the type of t1, t2. UF_CARD_SPLIT, + //-------------------------------------- end cardinality extension to UF //-------------------------------------- begin HO extension to UF // Encodes an n-ary application as a chain of binary HO_APPLY applications // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn)) UF_HO_APP_ENCODE, + // A lemma corresponding to the definition of a skolem k used to convert + // HO_APPLY terms to APPLY_UF terms. This is of the form: + // (forall x1 ... xn) (@ (@ k x1) ... xn) = t + // where notice that t is a function whose free variables (if any) are + // x1 ... xn. UF_HO_APP_CONV_SKOLEM, // Adds an extensionality lemma to witness that disequal functions have // different applications -- 2.30.2