GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_algebraic.h Lines: 0 18 0.0 %
Date: 2021-03-22 Branches: 0 10 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_algebraic.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Tim King
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 "cvc4_private.h"
18
19
#pragma once
20
21
#include <unordered_map>
22
#include <unordered_set>
23
24
#include "theory/bv/bv_subtheory.h"
25
#include "theory/bv/slicer.h"
26
#include "theory/substitutions.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace bv {
31
32
class AlgebraicSolver;
33
34
Node mergeExplanations(TNode expl1, TNode expl2);
35
Node mergeExplanations(const std::vector<Node>& expls);
36
37
/**
38
 * Non-context dependent substitution with explanations.
39
 *
40
 */
41
class SubstitutionEx
42
{
43
  struct SubstitutionElement
44
  {
45
    Node to;
46
    Node reason;
47
    SubstitutionElement() : to(), reason() {}
48
49
    SubstitutionElement(TNode t, TNode r) : to(t), reason(r) {}
50
  };
51
52
  struct SubstitutionStackElement
53
  {
54
    TNode node;
55
    bool childrenAdded;
56
    SubstitutionStackElement(TNode n, bool ca = false)
57
        : node(n), childrenAdded(ca)
58
    {
59
    }
60
  };
61
62
  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
63
      Substitutions;
64
  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
65
      SubstitutionsCache;
66
67
  Substitutions d_substitutions;
68
  SubstitutionsCache d_cache;
69
  bool d_cacheInvalid;
70
  theory::SubstitutionMap* d_modelMap;
71
72
  Node getReason(TNode node) const;
73
  bool hasCache(TNode node) const;
74
  Node getCache(TNode node) const;
75
  void storeCache(TNode from, TNode to, Node rason);
76
  Node internalApply(TNode node);
77
78
 public:
79
  SubstitutionEx(theory::SubstitutionMap* modelMap);
80
  /**
81
   * Returnst true if the substitution map did not contain from.
82
   *
83
   * @param from
84
   * @param to
85
   * @param reason
86
   *
87
   * @return
88
   */
89
  bool addSubstitution(TNode from, TNode to, TNode reason);
90
  Node apply(TNode node);
91
  Node explain(TNode node) const;
92
};
93
94
/**
95
 * In-processing worklist element, id keeps track of
96
 * original assertion.
97
 *
98
 */
99
struct WorklistElement
100
{
101
  Node node;
102
  unsigned id;
103
  WorklistElement(Node n, unsigned i) : node(n), id(i) {}
104
  WorklistElement() : node(), id(-1) {}
105
};
106
107
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
108
typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
109
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
110
111
class ExtractSkolemizer
112
{
113
  struct Extract
114
  {
115
    unsigned high;
116
    unsigned low;
117
    Extract(unsigned h, unsigned l) : high(h), low(l) {}
118
  };
119
120
  struct ExtractList
121
  {
122
    Base base;
123
    std::vector<Extract> extracts;
124
    ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {}
125
    ExtractList() : base(1), extracts() {}
126
    void addExtract(Extract& e);
127
  };
128
  typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
129
  context::Context d_emptyContext;
130
  VarExtractMap d_varToExtract;
131
  theory::SubstitutionMap* d_modelMap;
132
  theory::SubstitutionMap d_skolemSubst;
133
  theory::SubstitutionMap d_skolemSubstRev;
134
135
  void storeSkolem(TNode node, TNode skolem);
136
  void storeExtract(TNode var, unsigned high, unsigned low);
137
  void collectExtracts(TNode node, TNodeSet& seen);
138
  Node skolemize(TNode);
139
  Node unSkolemize(TNode);
140
141
  Node mkSkolem(Node node);
142
143
 public:
144
  ExtractSkolemizer(theory::SubstitutionMap* modelMap);
145
  void skolemize(std::vector<WorklistElement>&);
146
  void unSkolemize(std::vector<WorklistElement>&);
147
  ~ExtractSkolemizer();
148
};
149
150
class BVQuickCheck;
151
class QuickXPlain;
152
153
/**
154
 * AlgebraicSolver
155
 */
156
class AlgebraicSolver : public SubtheorySolver
157
{
158
  struct Statistics
159
  {
160
    IntStat d_numCallstoCheck;
161
    IntStat d_numSimplifiesToTrue;
162
    IntStat d_numSimplifiesToFalse;
163
    IntStat d_numUnsat;
164
    IntStat d_numSat;
165
    IntStat d_numUnknown;
166
    TimerStat d_solveTime;
167
    BackedStat<double> d_useHeuristic;
168
    Statistics();
169
    ~Statistics();
170
  };
171
172
  std::unique_ptr<SubstitutionMap> d_modelMap;
173
  std::unique_ptr<BVQuickCheck> d_quickSolver;
174
  context::CDO<bool> d_isComplete;
175
  context::CDO<bool>
176
      d_isDifficult; /**< flag to indicate whether the current assertions
177
                        contain expensive BV operators */
178
179
  unsigned long d_budget;
180
  std::vector<Node> d_explanations; /**< explanations for assertions indexed by
181
                                       assertion id */
182
  TNodeSet d_inputAssertions; /**< assertions in current context (for debugging
183
                                 purposes only) */
184
  NodeIdMap d_ids;            /**< map from assertions to ids */
185
  uint64_t d_numSolved;
186
  uint64_t d_numCalls;
187
188
  /** separate quickXplain module as it can reuse the current SAT solver */
189
  std::unique_ptr<QuickXPlain> d_quickXplain;
190
191
  Statistics d_statistics;
192
  bool useHeuristic();
193
  void setConflict(TNode conflict);
194
  bool isSubstitutableIn(TNode node, TNode in);
195
  bool checkExplanation(TNode expl);
196
  void storeExplanation(TNode expl);
197
  void storeExplanation(unsigned id, TNode expl);
198
  /**
199
   * Apply substitutions and rewriting to the worklist assertions to a fixpoint.
200
   * Subsitutions learned store in subst.
201
   *
202
   * @param worklist
203
   * @param subst
204
   */
205
  void processAssertions(std::vector<WorklistElement>& worklist,
206
                         SubstitutionEx& subst);
207
  /**
208
   * Attempt to solve the equation in fact, and if successful
209
   * add a substitution to subst.
210
   *
211
   * @param fact equation we are trying to solve
212
   * @param reason the reason in terms of original assertions
213
   * @param subst substitution map
214
   *
215
   * @return true if added a substitution to subst
216
   */
217
  bool solve(TNode fact, TNode reason, SubstitutionEx& subst);
218
  /**
219
   * Run a SAT solver on the given facts with the given budget.
220
   * Sets the isComplete flag and conflict accordingly.
221
   *
222
   * @param facts
223
   *
224
   * @return true if no conflict was detected.
225
   */
226
  bool quickCheck(std::vector<Node>& facts);
227
228
 public:
229
  AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
230
  ~AlgebraicSolver();
231
232
  void preRegister(TNode node) override {}
233
  bool check(Theory::Effort e) override;
234
  void explain(TNode literal, std::vector<TNode>& assumptions) override
235
  {
236
    Unreachable() << "AlgebraicSolver does not propagate.\n";
237
  }
238
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
239
  bool collectModelValues(TheoryModel* m,
240
                          const std::set<Node>& termSet) override;
241
  Node getModelValue(TNode node) override;
242
  bool isComplete() override;
243
  void assertFact(TNode fact) override;
244
};
245
246
}  // namespace bv
247
}  // namespace theory
248
}  // namespace CVC4