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 : 13880 : void UfProofRuleChecker::registerTo(ProofChecker* pc)
24 : : {
25 : : // add checkers
26 : 13880 : pc->registerChecker(ProofRule::REFL, this);
27 : 13880 : pc->registerChecker(ProofRule::SYMM, this);
28 : 13880 : pc->registerChecker(ProofRule::TRANS, this);
29 : 13880 : pc->registerChecker(ProofRule::CONG, this);
30 : 13880 : pc->registerChecker(ProofRule::NARY_CONG, this);
31 : 13880 : pc->registerChecker(ProofRule::PAIRWISE_CONG, this);
32 : 13880 : pc->registerChecker(ProofRule::TRUE_INTRO, this);
33 : 13880 : pc->registerChecker(ProofRule::TRUE_ELIM, this);
34 : 13880 : pc->registerChecker(ProofRule::FALSE_INTRO, this);
35 : 13880 : pc->registerChecker(ProofRule::FALSE_ELIM, this);
36 : 13880 : pc->registerChecker(ProofRule::HO_CONG, this);
37 : 13880 : pc->registerChecker(ProofRule::HO_APP_ENCODE, this);
38 : 13880 : }
39 : :
40 : 2411742 : Node UfProofRuleChecker::checkInternal(ProofRule id,
41 : : const std::vector<Node>& children,
42 : : const std::vector<Node>& args)
43 : : {
44 : : // compute what was proven
45 [ + + ]: 2411742 : if (id == ProofRule::REFL)
46 : : {
47 [ - + ][ - + ]: 329592 : Assert(children.empty());
[ - - ]
48 [ - + ][ - + ]: 329592 : Assert(args.size() == 1);
[ - - ]
49 : 329592 : return args[0].eqNode(args[0]);
50 : : }
51 [ + + ]: 2082150 : else if (id == ProofRule::SYMM)
52 : : {
53 [ - + ][ - + ]: 971166 : Assert(children.size() == 1);
[ - - ]
54 [ - + ][ - + ]: 971166 : Assert(args.empty());
[ - - ]
55 : 971166 : bool polarity = children[0].getKind() != Kind::NOT;
56 [ + + ]: 971166 : Node eqp = polarity ? children[0] : children[0][0];
57 [ - + ]: 971166 : if (eqp.getKind() != Kind::EQUAL)
58 : : {
59 : : // not a (dis)equality
60 : 0 : return Node::null();
61 : : }
62 : 1942332 : Node conc = eqp[1].eqNode(eqp[0]);
63 [ + + ]: 971166 : return polarity ? conc : conc.notNode();
64 : 971166 : }
65 [ + + ]: 1110984 : else if (id == ProofRule::TRANS)
66 : : {
67 [ - + ][ - + ]: 471328 : Assert(children.size() > 0);
[ - - ]
68 [ - + ][ - + ]: 471328 : Assert(args.empty());
[ - - ]
69 : 471328 : Node first;
70 : 471328 : Node curr;
71 [ + + ]: 1508465 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
72 : : {
73 : 1037137 : Node eqp = children[i];
74 [ - + ]: 1037137 : if (eqp.getKind() != Kind::EQUAL)
75 : : {
76 : 0 : return Node::null();
77 : : }
78 [ + + ]: 1037137 : if (first.isNull())
79 : : {
80 : 471328 : first = eqp[0];
81 : : }
82 [ - + ]: 565809 : else if (eqp[0] != curr)
83 : : {
84 : 0 : return Node::null();
85 : : }
86 : 1037137 : curr = eqp[1];
87 [ + - ]: 1037137 : }
88 : 471328 : return first.eqNode(curr);
89 : 471328 : }
90 [ + + ][ + + ]: 639656 : else if (id == ProofRule::CONG || id == ProofRule::NARY_CONG
91 [ + + ]: 34245 : || id == ProofRule::PAIRWISE_CONG)
92 : : {
93 [ - + ][ - + ]: 607236 : Assert(children.size() > 0);
[ - - ]
94 [ - + ]: 607236 : if (args.size() != 1)
95 : : {
96 : 0 : return Node::null();
97 : : }
98 : 607236 : Node t = args[0];
99 [ + - ]: 1214472 : Trace("uf-pfcheck") << "congruence " << id << " for " << args[0]
100 : 607236 : << std::endl;
101 : : // We do congruence over builtin kinds using operatorToKind
102 : 607236 : std::vector<Node> lchildren;
103 : 607236 : std::vector<Node> rchildren;
104 : 607236 : Kind k = args[0].getKind();
105 [ + + ]: 607236 : if (t.getMetaKind() == metakind::PARAMETERIZED)
106 : : {
107 : : // parameterized kinds require the operator
108 : 54576 : lchildren.push_back(t.getOperator());
109 : 54576 : rchildren.push_back(t.getOperator());
110 : : }
111 : : // congruence automatically adds variable lists
112 [ + + ]: 607236 : if (t.isClosure())
113 : : {
114 : 7822 : lchildren.push_back(t[0]);
115 : 7822 : rchildren.push_back(t[0]);
116 : : }
117 [ + + ]: 2448381 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
118 : : {
119 : 1841145 : Node eqp = children[i];
120 [ - + ]: 1841145 : if (eqp.getKind() != Kind::EQUAL)
121 : : {
122 : 0 : return Node::null();
123 : : }
124 : 1841145 : lchildren.push_back(eqp[0]);
125 : 1841145 : rchildren.push_back(eqp[1]);
126 [ + - ]: 1841145 : }
127 : 607236 : NodeManager* nm = nodeManager();
128 : 607236 : Node l = nm->mkNode(k, lchildren);
129 : 607236 : Node r = nm->mkNode(k, rchildren);
130 : 607236 : return l.eqNode(r);
131 : 607236 : }
132 [ + + ]: 32420 : else if (id == ProofRule::TRUE_INTRO)
133 : : {
134 [ - + ][ - + ]: 3174 : Assert(children.size() == 1);
[ - - ]
135 [ - + ][ - + ]: 3174 : Assert(args.empty());
[ - - ]
136 : 3174 : Node trueNode = nodeManager()->mkConst(true);
137 : 3174 : return children[0].eqNode(trueNode);
138 : 3174 : }
139 [ + + ]: 29246 : else if (id == ProofRule::TRUE_ELIM)
140 : : {
141 [ - + ][ - + ]: 21115 : Assert(children.size() == 1);
[ - - ]
142 [ - + ][ - + ]: 21115 : Assert(args.empty());
[ - - ]
143 [ + - ][ - + ]: 63345 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
144 [ + - ][ - + ]: 63345 : || !children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
145 : : {
146 : 0 : return Node::null();
147 : : }
148 : 21115 : return children[0][0];
149 : : }
150 [ + + ]: 8131 : else if (id == ProofRule::FALSE_INTRO)
151 : : {
152 [ - + ][ - + ]: 3908 : Assert(children.size() == 1);
[ - - ]
153 [ - + ][ - + ]: 3908 : Assert(args.empty());
[ - - ]
154 [ - + ]: 3908 : if (children[0].getKind() != Kind::NOT)
155 : : {
156 : 0 : return Node::null();
157 : : }
158 : 3908 : Node falseNode = nodeManager()->mkConst(false);
159 : 3908 : return children[0][0].eqNode(falseNode);
160 : 3908 : }
161 [ + + ]: 4223 : else if (id == ProofRule::FALSE_ELIM)
162 : : {
163 [ - + ][ - + ]: 3530 : Assert(children.size() == 1);
[ - - ]
164 [ - + ][ - + ]: 3530 : Assert(args.empty());
[ - - ]
165 [ + - ][ - + ]: 10590 : if (children[0].getKind() != Kind::EQUAL || !children[0][1].isConst()
[ - - ]
166 [ + - ][ - + ]: 10590 : || children[0][1].getConst<bool>())
[ + - ][ + - ]
[ - - ]
167 : : {
168 : 0 : return Node::null();
169 : : }
170 : 3530 : return children[0][0].notNode();
171 : : }
172 [ + + ]: 693 : if (id == ProofRule::HO_CONG)
173 : : {
174 : 686 : Kind k = Kind::HO_APPLY;
175 : : // kind argument is optional, defaults to HO_APPLY
176 [ + + ]: 686 : if (args.size() == 1)
177 : : {
178 [ - + ]: 481 : if (!getKind(args[0], k))
179 : : {
180 : 0 : return Node::null();
181 : : }
182 : : }
183 : 686 : std::vector<Node> lchildren;
184 : 686 : std::vector<Node> rchildren;
185 [ + + ]: 2772 : for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
186 : : {
187 : 2086 : Node eqp = children[i];
188 [ - + ]: 2086 : if (eqp.getKind() != Kind::EQUAL)
189 : : {
190 : 0 : return Node::null();
191 : : }
192 : 2086 : lchildren.push_back(eqp[0]);
193 : 2086 : rchildren.push_back(eqp[1]);
194 [ + - ]: 2086 : }
195 : 686 : NodeManager* nm = nodeManager();
196 : 686 : Node l = nm->mkNode(k, lchildren);
197 : 686 : Node r = nm->mkNode(k, rchildren);
198 : 686 : return l.eqNode(r);
199 : 686 : }
200 [ + - ]: 7 : else if (id == ProofRule::HO_APP_ENCODE)
201 : : {
202 [ - + ][ - + ]: 7 : Assert(args.size() == 1);
[ - - ]
203 : 7 : Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
204 : 7 : return args[0].eqNode(ret);
205 : 7 : }
206 : : // no rule
207 : 0 : return Node::null();
208 : : }
209 : :
210 : : } // namespace uf
211 : : } // namespace theory
212 : : } // namespace cvc5::internal
|
