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