diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:57:01 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:57:01 -0500 |
commit | c7892fd17983a27d06b56c47f8125d50c691451c (patch) | |
tree | f36040b5f38811d19f6b548e076799c1e82224c9 /src/theory/booleans | |
parent | 0695bc6fd69ac01873d541c8501de3c77ca21edf (diff) | |
parent | ce7c485182902ae43871057185095f71f74a8a58 (diff) |
Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index aec0cff58..de4bb30d2 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -64,6 +64,8 @@ public: else return ASSIGNED_TO_TRUE; } + typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + private: context::Context d_context; @@ -96,7 +98,7 @@ private: */ DataClearer< std::vector<TNode> > d_propagationQueueClearer; - /** Are we in conflict */ + /** Are we in conflict? */ context::CDO<bool> d_conflict; /** Map of substitutions */ @@ -107,8 +109,9 @@ private: */ DataClearer< std::vector<Node> > d_learnedLiteralClearer; - /** Back edges from nodes to where they are used */ - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + /** + * Back edges from nodes to where they are used. + */ BackEdgesMap d_backEdges; /** @@ -157,6 +160,7 @@ private: } } +public: /** True iff Node is assigned in circuit (either true or false). */ bool isAssigned(TNode n) const { AssignmentMap::const_iterator i = d_state.find(n); @@ -179,6 +183,7 @@ private: return (*i).second == ASSIGNED_TO_TRUE; } +private: /** Predicate for use in STL functions. */ class IsAssigned : public std::unary_function<TNode, bool> { CircuitPropagator& d_circuit; @@ -268,6 +273,13 @@ public: */ bool propagate() CVC4_WARN_UNUSED_RESULT; + /** + * Get the back edges of this circuit. + */ + const BackEdgesMap& getBackEdges() const { + return d_backEdges; + } + };/* class CircuitPropagator */ }/* CVC4::theory::booleans namespace */ |