Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Makai Mann, Aina Niemetz
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 integer and (IAND) solver.
14 : : */
15 : :
16 : : #include "theory/arith/nl/iand_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 : : #include "util/iand.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace arith {
34 : : namespace nl {
35 : :
36 : 32702 : IAndSolver::IAndSolver(Env& env, InferenceManager& im, NlModel& model)
37 : : : EnvObj(env),
38 : : d_im(im),
39 : : d_model(model),
40 : : d_iandUtils(env.getNodeManager()),
41 : 32702 : d_initRefine(userContext())
42 : : {
43 : 32702 : NodeManager* nm = nodeManager();
44 : 32702 : d_false = nm->mkConst(false);
45 : 32702 : d_true = nm->mkConst(true);
46 : 32702 : d_zero = nm->mkConstInt(Rational(0));
47 : 32702 : d_one = nm->mkConstInt(Rational(1));
48 : 32702 : d_two = nm->mkConstInt(Rational(2));
49 : 32702 : }
50 : :
51 : 32418 : IAndSolver::~IAndSolver() {}
52 : :
53 : 11139 : void IAndSolver::initLastCall(const std::vector<Node>& xts)
54 : : {
55 : 11139 : d_iands.clear();
56 : :
57 [ + - ]: 11139 : Trace("iand-mv") << "IAND terms : " << std::endl;
58 [ + + ]: 71170 : for (const Node& a : xts)
59 : : {
60 : 60031 : Kind ak = a.getKind();
61 [ + + ]: 60031 : if (ak != Kind::IAND)
62 : : {
63 : : // don't care about other terms
64 : 59246 : continue;
65 : : }
66 : 785 : size_t bsize = a.getOperator().getConst<IntAnd>().d_size;
67 : 785 : d_iands[bsize].push_back(a);
68 [ + - ]: 785 : Trace("iand-mv") << "- " << a << std::endl;
69 : : }
70 : 11139 : }
71 : :
72 : 11139 : void IAndSolver::checkInitialRefine()
73 : : {
74 [ + - ]: 11139 : Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl;
75 : 11139 : NodeManager* nm = nodeManager();
76 [ + + ]: 11876 : for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
77 : : {
78 : : // the reference bitwidth
79 : 737 : unsigned k = is.first;
80 [ + + ]: 1522 : for (const Node& i : is.second)
81 : : {
82 [ + + ]: 785 : if (d_initRefine.find(i) != d_initRefine.end())
83 : : {
84 : : // already sent initial axioms for i in this user context
85 : 630 : continue;
86 : : }
87 : 155 : d_initRefine.insert(i);
88 : 310 : Node op = i.getOperator();
89 : 155 : uint32_t bsize = op.getConst<IntAnd>().d_size;
90 : 465 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
91 : 465 : Node arg0Mod = nm->mkNode(Kind::INTS_MODULUS, i[0], twok);
92 : 465 : Node arg1Mod = nm->mkNode(Kind::INTS_MODULUS, i[1], twok);
93 : : // initial refinement lemmas
94 : 310 : std::vector<Node> conj;
95 : : // iand(x,y)=iand(y,x) is guaranteed by rewriting
96 [ - + ][ - + ]: 155 : Assert(i[0] <= i[1]);
[ - - ]
97 : : // conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0])));
98 : : // 0 <= iand(x,y) < 2^k
99 : 155 : conj.push_back(nm->mkNode(Kind::LEQ, d_zero, i));
100 : 155 : conj.push_back(nm->mkNode(Kind::LT, i, rewrite(d_iandUtils.twoToK(k))));
101 : : // iand(x,y)<=mod(x, 2^k)
102 : 155 : conj.push_back(nm->mkNode(Kind::LEQ, i, arg0Mod));
103 : : // iand(x,y)<=mod(y, 2^k)
104 : 155 : conj.push_back(nm->mkNode(Kind::LEQ, i, arg1Mod));
105 : : // x=y => iand(x,y)=mod(x, 2^k)
106 : 155 : conj.push_back(
107 : 310 : nm->mkNode(Kind::IMPLIES, i[0].eqNode(i[1]), i.eqNode(arg0Mod)));
108 [ - + ]: 310 : Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(Kind::AND, conj);
109 [ + - ]: 310 : Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
110 : 155 : << std::endl;
111 : 155 : d_im.addPendingLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE);
112 : : }
113 : : }
114 : 11139 : }
115 : :
116 : 2167 : void IAndSolver::checkFullRefine()
117 : : {
118 [ + - ]: 2167 : Trace("iand-check") << "IAndSolver::checkFullRefine";
119 [ + - ]: 2167 : Trace("iand-check") << "IAND terms: " << std::endl;
120 [ + + ]: 2661 : for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
121 : : {
122 : : // the reference bitwidth
123 : 494 : unsigned k = is.first;
124 [ + + ]: 1027 : for (const Node& i : is.second)
125 : : {
126 : 533 : Node valAndXY = d_model.computeAbstractModelValue(i);
127 : 533 : Node valAndXYC = d_model.computeConcreteModelValue(i);
128 [ - + ]: 533 : if (TraceIsOn("iand-check"))
129 : : {
130 : 0 : Node x = i[0];
131 : 0 : Node y = i[1];
132 : :
133 : 0 : Node valX = d_model.computeConcreteModelValue(x);
134 : 0 : Node valY = d_model.computeConcreteModelValue(y);
135 : :
136 [ - - ]: 0 : Trace("iand-check")
137 : 0 : << "* " << i << ", value = " << valAndXY << std::endl;
138 [ - - ]: 0 : Trace("iand-check") << " actual (" << valX << ", " << valY
139 : 0 : << ") = " << valAndXYC << std::endl;
140 : : // print the bit-vector versions
141 : 0 : Node bvalX = convertToBvK(k, valX);
142 : 0 : Node bvalY = convertToBvK(k, valY);
143 : 0 : Node bvalAndXY = convertToBvK(k, valAndXY);
144 : 0 : Node bvalAndXYC = convertToBvK(k, valAndXYC);
145 : :
146 [ - - ]: 0 : Trace("iand-check") << " bv-value = " << bvalAndXY << std::endl;
147 [ - - ]: 0 : Trace("iand-check") << " bv-actual (" << bvalX << ", " << bvalY
148 : 0 : << ") = " << bvalAndXYC << std::endl;
149 : : }
150 [ + + ]: 533 : if (valAndXY == valAndXYC)
151 : : {
152 [ + - ]: 39 : Trace("iand-check") << "...already correct" << std::endl;
153 : 39 : continue;
154 : : }
155 : :
156 : : // ************* additional lemma schemas go here
157 [ + + ]: 494 : if (options().smt.iandMode == options::IandMode::SUM)
158 : : {
159 : 30 : Node lem = sumBasedLemma(i); // add lemmas based on sum mode
160 [ + - ]: 30 : Trace("iand-lemma")
161 : 15 : << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl;
162 : : // note that lemma can contain div/mod, and will be preprocessed in the
163 : : // prop engine
164 : 15 : d_im.addPendingLemma(
165 : : lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
166 : : }
167 [ + + ]: 479 : else if (options().smt.iandMode == options::IandMode::BITWISE)
168 : : {
169 : 54 : Node lem = bitwiseLemma(i); // check for violated bitwise axioms
170 [ + - ]: 54 : Trace("iand-lemma")
171 : 27 : << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl;
172 : : // note that lemma can contain div/mod, and will be preprocessed in the
173 : : // prop engine
174 : 27 : d_im.addPendingLemma(
175 : : lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true);
176 : : }
177 : : else
178 : : {
179 : : // this is the most naive model-based schema based on model values
180 : 904 : Node lem = valueBasedLemma(i);
181 [ + - ]: 904 : Trace("iand-lemma")
182 : 452 : << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
183 : : // send the value lemma
184 : 452 : d_im.addPendingLemma(lem,
185 : : InferenceId::ARITH_NL_IAND_VALUE_REFINE,
186 : : nullptr,
187 : : true);
188 : : }
189 : : }
190 : : }
191 : 2167 : }
192 : :
193 : 0 : Node IAndSolver::convertToBvK(unsigned k, Node n) const
194 : : {
195 : 0 : Assert(n.isConst() && n.getType().isInteger());
196 : 0 : NodeManager* nm = nodeManager();
197 : 0 : Node iToBvOp = nm->mkConst(IntToBitVector(k));
198 : 0 : Node bn = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvOp, n);
199 : 0 : return rewrite(bn);
200 : : }
201 : :
202 : 0 : Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const
203 : : {
204 : 0 : NodeManager* nm = nodeManager();
205 : 0 : Node iAndOp = nm->mkConst(IntAnd(k));
206 : 0 : Node ret = nm->mkNode(Kind::IAND, iAndOp, x, y);
207 : 0 : ret = rewrite(ret);
208 : 0 : return ret;
209 : : }
210 : :
211 : 0 : Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const
212 : : {
213 : 0 : Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y)));
214 : 0 : ret = rewrite(ret);
215 : 0 : return ret;
216 : : }
217 : :
218 : 0 : Node IAndSolver::mkINot(unsigned k, Node x) const
219 : : {
220 : 0 : NodeManager* nm = nodeManager();
221 : 0 : Node ret = nm->mkNode(Kind::SUB, d_iandUtils.twoToKMinusOne(k), x);
222 : 0 : ret = rewrite(ret);
223 : 0 : return ret;
224 : : }
225 : :
226 : 452 : Node IAndSolver::valueBasedLemma(Node i)
227 : : {
228 : 452 : NodeManager* nm = nodeManager();
229 [ - + ][ - + ]: 452 : Assert(i.getKind() == Kind::IAND);
[ - - ]
230 : 904 : Node x = i[0];
231 : 904 : Node y = i[1];
232 : :
233 : 452 : uint32_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
234 : 1356 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bvsize)));
235 : 904 : Node valX = d_model.computeConcreteModelValue(x);
236 : 904 : Node valY = d_model.computeConcreteModelValue(y);
237 : 452 : valX = nm->mkNode(Kind::INTS_MODULUS, valX, twok);
238 : 452 : valY = nm->mkNode(Kind::INTS_MODULUS, valY, twok);
239 : :
240 : 1356 : Node valC = nm->mkNode(Kind::IAND, i.getOperator(), valX, valY);
241 : 452 : valC = rewrite(valC);
242 : :
243 : 1356 : Node xm = nm->mkNode(Kind::INTS_MODULUS, x, twok);
244 : 1356 : Node ym = nm->mkNode(Kind::INTS_MODULUS, y, twok);
245 : :
246 : : // (=>
247 : : // (and (= (mod x 2^n) (mod c1 2^n)) (= (mod y 2^n) (mod c2 2^n)))
248 : : // (= ((_ iand n) x y) rewrite(((_ iand n) (mod c1 2^n) (mod c2 2^n))))
249 : : // Note we use mod above since it ensures the the set of possible literals
250 : : // introduced is finite, since there are finitely many values mod 2^n.
251 : : Node lem = nm->mkNode(Kind::IMPLIES,
252 : 904 : nm->mkNode(Kind::AND, xm.eqNode(valX), ym.eqNode(valY)),
253 : 1808 : i.eqNode(valC));
254 : 904 : return lem;
255 : : }
256 : :
257 : 15 : Node IAndSolver::sumBasedLemma(Node i)
258 : : {
259 [ - + ][ - + ]: 15 : Assert(i.getKind() == Kind::IAND);
[ - - ]
260 : 30 : Node x = i[0];
261 : 30 : Node y = i[1];
262 : 15 : uint32_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
263 [ - + ][ - + ]: 15 : Assert(options().smt.BVAndIntegerGranularity <= 8);
[ - - ]
264 : 15 : uint32_t granularity = static_cast<uint32_t>(options().smt.BVAndIntegerGranularity);
265 : 15 : NodeManager* nm = nodeManager();
266 : : Node lem = nm->mkNode(
267 : 30 : Kind::EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity));
268 : 30 : return lem;
269 : : }
270 : :
271 : 27 : Node IAndSolver::bitwiseLemma(Node i)
272 : : {
273 [ - + ][ - + ]: 27 : Assert(i.getKind() == Kind::IAND);
[ - - ]
274 : 54 : Node x = i[0];
275 : 54 : Node y = i[1];
276 : :
277 : 27 : unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size;
278 [ - + ][ - + ]: 27 : Assert(options().smt.BVAndIntegerGranularity <= 8);
[ - - ]
279 : 27 : uint32_t granularity = static_cast<uint32_t>(options().smt.BVAndIntegerGranularity);
280 : :
281 : 81 : Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>();
282 : 81 : Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>();
283 : :
284 [ - + ][ - + ]: 27 : Assert(absI.isIntegral());
[ - - ]
285 [ - + ][ - + ]: 27 : Assert(concI.isIntegral());
[ - - ]
286 : :
287 : 54 : BitVector bvAbsI = BitVector(bvsize, absI.getNumerator());
288 : 54 : BitVector bvConcI = BitVector(bvsize, concI.getNumerator());
289 : :
290 : 27 : NodeManager* nm = nodeManager();
291 : 27 : Node lem = d_true;
292 : :
293 : : // compare each bit to bvI
294 : 54 : Node cond;
295 : 54 : Node bitIAnd;
296 : : uint32_t high_bit;
297 [ + + ]: 105 : for (uint32_t j = 0; j < bvsize; j += granularity)
298 : : {
299 : 78 : high_bit = j + granularity - 1;
300 : : // don't let high_bit pass bvsize
301 [ + + ]: 78 : if (high_bit >= bvsize)
302 : : {
303 : 4 : high_bit = bvsize - 1;
304 : : }
305 : :
306 : : // check if the abstraction differs from the concrete one on these bits
307 [ + + ]: 78 : if (bvAbsI.extract(high_bit, j) != bvConcI.extract(high_bit, j))
308 : : {
309 : 31 : bitIAnd = d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j);
310 : : // enforce bitwise equality
311 : 62 : lem = nm->mkNode(
312 : : Kind::AND,
313 : : lem,
314 : 93 : rewrite(d_iandUtils.iextract(high_bit, j, i)).eqNode(bitIAnd));
315 : : }
316 : : }
317 : 54 : return lem;
318 : : }
319 : :
320 : : } // namespace nl
321 : : } // namespace arith
322 : : } // namespace theory
323 : : } // namespace cvc5::internal
|
