*/
HO_CONG,
- //================================================= Array rules
- // ======== Read over write
- // Children: (P:(not (= i1 i2)))
- // Arguments: ((select (store a i1 e) i2))
- // ----------------------------------------
- // Conclusion: (= (select (store a i1 e) i2) (select a i2))
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Arrays -- Read over write**
+ *
+ * .. math::
+ *
+ * \inferrule{\neg (i_1 = i_2)\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)}
+ * {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)}
+ * \endverbatim
+ */
ARRAYS_READ_OVER_WRITE,
- // ======== Read over write, contrapositive
- // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
- // Arguments: none
- // ----------------------------------------
- // Conclusion: (= i1 i2)
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Arrays -- Read over write, contrapositive**
+ *
+ * .. math::
+ *
+ * \inferrule{\neg (\mathit{select}(\mathit{store}(a,i_2,e),i_1) =
+ * \mathit{select}(a,i_1))\mid -}{i_1=i_2}
+ * \endverbatim
+ */
ARRAYS_READ_OVER_WRITE_CONTRA,
- // ======== Read over write 1
- // Children: none
- // Arguments: ((select (store a i e) i))
- // ----------------------------------------
- // Conclusion: (= (select (store a i e) i) e)
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Arrays -- Read over write 1**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)}
+ * {\mathit{select}(\mathit{store}(a,i,e),i)=e}
+ * \endverbatim
+ */
ARRAYS_READ_OVER_WRITE_1,
- // ======== Extensionality
- // Children: (P:(not (= a b)))
- // Arguments: none
- // ----------------------------------------
- // Conclusion: (not (= (select a k) (select b k)))
- // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Arrays -- Arrays extensionality**
+ *
+ * .. math::
+ *
+ * \inferrule{\neg(a = b)\mid -}
+ * {\neg (\mathit{select}(a,k)=\mathit{select}(b,k))}
+ *
+ * where :math:`k` is
+ * :math:`\texttt{arrays::SkolemCache::getExtIndexSkolem}(\neg(a=b))`.
+ * \endverbatim
+ */
ARRAYS_EXT,
- // ======== EQ_RANGE expansion
- // Children: none
- // Arguments: ((eqrange a b i j))
- // ----------------------------------------
- // Conclusion: (=
- // (eqrange a b i j)
- // (forall ((x T))
- // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))))
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Arrays -- Expansion of array range equality**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid \mathit{eqrange}(a,b,i,j)}
+ * {\mathit{eqrange}(a,b,i,j)=
+ * \forall x.\> i \leq x \leq j \rightarrow
+ * \mathit{select}(a,x)=\mathit{select}(b,x)}
+ * \endverbatim
+ */
ARRAYS_EQ_RANGE_EXPAND,
- //================================================= Bit-Vector rules
- // Note: bitblast() represents the result of the bit-blasted term as a
- // bit-vector consisting of the output bits of the bit-blasted circuit
- // representation of the term. Terms are bit-blasted according to the
- // strategies defined in
- // theory/bv/bitblast/bitblast_strategies_template.h.
- // ======== Bitblast
- // Children: none
- // Arguments: (t)
- // ---------------------
- // Conclusion: (= t bitblast(t))
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Bit-vectors -- Bitblast**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid t}{t = \texttt{bitblast}(t)}
+ *
+ * where ``bitblast()`` represents the result of the bit-blasted term as a
+ * bit-vector consisting of the output bits of the bit-blasted circuit
+ * representation of the term. Terms are bit-blasted according to the
+ * strategies defined in ``theory/bv/bitblast/bitblast_strategies_template.h``.
+ * \endverbatim
+ */
BV_BITBLAST,
- // ======== Bitblast Bit-Vector Constant, Variable
- // Children: none
- // Arguments: (= t bitblast(t))
- // ---------------------
- // Conclusion: (= t bitblast(t))
- // ======== Bitblast Bit-Vector Terms
- // Children: none
- // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
- // ---------------------
- // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Bit-vectors -- Bitblast bit-vector constant, variable, and terms**
+ *
+ * For constant and variables:
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid t}{t = \texttt{bitblast}(t)}
+ *
+ * For terms:
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))}
+ * {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) =
+ * \texttt{bitblast}(t)}
+ *
+ * where :math:`t` is :math:`k(t_1,\dots,t_n)`.
+ * \endverbatim
+ */
BV_BITBLAST_STEP,
-
- // ======== Eager Atom
- // Children: none
- // Arguments: (F)
- // ---------------------
- // Conclusion: (= F F[0])
- // where F is of kind BITVECTOR_EAGER_ATOM
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Bit-vectors -- Bit-vector eager atom**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid F}{F = F[0]}
+ *
+ * where :math:`F` is of kind ``BITVECTOR_EAGER_ATOM``.
+ * \endverbatim
+ */
BV_EAGER_ATOM,
- //================================================= Datatype rules
- // ======== Unification
- // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
- // Arguments: (i)
- // ----------------------------------------
- // Conclusion: (= ti si)
- // where C is a constructor.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Datatypes -- Unification**
+ *
+ * .. math::
+ *
+ * \inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i}
+ *
+ * where :math:`C` is a constructor.
+ * \endverbatim
+ */
DT_UNIF,
- // ======== Instantiate
- // Children: none
- // Arguments: (t, n)
- // ----------------------------------------
- // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
- // where C is the n^th constructor of the type of T, and (_ is C) is the
- // discriminator (tester) for C.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Datatypes -- Instantiation**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid t,n}{\mathit{is}_C(t) =
+ * (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))}
+ *
+ * where :math:`C` is the :math:`n^{\mathit{th}}` constructor of the type of
+ * t, and :math:`\mathit{is}_C` is the discriminator (tester) for :math:`C`.
+ * \endverbatim
+ */
DT_INST,
- // ======== Collapse
- // Children: none
- // Arguments: ((sel_i (C_j t_1 ... t_n)))
- // ----------------------------------------
- // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
- // where C_j is a constructor, r is t_i if sel_i is a correctly applied
- // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
- // that the use of mkGroundTerm differs from the rewriter which uses
- // mkGroundValue in this case.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Datatypes -- Collapse**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{
+ * \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r}
+ *
+ * where :math:`C_j` is a constructor, :math:`r` is :math:`t_i` if
+ * :math:`\mathit{sel}_i` is a correctly applied selector, or
+ * ``TypeNode::mkGroundTerm()`` of the proper type otherwise. Notice that the
+ * use of ``mkGroundTerm`` differs from the rewriter which uses
+ * ``mkGroundValue`` in this case.
+ * \endverbatim
+ */
DT_COLLAPSE,
- // ======== Split
- // Children: none
- // Arguments: (t)
- // ----------------------------------------
- // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Datatypes -- Split**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)}
+ *
+ * where :math:`C_1,\dots,C_n` are all the constructors of the type of :math:`t`.
+ * \endverbatim
+ */
DT_SPLIT,
- // ======== Clash
- // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
- // Arguments: none
- // ----------------------------------------
- // Conclusion: false
- // for i != j.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Datatypes -- Clash**
+ *
+ * .. math::
+ *
+ * \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot}
+ * {if $i\neq j$}
+ *
+ * \endverbatim
+ */
DT_CLASH,
- //================================================= Quantifiers rules
- // ======== Skolem intro
- // Children: none
- // Arguments: (k)
- // ----------------------------------------
- // Conclusion: (= k t)
- // where t is the original form of skolem k.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Quantifiers -- Skolem introduction**
+ *
+ * .. math::
+ *
+ * \inferrule{-\mid k}{k = t}
+ *
+ * where :math:`t` is the original form of skolem :math:`k`.
+ * \endverbatim
+ */
SKOLEM_INTRO,
- // ======== Exists intro
- // Children: (P:F[t])
- // Arguments: ((exists ((x T)) F[x]))
- // ----------------------------------------
- // Conclusion: (exists ((x T)) F[x])
- // This rule verifies that F[x] indeed matches F[t] with a substitution
- // over x.
- EXISTS_INTRO,
- // ======== Skolemize
- // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
- // Arguments: none
- // ----------------------------------------
- // Conclusion: F*sigma
- // sigma maps x1 ... xn to their representative skolems obtained by
- // SkolemManager::mkSkolemize, returned in the skolems argument of that
- // method. Alternatively, can use negated forall as a premise. The witness
- // terms for the returned skolems can be obtained by
- // SkolemManager::getWitnessForm.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Quantifiers -- Skolemization**
+ *
+ * .. math::
+ *
+ * \inferrule{\exists x_1\dots x_n.\> F\mid -}{F\sigma}
+ *
+ * or
+ *
+ * .. math::
+ *
+ * \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma}
+ *
+ * where :math:`\sigma` maps :math:`x_1,\dots,x_n` to their representative
+ * skolems obtained by ``SkolemManager::mkSkolemize``, returned in the skolems
+ * argument of that method. The witness terms for the returned skolems can be
+ * obtained by ``SkolemManager::getWitnessForm``.
+ * \endverbatim
+ */
SKOLEMIZE,
- // ======== Instantiate
- // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
- // Arguments: (t1 ... tn, (id (t)?)? )
- // ----------------------------------------
- // Conclusion: F*sigma
- // where sigma maps x1 ... xn to t1 ... tn.
- //
- // The optional argument id indicates the inference id that caused the
- // instantiation. The term t indicates an additional term (e.g. the trigger)
- // associated with the instantiation, which depends on the id. If the id
- // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that
- // generated the instantiation.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Quantifiers -- Instantiation**
+ *
+ * .. math::
+ *
+ * \inferrule{\forall x_1\dots x_n.\> F\mid t_1,\dots,t_n, (id\, (t)?)?}
+ * {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}
+ *
+ * The optional argument :math:`id` indicates the inference id that caused the
+ * instantiation. The term :math:`t` indicates an additional term (e.g. the trigger)
+ * associated with the instantiation, which depends on the id. If the id
+ * has prefix ``QUANTIFIERS_INST_E_MATCHING``, then :math:`t` is the trigger that
+ * generated the instantiation.
+ * \endverbatim
+ */
INSTANTIATE,
- // ======== Alpha equivalence
- // Children: none
- // Arguments: (F, (y1 = z1), ..., (yn = zn) )
- // ----------------------------------------
- // Conclusion: (= F F*sigma)
- // sigma maps y1 ... yn to z1 ... zn, where y1 ... yn are unique bound
- // variables, and z1 ... zn are unique bound variables. Notice that this
- // rule is correct only when z1, ..., zn are not contained in
- // FV(F) \ { y1 ... yn }. The internal quantifiers proof checker does not
- // currently check that this is the case.
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Quantifiers -- Alpha equivalence**
+ *
+ * .. math::
+ *
+ * \inferruleSC{-\mid F, y_1=z_1,\dots, y_n=z_n}
+ * {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}}
+ * {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}
+ *
+ * Notice that this rule is correct only when :math:`z_1,\dots,z_n` are not
+ * contained in :math:`FV(F) \setminus \{ y_1,\dots, y_n \}`, where
+ * :math:`FV(\varphi)` are the free variables of :math:`\varphi`. The internal
+ * quantifiers proof checker does not currently check that this is the case.
+ * \endverbatim
+ */
ALPHA_EQUIV,
- // ======== (Trusted) quantifiers preprocess
- // Children: ?
- // Arguments: (F)
- // ---------------------------------------------------------------
- // Conclusion: F
- // where F is an equality of the form t = QuantifiersPreprocess::preprocess(t)
+ /**
+ * \verbatim embed:rst:leading-asterisk
+ * **Quantifiers -- (Trusted) quantifiers preprocessing**
+ *
+ * .. math::
+ *
+ * \inferrule{?\mid F}{F}
+ *
+ * where :math:`F` is an equality of the form :math:`t =
+ * \texttt{QuantifiersPreprocess::preprocess(t)}`.
+ * \endverbatim
+ */
QUANTIFIERS_PREPROCESS,
//================================================= String rules
//======================== Core solver
projects / cvc5.git / commitdiff