Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

10 files changed, 18 insertions, 18 deletions

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index bed637904..d0f5006e1 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,8 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/output.h"
 #include "context/context.h"
 #include "cvc5_private.h"
-#include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
+#include "proof/proof_node_manager.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
 #include "prop/minisat/mtl/Heap.h"
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 708441b0c..97abdb077 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -19,14 +19,14 @@
 #define CVC5__PROP__PROOF_CNF_STREAM_H
 
 #include "context/cdhashmap.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/lazy_proof.h"
+#include "proof/proof_node.h"
+#include "proof/proof_node_manager.h"
+#include "proof/theory_proof_step_buffer.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_proof_manager.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/theory_proof_step_buffer.h"
 
 namespace cvc5 {
 namespace prop {
diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
index b4a8d1b17..0065ed99e 100644
--- a/src/prop/proof_post_processor.h
+++ b/src/prop/proof_post_processor.h
@@ -21,7 +21,7 @@
 #include <map>
 #include <unordered_set>
 
-#include "expr/proof_node_updater.h"
+#include "proof/proof_node_updater.h"
 #include "prop/proof_cnf_stream.h"
 
 namespace cvc5 {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a12816906..8903d4bc3 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -22,9 +22,9 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "proof/trust_node.h"
 #include "prop/skolem_def_manager.h"
 #include "theory/output_channel.h"
-#include "theory/trust_node.h"
 #include "util/result.h"
 
 namespace cvc5 {
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 000cebb72..09c5fb915 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -15,8 +15,8 @@
 
 #include "prop/prop_proof_manager.h"
 
-#include "expr/proof_ensure_closed.h"
-#include "expr/proof_node_algorithm.h"
+#include "proof/proof_ensure_closed.h"
+#include "proof/proof_node_algorithm.h"
 #include "prop/prop_proof_manager.h"
 #include "prop/sat_solver.h"
 
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index 1374acf8d..e415ed441 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -19,8 +19,8 @@
 #define CVC5__PROP_PROOF_MANAGER_H
 
 #include "context/cdlist.h"
-#include "expr/proof.h"
-#include "expr/proof_node_manager.h"
+#include "proof/proof.h"
+#include "proof/proof_node_manager.h"
 #include "prop/proof_post_processor.h"
 #include "prop/sat_proof_manager.h"
 
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 60a4c9704..5bec41e2b 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -15,11 +15,11 @@
 
 #include "prop/sat_proof_manager.h"
 
-#include "expr/proof_node_algorithm.h"
 #include "options/proof_options.h"
+#include "proof/proof_node_algorithm.h"
+#include "proof/theory_proof_step_buffer.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
-#include "theory/theory_proof_step_buffer.h"
 
 namespace cvc5 {
 namespace prop {
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index a53f66cec..a224f3a28 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -19,9 +19,9 @@
 #define CVC5__SAT_PROOF_MANAGER_H
 
 #include "context/cdhashset.h"
-#include "expr/buffered_proof_generator.h"
-#include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
+#include "proof/buffered_proof_generator.h"
+#include "proof/lazy_proof_chain.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/sat_solver_types.h"
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 963810594..9ad54e292 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -23,8 +23,8 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
 #include "proof/clause_id.h"
+#include "proof/proof_node_manager.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/sat_solver_types.h"
 #include "util/statistics_stats.h"
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index afd99ae83..d6ae1f975 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,11 +26,11 @@
 
 #include "context/cdqueue.h"
 #include "expr/node.h"
+#include "proof/trust_node.h"
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
-#include "theory/trust_node.h"
 #include "util/resource_manager.h"
 
 namespace cvc5 {