From 3ebf1214385a12be5e952bf7424ba760393d804b Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 31 Mar 2022 00:35:40 -0300 Subject: [PATCH] [proofs] [doc] Documenting arrays, bit-vectors, datatypes and quantifiers rules (#8465) --- src/proof/proof_rule.cpp | 1 - src/proof/proof_rule.h | 383 ++++++++++++++--------- src/smt/witness_form.cpp | 23 -- src/smt/witness_form.h | 4 - src/theory/quantifiers/proof_checker.cpp | 29 +- 5 files changed, 239 insertions(+), 201 deletions(-) diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 2d26c780f..454493844 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -133,7 +133,6 @@ const char* toString(PfRule id) case PfRule::DT_CLASH: return "DT_CLASH"; //================================================= Quantifiers rules case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; - case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; case PfRule::SKOLEMIZE: return "SKOLEMIZE"; case PfRule::INSTANTIATE: return "INSTANTIATE"; case PfRule::ALPHA_EQUIV: return "ALPHA_EQUIV"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 3c568cefc..a7b423638 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1126,171 +1126,264 @@ enum class PfRule : uint32_t */ 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 diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 0afb92ca1..eb487b7fb 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -134,28 +134,5 @@ const std::unordered_set& WitnessFormGenerator::getWitnessFormEqs() const return d_eqs; } -ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists) -{ - Assert(exists.getKind() == kind::EXISTS); - if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL - && exists[1][0] == exists[0][0]) - { - Node tpurified = exists[1][1]; - Trace("witness-form") << "convertExistsInternal: infer purification " - << exists << " for " << tpurified << std::endl; - // ------ REFL - // t = t - // ---------------- EXISTS_INTRO - // exists x. x = t - // The concluded existential is then used to construct the witness term - // via witness intro. - Node teq = tpurified.eqNode(tpurified); - d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified}); - d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists}); - return &d_pskPf; - } - return nullptr; -} - } // namespace smt } // namespace cvc5::internal diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 0a63775ec..dd490f9b6 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -88,10 +88,6 @@ class WitnessFormGenerator : public ProofGenerator * of this class (d_tcpg). */ Node convertToWitnessForm(Node t); - /** - * Return a proof generator that can prove the given axiom exists. - */ - ProofGenerator* convertExistsInternal(Node exists); /** The rewriter we are using */ theory::Rewriter* d_rewriter; /** The term conversion proof generator */ diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 5553e4cef..be88b60c4 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -29,7 +29,6 @@ void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) { // add checkers pc->registerChecker(PfRule::SKOLEM_INTRO, this); - pc->registerChecker(PfRule::EXISTS_INTRO, this); pc->registerChecker(PfRule::SKOLEMIZE, this); pc->registerChecker(PfRule::INSTANTIATE, this); pc->registerChecker(PfRule::ALPHA_EQUIV, this); @@ -42,33 +41,7 @@ Node QuantifiersProofRuleChecker::checkInternal( { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - // compute what was proven - if (id == PfRule::EXISTS_INTRO) - { - Assert(children.size() == 1); - Assert(args.size() == 1); - Node p = children[0]; - Node exists = args[0]; - if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1) - { - return Node::null(); - } - std::unordered_map subs; - if (!expr::match(exists[1], p, subs)) - { - return Node::null(); - } - // substitution must contain only the variable of the existential - for (const std::pair& s : subs) - { - if (s.first != exists[0][0]) - { - return Node::null(); - } - } - return exists; - } - else if (id == PfRule::SKOLEM_INTRO) + if (id == PfRule::SKOLEM_INTRO) { Assert(children.empty()); Assert(args.size() == 1); -- 2.30.2