From 0268f2243ec8939f3e72db2761724418415818a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Oct 2017 09:49:53 -0700 Subject: [PATCH] remove ast.h reference Signed-off-by: Nikolaj Bjorner --- src/util/min_cut.cpp | 7 +++++-- src/util/min_cut.h | 1 - 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/util/min_cut.cpp b/src/util/min_cut.cpp index 2f7bdb862..b7c30f546 100644 --- a/src/util/min_cut.cpp +++ b/src/util/min_cut.cpp @@ -16,6 +16,7 @@ Revision History: --*/ #include "util/min_cut.h" +#include "util/trace.h" min_cut::min_cut() { // push back two empty vectors for source and sink @@ -74,7 +75,8 @@ void min_cut::compute_min_cut(unsigned_vector& cut_nodes) { bool_vector reachable(m_edges.size()); compute_reachable_nodes(reachable); - // find all edges between reachable and unreachable nodes and for each such edge, add corresponding lemma to unsat-core + // find all edges between reachable and unreachable nodes and + // for each such edge, add corresponding lemma to unsat-core compute_cut_and_add_lemmas(reachable, cut_nodes); } @@ -91,7 +93,8 @@ void min_cut::compute_initial_distances() { if (!visited[current]) { bool exists_unvisited_parent = false; - // add unprocessed parents to stack for DFS. If there is at least one unprocessed parent, don't compute the result + // add unprocessed parents to stack for DFS. If there is at least + // one unprocessed parent, don't compute the result // for current now, but wait until those unprocessed parents are processed for (auto const& edge : m_edges[current]) { unsigned parent = edge.node; diff --git a/src/util/min_cut.h b/src/util/min_cut.h index 5a783a8d0..51a330126 100644 --- a/src/util/min_cut.h +++ b/src/util/min_cut.h @@ -19,7 +19,6 @@ Revision History: #ifndef MIN_CUT_H_ #define MIN_CUT_H_ -#include "ast/ast.h" #include "util/vector.h"