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 pow2 solver.
11 : : */
12 : :
13 : : #include "theory/arith/nl/pow2_solver.h"
14 : :
15 : : #include "options/arith_options.h"
16 : : #include "options/smt_options.h"
17 : : #include "preprocessing/passes/bv_to_int.h"
18 : : #include "proof/proof.h"
19 : : #include "smt/env.h"
20 : : #include "theory/arith/arith_msum.h"
21 : : #include "theory/arith/arith_utilities.h"
22 : : #include "theory/arith/inference_manager.h"
23 : : #include "theory/arith/nl/nl_model.h"
24 : : #include "theory/rewriter.h"
25 : : #include "util/bitvector.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace arith {
32 : : namespace nl {
33 : :
34 : 14965 : Pow2Solver::Pow2Solver(Env& env, InferenceManager& im, NlModel& model)
35 : 14965 : : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext())
36 : : {
37 : 14965 : NodeManager* nm = nodeManager();
38 : 14965 : d_false = nm->mkConst(false);
39 : 14965 : d_true = nm->mkConst(true);
40 : 14965 : d_zero = nm->mkConstInt(Rational(0));
41 : 14965 : d_one = nm->mkConstInt(Rational(1));
42 : 14965 : d_two = nm->mkConstInt(Rational(2));
43 [ + + ]: 14965 : if (env.isTheoryProofProducing())
44 : : {
45 : 10662 : d_proof.reset(
46 : 10662 : new CDProofSet<CDProof>(env, env.getUserContext(), "nl-pow2"));
47 : : }
48 : 14965 : }
49 : :
50 : 14958 : Pow2Solver::~Pow2Solver() {}
51 : :
52 : 339 : bool Pow2Solver::isProofEnabled() const { return d_proof.get() != nullptr; }
53 : :
54 : 105 : CDProof* Pow2Solver::getProof()
55 : : {
56 [ - + ][ - + ]: 105 : Assert(isProofEnabled());
[ - - ]
57 : 105 : return d_proof->allocateProof(d_env.getUserContext());
58 : : }
59 : :
60 : 11019 : void Pow2Solver::initLastCall(const std::vector<Node>& xts)
61 : : {
62 : 11019 : d_pow2s.clear();
63 [ + - ]: 11019 : Trace("pow2-mv") << "POW2 terms : " << std::endl;
64 [ + + ]: 73374 : for (const Node& a : xts)
65 : : {
66 : 62355 : Kind ak = a.getKind();
67 [ + + ]: 62355 : if (ak != Kind::POW2)
68 : : {
69 : : // don't care about other terms
70 : 61551 : continue;
71 : : }
72 : 804 : d_pow2s.push_back(a);
73 : : }
74 [ + - ]: 11019 : Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl;
75 : 11019 : }
76 : :
77 : 11019 : void Pow2Solver::checkInitialRefine()
78 : : {
79 [ + - ]: 11019 : Trace("pow2-check") << "Pow2Solver::checkInitialRefine" << std::endl;
80 : 11019 : NodeManager* nm = nodeManager();
81 [ + + ]: 11823 : for (const Node& i : d_pow2s)
82 : : {
83 [ + + ]: 804 : if (d_initRefine.find(i) != d_initRefine.end())
84 : : {
85 : : // already sent initial axioms for i in this user context
86 : 648 : continue;
87 : : }
88 : 156 : d_initRefine.insert(i);
89 : : // initial refinement lemmas
90 : 156 : std::vector<Node> conj;
91 : : // x>=0 -> pow2(x) > 0
92 : 312 : Node xgeq0 = nm->mkNode(Kind::GEQ, i[0], d_zero);
93 : 312 : Node nonegative = nm->mkNode(Kind::GT, i, d_zero);
94 : 156 : conj.push_back(nm->mkNode(Kind::IMPLIES, xgeq0, nonegative));
95 : :
96 : : // even: x != 0 -> pow2(x) mod 2 = 0
97 : 312 : Node xgt0 = nm->mkNode(Kind::DISTINCT, i[0], d_zero);
98 : 312 : Node mod2 = nm->mkNode(Kind::INTS_MODULUS, i, d_two);
99 : 312 : Node even = nm->mkNode(Kind::EQUAL, mod2, d_zero);
100 : 156 : conj.push_back(nm->mkNode(Kind::IMPLIES, xgt0, even));
101 : :
102 : : // neg: x < 0 -> pow2(x) = 0
103 : 312 : Node xlt0 = nm->mkNode(Kind::LT, i[0], d_zero);
104 : 312 : Node eq0 = nm->mkNode(Kind::EQUAL, i, mkZero(i.getType()));
105 : 312 : Node neg = nm->mkNode(Kind::IMPLIES, xlt0, eq0);
106 : 156 : conj.push_back(neg);
107 : :
108 : 156 : Node lem = nm->mkAnd(conj);
109 [ + - ]: 312 : Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; INIT_REFINE"
110 : 156 : << std::endl;
111 : 156 : CDProof* proof = nullptr;
112 [ + + ]: 156 : if (isProofEnabled())
113 : : {
114 : 75 : proof = getProof();
115 : 150 : proof->addStep(lem, ProofRule::ARITH_POW2_INIT, {}, {i[0]});
116 : : }
117 [ + + ]: 156 : d_im.addPendingLemma(lem, InferenceId::ARITH_NL_POW2_INIT_REFINE, proof);
118 : 156 : }
119 : 11019 : }
120 : :
121 : 2018 : void Pow2Solver::sortPow2sBasedOnModel()
122 : : {
123 : : struct
124 : : {
125 : 40 : bool operator()(Node a, Node b, NlModel& model) const
126 : : {
127 : 80 : return model.computeConcreteModelValue(a[0])
128 : 120 : < model.computeConcreteModelValue(b[0]);
129 : : }
130 : : } modelSort;
131 : : using namespace std::placeholders;
132 : 2018 : std::sort(
133 : 4036 : d_pow2s.begin(), d_pow2s.end(), std::bind(modelSort, _1, _2, d_model));
134 : 2018 : }
135 : :
136 : 2018 : void Pow2Solver::checkFullRefine()
137 : : {
138 [ + - ]: 2018 : Trace("pow2-check") << "Pow2Solver::checkFullRefine" << std::endl;
139 : 2018 : NodeManager* nm = nodeManager();
140 : 2018 : sortPow2sBasedOnModel();
141 : : // add lemmas for each pow2 term
142 [ + + ]: 2143 : for (uint64_t i = 0, size = d_pow2s.size(); i < size; i++)
143 : : {
144 : 125 : Node n = d_pow2s[i];
145 : 125 : Node valPow2xAbstract = d_model.computeAbstractModelValue(n);
146 : 125 : Node valPow2xConcrete = d_model.computeConcreteModelValue(n);
147 : 250 : Node valXConcrete = d_model.computeConcreteModelValue(n[0]);
148 [ - + ]: 125 : if (TraceIsOn("pow2-check"))
149 : : {
150 [ - - ]: 0 : Trace("pow2-check") << "* " << i << ", value = " << valPow2xAbstract
151 : 0 : << std::endl;
152 [ - - ]: 0 : Trace("pow2-check") << " actual " << valXConcrete << " = "
153 : 0 : << valPow2xConcrete << std::endl;
154 : : }
155 [ + + ]: 125 : if (valPow2xAbstract == valPow2xConcrete)
156 : : {
157 [ + - ]: 18 : Trace("pow2-check") << "...already correct" << std::endl;
158 : 18 : continue;
159 : : }
160 : :
161 : 107 : Integer x = valXConcrete.getConst<Rational>().getNumerator();
162 : 107 : Integer pow2x = valPow2xAbstract.getConst<Rational>().getNumerator();
163 : : // add monotinicity lemmas
164 [ + + ]: 129 : for (uint64_t j = i + 1; j < size; j++)
165 : : {
166 : 22 : Node m = d_pow2s[j];
167 : 22 : Node valPow2yAbstract = d_model.computeAbstractModelValue(m);
168 : 44 : Node valYConcrete = d_model.computeConcreteModelValue(m[0]);
169 : :
170 : 22 : Integer y = valYConcrete.getConst<Rational>().getNumerator();
171 : 22 : Integer pow2y = valPow2yAbstract.getConst<Rational>().getNumerator();
172 : :
173 [ + - ][ + + ]: 22 : if (x >= 0 && x < y && pow2x >= pow2y)
[ + - ][ + - ]
[ + + ][ - - ]
174 : : {
175 : : // 0 <= x /\ x < y => pow2(x) < pow2(y)
176 : 24 : Node x_lt_y = nm->mkNode(Kind::LT, n[0], m[0]);
177 : 24 : Node xgeq0 = nm->mkNode(Kind::LEQ, d_zero, n[0]);
178 : 24 : Node assumption = nm->mkNode(Kind::AND, xgeq0, x_lt_y);
179 : 24 : Node conclusion = nm->mkNode(Kind::LT, n, m);
180 : 24 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
181 : 12 : CDProof* proof = nullptr;
182 [ + + ]: 12 : if (isProofEnabled())
183 : : {
184 : 6 : proof = getProof();
185 [ + + ][ - - ]: 18 : proof->addStep(lem, ProofRule::ARITH_POW2_MONOTONE, {}, {n[0], m[0]});
186 : : }
187 [ + + ]: 12 : d_im.addPendingLemma(
188 : : lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, proof, true);
189 : 12 : }
190 [ + + ][ - + ]: 10 : else if (y >= 0 && y < x && pow2x <= pow2y)
[ - - ][ + - ]
[ - + ][ - - ]
191 : : {
192 : : // 0 <= y /\ y < x => pow2(y) < pow2(x).
193 : 0 : Node y_lt_x = nm->mkNode(Kind::LT, m[0], n[0]);
194 : 0 : Node ygeq0 = nm->mkNode(Kind::LEQ, d_zero, m[0]);
195 : 0 : Node assumption = nm->mkNode(Kind::AND, ygeq0, y_lt_x);
196 : 0 : Node conclusion = nm->mkNode(Kind::LT, m, n);
197 : 0 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
198 : 0 : CDProof* proof = nullptr;
199 [ - - ]: 0 : if (isProofEnabled())
200 : : {
201 : 0 : proof = getProof();
202 : 0 : proof->addStep(lem, ProofRule::ARITH_POW2_MONOTONE, {}, {m[0], n[0]});
203 : : }
204 [ - - ]: 0 : d_im.addPendingLemma(
205 : : lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, proof, true);
206 : 0 : }
207 : 22 : }
208 : :
209 : : // div 0: x div pow2(x) = 0 whenever x >= 0
210 [ + - ][ + + ]: 107 : if (x >= 0 && x > pow2x)
[ + - ][ + + ]
[ - - ]
211 : : {
212 : 76 : Node assumption = nm->mkNode(Kind::GEQ, n[0], d_zero);
213 : 76 : Node div_zero = nm->mkNode(Kind::INTS_DIVISION, n[0], n);
214 : 76 : Node conclusion = nm->mkNode(Kind::EQUAL, div_zero, d_zero);
215 : 76 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
216 : 38 : CDProof* proof = nullptr;
217 [ + + ]: 38 : if (isProofEnabled())
218 : : {
219 : 15 : proof = getProof();
220 : 30 : proof->addStep(lem, ProofRule::ARITH_POW2_DIV0, {}, {n[0]});
221 : : }
222 [ + + ]: 38 : d_im.addPendingLemma(
223 : : lem, InferenceId::ARITH_NL_POW2_DIV0_CASE_REFINE, proof, true);
224 : 38 : }
225 : :
226 : : // lower bound: x >= k /\ k >= 7 => pow2(x) > kx + k^2
227 : 107 : if (x >= 7 && pow2x <= x * x * 2)
228 : : {
229 : 28 : Node d_seven = nm->mkConstInt(Rational(7));
230 : 56 : Node k_gt_5 = nm->mkNode(Kind::GEQ, valXConcrete, d_seven);
231 : 56 : Node x_gt_k = nm->mkNode(Kind::GEQ, n[0], valXConcrete);
232 : 56 : Node assumption = nm->mkNode(Kind::AND, x_gt_k, k_gt_5);
233 : 56 : Node kx = nm->mkNode(Kind::MULT, valXConcrete, n[0]);
234 : 56 : Node k_squar = nm->mkNode(Kind::MULT, valXConcrete, valXConcrete);
235 : 56 : Node kx_plus_k_squar = nm->mkNode(Kind::ADD, kx, k_squar);
236 : 56 : Node conclusion = nm->mkNode(Kind::GT, n, kx_plus_k_squar);
237 : 56 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
238 : 28 : CDProof* proof = nullptr;
239 [ + + ]: 28 : if (isProofEnabled())
240 : : {
241 : 9 : proof = getProof();
242 [ + + ][ - - ]: 27 : proof->addStep(
243 : : lem, ProofRule::ARITH_POW2_LOWER_BOUND, {}, {n[0], valXConcrete});
244 : : }
245 [ + + ]: 28 : d_im.addPendingLemma(
246 : : lem, InferenceId::ARITH_NL_POW2_LOWER_BOUND_CASE_REFINE, proof, true);
247 : 28 : }
248 : :
249 : : // Place holder for additional lemma schemas
250 : :
251 : : // End of additional lemma schemas
252 : :
253 : : // this is the most naive model-based schema based on model values
254 : 107 : Node lem = valueBasedLemma(n);
255 [ + - ]: 214 : Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE"
256 : 107 : << std::endl;
257 : : // send the value lemma
258 : 107 : d_im.addPendingLemma(
259 : : lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true);
260 [ + + ][ + + ]: 179 : }
[ + + ][ + + ]
261 : 2018 : }
262 : :
263 : 107 : Node Pow2Solver::valueBasedLemma(Node i)
264 : : {
265 [ - + ][ - + ]: 107 : Assert(i.getKind() == Kind::POW2);
[ - - ]
266 : 107 : Node x = i[0];
267 : :
268 : 107 : Node valX = d_model.computeConcreteModelValue(x);
269 : :
270 : 107 : NodeManager* nm = nodeManager();
271 : 107 : Node valC = nm->mkNode(Kind::POW2, valX);
272 : 107 : valC = rewrite(valC);
273 : :
274 [ + + ][ - - ]: 535 : return nm->mkNode(Kind::IMPLIES, {x.eqNode(valX), i.eqNode(valC)});
275 : 107 : }
276 : :
277 : : } // namespace nl
278 : : } // namespace arith
279 : : } // namespace theory
280 : : } // namespace cvc5::internal
|
