summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r--src/prop/cnf_stream.cpp22
1 files changed, 11 insertions, 11 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index b0b135b04..ffbc67cc4 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -15,23 +15,23 @@
** A CNF converter that takes in asserts and has the side effect
** of given an equisatisfiable stream of assertions to PropEngine.
**/
+#include <queue>
-#include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/theory.h"
-#include "expr/node.h"
-#include "util/cvc4_assert.h"
-#include "util/output.h"
-#include "expr/command.h"
+#include "base/cvc4_assert.h"
+#include "base/output.h"
#include "expr/expr.h"
-#include "prop/theory_proxy.h"
-#include "theory/bv/options.h"
+#include "expr/node.h"
+#include "options/bv_options.h"
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
+#include "prop/cnf_stream.h"
#include "prop/minisat/minisat.h"
+#include "prop/prop_engine.h"
+#include "prop/theory_proxy.h"
#include "smt/smt_engine_scope.h"
-#include <queue>
+#include "smt_util/command.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
using namespace std;
using namespace CVC4::kind;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback