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