GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv.cpp Lines: 76 89 85.4 %
Date: 2021-03-23 Branches: 59 151 39.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Andrew Reynolds, Liana Hadarean
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
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
16
#include "theory/bv/theory_bv.h"
17
18
#include "options/bv_options.h"
19
#include "options/smt_options.h"
20
#include "theory/bv/bv_solver_bitblast.h"
21
#include "theory/bv/bv_solver_lazy.h"
22
#include "theory/bv/bv_solver_simple.h"
23
#include "theory/bv/theory_bv_utils.h"
24
#include "theory/ee_setup_info.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace bv {
29
30
8997
TheoryBV::TheoryBV(context::Context* c,
31
                   context::UserContext* u,
32
                   OutputChannel& out,
33
                   Valuation valuation,
34
                   const LogicInfo& logicInfo,
35
                   ProofNodeManager* pnm,
36
8997
                   std::string name)
37
    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
38
      d_internal(nullptr),
39
      d_rewriter(),
40
      d_state(c, u, valuation),
41
      d_im(*this, d_state, nullptr, "theory::bv"),
42
8997
      d_notify(d_im)
43
{
44
8997
  switch (options::bvSolver())
45
  {
46
    case options::BVSolver::BITBLAST:
47
      d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
48
      break;
49
50
8987
    case options::BVSolver::LAZY:
51
8987
      d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
52
8987
      break;
53
54
10
    default:
55
10
      AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
56
10
      d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm));
57
  }
58
8997
  d_theoryState = &d_state;
59
8997
  d_inferManager = &d_im;
60
8997
}
61
62
17988
TheoryBV::~TheoryBV() {}
63
64
8997
TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
65
66
8997
bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
67
{
68
8997
  bool need_ee = d_internal->needsEqualityEngine(esi);
69
70
  /* Set up default notify class for equality engine. */
71
8997
  if (need_ee && esi.d_notify == nullptr)
72
  {
73
    esi.d_notify = &d_notify;
74
    esi.d_name = "theory::bv::ee";
75
  }
76
77
8997
  return need_ee;
78
}
79
80
8997
void TheoryBV::finishInit()
81
{
82
  // these kinds are semi-evaluated in getModelValue (applications of this
83
  // kind are treated as variables)
84
8997
  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
85
8997
  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
86
8997
  d_internal->finishInit();
87
88
8997
  eq::EqualityEngine* ee = getEqualityEngine();
89
8997
  if (ee)
90
  {
91
    // The kinds we are treating as function application in congruence
92
8954
    ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
93
    //    ee->addFunctionKind(kind::BITVECTOR_AND);
94
    //    ee->addFunctionKind(kind::BITVECTOR_OR);
95
    //    ee->addFunctionKind(kind::BITVECTOR_XOR);
96
    //    ee->addFunctionKind(kind::BITVECTOR_NOT);
97
    //    ee->addFunctionKind(kind::BITVECTOR_NAND);
98
    //    ee->addFunctionKind(kind::BITVECTOR_NOR);
99
    //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
100
    //    ee->addFunctionKind(kind::BITVECTOR_COMP);
101
8954
    ee->addFunctionKind(kind::BITVECTOR_MULT, true);
102
8954
    ee->addFunctionKind(kind::BITVECTOR_PLUS, true);
103
8954
    ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
104
    //    ee->addFunctionKind(kind::BITVECTOR_SUB);
105
    //    ee->addFunctionKind(kind::BITVECTOR_NEG);
106
    //    ee->addFunctionKind(kind::BITVECTOR_UDIV);
107
    //    ee->addFunctionKind(kind::BITVECTOR_UREM);
108
    //    ee->addFunctionKind(kind::BITVECTOR_SDIV);
109
    //    ee->addFunctionKind(kind::BITVECTOR_SREM);
110
    //    ee->addFunctionKind(kind::BITVECTOR_SMOD);
111
    //    ee->addFunctionKind(kind::BITVECTOR_SHL);
112
    //    ee->addFunctionKind(kind::BITVECTOR_LSHR);
113
    //    ee->addFunctionKind(kind::BITVECTOR_ASHR);
114
    //    ee->addFunctionKind(kind::BITVECTOR_ULT);
115
    //    ee->addFunctionKind(kind::BITVECTOR_ULE);
116
    //    ee->addFunctionKind(kind::BITVECTOR_UGT);
117
    //    ee->addFunctionKind(kind::BITVECTOR_UGE);
118
    //    ee->addFunctionKind(kind::BITVECTOR_SLT);
119
    //    ee->addFunctionKind(kind::BITVECTOR_SLE);
120
    //    ee->addFunctionKind(kind::BITVECTOR_SGT);
121
    //    ee->addFunctionKind(kind::BITVECTOR_SGE);
122
8954
    ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
123
8954
    ee->addFunctionKind(kind::INT_TO_BITVECTOR);
124
  }
125
8997
}
126
127
304231
TrustNode TheoryBV::expandDefinition(Node node)
128
{
129
608462
  Debug("bitvector-expandDefinition")
130
304231
      << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
131
132
608462
  Node ret;
133
304231
  switch (node.getKind())
134
  {
135
    case kind::BITVECTOR_SDIV:
136
    case kind::BITVECTOR_SREM:
137
    case kind::BITVECTOR_SMOD:
138
      ret = TheoryBVRewriter::eliminateBVSDiv(node);
139
      break;
140
141
304231
    default: break;
142
  }
143
304231
  if (!ret.isNull() && node != ret)
144
  {
145
    return TrustNode::mkTrustRewrite(node, ret, nullptr);
146
  }
147
304231
  return TrustNode::null();
148
}
149
150
212781
void TheoryBV::preRegisterTerm(TNode node)
151
{
152
212781
  d_internal->preRegisterTerm(node);
153
154
212781
  eq::EqualityEngine* ee = getEqualityEngine();
155
212781
  if (ee)
156
  {
157
209859
    if (node.getKind() == kind::EQUAL)
158
    {
159
51757
      ee->addTriggerPredicate(node);
160
    }
161
    else
162
    {
163
158102
      ee->addTerm(node);
164
    }
165
  }
166
212781
}
167
168
220143
bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
169
170
6114
void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
171
172
35320
bool TheoryBV::preNotifyFact(
173
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
174
{
175
35320
  return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
176
}
177
178
void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
179
{
180
  d_internal->notifyFact(atom, pol, fact, isInternal);
181
}
182
183
8487
bool TheoryBV::needsCheckLastEffort()
184
{
185
8487
  return d_internal->needsCheckLastEffort();
186
}
187
188
7378
bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
189
{
190
7378
  return d_internal->collectModelValues(m, termSet);
191
}
192
193
842479
void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
194
195
3388
Theory::PPAssertStatus TheoryBV::ppAssert(
196
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
197
{
198
3388
  return d_internal->ppAssert(tin, outSubstitutions);
199
}
200
201
303366
TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
202
{
203
  // first, see if we need to expand definitions
204
606732
  TrustNode texp = expandDefinition(t);
205
303366
  if (!texp.isNull())
206
  {
207
    return texp;
208
  }
209
303366
  return d_internal->ppRewrite(t);
210
}
211
212
12418
void TheoryBV::presolve() { d_internal->presolve(); }
213
214
57528
EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
215
{
216
57528
  return d_internal->getEqualityStatus(a, b);
217
}
218
219
18775
TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
220
221
39998
void TheoryBV::notifySharedTerm(TNode t)
222
{
223
39998
  d_internal->notifySharedTerm(t);
224
39998
}
225
226
92002
void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
227
{
228
92002
  d_internal->ppStaticLearn(in, learned);
229
92002
}
230
231
3
bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
232
                                std::vector<Node>& new_assertions)
233
{
234
3
  return d_internal->applyAbstraction(assertions, new_assertions);
235
}
236
237
}  // namespace bv
238
}  // namespace theory
239
26685
}  // namespace CVC4