1 /********************* */
2 /*! \file circuit_propagator.h
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-2020 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
12 ** \brief A non-clausal circuit propagator for Boolean simplification
14 ** A non-clausal circuit propagator for Boolean simplification.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
20 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
24 #include <unordered_map>
27 #include "context/cdhashmap.h"
28 #include "context/cdhashset.h"
29 #include "context/cdo.h"
30 #include "context/context.h"
31 #include "expr/lazy_proof_chain.h"
32 #include "expr/node.h"
33 #include "expr/proof_generator.h"
34 #include "expr/proof_node.h"
35 #include "theory/eager_proof_generator.h"
36 #include "theory/theory.h"
37 #include "theory/trust_node.h"
38 #include "util/hash.h"
45 * The main purpose of the CircuitPropagator class is to maintain the
46 * state of the circuit for subsequent calls to propagate(), so that
47 * the same fact is not output twice, so that the same edge in the
48 * circuit isn't propagated twice, etc.
50 class CircuitPropagator
54 * Value of a particular node
58 /** Node is currently unassigned */
60 /** Node is assigned to true */
62 /** Node is assigned to false */
66 typedef std::unordered_map
<Node
, std::vector
<Node
>, NodeHashFunction
>
70 * Construct a new CircuitPropagator.
72 CircuitPropagator(bool enableForward
= true, bool enableBackward
= true);
74 /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
75 bool getAssignment(TNode n
) const
77 AssignmentMap::iterator i
= d_state
.find(n
);
78 Assert(i
!= d_state
.end() && (*i
).second
!= UNASSIGNED
);
79 return (*i
).second
== ASSIGNED_TO_TRUE
;
82 // Use custom context to ensure propagator is reset after use
83 void initialize() { d_context
.push(); }
85 void setNeedsFinish(bool value
) { d_needsFinish
= value
; }
87 bool getNeedsFinish() { return d_needsFinish
; }
89 std::vector
<TrustNode
>& getLearnedLiterals() { return d_learnedLiterals
; }
91 /** Finish the computation and pop the internal context */
94 /** Assert for propagation */
95 void assertTrue(TNode assertion
);
98 * Propagate through the asserted circuit propagator. New information
99 * discovered by the propagator are put in the substitutions vector used in
102 * @return a trust node encapsulating the proof for a conflict as a lemma that
103 * proves false, or the null trust node otherwise
105 TrustNode
propagate() CVC4_WARN_UNUSED_RESULT
;
108 * Get the back edges of this circuit.
110 const BackEdgesMap
& getBackEdges() const { return d_backEdges
; }
112 /** Invert a set value */
113 static inline AssignmentStatus
neg(AssignmentStatus value
)
115 Assert(value
!= UNASSIGNED
);
116 if (value
== ASSIGNED_TO_TRUE
)
117 return ASSIGNED_TO_FALSE
;
119 return ASSIGNED_TO_TRUE
;
122 /** True iff Node is assigned in circuit (either true or false). */
123 bool isAssigned(TNode n
) const
125 AssignmentMap::const_iterator i
= d_state
.find(n
);
126 return i
!= d_state
.end() && ((*i
).second
!= UNASSIGNED
);
129 /** True iff Node is assigned to the value. */
130 bool isAssignedTo(TNode n
, bool value
) const
132 AssignmentMap::const_iterator i
= d_state
.find(n
);
133 if (i
== d_state
.end()) return false;
134 if (value
&& ((*i
).second
== ASSIGNED_TO_TRUE
)) return true;
135 if (!value
&& ((*i
).second
== ASSIGNED_TO_FALSE
)) return true;
139 * Set proof node manager, context and parent proof generator.
141 * If parent is non-null, then it is responsible for the proofs provided
144 void setProof(ProofNodeManager
* pnm
,
145 context::Context
* ctx
,
146 ProofGenerator
* defParent
);
149 /** A context-notify object that clears out stale data. */
151 class DataClearer
: context::ContextNotifyObj
154 DataClearer(context::Context
* context
, T
& data
)
155 : context::ContextNotifyObj(context
), d_data(data
)
160 void contextNotifyPop() override
162 Trace("circuit-prop")
163 << "CircuitPropagator::DataClearer: clearing data "
164 << "(size was " << d_data
.size() << ")" << std::endl
;
170 }; /* class DataClearer<T> */
172 /** Predicate for use in STL functions. */
173 class IsAssigned
: public std::unary_function
<TNode
, bool>
175 CircuitPropagator
& d_circuit
;
178 IsAssigned(CircuitPropagator
& circuit
) : d_circuit(circuit
) {}
180 bool operator()(TNode in
) const { return d_circuit
.isAssigned(in
); }
181 }; /* class IsAssigned */
183 /** Predicate for use in STL functions. */
184 class IsAssignedTo
: public std::unary_function
<TNode
, bool>
186 CircuitPropagator
& d_circuit
;
190 IsAssignedTo(CircuitPropagator
& circuit
, bool value
)
191 : d_circuit(circuit
), d_value(value
)
195 bool operator()(TNode in
) const
197 return d_circuit
.isAssignedTo(in
, d_value
);
199 }; /* class IsAssignedTo */
202 * Assignment status of each node.
204 typedef context::CDHashMap
<TNode
, AssignmentStatus
, TNodeHashFunction
>
208 * Assign Node in circuit with the value and add it to the queue; note
211 void assignAndEnqueue(TNode n
,
213 std::shared_ptr
<ProofNode
> proof
= nullptr);
216 * Store a conflict for the case that we have derived both n and n.negate()
219 void makeConflict(Node n
);
222 * Compute the map from nodes to the nodes that use it.
224 void computeBackEdges(TNode node
);
227 * Propagate new information forward in circuit to
228 * the parents of "in".
230 void propagateForward(TNode child
, bool assignment
);
233 * Propagate new information backward in circuit to
234 * the children of "in".
236 void propagateBackward(TNode parent
, bool assignment
);
238 /** Are proofs enabled? */
239 bool isProofEnabled() const;
241 context::Context d_context
;
243 /** The propagation queue */
244 std::vector
<TNode
> d_propagationQueue
;
247 * We have a propagation queue "clearer" object for when the user
248 * context pops. Normally the propagation queue should be empty,
249 * but this keeps us safe in case there's still some rubbish around
252 DataClearer
<std::vector
<TNode
>> d_propagationQueueClearer
;
254 /** Are we in conflict? */
255 context::CDO
<TrustNode
> d_conflict
;
257 /** Map of substitutions */
258 std::vector
<TrustNode
> d_learnedLiterals
;
261 * Similar data clearer for learned literals.
263 DataClearer
<std::vector
<TrustNode
>> d_learnedLiteralClearer
;
266 * Back edges from nodes to where they are used.
268 BackEdgesMap d_backEdges
;
271 * Similar data clearer for back edges.
273 DataClearer
<BackEdgesMap
> d_backEdgesClearer
;
275 /** Nodes that have been attached already (computed forward edges for) */
276 // All the nodes we've visited so far
277 context::CDHashSet
<Node
, NodeHashFunction
> d_seen
;
279 AssignmentMap d_state
;
281 /** Whether to perform forward propagation */
282 const bool d_forwardPropagation
;
284 /** Whether to perform backward propagation */
285 const bool d_backwardPropagation
;
287 /* Does the current state require a call to finish()? */
290 /** Adds a new proof for f, or drops it if we already have a proof */
291 void addProof(TNode f
, std::shared_ptr
<ProofNode
> pf
);
293 /** A pointer to the proof manager */
294 ProofNodeManager
* d_pnm
;
295 /** Eager proof generator that actually stores the proofs */
296 std::unique_ptr
<EagerProofGenerator
> d_epg
;
297 /** Connects the proofs to subproofs internally */
298 std::unique_ptr
<LazyCDProofChain
> d_proofInternal
;
299 /** Connects the proofs to assumptions externally */
300 std::unique_ptr
<LazyCDProofChain
> d_proofExternal
;
301 }; /* class CircuitPropagator */
303 } // namespace booleans
304 } // namespace theory
307 #endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */