1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Makai Mann, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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_state.h" |
23 |
|
#include "theory/arith/arith_utilities.h" |
24 |
|
#include "theory/arith/inference_manager.h" |
25 |
|
#include "theory/arith/nl/nl_model.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
#include "util/bitvector.h" |
28 |
|
#include "util/iand.h" |
29 |
|
|
30 |
|
using namespace cvc5::kind; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace arith { |
35 |
|
namespace nl { |
36 |
|
|
37 |
5208 |
IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model) |
38 |
|
: d_im(im), |
39 |
|
d_model(model), |
40 |
|
d_astate(state), |
41 |
5208 |
d_initRefine(state.getUserContext()) |
42 |
|
{ |
43 |
5208 |
NodeManager* nm = NodeManager::currentNM(); |
44 |
5208 |
d_false = nm->mkConst(false); |
45 |
5208 |
d_true = nm->mkConst(true); |
46 |
5208 |
d_zero = nm->mkConst(Rational(0)); |
47 |
5208 |
d_one = nm->mkConst(Rational(1)); |
48 |
5208 |
d_two = nm->mkConst(Rational(2)); |
49 |
5208 |
} |
50 |
|
|
51 |
5206 |
IAndSolver::~IAndSolver() {} |
52 |
|
|
53 |
3207 |
void IAndSolver::initLastCall(const std::vector<Node>& assertions, |
54 |
|
const std::vector<Node>& false_asserts, |
55 |
|
const std::vector<Node>& xts) |
56 |
|
{ |
57 |
3207 |
d_iands.clear(); |
58 |
|
|
59 |
3207 |
Trace("iand-mv") << "IAND terms : " << std::endl; |
60 |
25687 |
for (const Node& a : xts) |
61 |
|
{ |
62 |
22480 |
Kind ak = a.getKind(); |
63 |
22480 |
if (ak != IAND) |
64 |
|
{ |
65 |
|
// don't care about other terms |
66 |
22170 |
continue; |
67 |
|
} |
68 |
310 |
size_t bsize = a.getOperator().getConst<IntAnd>().d_size; |
69 |
310 |
d_iands[bsize].push_back(a); |
70 |
|
} |
71 |
|
|
72 |
3207 |
Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl; |
73 |
3207 |
} |
74 |
|
|
75 |
3207 |
void IAndSolver::checkInitialRefine() |
76 |
|
{ |
77 |
3207 |
Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl; |
78 |
3207 |
NodeManager* nm = NodeManager::currentNM(); |
79 |
3510 |
for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands) |
80 |
|
{ |
81 |
|
// the reference bitwidth |
82 |
303 |
unsigned k = is.first; |
83 |
613 |
for (const Node& i : is.second) |
84 |
|
{ |
85 |
310 |
if (d_initRefine.find(i) != d_initRefine.end()) |
86 |
|
{ |
87 |
|
// already sent initial axioms for i in this user context |
88 |
221 |
continue; |
89 |
|
} |
90 |
89 |
d_initRefine.insert(i); |
91 |
178 |
Node op = i.getOperator(); |
92 |
|
// initial refinement lemmas |
93 |
178 |
std::vector<Node> conj; |
94 |
|
// iand(x,y)=iand(y,x) is guaranteed by rewriting |
95 |
89 |
Assert(i[0] <= i[1]); |
96 |
|
// conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0]))); |
97 |
|
// 0 <= iand(x,y) < 2^k |
98 |
89 |
conj.push_back(nm->mkNode(LEQ, d_zero, i)); |
99 |
89 |
conj.push_back(nm->mkNode(LT, i, d_iandUtils.twoToK(k))); |
100 |
|
// iand(x,y)<=x |
101 |
89 |
conj.push_back(nm->mkNode(LEQ, i, i[0])); |
102 |
|
// iand(x,y)<=y |
103 |
89 |
conj.push_back(nm->mkNode(LEQ, i, i[1])); |
104 |
|
// x=y => iand(x,y)=x |
105 |
89 |
conj.push_back(nm->mkNode(IMPLIES, i[0].eqNode(i[1]), i.eqNode(i[0]))); |
106 |
178 |
Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); |
107 |
178 |
Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" |
108 |
89 |
<< std::endl; |
109 |
89 |
d_im.addPendingLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); |
110 |
|
} |
111 |
|
} |
112 |
3207 |
} |
113 |
|
|
114 |
451 |
void IAndSolver::checkFullRefine() |
115 |
|
{ |
116 |
451 |
Trace("iand-check") << "IAndSolver::checkFullRefine"; |
117 |
451 |
Trace("iand-check") << "IAND terms: " << std::endl; |
118 |
617 |
for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands) |
119 |
|
{ |
120 |
|
// the reference bitwidth |
121 |
166 |
unsigned k = is.first; |
122 |
336 |
for (const Node& i : is.second) |
123 |
|
{ |
124 |
339 |
Node valAndXY = d_model.computeAbstractModelValue(i); |
125 |
339 |
Node valAndXYC = d_model.computeConcreteModelValue(i); |
126 |
170 |
if (Trace.isOn("iand-check")) |
127 |
|
{ |
128 |
|
Node x = i[0]; |
129 |
|
Node y = i[1]; |
130 |
|
|
131 |
|
Node valX = d_model.computeConcreteModelValue(x); |
132 |
|
Node valY = d_model.computeConcreteModelValue(y); |
133 |
|
|
134 |
|
Trace("iand-check") |
135 |
|
<< "* " << i << ", value = " << valAndXY << std::endl; |
136 |
|
Trace("iand-check") << " actual (" << valX << ", " << valY |
137 |
|
<< ") = " << valAndXYC << std::endl; |
138 |
|
// print the bit-vector versions |
139 |
|
Node bvalX = convertToBvK(k, valX); |
140 |
|
Node bvalY = convertToBvK(k, valY); |
141 |
|
Node bvalAndXY = convertToBvK(k, valAndXY); |
142 |
|
Node bvalAndXYC = convertToBvK(k, valAndXYC); |
143 |
|
|
144 |
|
Trace("iand-check") << " bv-value = " << bvalAndXY << std::endl; |
145 |
|
Trace("iand-check") << " bv-actual (" << bvalX << ", " << bvalY |
146 |
|
<< ") = " << bvalAndXYC << std::endl; |
147 |
|
} |
148 |
171 |
if (valAndXY == valAndXYC) |
149 |
|
{ |
150 |
1 |
Trace("iand-check") << "...already correct" << std::endl; |
151 |
1 |
continue; |
152 |
|
} |
153 |
|
|
154 |
|
// ************* additional lemma schemas go here |
155 |
169 |
if (d_astate.options().smt.iandMode == options::IandMode::SUM) |
156 |
|
{ |
157 |
8 |
Node lem = sumBasedLemma(i); // add lemmas based on sum mode |
158 |
8 |
Trace("iand-lemma") |
159 |
4 |
<< "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; |
160 |
|
// note that lemma can contain div/mod, and will be preprocessed in the |
161 |
|
// prop engine |
162 |
4 |
d_im.addPendingLemma( |
163 |
|
lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); |
164 |
|
} |
165 |
165 |
else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE) |
166 |
|
{ |
167 |
24 |
Node lem = bitwiseLemma(i); // check for violated bitwise axioms |
168 |
24 |
Trace("iand-lemma") |
169 |
12 |
<< "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl; |
170 |
|
// note that lemma can contain div/mod, and will be preprocessed in the |
171 |
|
// prop engine |
172 |
12 |
d_im.addPendingLemma( |
173 |
|
lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true); |
174 |
|
} |
175 |
|
else |
176 |
|
{ |
177 |
|
// this is the most naive model-based schema based on model values |
178 |
306 |
Node lem = valueBasedLemma(i); |
179 |
306 |
Trace("iand-lemma") |
180 |
153 |
<< "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; |
181 |
|
// send the value lemma |
182 |
153 |
d_im.addPendingLemma(lem, |
183 |
|
InferenceId::ARITH_NL_IAND_VALUE_REFINE, |
184 |
|
nullptr, |
185 |
|
true); |
186 |
|
} |
187 |
|
} |
188 |
|
} |
189 |
451 |
} |
190 |
|
|
191 |
|
Node IAndSolver::convertToBvK(unsigned k, Node n) const |
192 |
|
{ |
193 |
|
Assert(n.isConst() && n.getType().isInteger()); |
194 |
|
NodeManager* nm = NodeManager::currentNM(); |
195 |
|
Node iToBvOp = nm->mkConst(IntToBitVector(k)); |
196 |
|
Node bn = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvOp, n); |
197 |
|
return Rewriter::rewrite(bn); |
198 |
|
} |
199 |
|
|
200 |
|
Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const |
201 |
|
{ |
202 |
|
NodeManager* nm = NodeManager::currentNM(); |
203 |
|
Node iAndOp = nm->mkConst(IntAnd(k)); |
204 |
|
Node ret = nm->mkNode(IAND, iAndOp, x, y); |
205 |
|
ret = Rewriter::rewrite(ret); |
206 |
|
return ret; |
207 |
|
} |
208 |
|
|
209 |
|
Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const |
210 |
|
{ |
211 |
|
Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y))); |
212 |
|
ret = Rewriter::rewrite(ret); |
213 |
|
return ret; |
214 |
|
} |
215 |
|
|
216 |
|
Node IAndSolver::mkINot(unsigned k, Node x) const |
217 |
|
{ |
218 |
|
NodeManager* nm = NodeManager::currentNM(); |
219 |
|
Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x); |
220 |
|
ret = Rewriter::rewrite(ret); |
221 |
|
return ret; |
222 |
|
} |
223 |
|
|
224 |
153 |
Node IAndSolver::valueBasedLemma(Node i) |
225 |
|
{ |
226 |
153 |
Assert(i.getKind() == IAND); |
227 |
306 |
Node x = i[0]; |
228 |
306 |
Node y = i[1]; |
229 |
|
|
230 |
306 |
Node valX = d_model.computeConcreteModelValue(x); |
231 |
306 |
Node valY = d_model.computeConcreteModelValue(y); |
232 |
|
|
233 |
153 |
NodeManager* nm = NodeManager::currentNM(); |
234 |
306 |
Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY); |
235 |
153 |
valC = Rewriter::rewrite(valC); |
236 |
|
|
237 |
|
Node lem = nm->mkNode( |
238 |
153 |
IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC)); |
239 |
306 |
return lem; |
240 |
|
} |
241 |
|
|
242 |
4 |
Node IAndSolver::sumBasedLemma(Node i) |
243 |
|
{ |
244 |
4 |
Assert(i.getKind() == IAND); |
245 |
8 |
Node x = i[0]; |
246 |
8 |
Node y = i[1]; |
247 |
4 |
size_t bvsize = i.getOperator().getConst<IntAnd>().d_size; |
248 |
4 |
uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; |
249 |
4 |
NodeManager* nm = NodeManager::currentNM(); |
250 |
|
Node lem = nm->mkNode( |
251 |
4 |
EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity)); |
252 |
8 |
return lem; |
253 |
|
} |
254 |
|
|
255 |
12 |
Node IAndSolver::bitwiseLemma(Node i) |
256 |
|
{ |
257 |
12 |
Assert(i.getKind() == IAND); |
258 |
24 |
Node x = i[0]; |
259 |
24 |
Node y = i[1]; |
260 |
|
|
261 |
12 |
unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size; |
262 |
12 |
uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; |
263 |
|
|
264 |
24 |
Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>(); |
265 |
24 |
Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>(); |
266 |
|
|
267 |
12 |
Assert(absI.isIntegral()); |
268 |
12 |
Assert(concI.isIntegral()); |
269 |
|
|
270 |
24 |
BitVector bvAbsI = BitVector(bvsize, absI.getNumerator()); |
271 |
24 |
BitVector bvConcI = BitVector(bvsize, concI.getNumerator()); |
272 |
|
|
273 |
12 |
NodeManager* nm = NodeManager::currentNM(); |
274 |
12 |
Node lem = d_true; |
275 |
|
|
276 |
|
// compare each bit to bvI |
277 |
24 |
Node cond; |
278 |
24 |
Node bitIAnd; |
279 |
|
unsigned high_bit; |
280 |
38 |
for (unsigned j = 0; j < bvsize; j += granularity) |
281 |
|
{ |
282 |
26 |
high_bit = j + granularity - 1; |
283 |
|
// don't let high_bit pass bvsize |
284 |
26 |
if (high_bit >= bvsize) |
285 |
|
{ |
286 |
4 |
high_bit = bvsize - 1; |
287 |
|
} |
288 |
|
|
289 |
|
// check if the abstraction differs from the concrete one on these bits |
290 |
26 |
if (bvAbsI.extract(high_bit, j) != bvConcI.extract(high_bit, j)) |
291 |
|
{ |
292 |
16 |
bitIAnd = d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j); |
293 |
|
// enforce bitwise equality |
294 |
16 |
lem = nm->mkNode( |
295 |
32 |
AND, lem, d_iandUtils.iextract(high_bit, j, i).eqNode(bitIAnd)); |
296 |
|
} |
297 |
|
} |
298 |
24 |
return lem; |
299 |
|
} |
300 |
|
|
301 |
|
} // namespace nl |
302 |
|
} // namespace arith |
303 |
|
} // namespace theory |
304 |
29502 |
} // namespace cvc5 |