mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

missing files

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-25 09:00:35 -07:00
parent 7148226823
commit f5f1d019d8
2 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/min_cut.cpp
View file

@ -28,9 +28,9 @@ unsigned min_cut::new_node() {
return m_edges.size() - 1; return m_edges.size() - 1;
} }
void min_cut::add_edge(unsigned int i, unsigned int j) { void min_cut::add_edge(unsigned int i, unsigned int j, unsigned capacity) {
m_edges.reserve(i + 1); m_edges.reserve(i + 1);
m_edges[i].push_back(edge(j, 1)); m_edges[i].push_back(edge(j, capacity));
TRACE("spacer.mincut", tout << "adding edge (" << i << "," << j << ")\n";); TRACE("spacer.mincut", tout << "adding edge (" << i << "," << j << ")\n";);
} }

14
src/util/min_cut.h
View file

@ -27,12 +27,20 @@ class min_cut {
public: public:
min_cut(); min_cut();
unsigned new_node();
/* /*
\brief add an edge (with unit capacity) \brief create a node
*/ */
void add_edge(unsigned i, unsigned j); unsigned new_node();
/*
\brief add an i -> j edge with (unit) capacity
*/
void add_edge(unsigned i, unsigned j, unsigned capacity = 1);
/*
\brief produce a min cut between source node = 0 and target node = 1.
NB. the function changes capacities on edges.
*/
void compute_min_cut(unsigned_vector& cut_nodes); void compute_min_cut(unsigned_vector& cut_nodes);
private: private: