summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_strategy_cbqi.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp12
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index eff1c0d9b..a4632398d 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -11,17 +11,17 @@
**
** \brief Implementation of counterexample-guided quantifier instantiation strategies
**/
-
#include "theory/quantifiers/inst_strategy_cbqi.h"
-#include "theory/arith/theory_arith.h"
+
+#include "options/quantifiers_options.h"
+#include "smt_util/ite_removal.h"
#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
-#include "util/ite_removal.h"
+#include "theory/theory_engine.h"
using namespace std;
using namespace CVC4;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback