diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-28 10:03:13 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-28 15:40:22 -0700 |
commit | 85842c3ad03ab94586c6b34eb01149f449bff52d (patch) | |
tree | 1e621c5775f051972c4e9bb6e56f3a9292104ad2 /src/theory/booleans | |
parent | af950306f906801dbc3411e57bf74c77f2578ba1 (diff) |
Reorder circuit propagator class.
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 363 |
1 files changed, 189 insertions, 174 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index bd6da8742..adb1eb42f 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -23,33 +23,32 @@ #include <unordered_map> #include <vector> -#include "theory/theory.h" -#include "context/context.h" -#include "util/hash.h" -#include "expr/node.h" -#include "context/cdhashset.h" #include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/theory.h" +#include "util/hash.h" namespace CVC4 { namespace theory { namespace booleans { - /** * The main purpose of the CircuitPropagator class is to maintain the * state of the circuit for subsequent calls to propagate(), so that * the same fact is not output twice, so that the same edge in the * circuit isn't propagated twice, etc. */ -class CircuitPropagator { - -public: - +class CircuitPropagator +{ + public: /** * Value of a particular node */ - enum AssignmentStatus { + enum AssignmentStatus + { /** Node is currently unassigned */ UNASSIGNED = 0, /** Node is assigned to true */ @@ -58,119 +57,85 @@ public: ASSIGNED_TO_FALSE, }; - /** Invert a set value */ - static inline AssignmentStatus neg(AssignmentStatus value) { - Assert(value != UNASSIGNED); - if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE; - else return ASSIGNED_TO_TRUE; - } - - typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; - -private: - - context::Context d_context; - - /** The propagation queue */ - std::vector<TNode> d_propagationQueue; - - /** A context-notify object that clears out stale data. */ - template <class T> - class DataClearer : context::ContextNotifyObj { - T& d_data; - protected: - void contextNotifyPop() override - { - Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data " - << "(size was " << d_data.size() << ")" << std::endl; - d_data.clear(); - } - public: - DataClearer(context::Context* context, T& data) : - context::ContextNotifyObj(context), - d_data(data) { - } - };/* class DataClearer<T> */ + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> + BackEdgesMap; /** - * We have a propagation queue "clearer" object for when the user - * context pops. Normally the propagation queue should be empty, - * but this keeps us safe in case there's still some rubbish around - * on the queue. + * Construct a new CircuitPropagator. */ - DataClearer< std::vector<TNode> > d_propagationQueueClearer; + CircuitPropagator(std::vector<Node>& outLearnedLiterals, + bool enableForward = true, + bool enableBackward = true) + : d_context(), + d_propagationQueue(), + d_propagationQueueClearer(&d_context, d_propagationQueue), + d_conflict(&d_context, false), + d_learnedLiterals(outLearnedLiterals), + d_learnedLiteralClearer(&d_context, outLearnedLiterals), + d_backEdges(), + d_backEdgesClearer(&d_context, d_backEdges), + d_seen(&d_context), + d_state(&d_context), + d_forwardPropagation(enableForward), + d_backwardPropagation(enableBackward), + d_needsFinish(false) + { + } - /** Are we in conflict? */ - context::CDO<bool> d_conflict; + /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ + bool getAssignment(TNode n) const + { + AssignmentMap::iterator i = d_state.find(n); + Assert(i != d_state.end() && (*i).second != UNASSIGNED); + return (*i).second == ASSIGNED_TO_TRUE; + } - /** Map of substitutions */ - std::vector<Node>& d_learnedLiterals; + // Use custom context to ensure propagator is reset after use + void initialize() { d_context.push(); } - /** - * Similar data clearer for learned literals. - */ - DataClearer< std::vector<Node> > d_learnedLiteralClearer; + void setNeedsFinish(bool value) { d_needsFinish = value; } - /** - * Back edges from nodes to where they are used. - */ - BackEdgesMap d_backEdges; + bool getNeedsFinish() { return d_needsFinish; } - /** - * Similar data clearer for back edges. - */ - DataClearer<BackEdgesMap> d_backEdgesClearer; + void finish() { d_context.pop(); } - /** Nodes that have been attached already (computed forward edges for) */ - // All the nodes we've visited so far - context::CDHashSet<Node, NodeHashFunction> d_seen; + /** Assert for propagation */ + void assertTrue(TNode assertion); /** - * Assignment status of each node. + * Propagate through the asserted circuit propagator. New information + * discovered by the propagator are put in the substitutions vector used in + * construction. + * + * @return true iff conflict found */ - typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; - AssignmentMap d_state; + bool propagate() CVC4_WARN_UNUSED_RESULT; /** - * Assign Node in circuit with the value and add it to the queue; note conflicts. + * Get the back edges of this circuit. */ - void assignAndEnqueue(TNode n, bool value) { - - Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl; + const BackEdgesMap& getBackEdges() const { return d_backEdges; } - if (n.getKind() == kind::CONST_BOOLEAN) { - // Assigning a constant to the opposite value is dumb - if (value != n.getConst<bool>()) { - d_conflict = true; - return; - } - } - - // Get the current assignment - AssignmentStatus state = d_state[n]; - - if(state != UNASSIGNED) { - // If the node is already assigned we might have a conflict - if(value != (state == ASSIGNED_TO_TRUE)) { - d_conflict = true; - } - } else { - // If unassigned, mark it as assigned - d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; - // Add for further propagation - d_propagationQueue.push_back(n); - } + /** Invert a set value */ + static inline AssignmentStatus neg(AssignmentStatus value) + { + Assert(value != UNASSIGNED); + if (value == ASSIGNED_TO_TRUE) + return ASSIGNED_TO_FALSE; + else + return ASSIGNED_TO_TRUE; } -public: /** True iff Node is assigned in circuit (either true or false). */ - bool isAssigned(TNode n) const { + bool isAssigned(TNode n) const + { AssignmentMap::const_iterator i = d_state.find(n); return i != d_state.end() && ((*i).second != UNASSIGNED); } /** True iff Node is assigned to the value. */ - bool isAssignedTo(TNode n, bool value) const { + bool isAssignedTo(TNode n, bool value) const + { AssignmentMap::const_iterator i = d_state.find(n); if (i == d_state.end()) return false; if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true; @@ -178,41 +143,103 @@ public: return false; } - /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ - bool getAssignment(TNode n) const { - AssignmentMap::iterator i = d_state.find(n); - Assert(i != d_state.end() && (*i).second != UNASSIGNED); - return (*i).second == ASSIGNED_TO_TRUE; - } + private: + /** A context-notify object that clears out stale data. */ + template <class T> + class DataClearer : context::ContextNotifyObj + { + public: + DataClearer(context::Context* context, T& data) + : context::ContextNotifyObj(context), d_data(data) + { + } + + protected: + void contextNotifyPop() override + { + Trace("circuit-prop") + << "CircuitPropagator::DataClearer: clearing data " + << "(size was " << d_data.size() << ")" << std::endl; + d_data.clear(); + } + + private: + T& d_data; + }; /* class DataClearer<T> */ -private: /** Predicate for use in STL functions. */ - class IsAssigned : public std::unary_function<TNode, bool> { + class IsAssigned : public std::unary_function<TNode, bool> + { CircuitPropagator& d_circuit; - public: - IsAssigned(CircuitPropagator& circuit) : - d_circuit(circuit) { - } - bool operator()(TNode in) const { - return d_circuit.isAssigned(in); - } - };/* class IsAssigned */ + public: + IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {} + + bool operator()(TNode in) const { return d_circuit.isAssigned(in); } + }; /* class IsAssigned */ /** Predicate for use in STL functions. */ - class IsAssignedTo : public std::unary_function<TNode, bool> { + class IsAssignedTo : public std::unary_function<TNode, bool> + { CircuitPropagator& d_circuit; bool d_value; - public: - IsAssignedTo(CircuitPropagator& circuit, bool value) : - d_circuit(circuit), - d_value(value) { + + public: + IsAssignedTo(CircuitPropagator& circuit, bool value) + : d_circuit(circuit), d_value(value) + { } - bool operator()(TNode in) const { + bool operator()(TNode in) const + { return d_circuit.isAssignedTo(in, d_value); } - };/* class IsAssignedTo */ + }; /* class IsAssignedTo */ + + /** + * Assignment status of each node. + */ + typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> + AssignmentMap; + + /** + * Assign Node in circuit with the value and add it to the queue; note + * conflicts. + */ + void assignAndEnqueue(TNode n, bool value) + { + Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " + << (value ? "true" : "false") << ")" << std::endl; + + if (n.getKind() == kind::CONST_BOOLEAN) + { + // Assigning a constant to the opposite value is dumb + if (value != n.getConst<bool>()) + { + d_conflict = true; + return; + } + } + + // Get the current assignment + AssignmentStatus state = d_state[n]; + + if (state != UNASSIGNED) + { + // If the node is already assigned we might have a conflict + if (value != (state == ASSIGNED_TO_TRUE)) + { + d_conflict = true; + } + } + else + { + // If unassigned, mark it as assigned + d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; + // Add for further propagation + d_propagationQueue.push_back(n); + } + } /** * Compute the map from nodes to the nodes that use it. @@ -231,71 +258,59 @@ private: */ void propagateBackward(TNode parent, bool assignment); - /** Whether to perform forward propagation */ - const bool d_forwardPropagation; - - /** Whether to perform backward propagation */ - const bool d_backwardPropagation; + context::Context d_context; - /* Does the current state require a call to finish()? */ - bool d_needsFinish; + /** The propagation queue */ + std::vector<TNode> d_propagationQueue; -public: /** - * Construct a new CircuitPropagator. + * We have a propagation queue "clearer" object for when the user + * context pops. Normally the propagation queue should be empty, + * but this keeps us safe in case there's still some rubbish around + * on the queue. */ - CircuitPropagator(std::vector<Node>& outLearnedLiterals, - bool enableForward = true, - bool enableBackward = true) - : d_context(), - d_propagationQueue(), - d_propagationQueueClearer(&d_context, d_propagationQueue), - d_conflict(&d_context, false), - d_learnedLiterals(outLearnedLiterals), - d_learnedLiteralClearer(&d_context, outLearnedLiterals), - d_backEdges(), - d_backEdgesClearer(&d_context, d_backEdges), - d_seen(&d_context), - d_state(&d_context), - d_forwardPropagation(enableForward), - d_backwardPropagation(enableBackward), - d_needsFinish(false) - { - } - - // Use custom context to ensure propagator is reset after use - void initialize() - { d_context.push(); } - - void setNeedsFinish(bool value) { d_needsFinish = value; } + DataClearer<std::vector<TNode> > d_propagationQueueClearer; - bool getNeedsFinish() { return d_needsFinish; } + /** Are we in conflict? */ + context::CDO<bool> d_conflict; - void finish() - { d_context.pop(); } + /** Map of substitutions */ + std::vector<Node>& d_learnedLiterals; - /** Assert for propagation */ - void assertTrue(TNode assertion); + /** + * Similar data clearer for learned literals. + */ + DataClearer<std::vector<Node> > d_learnedLiteralClearer; /** - * Propagate through the asserted circuit propagator. New information discovered by the propagator - * are put in the substitutions vector used in construction. - * - * @return true iff conflict found + * Back edges from nodes to where they are used. */ - bool propagate() CVC4_WARN_UNUSED_RESULT; + BackEdgesMap d_backEdges; /** - * Get the back edges of this circuit. + * Similar data clearer for back edges. */ - const BackEdgesMap& getBackEdges() const { - return d_backEdges; - } + DataClearer<BackEdgesMap> d_backEdgesClearer; + + /** Nodes that have been attached already (computed forward edges for) */ + // All the nodes we've visited so far + context::CDHashSet<Node, NodeHashFunction> d_seen; + + AssignmentMap d_state; + + /** Whether to perform forward propagation */ + const bool d_forwardPropagation; + + /** Whether to perform backward propagation */ + const bool d_backwardPropagation; + + /* Does the current state require a call to finish()? */ + bool d_needsFinish; -};/* class CircuitPropagator */ +}; /* class CircuitPropagator */ -}/* CVC4::theory::booleans namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace booleans +} // namespace theory +} // namespace CVC4 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ |