diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-29 17:39:12 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 15:39:29 -0500 |
commit | 1885fb09079e71b0b99cb06de90fa1abb475a068 (patch) | |
tree | 948091bac92eff85a96b0e45e6c94c6db1bb7bef /src/theory/booleans | |
parent | 458d47b2330418fb0045197e12edc9c730034180 (diff) |
new miplib pass, works for 1 or 2 vars
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 */ |