GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver_lazy.h Lines: 19 20 95.0 %
Date: 2021-03-23 Branches: 14 42 33.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_lazy.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, 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 Lazy bit-vector solver.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
18
#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
23
#include "context/cdhashset.h"
24
#include "context/cdlist.h"
25
#include "context/context.h"
26
#include "theory/bv/bv_solver.h"
27
#include "theory/bv/bv_subtheory.h"
28
#include "theory/bv/theory_bv.h"
29
#include "util/hash.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace bv {
34
35
class CoreSolver;
36
class InequalitySolver;
37
class AlgebraicSolver;
38
class BitblastSolver;
39
class EagerBitblastSolver;
40
class AbstractionModule;
41
42
class BVSolverLazy : public BVSolver
43
{
44
  /** Back reference to TheoryBV */
45
  TheoryBV& d_bv;
46
47
  /** The context we are using */
48
  context::Context* d_context;
49
50
  /** Context dependent set of atoms we already propagated */
51
  context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
52
  context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
53
54
  std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
55
  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
56
      d_subtheoryMap;
57
58
 public:
59
  BVSolverLazy(TheoryBV& bv,
60
               context::Context* c,
61
               context::UserContext* u,
62
               ProofNodeManager* pnm = nullptr,
63
               std::string name = "");
64
65
  ~BVSolverLazy();
66
67
  //--------------------------------- initialization
68
69
  /**
70
   * Returns true if we need an equality engine. If so, we initialize the
71
   * information regarding how it should be setup. For details, see the
72
   * documentation in Theory::needsEqualityEngine.
73
   */
74
  bool needsEqualityEngine(EeSetupInfo& esi) override;
75
76
  /** finish initialization */
77
  void finishInit() override;
78
  //--------------------------------- end initialization
79
80
  void preRegisterTerm(TNode n) override;
81
82
  bool preCheck(Theory::Effort e) override;
83
84
  bool needsCheckLastEffort() override;
85
86
  void propagate(Theory::Effort e) override;
87
88
  TrustNode explain(TNode n) override;
89
90
  bool collectModelValues(TheoryModel* m,
91
                          const std::set<Node>& termSet) override;
92
93
  std::string identify() const override { return std::string("BVSolverLazy"); }
94
95
  Theory::PPAssertStatus ppAssert(
96
      TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
97
98
  TrustNode ppRewrite(TNode t) override;
99
100
  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
101
102
  void presolve() override;
103
104
  bool applyAbstraction(const std::vector<Node>& assertions,
105
                        std::vector<Node>& new_assertions) override;
106
107
21
  bool isLeaf(TNode node) { return d_bv.isLeaf(node); }
108
109
 private:
110
  class Statistics
111
  {
112
   public:
113
    AverageStat d_avgConflictSize;
114
    IntStat d_solveSubstitutions;
115
    TimerStat d_solveTimer;
116
    IntStat d_numCallsToCheckFullEffort;
117
    IntStat d_numCallsToCheckStandardEffort;
118
    TimerStat d_weightComputationTimer;
119
    IntStat d_numMultSlice;
120
    Statistics();
121
    ~Statistics();
122
  };
123
124
  Statistics d_statistics;
125
126
  void check(Theory::Effort e);
127
  void spendResource(ResourceManager::Resource r);
128
129
  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
130
  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
131
  NodeSet d_staticLearnCache;
132
133
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
134
135
  context::CDO<bool> d_lemmasAdded;
136
137
  // Are we in conflict?
138
  context::CDO<bool> d_conflict;
139
140
  // Invalidate the model cache if check was called
141
  context::CDO<bool> d_invalidateModelCache;
142
143
  /** The conflict node */
144
  Node d_conflictNode;
145
146
  /** Literals to propagate */
147
  context::CDList<Node> d_literalsToPropagate;
148
149
  /** Index of the next literal to propagate */
150
  context::CDO<unsigned> d_literalsToPropagateIndex;
151
152
  /**
153
   * Keeps a map from nodes to the subtheory that propagated it so that we can
154
   * explain it properly.
155
   */
156
  typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
157
  PropagatedMap d_propagatedBy;
158
159
  std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
160
  std::unique_ptr<AbstractionModule> d_abstractionModule;
161
  bool d_calledPreregister;
162
163
3643071
  bool wasPropagatedBySubtheory(TNode literal) const
164
  {
165
3643071
    return d_propagatedBy.find(literal) != d_propagatedBy.end();
166
  }
167
168
1457648
  SubTheory getPropagatingSubtheory(TNode literal) const
169
  {
170
1457648
    Assert(wasPropagatedBySubtheory(literal));
171
1457648
    PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
172
1457648
    return (*find).second;
173
  }
174
175
  /** Should be called to propagate the literal.  */
176
  bool storePropagation(TNode literal, SubTheory subtheory);
177
178
  /**
179
   * Explains why this literal (propagated by subtheory) is true by adding
180
   * assumptions.
181
   */
182
  void explain(TNode literal, std::vector<TNode>& assumptions);
183
184
  void notifySharedTerm(TNode t) override;
185
186
42258
  bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
187
188
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
189
190
  Node getModelValue(TNode var);
191
192
2860179
  inline std::string indent()
193
  {
194
2860179
    std::string indentStr(d_context->getLevel(), ' ');
195
2860179
    return indentStr;
196
  }
197
198
  void setConflict(Node conflict = Node::null());
199
200
5171704
  bool inConflict() { return d_conflict; }
201
202
  void sendConflict();
203
204
1098
  void lemma(TNode node)
205
  {
206
1098
    d_im.lemma(node, InferenceId::BV_LAZY_LEMMA);
207
1098
    d_lemmasAdded = true;
208
1098
  }
209
210
  void checkForLemma(TNode node);
211
212
41017
  size_t numAssertions() { return d_bv.numAssertions(); }
213
214
1138157
  theory::Assertion get() { return d_bv.get(); }
215
216
1566174
  bool done() { return d_bv.done(); }
217
218
  friend class LazyBitblaster;
219
  friend class TLazyBitblaster;
220
  friend class EagerBitblaster;
221
  friend class BitblastSolver;
222
  friend class EqualitySolver;
223
  friend class CoreSolver;
224
  friend class InequalitySolver;
225
  friend class AlgebraicSolver;
226
  friend class EagerBitblastSolver;
227
}; /* class BVSolverLazy */
228
229
}  // namespace bv
230
}  // namespace theory
231
232
}  // namespace CVC4
233
234
#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */