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