GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/circuit_propagator.h Lines: 29 29 100.0 %
Date: 2021-03-23 Branches: 52 100 52.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file circuit_propagator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Aina Niemetz, 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 A non-clausal circuit propagator for Boolean simplification
13
 **
14
 ** A non-clausal circuit propagator for Boolean simplification.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
20
#define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
21
22
#include <memory>
23
#include <unordered_map>
24
#include <vector>
25
26
#include "context/cdhashmap.h"
27
#include "context/cdhashset.h"
28
#include "context/cdo.h"
29
#include "context/context.h"
30
#include "expr/lazy_proof_chain.h"
31
#include "expr/node.h"
32
#include "theory/trust_node.h"
33
34
namespace CVC4 {
35
36
class ProofGenerator;
37
class ProofNode;
38
39
namespace theory {
40
41
class EagerProofGenerator;
42
43
namespace booleans {
44
45
/**
46
 * The main purpose of the CircuitPropagator class is to maintain the
47
 * state of the circuit for subsequent calls to propagate(), so that
48
 * the same fact is not output twice, so that the same edge in the
49
 * circuit isn't propagated twice, etc.
50
 */
51
9600
class CircuitPropagator
52
{
53
 public:
54
  /**
55
   * Value of a particular node
56
   */
57
  enum AssignmentStatus
58
  {
59
    /** Node is currently unassigned */
60
    UNASSIGNED = 0,
61
    /** Node is assigned to true */
62
    ASSIGNED_TO_TRUE,
63
    /** Node is assigned to false */
64
    ASSIGNED_TO_FALSE,
65
  };
66
67
  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
68
      BackEdgesMap;
69
70
  /**
71
   * Construct a new CircuitPropagator.
72
   */
73
  CircuitPropagator(bool enableForward = true, bool enableBackward = true);
74
75
  /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
76
682064
  bool getAssignment(TNode n) const
77
  {
78
682064
    AssignmentMap::iterator i = d_state.find(n);
79
682064
    Assert(i != d_state.end() && (*i).second != UNASSIGNED);
80
682064
    return (*i).second == ASSIGNED_TO_TRUE;
81
  }
82
83
  // Use custom context to ensure propagator is reset after use
84
10355
  void initialize() { d_context.push(); }
85
86
20710
  void setNeedsFinish(bool value) { d_needsFinish = value; }
87
88
19955
  bool getNeedsFinish() { return d_needsFinish; }
89
90
21222
  std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
91
92
  /** Finish the computation and pop the internal context */
93
  void finish();
94
95
  /** Assert for propagation */
96
  void assertTrue(TNode assertion);
97
98
  /**
99
   * Propagate through the asserted circuit propagator. New information
100
   * discovered by the propagator are put in the substitutions vector used in
101
   * construction.
102
   *
103
   * @return a trust node encapsulating the proof for a conflict as a lemma that
104
   * proves false, or the null trust node otherwise
105
   */
106
  TrustNode propagate() CVC4_WARN_UNUSED_RESULT;
107
108
  /**
109
   * Get the back edges of this circuit.
110
   */
111
8
  const BackEdgesMap& getBackEdges() const { return d_backEdges; }
112
113
  /** Invert a set value */
114
  static inline AssignmentStatus neg(AssignmentStatus value)
115
  {
116
    Assert(value != UNASSIGNED);
117
    if (value == ASSIGNED_TO_TRUE)
118
      return ASSIGNED_TO_FALSE;
119
    else
120
      return ASSIGNED_TO_TRUE;
121
  }
122
123
  /** True iff Node is assigned in circuit (either true or false). */
124
13030
  bool isAssigned(TNode n) const
125
  {
126
13030
    AssignmentMap::const_iterator i = d_state.find(n);
127
13030
    return i != d_state.end() && ((*i).second != UNASSIGNED);
128
  }
129
130
  /** True iff Node is assigned to the value. */
131
19768831
  bool isAssignedTo(TNode n, bool value) const
132
  {
133
19768831
    AssignmentMap::const_iterator i = d_state.find(n);
134
19768831
    if (i == d_state.end()) return false;
135
18667295
    if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
136
842675
    if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
137
127948
    return false;
138
  }
139
  /**
140
   * Set proof node manager, context and parent proof generator.
141
   *
142
   * If parent is non-null, then it is responsible for the proofs provided
143
   * to this class.
144
   */
145
  void setProof(ProofNodeManager* pnm,
146
                context::Context* ctx,
147
                ProofGenerator* defParent);
148
149
 private:
150
  /** A context-notify object that clears out stale data. */
151
  template <class T>
152
28800
  class DataClearer : context::ContextNotifyObj
153
  {
154
   public:
155
28863
    DataClearer(context::Context* context, T& data)
156
28863
        : context::ContextNotifyObj(context), d_data(data)
157
    {
158
28863
    }
159
160
   protected:
161
31065
    void contextNotifyPop() override
162
    {
163
93195
      Trace("circuit-prop")
164
31065
          << "CircuitPropagator::DataClearer: clearing data "
165
62130
          << "(size was " << d_data.size() << ")" << std::endl;
166
31065
      d_data.clear();
167
31065
    }
168
169
   private:
170
    T& d_data;
171
  }; /* class DataClearer<T> */
172
173
  /**
174
   * Assignment status of each node.
175
   */
176
  typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction>
177
      AssignmentMap;
178
179
  /**
180
   * Assign Node in circuit with the value and add it to the queue; note
181
   * conflicts.
182
   */
183
  void assignAndEnqueue(TNode n,
184
                        bool value,
185
                        std::shared_ptr<ProofNode> proof = nullptr);
186
187
  /**
188
   * Store a conflict for the case that we have derived both n and n.negate()
189
   * to be true.
190
   */
191
  void makeConflict(Node n);
192
193
  /**
194
   * Compute the map from nodes to the nodes that use it.
195
   */
196
  void computeBackEdges(TNode node);
197
198
  /**
199
   * Propagate new information forward in circuit to
200
   * the parents of "in".
201
   */
202
  void propagateForward(TNode child, bool assignment);
203
204
  /**
205
   * Propagate new information backward in circuit to
206
   * the children of "in".
207
   */
208
  void propagateBackward(TNode parent, bool assignment);
209
210
  /** Are proofs enabled? */
211
  bool isProofEnabled() const;
212
213
  context::Context d_context;
214
215
  /** The propagation queue */
216
  std::vector<TNode> d_propagationQueue;
217
218
  /**
219
   * We have a propagation queue "clearer" object for when the user
220
   * context pops.  Normally the propagation queue should be empty,
221
   * but this keeps us safe in case there's still some rubbish around
222
   * on the queue.
223
   */
224
  DataClearer<std::vector<TNode>> d_propagationQueueClearer;
225
226
  /** Are we in conflict? */
227
  context::CDO<TrustNode> d_conflict;
228
229
  /** Map of substitutions */
230
  std::vector<TrustNode> d_learnedLiterals;
231
232
  /**
233
   * Similar data clearer for learned literals.
234
   */
235
  DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
236
237
  /**
238
   * Back edges from nodes to where they are used.
239
   */
240
  BackEdgesMap d_backEdges;
241
242
  /**
243
   * Similar data clearer for back edges.
244
   */
245
  DataClearer<BackEdgesMap> d_backEdgesClearer;
246
247
  /** Nodes that have been attached already (computed forward edges for) */
248
  // All the nodes we've visited so far
249
  context::CDHashSet<Node, NodeHashFunction> d_seen;
250
251
  AssignmentMap d_state;
252
253
  /** Whether to perform forward propagation */
254
  const bool d_forwardPropagation;
255
256
  /** Whether to perform backward propagation */
257
  const bool d_backwardPropagation;
258
259
  /* Does the current state require a call to finish()? */
260
  bool d_needsFinish;
261
262
  /** Adds a new proof for f, or drops it if we already have a proof */
263
  void addProof(TNode f, std::shared_ptr<ProofNode> pf);
264
265
  /** A pointer to the proof manager */
266
  ProofNodeManager* d_pnm;
267
  /** Eager proof generator that actually stores the proofs */
268
  std::unique_ptr<EagerProofGenerator> d_epg;
269
  /** Connects the proofs to subproofs internally */
270
  std::unique_ptr<LazyCDProofChain> d_proofInternal;
271
  /** Connects the proofs to assumptions externally */
272
  std::unique_ptr<LazyCDProofChain> d_proofExternal;
273
}; /* class CircuitPropagator */
274
275
}  // namespace booleans
276
}  // namespace theory
277
}  // namespace CVC4
278
279
#endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */