summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r--src/theory/arith/nl/cad/proof_checker.h2
-rw-r--r--src/theory/arith/nl/cad/proof_generator.cpp2
-rw-r--r--src/theory/arith/nl/cad/proof_generator.h4
-rw-r--r--src/theory/arith/nl/ext/ext_state.cpp4
-rw-r--r--src/theory/arith/nl/ext/ext_state.h2
-rw-r--r--src/theory/arith/nl/ext/factoring_check.cpp4
-rw-r--r--src/theory/arith/nl/ext/monomial_bounds_check.cpp2
-rw-r--r--src/theory/arith/nl/ext/monomial_check.cpp6
-rw-r--r--src/theory/arith/nl/ext/proof_checker.h4
-rw-r--r--src/theory/arith/nl/ext/split_zero_check.cpp4
-rw-r--r--src/theory/arith/nl/ext/tangent_plane_check.cpp4
-rw-r--r--src/theory/arith/nl/transcendental/exponential_solver.cpp2
-rw-r--r--src/theory/arith/nl/transcendental/proof_checker.h4
-rw-r--r--src/theory/arith/nl/transcendental/sine_solver.cpp2
-rw-r--r--src/theory/arith/nl/transcendental/transcendental_state.cpp2
-rw-r--r--src/theory/arith/nl/transcendental/transcendental_state.h2
16 files changed, 25 insertions, 25 deletions
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index d7ce05b60..8cc544fc4 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -19,7 +19,7 @@
#define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
#include "expr/node.h"
-#include "expr/proof_checker.h"
+#include "proof/proof_checker.h"
namespace cvc5 {
namespace theory {
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index b0d785b2a..374a7e4ef 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -17,7 +17,7 @@
#ifdef CVC5_POLY_IMP
-#include "theory/lazy_tree_proof_generator.h"
+#include "proof/lazy_tree_proof_generator.h"
#include "theory/arith/nl/poly_conversion.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index b493455a6..613db7565 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -25,9 +25,9 @@
#include <vector>
#include "expr/node.h"
-#include "expr/proof_set.h"
+#include "proof/lazy_tree_proof_generator.h"
+#include "proof/proof_set.h"
#include "theory/arith/nl/cad/cdcac_utils.h"
-#include "theory/lazy_tree_proof_generator.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 9ebd42d55..c1937797e 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -18,11 +18,11 @@
#include <vector>
#include "expr/node.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/ext/monomial.h"
-#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/nl_model.h"
namespace cvc5 {
namespace theory {
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index b0a4fd859..7c2cc1b9b 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -19,7 +19,7 @@
#include <vector>
#include "expr/node.h"
-#include "expr/proof_set.h"
+#include "proof/proof_set.h"
#include "theory/arith/nl/ext/monomial.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index c4bba6ec8..d6b732eb9 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -16,12 +16,12 @@
#include "theory/arith/nl/ext/factoring_check.h"
#include "expr/node.h"
-#include "expr/proof.h"
#include "expr/skolem_manager.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/ext/ext_state.h"
+#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 44f59c521..0deb2c99d 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -16,8 +16,8 @@
#include "theory/arith/nl/ext/monomial_bounds_check.h"
#include "expr/node.h"
-#include "expr/proof.h"
#include "options/arith_options.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 404916453..bf38bc8f0 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -16,12 +16,12 @@
#include "theory/arith/nl/ext/monomial_check.h"
#include "expr/node.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/nl/ext/ext_state.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/nl_model.h"
namespace cvc5 {
namespace theory {
diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h
index 400126510..bf28cea59 100644
--- a/src/theory/arith/nl/ext/proof_checker.h
+++ b/src/theory/arith/nl/ext/proof_checker.h
@@ -19,8 +19,8 @@
#define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
#include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_node.h"
namespace cvc5 {
namespace theory {
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index ace7e0868..6d9faa356 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -16,11 +16,11 @@
#include "theory/arith/nl/ext/split_zero_check.h"
#include "expr/node.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/ext/ext_state.h"
+#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index a66f1396c..9efa9c0f2 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -16,11 +16,11 @@
#include "theory/arith/nl/ext/tangent_plane_check.h"
#include "expr/node.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/ext/ext_state.h"
+#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
namespace cvc5 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 11e2b9cc8..73279a782 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -20,8 +20,8 @@
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
-#include "expr/proof.h"
#include "options/arith_options.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h
index 8675afe39..06359e62a 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.h
+++ b/src/theory/arith/nl/transcendental/proof_checker.h
@@ -19,8 +19,8 @@
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
#include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_node.h"
namespace cvc5 {
namespace theory {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 26d959878..6fdd4cc15 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -20,9 +20,9 @@
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
-#include "expr/proof.h"
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
+#include "proof/proof.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index c0f5d23b2..db20713f1 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -15,7 +15,7 @@
#include "theory/arith/nl/transcendental/transcendental_state.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nl_model.h"
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 74f005294..56cbec79a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -17,7 +17,7 @@
#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
#include "expr/node.h"
-#include "expr/proof_set.h"
+#include "proof/proof_set.h"
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/nl/transcendental/proof_checker.h"
#include "theory/arith/nl/transcendental/taylor_generator.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback