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").

7 files changed, 12 insertions, 12 deletions

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 29a4187ec..d214babae 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -15,10 +15,10 @@
 
 #include "theory/strings/infer_proof_cons.h"
 
-#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
+#include "proof/proof_node_manager.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_operation.h"
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index af905cbad..bba03dd28 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -21,12 +21,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_rule.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_rule.h"
+#include "proof/theory_proof_step_buffer.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
-#include "theory/theory_proof_step_buffer.h"
 #include "theory/uf/proof_equality_engine.h"
 
 namespace cvc5 {
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index cf9c64bb1..da44100f9 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -24,7 +24,7 @@
 #include "context/cdhashset.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
+#include "proof/proof_node_manager.h"
 #include "theory/ext_theory.h"
 #include "theory/inference_manager_buffered.h"
 #include "theory/output_channel.h"
diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h
index d3ede53ec..56afaed84 100644
--- a/src/theory/strings/proof_checker.h
+++ b/src/theory/strings/proof_checker.h
@@ -19,8 +19,8 @@
 #define CVC5__THEORY__STRINGS__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/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index b9af7a23f..c3580d963 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -15,8 +15,8 @@
 
 #include "theory/strings/regexp_elim.h"
 
-#include "expr/proof_node_manager.h"
 #include "options/strings_options.h"
+#include "proof/proof_node_manager.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"
 #include "theory/strings/theory_strings_utils.h"
diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h
index 5387548de..6187a7137 100644
--- a/src/theory/strings/regexp_elim.h
+++ b/src/theory/strings/regexp_elim.h
@@ -18,8 +18,8 @@
 #define CVC5__THEORY__STRINGS__REGEXP_ELIM_H
 
 #include "expr/node.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/trust_node.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/trust_node.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 7c399759b..7d660e019 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -20,8 +20,8 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "expr/proof_node_manager.h"
-#include "theory/eager_proof_generator.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/proof_node_manager.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"