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, 11 insertions, 11 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 9effdbec7..71f4028ec 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,12 +15,12 @@
 
 #include "theory/quantifiers/instantiate.h"
 
-#include "expr/lazy_proof.h"
 #include "expr/node_algorithm.h"
-#include "expr/proof_node_manager.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "proof/lazy_proof.h"
+#include "proof/proof_node_manager.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 9b410dd08..95a396d51 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -22,7 +22,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "expr/proof.h"
+#include "proof/proof.h"
 #include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h
index 618ac8301..23441772e 100644
--- a/src/theory/quantifiers/proof_checker.h
+++ b/src/theory/quantifiers/proof_checker.h
@@ -19,8 +19,8 @@
 #define CVC5__THEORY__QUANTIFIERS__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/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index cfc4eca2e..ae7f75f34 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -18,8 +18,8 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
 #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
 
+#include "proof/trust_node.h"
 #include "theory/theory_rewriter.h"
-#include "theory/trust_node.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index c9234db2c..fa91b1782 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -17,11 +17,11 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "expr/proof.h"
-#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "proof/proof.h"
+#include "proof/proof_node_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_registry.h"
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 2a09913a9..c8e6ec7dd 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -24,8 +24,8 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/type_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 {
 
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6bfedb0a2..c74146c9c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -15,8 +15,8 @@
 
 #include "theory/quantifiers/theory_quantifiers.h"
 
-#include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
+#include "proof/proof_node_manager.h"
 #include "theory/quantifiers/quantifiers_macros.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"