summaryrefslogtreecommitdiff
path: root/src/theory/arith/error_set.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/error_set.h')
-rw-r--r--src/theory/arith/error_set.h28
1 files changed, 5 insertions, 23 deletions
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 5843e0f7b..f12e38c12 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -20,36 +20,18 @@
#pragma once
+#include <vector>
+
+#include "expr/statistics_registry.h"
+#include "options/arith_heuristic_pivot_rule.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
+#include "theory/arith/callbacks.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
-#include "theory/arith/arith_heuristic_pivot_rule.h"
#include "theory/arith/tableau_sizes.h"
-#include "theory/arith/callbacks.h"
-
-#include "util/statistics_registry.h"
#include "util/bin_heap.h"
-// #if CVC4_GCC_HAS_PB_DS_BUG
-// // Unfortunate bug in some older GCCs (e.g., v4.2):
-// // http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
-// // Requires some header-hacking to work around
-// # define __throw_container_error inline __throw_container_error
-// # define __throw_insert_error inline __throw_insert_error
-// # define __throw_join_error inline __throw_join_error
-// # define __throw_resize_error inline __throw_resize_error
-// # include <ext/pb_ds/exception.hpp>
-// # undef __throw_container_error
-// # undef __throw_insert_error
-// # undef __throw_join_error
-// # undef __throw_resize_error
-// #endif /* CVC4_GCC_HAS_PB_DS_BUG */
-
-// #include <ext/pb_ds/priority_queue.hpp>
-
-#include <vector>
-
namespace CVC4 {
namespace theory {
namespace arith {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback