Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of equality proof checker.
11 : : */
12 : :
13 : : #include "theory/uf/proof_checker.h"
14 : :
15 : : #include "theory/uf/theory_uf_rewriter.h"
16 : :
17 : : using namespace cvc5::internal::kind;
18 : :
19 : : namespace cvc5::internal {
20 : : namespace theory {
21 : : namespace uf {
22 : :
23 : 20020 : void UfProofRuleChecker::registerTo(ProofChecker* pc)
24 : : {
25 : : // add checkers
26 : 20020 : pc->registerChecker(ProofRule::REFL, this);
27 : 20020 : pc->registerChecker(ProofRule::SYMM, this);
28 : 20020 : pc->registerChecker(ProofRule::TRANS, this);
29 : 20020 : pc->registerChecker(ProofRule::CONG, this);
30 : 20020 : pc->registerChecker(ProofRule::NARY_CONG, this);
31 : 20020 : pc->registerChecker(ProofRule::PAIRWISE_CONG, this);
32 : 20020 : pc->registerChecker(ProofRule::TRUE_INTRO, this);
33 : 20020 : pc->registerChecker(ProofRule::TRUE_ELIM, this);
34 : 20020 : pc->registerChecker(ProofRule::FALSE_INTRO, this);
35 : 20020 : pc->registerChecker(ProofRule::FALSE_ELIM, this);
36 : 20020 : pc->registerChecker(ProofRule::HO_CONG, this);
37 : 20020 : pc->registerChecker(ProofRule::HO_APP_ENCODE, this);
38 : 20020 : }
39 : :
40 : 3976890 : Node UfProofRuleChecker::checkInternal(ProofRule id,
41 : : const std::vector<Node>& children,
42 : : const std::vector<Node>& args)
43 : : {
44 : : // compute what was proven
45 [ + + ]: 3976890 : if (id == ProofRule::REFL)
46 : : {
47 [ - + ][ - + ]: 643536 : Assert(children.empty());
[ - - ]
48 [ - + ][ - + ]: 643536 : Assert(args.size() == 1);
[ - - ]
49 : 643536 : return args[0].eqNode(args[0]);
50 : : }
51 [ + + ]: 3333354 : else if (id == ProofRule::SYMM)
52 : : {
53 [ - + ][ - + ]: 1359992 : Assert(children.size() == 1);
[ - - ]
54 [ - + ][ - + ]: 1359992 : Assert(args.empty());
[ - - ]
55 : 1359992 : bool polarity = children[0].getKind() != Kind::NOT;
56 [ + + ]: 1359992 : Node eqp = polarity ? children[0] : children[0][0];
57 [ - + ]: 1359992 : if (eqp.getKind() != Kind::EQUAL)
58 : : {
59 : : // not a (dis)equality
60 : 0 : return Node::null();
61 : : }
62 : 2719984 : Node conc = eqp[1].eqNode(eqp[0]);
63 [ + + ]: 1359992 : return polarity ? conc : conc.notNode();
64 : 1359992 : }
65 [ + + ]: 1973362 : else if (id == ProofRule::TRANS)
66 : : {
67 [ - + ][ - + ]: 878958 : Assert(children.size() > 0);
[ - - ]
68 [ - + ][ - + ]: 878958 : Assert(args.empty());
[ - - ]
69 : 878958 : Node first;
70 : 878958 : Node curr;
71 [ + + ]: 2911260 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
72 : : {
73 : 2032302 : Node eqp = children[i];
74 [ - + ]: 2032302 : if (eqp.getKind() != Kind::EQUAL)
75 : : {
76 : 0 : return Node::null();
77 : : }
78 [ + + ]: 2032302 : if (first.isNull())
79 : : {
80 : 878958 : first = eqp[0];
81 : : }
82 [ - + ]: 1153344 : else if (eqp[0] != curr)
83 : : {
84 : 0 : return Node::null();
85 : : }
86 : 2032302 : curr = eqp[1];
87 [ + - ]: 2032302 : }
88 : 878958 : return first.eqNode(curr);
89 : 878958 : }
90 [ + + ][ + + ]: 1094404 : else if (id == ProofRule::CONG || id == ProofRule::NARY_CONG
91 [ + + ]: 79740 : || id == ProofRule::PAIRWISE_CONG)
92 : : {
93 [ - + ][ - + ]: 1017211 : Assert(children.size() > 0);
[ - - ]
94 [ - + ]: 1017211 : if (args.size() != 1)
95 : : {
96 : 0 : return Node::null();
97 : : }
98 : 1017211 : Node t = args[0];
99 [ + - ]: 2034422 : Trace("uf-pfcheck") << "congruence " << id << " for " << args[0]
100 : 1017211 : << std::endl;
101 : : // We do congruence over builtin kinds using operatorToKind
102 : 1017211 : std::vector<Node> lchildren;
103 : 1017211 : std::vector<Node> rchildren;
104 : 1017211 : Kind k = args[0].getKind();
105 [ + + ]: 1017211 : if (t.getMetaKind() == metakind::PARAMETERIZED)
106 : : {
107 : : // parameterized kinds require the operator
108 : 179387 : lchildren.push_back(t.getOperator());
109 : 179387 : rchildren.push_back(t.getOperator());
110 : : }
111 : : // congruence automatically adds variable lists
112 [ + + ]: 1017211 : if (t.isClosure())
113 : : {
114 : 12233 : lchildren.push_back(t[0]);
115 : 12233 : rchildren.push_back(t[0]);
116 : : }
117 [ + + ]: 3861077 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
118 : : {
119 : 2843866 : Node eqp = children[i];
120 [ - + ]: 2843866 : if (eqp.getKind() != Kind::EQUAL)
121 : : {
122 : 0 : return Node::null();
123 : : }
124 : 2843866 : lchildren.push_back(eqp[0]);
125 : 2843866 : rchildren.push_back(eqp[1]);
126 [ + - ]: 2843866 : }
127 : 1017211 : NodeManager* nm = nodeManager();
128 : 1017211 : Node l = nm->mkNode(k, lchildren);
129 : 1017211 : Node r = nm->mkNode(k, rchildren);
130 : 1017211 : return l.eqNode(r);
131 : 1017211 : }
132 [ + + ]: 77193 : else if (id == ProofRule::TRUE_INTRO)
133 : : {
134 [ - + ][ - + ]: 5060 : Assert(children.size() == 1);
[ - - ]
135 [ - + ][ - + ]: 5060 : Assert(args.empty());
[ - - ]
136 : 5060 : Node trueNode = nodeManager()->mkConst(true);
137 : 5060 : return children[0].eqNode(trueNode);
138 : 5060 : }
139 [ + + ]: 72133 : else if (id == ProofRule::TRUE_ELIM)
140 : : {
141 [ - + ][ - + ]: 46908 : Assert(children.size() == 1);
[ - - ]
142 [ - + ][ - + ]: 46908 : Assert(args.empty());
[ - - ]
143 [ + - ][ - + ]: 140724 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
144 [ + - ][ - + ]: 140724 : || !children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
145 : : {
146 : 0 : return Node::null();
147 : : }
148 : 46908 : return children[0][0];
149 : : }
150 [ + + ]: 25225 : else if (id == ProofRule::FALSE_INTRO)
151 : : {
152 [ - + ][ - + ]: 7649 : Assert(children.size() == 1);
[ - - ]
153 [ - + ][ - + ]: 7649 : Assert(args.empty());
[ - - ]
154 [ - + ]: 7649 : if (children[0].getKind() != Kind::NOT)
155 : : {
156 : 0 : return Node::null();
157 : : }
158 : 7649 : Node falseNode = nodeManager()->mkConst(false);
159 : 7649 : return children[0][0].eqNode(falseNode);
160 : 7649 : }
161 [ + + ]: 17576 : else if (id == ProofRule::FALSE_ELIM)
162 : : {
163 [ - + ][ - + ]: 16484 : Assert(children.size() == 1);
[ - - ]
164 [ - + ][ - + ]: 16484 : Assert(args.empty());
[ - - ]
165 [ + - ][ - + ]: 49452 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
166 [ + - ][ - + ]: 49452 : || children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
167 : : {
168 : 0 : return Node::null();
169 : : }
170 : 16484 : return children[0][0].notNode();
171 : : }
172 [ + + ]: 1092 : if (id == ProofRule::HO_CONG)
173 : : {
174 : 1069 : Kind k = Kind::HO_APPLY;
175 : : // kind argument is optional, defaults to HO_APPLY
176 [ + + ]: 1069 : if (args.size() == 1)
177 : : {
178 [ - + ]: 821 : if (!getKind(args[0], k))
179 : : {
180 : 0 : return Node::null();
181 : : }
182 : : }
183 : 1069 : std::vector<Node> lchildren;
184 : 1069 : std::vector<Node> rchildren;
185 [ + + ]: 4488 : for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
186 : : {
187 : 3419 : Node eqp = children[i];
188 [ - + ]: 3419 : if (eqp.getKind() != Kind::EQUAL)
189 : : {
190 : 0 : return Node::null();
191 : : }
192 : 3419 : lchildren.push_back(eqp[0]);
193 : 3419 : rchildren.push_back(eqp[1]);
194 [ + - ]: 3419 : }
195 : 1069 : NodeManager* nm = nodeManager();
196 : 1069 : Node l = nm->mkNode(k, lchildren);
197 : 1069 : Node r = nm->mkNode(k, rchildren);
198 : 1069 : return l.eqNode(r);
199 : 1069 : }
200 [ + - ]: 23 : else if (id == ProofRule::HO_APP_ENCODE)
201 : : {
202 [ - + ][ - + ]: 23 : Assert(args.size() == 1);
[ - - ]
203 : 23 : Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
204 : 23 : return args[0].eqNode(ret);
205 : 23 : }
206 : : // no rule
207 : 0 : return Node::null();
208 : : }
209 : :
210 : : } // namespace uf
211 : : } // namespace theory
212 : : } // namespace cvc5::internal
|
