Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Yoni Zohar, Aina Niemetz, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of pow2 solver.
14 : : */
15 : :
16 : : #include "theory/arith/nl/pow2_solver.h"
17 : :
18 : : #include "options/arith_options.h"
19 : : #include "options/smt_options.h"
20 : : #include "preprocessing/passes/bv_to_int.h"
21 : : #include "theory/arith/arith_msum.h"
22 : : #include "theory/arith/arith_utilities.h"
23 : : #include "theory/arith/inference_manager.h"
24 : : #include "theory/arith/nl/nl_model.h"
25 : : #include "theory/rewriter.h"
26 : : #include "util/bitvector.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace arith {
33 : : namespace nl {
34 : :
35 : 32702 : Pow2Solver::Pow2Solver(Env& env,
36 : : InferenceManager& im,
37 : 32702 : NlModel& model)
38 : 32702 : : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext())
39 : : {
40 : 32702 : NodeManager* nm = nodeManager();
41 : 32702 : d_false = nm->mkConst(false);
42 : 32702 : d_true = nm->mkConst(true);
43 : 32702 : d_zero = nm->mkConstInt(Rational(0));
44 : 32702 : d_one = nm->mkConstInt(Rational(1));
45 : 32702 : d_two = nm->mkConstInt(Rational(2));
46 : 32702 : }
47 : :
48 : 32418 : Pow2Solver::~Pow2Solver() {}
49 : :
50 : 10986 : void Pow2Solver::initLastCall(const std::vector<Node>& xts)
51 : : {
52 : 10986 : d_pow2s.clear();
53 [ + - ]: 10986 : Trace("pow2-mv") << "POW2 terms : " << std::endl;
54 [ + + ]: 70779 : for (const Node& a : xts)
55 : : {
56 : 59793 : Kind ak = a.getKind();
57 [ + + ]: 59793 : if (ak != Kind::POW2)
58 : : {
59 : : // don't care about other terms
60 : 58925 : continue;
61 : : }
62 : 868 : d_pow2s.push_back(a);
63 : : }
64 [ + - ]: 10986 : Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl;
65 : 10986 : }
66 : :
67 : 10986 : void Pow2Solver::checkInitialRefine()
68 : : {
69 [ + - ]: 10986 : Trace("pow2-check") << "Pow2Solver::checkInitialRefine" << std::endl;
70 : 10986 : NodeManager* nm = nodeManager();
71 [ + + ]: 11854 : for (const Node& i : d_pow2s)
72 : : {
73 [ + + ]: 868 : if (d_initRefine.find(i) != d_initRefine.end())
74 : : {
75 : : // already sent initial axioms for i in this user context
76 : 706 : continue;
77 : : }
78 : 162 : d_initRefine.insert(i);
79 : : // initial refinement lemmas
80 : 324 : std::vector<Node> conj;
81 : : // x>=0 -> pow2(x) > 0
82 : 486 : Node xgeq0 = nm->mkNode(Kind::GEQ, i[0], d_zero);
83 : 486 : Node nonegative = nm->mkNode(Kind::GT, i, d_zero);
84 : 162 : conj.push_back(nm->mkNode(Kind::IMPLIES, xgeq0, nonegative));
85 : :
86 : : // even: x != 0 -> pow2(x) mod 2 = 0
87 : 486 : Node xgt0 = nm->mkNode(Kind::DISTINCT, i[0], d_zero);
88 : 486 : Node mod2 = nm->mkNode(Kind::INTS_MODULUS, i, d_two);
89 : 486 : Node even = nm->mkNode(Kind::EQUAL, mod2, d_zero);
90 : 162 : conj.push_back(nm->mkNode(Kind::IMPLIES, xgt0, even));
91 : :
92 : 324 : Node lem = nm->mkAnd(conj);
93 [ + - ]: 324 : Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; INIT_REFINE"
94 : 162 : << std::endl;
95 : 162 : d_im.addPendingLemma(lem, InferenceId::ARITH_NL_POW2_INIT_REFINE);
96 : : }
97 : 10986 : }
98 : :
99 : 2167 : void Pow2Solver::sortPow2sBasedOnModel()
100 : : {
101 : : struct
102 : : {
103 : 50 : bool operator()(Node a, Node b, NlModel& model) const
104 : : {
105 : 100 : return model.computeConcreteModelValue(a[0])
106 : 150 : < model.computeConcreteModelValue(b[0]);
107 : : }
108 : : } modelSort;
109 : : using namespace std::placeholders;
110 : 2167 : std::sort(
111 : 4334 : d_pow2s.begin(), d_pow2s.end(), std::bind(modelSort, _1, _2, d_model));
112 : 2167 : }
113 : :
114 : 2167 : void Pow2Solver::checkFullRefine()
115 : : {
116 [ + - ]: 2167 : Trace("pow2-check") << "Pow2Solver::checkFullRefine" << std::endl;
117 : 2167 : NodeManager* nm = nodeManager();
118 : 2167 : sortPow2sBasedOnModel();
119 : : // add lemmas for each pow2 term
120 [ + + ]: 2339 : for (uint64_t i = 0, size = d_pow2s.size(); i < size; i++)
121 : : {
122 : 172 : Node n = d_pow2s[i];
123 : 172 : Node valPow2xAbstract = d_model.computeAbstractModelValue(n);
124 : 172 : Node valPow2xConcrete = d_model.computeConcreteModelValue(n);
125 : 344 : Node valXConcrete = d_model.computeConcreteModelValue(n[0]);
126 [ - + ]: 172 : if (TraceIsOn("pow2-check"))
127 : : {
128 [ - - ]: 0 : Trace("pow2-check") << "* " << i << ", value = " << valPow2xAbstract
129 : 0 : << std::endl;
130 [ - - ]: 0 : Trace("pow2-check") << " actual " << valXConcrete << " = "
131 : 0 : << valPow2xConcrete << std::endl;
132 : : }
133 [ + + ]: 172 : if (valPow2xAbstract == valPow2xConcrete)
134 : : {
135 [ + - ]: 27 : Trace("pow2-check") << "...already correct" << std::endl;
136 : 27 : continue;
137 : : }
138 : :
139 : 290 : Integer x = valXConcrete.getConst<Rational>().getNumerator();
140 : 290 : Integer pow2x = valPow2xAbstract.getConst<Rational>().getNumerator();
141 : : // add monotinicity lemmas
142 [ + + ]: 177 : for (uint64_t j = i + 1; j < size; j++)
143 : : {
144 : 64 : Node m = d_pow2s[j];
145 : 64 : Node valPow2yAbstract = d_model.computeAbstractModelValue(m);
146 : 96 : Node valYConcrete = d_model.computeConcreteModelValue(m[0]);
147 : :
148 : 64 : Integer y = valYConcrete.getConst<Rational>().getNumerator();
149 : 64 : Integer pow2y = valPow2yAbstract.getConst<Rational>().getNumerator();
150 : :
151 [ + + ][ + + ]: 32 : if (x >= 0 && x < y && pow2x >= pow2y)
[ + - ][ + - ]
[ + + ][ - - ]
152 : : {
153 : : // 0 <= x /\ x < y => pow2(x) < pow2(y)
154 : 42 : Node x_lt_y = nm->mkNode(Kind::LT, n[0], m[0]);
155 : 42 : Node xgeq0 = nm->mkNode(Kind::LEQ, d_zero, n[0]);
156 : 42 : Node assumption = nm->mkNode(Kind::AND, xgeq0, x_lt_y);
157 : 42 : Node conclusion = nm->mkNode(Kind::LT, n, m);
158 : 42 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
159 : 14 : d_im.addPendingLemma(
160 : : lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, nullptr, true);
161 : : }
162 [ + + ][ + - ]: 18 : else if (y <= 0 && y < x && pow2x <= pow2y)
[ - + ][ + - ]
[ - + ][ - - ]
163 : : {
164 : : // 0 <= y /\ y < x => pow2(y) < pow2(x)
165 : 0 : Node assumption = nm->mkNode(Kind::LT, m[0], n[0]);
166 : 0 : Node conclusion = nm->mkNode(Kind::LT, m, n);
167 : 0 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
168 : 0 : d_im.addPendingLemma(
169 : : lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, nullptr, true);
170 : : }
171 : : }
172 : :
173 : : // neg lemmas: pow2(x) = 0 whenever x < 0
174 : 145 : if (x < 0 && pow2x != 0)
175 : : {
176 : 87 : Node assumption = nm->mkNode(Kind::LT, n[0], d_zero);
177 : 87 : Node conclusion = nm->mkNode(Kind::EQUAL, n, mkZero(n.getType()));
178 : 87 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
179 : 29 : d_im.addPendingLemma(
180 : : lem, InferenceId::ARITH_NL_POW2_NEG_REFINE, nullptr, true);
181 : : }
182 : :
183 : : // div 0: x div pow2(x) = 0 whenever x >= 0
184 [ + + ][ + + ]: 145 : if (x >= 0 && x > pow2x)
[ + - ][ + + ]
[ - - ]
185 : : {
186 : 126 : Node assumption = nm->mkNode(Kind::GEQ, n[0], d_zero);
187 : 126 : Node div_zero = nm->mkNode(Kind::INTS_DIVISION, n[0], n);
188 : 126 : Node conclusion = nm->mkNode(Kind::EQUAL, div_zero, d_zero);
189 : 126 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
190 : 42 : d_im.addPendingLemma(
191 : : lem, InferenceId::ARITH_NL_POW2_DIV0_CASE_REFINE, nullptr, true);
192 : : }
193 : :
194 : : // lower bound: x >= 7 => pow2(x) > kx + k^2
195 : 145 : if (x >= 7 && pow2x <= x * x * 2)
196 : : {
197 : 62 : Node d_seven = nm->mkConstInt(Rational(7));
198 : 93 : Node k_gt_5 = nm->mkNode(Kind::GEQ, valXConcrete, d_seven);
199 : 93 : Node x_gt_k = nm->mkNode(Kind::GEQ, n[0], valXConcrete);
200 : 93 : Node assumption = nm->mkNode(Kind::AND, x_gt_k, k_gt_5);
201 : 93 : Node kx = nm->mkNode(Kind::MULT, valXConcrete, n[0]);
202 : 93 : Node k_squar = nm->mkNode(Kind::MULT, valXConcrete, valXConcrete);
203 : 93 : Node kx_plus_k_squar = nm->mkNode(Kind::ADD, kx, k_squar);
204 : 93 : Node conclusion = nm->mkNode(Kind::GT, n, kx_plus_k_squar);
205 : 93 : Node lem = nm->mkNode(Kind::IMPLIES, assumption, conclusion);
206 : 31 : d_im.addPendingLemma(lem,
207 : : InferenceId::ARITH_NL_POW2_LOWER_BOUND_CASE_REFINE,
208 : : nullptr,
209 : : true);
210 : : }
211 : :
212 : : // Place holder for additional lemma schemas
213 : :
214 : : // End of additional lemma schemas
215 : :
216 : : // this is the most naive model-based schema based on model values
217 : 290 : Node lem = valueBasedLemma(n);
218 [ + - ]: 290 : Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE"
219 : 145 : << std::endl;
220 : : // send the value lemma
221 : 145 : d_im.addPendingLemma(
222 : : lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true);
223 : : }
224 : 2167 : }
225 : :
226 : 145 : Node Pow2Solver::valueBasedLemma(Node i)
227 : : {
228 [ - + ][ - + ]: 145 : Assert(i.getKind() == Kind::POW2);
[ - - ]
229 : 290 : Node x = i[0];
230 : :
231 : 290 : Node valX = d_model.computeConcreteModelValue(x);
232 : :
233 : 145 : NodeManager* nm = nodeManager();
234 : 145 : Node valC = nm->mkNode(Kind::POW2, valX);
235 : 145 : valC = rewrite(valC);
236 : :
237 : 290 : return nm->mkNode(Kind::IMPLIES, x.eqNode(valX), i.eqNode(valC));
238 : : }
239 : :
240 : : } // namespace nl
241 : : } // namespace arith
242 : : } // namespace theory
243 : : } // namespace cvc5::internal
|
