GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_inequality.cpp Lines: 111 142 78.2 %
Date: 2021-03-22 Branches: 259 648 40.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_inequality.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Andrew Reynolds
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 Algebraic solver.
13
 **
14
 ** Algebraic solver.
15
 **/
16
17
#include "theory/bv/bv_subtheory_inequality.h"
18
19
#include "options/smt_options.h"
20
#include "smt/smt_statistics_registry.h"
21
#include "theory/bv/bv_solver_lazy.h"
22
#include "theory/bv/theory_bv_utils.h"
23
#include "theory/rewriter.h"
24
#include "theory/theory_model.h"
25
26
using namespace std;
27
using namespace CVC4;
28
using namespace CVC4::context;
29
using namespace CVC4::theory;
30
using namespace CVC4::theory::bv;
31
using namespace CVC4::theory::bv::utils;
32
33
180735
bool InequalitySolver::check(Theory::Effort e) {
34
180735
  Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
35
361470
  TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime);
36
180735
  ++(d_statistics.d_numCallstoCheck);
37
180735
  d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
38
39
180735
  bool ok = true;
40
2370857
  while (!done() && ok) {
41
2190122
    TNode fact = get();
42
1095061
    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n";
43
1095061
    if (fact.getKind() == kind::EQUAL) {
44
689894
      TNode a = fact[0];
45
344947
      if( a.getType().isBitVector() ){
46
689762
        TNode b = fact[1];
47
344881
        ok = addInequality(a, b, false, fact);
48
344881
        if (ok)
49
344815
          ok = addInequality(b, a, false, fact);
50
      }
51
750114
    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
52
579396
      TNode a = fact[0][0];
53
289698
      if( a.getType().isBitVector() ){
54
579220
        TNode b = fact[0][1];
55
289610
        ok = d_inequalityGraph.addDisequality(a, b, fact);
56
      }
57
    }
58
1095061
    if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
59
      TNode a = fact[0][1];
60
      TNode b = fact[0][0];
61
      ok = addInequality(a, b, true, fact);
62
      // propagate
63
      // NodeManager *nm = NodeManager::currentNM();
64
      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
65
      //   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
66
      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
67
      //   d_explanations[neq] = fact;
68
      // }
69
1095061
    } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
70
293288
      TNode a = fact[0][1];
71
293288
      TNode b = fact[0][0];
72
146644
      ok = addInequality(a, b, false, fact);
73
948417
    } else if (fact.getKind() == kind::BITVECTOR_ULT) {
74
171228
      TNode a = fact[0];
75
171228
      TNode b = fact[1];
76
85614
      ok = addInequality(a, b, true, fact);
77
      // propagate
78
      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
79
      //   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, a, b));
80
      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
81
      //   d_explanations[neq] = fact;
82
      // }
83
862803
    } else if (fact.getKind() == kind::BITVECTOR_ULE) {
84
      TNode a = fact[0];
85
      TNode b = fact[1];
86
      ok = addInequality(a, b, false, fact);
87
    }
88
  }
89
90
180735
  if (!ok) {
91
1134
    std::vector<TNode> conflict;
92
567
    d_inequalityGraph.getConflict(conflict);
93
1134
    Node confl = utils::flattenAnd(conflict);
94
567
    d_bv->setConflict(confl);
95
567
    Debug("bv-subtheory-inequality") << "InequalitySolver::conflict:  "<< confl <<"\n";
96
567
    return false;
97
  }
98
99
180168
  if (isComplete() && Theory::fullEffort(e)) {
100
    // make sure all the disequalities we didn't split on are still satisifed
101
    // and split on the ones that are not
102
88
    std::vector<Node> lemmas;
103
44
    d_inequalityGraph.checkDisequalities(lemmas);
104
52
    for(unsigned i = 0; i < lemmas.size(); ++i) {
105
8
      d_bv->lemma(lemmas[i]);
106
    }
107
  }
108
180168
  Debug("bv-subtheory-inequality") << "InequalitySolver done. ";
109
180168
  return true;
110
}
111
112
31866
EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b)
113
{
114
31866
  if (!isComplete()) return EQUALITY_UNKNOWN;
115
116
74
  NodeManager* nm = NodeManager::currentNM();
117
148
  Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
118
148
  Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
119
120
  // if an inequality containing the terms has been asserted then we know
121
  // the equality is false
122
74
  if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a))
123
  {
124
    return EQUALITY_FALSE;
125
  }
126
127
222
  if (!d_inequalityGraph.hasValueInModel(a)
128
222
      || !d_inequalityGraph.hasValueInModel(b))
129
  {
130
74
    return EQUALITY_UNKNOWN;
131
  }
132
133
  // TODO: check if this disequality is entailed by inequalities via
134
  // transitivity
135
136
  BitVector a_val = d_inequalityGraph.getValueInModel(a);
137
  BitVector b_val = d_inequalityGraph.getValueInModel(b);
138
139
  if (a_val == b_val)
140
  {
141
    return EQUALITY_TRUE_IN_MODEL;
142
  }
143
  else
144
  {
145
    return EQUALITY_FALSE_IN_MODEL;
146
  }
147
}
148
149
1137863
void InequalitySolver::assertFact(TNode fact) {
150
1137863
  d_assertionQueue.push_back(fact);
151
1137863
  d_assertionSet.insert(fact);
152
1137863
  if (!isInequalityOnly(fact)) {
153
713901
    d_isComplete = false;
154
  }
155
1137863
}
156
157
1203905
bool InequalitySolver::isInequalityOnly(TNode node) {
158
1203905
  if (node.getKind() == kind::NOT) {
159
585959
    node = node[0];
160
  }
161
162
1203905
  if (node.getAttribute(IneqOnlyComputedAttribute())) {
163
895785
    return node.getAttribute(IneqOnlyAttribute());
164
  }
165
166
887137
  if (node.getKind() != kind::EQUAL &&
167
535236
      node.getKind() != kind::BITVECTOR_ULT &&
168
528678
      node.getKind() != kind::BITVECTOR_ULE &&
169
526040
      node.getKind() != kind::CONST_BITVECTOR &&
170
521578
      node.getKind() != kind::SELECT &&
171
827100
      node.getKind() != kind::STORE &&
172
259103
      node.getMetaKind() != kind::metakind::VARIABLE) {
173
    // not worth caching
174
249975
    return false;
175
  }
176
58145
  bool res = true;
177
124187
  for (unsigned i = 0; res && i < node.getNumChildren(); ++i) {
178
66042
    res = res && isInequalityOnly(node[i]);
179
  }
180
58145
  node.setAttribute(IneqOnlyComputedAttribute(), true);
181
58145
  node.setAttribute(IneqOnlyAttribute(), res);
182
58145
  return res;
183
}
184
185
void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
186
  Assert(d_explanations.find(literal) != d_explanations.end());
187
  TNode explanation = d_explanations[literal];
188
  assumptions.push_back(explanation);
189
  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
190
}
191
192
void InequalitySolver::propagate(Theory::Effort e) { Assert(false); }
193
30
bool InequalitySolver::collectModelValues(TheoryModel* m,
194
                                          const std::set<Node>& termSet)
195
{
196
30
  Debug("bitvector-model") << "InequalitySolver::collectModelValues \n";
197
60
  std::vector<Node> model;
198
30
  d_inequalityGraph.getAllValuesInModel(model);
199
238
  for (unsigned i = 0; i < model.size(); ++i) {
200
208
    Assert(model[i].getKind() == kind::EQUAL);
201
208
    if (!m->assertEquality(model[i][0], model[i][1], true))
202
    {
203
      return false;
204
    }
205
  }
206
30
  return true;
207
}
208
209
Node InequalitySolver::getModelValue(TNode var) {
210
  Assert(isInequalityOnly(var));
211
  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
212
  Assert(isComplete());
213
  Node result = Node();
214
  if (!d_inequalityGraph.hasValueInModel(var)) {
215
    Assert(d_bv->isSharedTerm(var));
216
  } else {
217
    BitVector val = d_inequalityGraph.getValueInModel(var);
218
    result = utils::mkConst(val);
219
  }
220
  Debug("bitvector-model") << " => " << result <<"\n";
221
  return result;
222
}
223
224
209873
void InequalitySolver::preRegister(TNode node) {
225
209873
  Kind kind = node.getKind();
226
209873
  if (kind == kind::EQUAL ||
227
158110
      kind == kind::BITVECTOR_ULE ||
228
      kind == kind::BITVECTOR_ULT) {
229
65272
    d_ineqTerms.insert(node[0]);
230
65272
    d_ineqTerms.insert(node[1]);
231
  }
232
209873
}
233
234
921954
bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact)
235
{
236
921954
  bool ok = d_inequalityGraph.addInequality(a, b, strict, fact);
237
921954
  if (!ok || !strict) return ok;
238
239
170550
  Node one = utils::mkConst(utils::getSize(a), 1);
240
  Node a_plus_one = Rewriter::rewrite(
241
170550
      NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, a, one));
242
85275
  if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end())
243
  {
244
729
    ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact);
245
  }
246
85275
  return ok;
247
}
248
249
8954
InequalitySolver::Statistics::Statistics()
250
    : d_numCallstoCheck("theory::bv::inequality::NumCallsToCheck", 0),
251
8954
      d_solveTime("theory::bv::inequality::SolveTime")
252
{
253
8954
  smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
254
8954
  smtStatisticsRegistry()->registerStat(&d_solveTime);
255
8954
}
256
257
17902
InequalitySolver::Statistics::~Statistics()
258
{
259
8951
  smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
260
8951
  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
261
35627
}