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 : 18893 : void UfProofRuleChecker::registerTo(ProofChecker* pc)
24 : : {
25 : : // add checkers
26 : 18893 : pc->registerChecker(ProofRule::REFL, this);
27 : 18893 : pc->registerChecker(ProofRule::SYMM, this);
28 : 18893 : pc->registerChecker(ProofRule::TRANS, this);
29 : 18893 : pc->registerChecker(ProofRule::CONG, this);
30 : 18893 : pc->registerChecker(ProofRule::NARY_CONG, this);
31 : 18893 : pc->registerChecker(ProofRule::PAIRWISE_CONG, this);
32 : 18893 : pc->registerChecker(ProofRule::TRUE_INTRO, this);
33 : 18893 : pc->registerChecker(ProofRule::TRUE_ELIM, this);
34 : 18893 : pc->registerChecker(ProofRule::FALSE_INTRO, this);
35 : 18893 : pc->registerChecker(ProofRule::FALSE_ELIM, this);
36 : 18893 : pc->registerChecker(ProofRule::HO_CONG, this);
37 : 18893 : pc->registerChecker(ProofRule::HO_APP_ENCODE, this);
38 : 18893 : }
39 : :
40 : 3927638 : Node UfProofRuleChecker::checkInternal(ProofRule id,
41 : : const std::vector<Node>& children,
42 : : const std::vector<Node>& args)
43 : : {
44 : : // compute what was proven
45 [ + + ]: 3927638 : if (id == ProofRule::REFL)
46 : : {
47 [ - + ][ - + ]: 622645 : Assert(children.empty());
[ - - ]
48 [ - + ][ - + ]: 622645 : Assert(args.size() == 1);
[ - - ]
49 : 622645 : return args[0].eqNode(args[0]);
50 : : }
51 [ + + ]: 3304993 : else if (id == ProofRule::SYMM)
52 : : {
53 [ - + ][ - + ]: 1418660 : Assert(children.size() == 1);
[ - - ]
54 [ - + ][ - + ]: 1418660 : Assert(args.empty());
[ - - ]
55 : 1418660 : bool polarity = children[0].getKind() != Kind::NOT;
56 [ + + ]: 1418660 : Node eqp = polarity ? children[0] : children[0][0];
57 [ - + ]: 1418660 : if (eqp.getKind() != Kind::EQUAL)
58 : : {
59 : : // not a (dis)equality
60 : 0 : return Node::null();
61 : : }
62 : 2837320 : Node conc = eqp[1].eqNode(eqp[0]);
63 [ + + ]: 1418660 : return polarity ? conc : conc.notNode();
64 : 1418660 : }
65 [ + + ]: 1886333 : else if (id == ProofRule::TRANS)
66 : : {
67 [ - + ][ - + ]: 831955 : Assert(children.size() > 0);
[ - - ]
68 [ - + ][ - + ]: 831955 : Assert(args.empty());
[ - - ]
69 : 831955 : Node first;
70 : 831955 : Node curr;
71 [ + + ]: 2763541 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
72 : : {
73 : 1931586 : Node eqp = children[i];
74 [ - + ]: 1931586 : if (eqp.getKind() != Kind::EQUAL)
75 : : {
76 : 0 : return Node::null();
77 : : }
78 [ + + ]: 1931586 : if (first.isNull())
79 : : {
80 : 831955 : first = eqp[0];
81 : : }
82 [ - + ]: 1099631 : else if (eqp[0] != curr)
83 : : {
84 : 0 : return Node::null();
85 : : }
86 : 1931586 : curr = eqp[1];
87 [ + - ]: 1931586 : }
88 : 831955 : return first.eqNode(curr);
89 : 831955 : }
90 [ + + ][ + + ]: 1054378 : else if (id == ProofRule::CONG || id == ProofRule::NARY_CONG
91 [ + + ]: 77827 : || id == ProofRule::PAIRWISE_CONG)
92 : : {
93 [ - + ][ - + ]: 979038 : Assert(children.size() > 0);
[ - - ]
94 [ - + ]: 979038 : if (args.size() != 1)
95 : : {
96 : 0 : return Node::null();
97 : : }
98 : 979038 : Node t = args[0];
99 [ + - ]: 1958076 : Trace("uf-pfcheck") << "congruence " << id << " for " << args[0]
100 : 979038 : << std::endl;
101 : : // We do congruence over builtin kinds using operatorToKind
102 : 979038 : std::vector<Node> lchildren;
103 : 979038 : std::vector<Node> rchildren;
104 : 979038 : Kind k = args[0].getKind();
105 [ + + ]: 979038 : if (t.getMetaKind() == metakind::PARAMETERIZED)
106 : : {
107 : : // parameterized kinds require the operator
108 : 173330 : lchildren.push_back(t.getOperator());
109 : 173330 : rchildren.push_back(t.getOperator());
110 : : }
111 : : // congruence automatically adds variable lists
112 [ + + ]: 979038 : if (t.isClosure())
113 : : {
114 : 12104 : lchildren.push_back(t[0]);
115 : 12104 : rchildren.push_back(t[0]);
116 : : }
117 [ + + ]: 3735265 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
118 : : {
119 : 2756227 : Node eqp = children[i];
120 [ - + ]: 2756227 : if (eqp.getKind() != Kind::EQUAL)
121 : : {
122 : 0 : return Node::null();
123 : : }
124 : 2756227 : lchildren.push_back(eqp[0]);
125 : 2756227 : rchildren.push_back(eqp[1]);
126 [ + - ]: 2756227 : }
127 : 979038 : NodeManager* nm = nodeManager();
128 : 979038 : Node l = nm->mkNode(k, lchildren);
129 : 979038 : Node r = nm->mkNode(k, rchildren);
130 : 979038 : return l.eqNode(r);
131 : 979038 : }
132 [ + + ]: 75340 : else if (id == ProofRule::TRUE_INTRO)
133 : : {
134 [ - + ][ - + ]: 4946 : Assert(children.size() == 1);
[ - - ]
135 [ - + ][ - + ]: 4946 : Assert(args.empty());
[ - - ]
136 : 4946 : Node trueNode = nodeManager()->mkConst(true);
137 : 4946 : return children[0].eqNode(trueNode);
138 : 4946 : }
139 [ + + ]: 70394 : else if (id == ProofRule::TRUE_ELIM)
140 : : {
141 [ - + ][ - + ]: 45464 : Assert(children.size() == 1);
[ - - ]
142 [ - + ][ - + ]: 45464 : Assert(args.empty());
[ - - ]
143 [ + - ][ - + ]: 136392 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
144 [ + - ][ - + ]: 136392 : || !children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
145 : : {
146 : 0 : return Node::null();
147 : : }
148 : 45464 : return children[0][0];
149 : : }
150 [ + + ]: 24930 : else if (id == ProofRule::FALSE_INTRO)
151 : : {
152 [ - + ][ - + ]: 7534 : Assert(children.size() == 1);
[ - - ]
153 [ - + ][ - + ]: 7534 : Assert(args.empty());
[ - - ]
154 [ - + ]: 7534 : if (children[0].getKind() != Kind::NOT)
155 : : {
156 : 0 : return Node::null();
157 : : }
158 : 7534 : Node falseNode = nodeManager()->mkConst(false);
159 : 7534 : return children[0][0].eqNode(falseNode);
160 : 7534 : }
161 [ + + ]: 17396 : else if (id == ProofRule::FALSE_ELIM)
162 : : {
163 [ - + ][ - + ]: 16306 : Assert(children.size() == 1);
[ - - ]
164 [ - + ][ - + ]: 16306 : Assert(args.empty());
[ - - ]
165 [ + - ][ - + ]: 48918 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
166 [ + - ][ - + ]: 48918 : || children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
167 : : {
168 : 0 : return Node::null();
169 : : }
170 : 16306 : return children[0][0].notNode();
171 : : }
172 [ + + ]: 1090 : if (id == ProofRule::HO_CONG)
173 : : {
174 : 1067 : Kind k = Kind::HO_APPLY;
175 : : // kind argument is optional, defaults to HO_APPLY
176 [ + + ]: 1067 : if (args.size() == 1)
177 : : {
178 [ - + ]: 819 : if (!getKind(args[0], k))
179 : : {
180 : 0 : return Node::null();
181 : : }
182 : : }
183 : 1067 : std::vector<Node> lchildren;
184 : 1067 : std::vector<Node> rchildren;
185 [ + + ]: 4482 : for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
186 : : {
187 : 3415 : Node eqp = children[i];
188 [ - + ]: 3415 : if (eqp.getKind() != Kind::EQUAL)
189 : : {
190 : 0 : return Node::null();
191 : : }
192 : 3415 : lchildren.push_back(eqp[0]);
193 : 3415 : rchildren.push_back(eqp[1]);
194 [ + - ]: 3415 : }
195 : 1067 : NodeManager* nm = nodeManager();
196 : 1067 : Node l = nm->mkNode(k, lchildren);
197 : 1067 : Node r = nm->mkNode(k, rchildren);
198 : 1067 : return l.eqNode(r);
199 : 1067 : }
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
|
