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 : : * Common functions for dealing with proof nodes.
11 : : */
12 : :
13 : : #include "theory/arith/arith_proof_utilities.h"
14 : :
15 : : #include "proof/proof_node_algorithm.h"
16 : : #include "proof/proof_node_manager.h"
17 : : #include "theory/arith/arith_poly_norm.h"
18 : : #include "util/rational.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace arith {
23 : :
24 : 734297 : std::vector<Node> getMacroSumUbCoeff(NodeManager* nm,
25 : : const std::vector<Pf>& pfs,
26 : : const std::vector<Node>& coeffs)
27 : : {
28 [ - + ][ - + ]: 734297 : Assert(pfs.size() == coeffs.size());
[ - - ]
29 : :
30 : 734297 : std::vector<Node> premises;
31 [ + + ]: 2689614 : for (const Pf& p : pfs)
32 : : {
33 : 1955317 : premises.push_back(p->getResult());
34 : : }
35 : 1468594 : return getMacroSumUbCoeff(nm, premises, coeffs);
36 : 734297 : }
37 : 734347 : std::vector<Node> getMacroSumUbCoeff(NodeManager* nm,
38 : : const std::vector<Node>& premises,
39 : : const std::vector<Node>& coeffs)
40 : : {
41 [ - + ][ - + ]: 734347 : Assert(premises.size() == coeffs.size());
[ - - ]
42 : :
43 : 734347 : std::vector<Node> ret;
44 : 734347 : TypeNode itype = nm->integerType();
45 : 734347 : TypeNode rtype = nm->realType();
46 : : // For each coefficient, we must use a real if the lhs or rhs of the relation
47 : : // is a real, or if the coefficient is not integral.
48 [ + + ]: 2689764 : for (size_t i = 0, ncoeff = coeffs.size(); i < ncoeff; i++)
49 : : {
50 [ - + ][ - + ]: 1955417 : Assert(coeffs[i].isConst());
[ - - ]
51 : 1955417 : Node res = premises[i];
52 : 1955417 : Assert(res.getType().isBoolean() && res.getNumChildren() == 2);
53 : 1955417 : const Rational& r = coeffs[i].getConst<Rational>();
54 : 3839580 : bool isReal = !r.isIntegral() || res[0].getType().isReal()
55 : 3839580 : || res[1].getType().isReal();
56 [ + + ]: 1955417 : ret.push_back(nm->mkConstRealOrInt(isReal ? rtype : itype, r));
57 : 1955417 : }
58 : 1468694 : return ret;
59 : 734347 : }
60 : :
61 : 37565 : Node expandMacroSumUb(NodeManager* nm,
62 : : const std::vector<Node>& children,
63 : : const std::vector<Node>& args,
64 : : CDProof* cdp)
65 : : {
66 [ - + ]: 37565 : if (TraceIsOn("macro::arith"))
67 : : {
68 [ - - ]: 0 : Trace("macro::arith") << "Expand MACRO_ARITH_SCALE_SUM_UB" << std::endl;
69 [ - - ]: 0 : for (const auto& child : children)
70 : : {
71 [ - - ]: 0 : Trace("macro::arith") << " child: " << child << std::endl;
72 : : }
73 [ - - ]: 0 : Trace("macro::arith") << " args: " << args << std::endl;
74 : : }
75 [ - + ][ - + ]: 37565 : Assert(args.size() == children.size());
[ - - ]
76 : 37565 : ProofStepBuffer steps{cdp->getManager()->getChecker()};
77 : :
78 : : // Scale all children, accumulating
79 : 37565 : std::vector<Node> scaledRels;
80 : 37565 : Node one = nm->mkConstInt(Rational(1));
81 [ + + ]: 218849 : for (size_t i = 0; i < children.size(); ++i)
82 : : {
83 : 181284 : TNode child = children[i];
84 : 181284 : TNode scalar = args[i];
85 [ + + ]: 181284 : if (scalar.getConst<Rational>() == 1)
86 : : {
87 : : // if scaled by one, just take original
88 : 75044 : scaledRels.push_back(child);
89 : 75044 : continue;
90 : : }
91 : 106240 : bool isPos = scalar.getConst<Rational>() > 0;
92 : : Node scalarCmp =
93 : : nm->mkNode(isPos ? Kind::GT : Kind::LT,
94 : : scalar,
95 [ + + ]: 212480 : nm->mkConstRealOrInt(scalar.getType(), Rational(0)));
96 : : // (= scalarCmp true)
97 : 424960 : Node scalarCmpOrTrue = steps.tryStep(ProofRule::EVALUATE, {}, {scalarCmp});
98 [ - + ][ - + ]: 106240 : Assert(!scalarCmpOrTrue.isNull());
[ - - ]
99 : : // scalarCmp
100 : 212480 : steps.addStep(ProofRule::TRUE_ELIM, {scalarCmpOrTrue}, {}, scalarCmp);
101 : : // (and scalarCmp relation)
102 : : Node scalarCmpAndRel =
103 : 531200 : steps.tryStep(ProofRule::AND_INTRO, {scalarCmp, child}, {});
104 [ - + ][ - + ]: 106240 : Assert(!scalarCmpAndRel.isNull());
[ - - ]
105 : : // (=> (and scalarCmp relation) scaled)
106 : 212480 : Node impl = steps.tryStep(
107 : : isPos ? ProofRule::ARITH_MULT_POS : ProofRule::ARITH_MULT_NEG,
108 : : {},
109 [ + + ]: 318720 : {scalar, child});
110 [ - + ][ - + ]: 106240 : Assert(!impl.isNull());
[ - - ]
111 : : // scaled
112 : : Node scaled =
113 : 531200 : steps.tryStep(ProofRule::MODUS_PONENS, {scalarCmpAndRel, impl}, {});
114 [ - + ][ - + ]: 106240 : Assert(!scaled.isNull());
[ - - ]
115 : 106240 : scaledRels.emplace_back(scaled);
116 [ + + ][ + + ]: 256328 : }
117 : :
118 : 75130 : Node sumBounds = steps.tryStep(ProofRule::ARITH_SUM_UB, scaledRels, {});
119 : 37565 : cdp->addSteps(steps);
120 [ + - ]: 37565 : Trace("macro::arith") << "Expansion done. Proved: " << sumBounds << std::endl;
121 : 75130 : return sumBounds;
122 : 37565 : }
123 : :
124 : : /**
125 : : * Is n a (possibly negated) arithmetic relation, i.e. one that can be related
126 : : * to another arithmetic relation via polynomial normalization?
127 : : */
128 : 8669873 : bool isArithRel(const Node& n)
129 : : {
130 [ + + ]: 8669873 : Node atom = n.getKind() == Kind::NOT ? n[0] : n;
131 : 8669873 : Kind k = atom.getKind();
132 [ + + ][ + + ]: 8669873 : if (k != Kind::EQUAL && k != Kind::GEQ && k != Kind::LEQ && k != Kind::GT
[ + + ][ + + ]
133 [ + + ]: 1960163 : && k != Kind::LT)
134 : : {
135 : 844070 : return false;
136 : : }
137 : 7825803 : return atom[0].getType().isRealOrInt();
138 : 8669873 : }
139 : :
140 : 5168073 : std::shared_ptr<ProofNode> ensurePredTransform(ProofNodeManager* pnm,
141 : : std::shared_ptr<ProofNode>& pf,
142 : : const Node& pred)
143 : : {
144 : 5168073 : Node res = pf->getResult();
145 [ + + ]: 5168073 : if (res == pred)
146 : : {
147 : 785963 : return pf;
148 : : }
149 : : // The rewriter does not normalize equalities and does not change the type
150 : : // of an equality, hence e.g. (= (+ x 1) 2) and (= x 1), or
151 : : // (= (to_real x) 0.0) and (= x 0), have distinct rewritten forms and cannot
152 : : // be related by MACRO_SR_PRED_TRANSFORM. We relate such predicates by
153 : : // polynomial normalization instead, whenever possible.
154 [ + + ]: 4382110 : if (Pf epf = mkArithPolyNormRel(pnm, res, pred); epf != nullptr)
155 : : {
156 [ + + ][ - - ]: 6355533 : return pnm->mkNode(ProofRule::EQ_RESOLVE, {pf, epf}, {}, pred);
157 [ + + ]: 4382110 : }
158 : : // give the predicate as the expected result, which is important for
159 : : // performance (does not require proof checking).
160 : 6790797 : return pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM, {pf}, {pred}, pred);
161 : 5168073 : }
162 : :
163 : 4389823 : std::shared_ptr<ProofNode> mkArithPolyNormRel(ProofNodeManager* pnm,
164 : : const Node& a,
165 : : const Node& b)
166 : : {
167 : 4389823 : bool negated = (a.getKind() == Kind::NOT);
168 [ + + ][ + + ]: 4389823 : if (!isArithRel(a) || !isArithRel(b) || negated != (b.getKind() == Kind::NOT))
[ + + ][ + + ]
169 : : {
170 : 1756370 : return nullptr;
171 : : }
172 [ + + ]: 2633453 : Node aatom = negated ? a[0] : a;
173 [ + + ]: 2633453 : Node batom = negated ? b[0] : b;
174 : 2633453 : Rational ca, cb;
175 [ + + ]: 2633453 : if (!PolyNorm::isArithPolyNormRel(aatom, batom, ca, cb))
176 : : {
177 : 507229 : return nullptr;
178 : : }
179 : 4252448 : Node premise = PolyNorm::getArithPolyNormRelPremise(aatom, batom, ca, cb);
180 : 8504896 : Pf ppf = pnm->mkNode(ProofRule::ARITH_POLY_NORM, {}, {premise}, premise);
181 : 2126224 : Node equiv = aatom.eqNode(batom);
182 : 12757344 : Pf epf = pnm->mkNode(ProofRule::ARITH_POLY_NORM_REL, {ppf}, {equiv}, equiv);
183 [ + + ]: 2126224 : if (negated)
184 : : {
185 : : // lift the equivalence of the atoms to the negated relations
186 : 320171 : Node nequiv = a.eqNode(b);
187 : 320171 : std::vector<Node> cargs;
188 : 320171 : ProofRule cr = expr::getCongRule(a, cargs);
189 : 640342 : epf = pnm->mkNode(cr, {epf}, cargs, nequiv);
190 : 320171 : }
191 : 2126224 : return epf;
192 : 2633453 : }
193 : :
194 : 1172 : bool addArithPolyNormRel(CDProof& cdp, const Node& a, const Node& b)
195 : : {
196 : 1172 : Pf pf = mkArithPolyNormRel(cdp.getManager(), a, b);
197 [ - + ]: 1172 : if (pf == nullptr)
198 : : {
199 : 0 : return false;
200 : : }
201 : 1172 : cdp.addProof(pf);
202 : 1172 : return true;
203 : 1172 : }
204 : :
205 : : } // namespace arith
206 : : } // namespace theory
207 : : } // namespace cvc5::internal
|
