GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/iand_solver.cpp Lines: 116 152 76.3 %
Date: 2021-03-23 Branches: 257 740 34.7 %

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