From 487f15f90a73f47889a13ed8eba3dbe84129d6f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Oct 2016 23:49:45 -0700 Subject: [PATCH] better encodings for at-most-1, #755 Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.h | 2 -- src/util/sorting_network.h | 1 - 2 files changed, 3 deletions(-) diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index d0649729b..e1b16f0c9 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -119,8 +119,6 @@ public: app* mk_fresh_bool(); - expr_ref mk_at_most_1(unsigned num_args, expr * const * args); - private: rational to_rational(parameter const& p) const; diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index a29428dbc..242d4f43e 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -205,7 +205,6 @@ Notes: return mk_at_most_1(full, n, xs); } else { - std::cout << "sort " << k << "\n"; SASSERT(2*k <= n); m_t = full?LE_FULL:LE; card(k + 1, n, xs, out);