diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-24 13:51:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-24 15:51:09 -0300 |
| commit | bd33d20609999f6f847aeb63a42350aeb3041406 (patch) | |
| tree | 8b4a3ccb0ab48b65bd70222dbfd572de8743bcd9 | |
| parent | 1516e3b5d9436be86841a52002fc728fcd52dd34 (diff) | |
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").
161 files changed, 397 insertions, 400 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5362baad8..025f10117 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -136,9 +136,50 @@ libcvc5_add_sources( printer/smt2/smt2_printer.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h + proof/buffered_proof_generator.cpp + proof/buffered_proof_generator.h + proof/conv_proof_generator.cpp + proof/conv_proof_generator.h + proof/conv_seq_proof_generator.cpp + proof/conv_seq_proof_generator.h proof/clause_id.h proof/dot/dot_printer.cpp proof/dot/dot_printer.h + proof/eager_proof_generator.cpp + proof/eager_proof_generator.h + proof/lazy_proof.cpp + proof/lazy_proof.h + proof/lazy_proof_chain.cpp + proof/lazy_proof_chain.h + proof/lazy_tree_proof_generator.cpp + proof/lazy_tree_proof_generator.h + proof/proof.cpp + proof/proof.h + proof/proof_checker.cpp + proof/proof_checker.h + proof/proof_ensure_closed.cpp + proof/proof_ensure_closed.h + proof/proof_generator.cpp + proof/proof_generator.h + proof/proof_node.cpp + proof/proof_node.h + proof/proof_node_algorithm.cpp + proof/proof_node_algorithm.h + proof/proof_node_to_sexpr.cpp + proof/proof_node_to_sexpr.h + proof/proof_node_manager.cpp + proof/proof_node_manager.h + proof/proof_node_updater.cpp + proof/proof_node_updater.h + proof/proof_rule.cpp + proof/proof_rule.h + proof/proof_set.h + proof/proof_step_buffer.cpp + proof/proof_step_buffer.h + proof/trust_node.cpp + proof/trust_node.h + proof/theory_proof_step_buffer.cpp + proof/theory_proof_step_buffer.h proof/unsat_core.cpp proof/unsat_core.h prop/bv_sat_solver_notify.h @@ -600,8 +641,6 @@ libcvc5_add_sources( theory/decision_manager.h theory/decision_strategy.cpp theory/decision_strategy.h - theory/eager_proof_generator.cpp - theory/eager_proof_generator.h theory/ee_manager.cpp theory/ee_manager.h theory/ee_manager_distributed.cpp @@ -631,8 +670,6 @@ libcvc5_add_sources( theory/inference_id.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h - theory/lazy_tree_proof_generator.cpp - theory/lazy_tree_proof_generator.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp @@ -1029,14 +1066,10 @@ libcvc5_add_sources( theory/theory_model_builder.h theory/theory_preprocessor.cpp theory/theory_preprocessor.h - theory/theory_proof_step_buffer.cpp - theory/theory_proof_step_buffer.h theory/theory_rewriter.cpp theory/theory_rewriter.h theory/theory_state.cpp theory/theory_state.h - theory/trust_node.cpp - theory/trust_node.h theory/trust_substitutions.cpp theory/trust_substitutions.h theory/type_enumerator.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9bf63dcfc..094c7bcbd 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -24,8 +24,6 @@ libcvc5_add_sources( attribute_unique_id.h bound_var_manager.cpp bound_var_manager.h - buffered_proof_generator.cpp - buffered_proof_generator.h emptyset.cpp emptyset.h emptybag.cpp @@ -33,10 +31,6 @@ libcvc5_add_sources( expr_iomanip.cpp expr_iomanip.h kind_map.h - lazy_proof.cpp - lazy_proof.h - lazy_proof_chain.cpp - lazy_proof_chain.h match_trie.cpp match_trie.h node.cpp @@ -58,37 +52,12 @@ libcvc5_add_sources( sequence.cpp sequence.h node_visitor.h - proof.cpp - proof.h - proof_checker.cpp - proof_checker.h - proof_ensure_closed.cpp - proof_ensure_closed.h - proof_generator.cpp - proof_generator.h - proof_node.cpp - proof_node.h - proof_node_algorithm.cpp - proof_node_algorithm.h - proof_node_to_sexpr.cpp - proof_node_to_sexpr.h - proof_node_manager.cpp - proof_node_manager.h - proof_node_updater.cpp - proof_node_updater.h - proof_rule.cpp - proof_rule.h - proof_set.h - proof_step_buffer.cpp - proof_step_buffer.h skolem_manager.cpp skolem_manager.h symbol_manager.cpp symbol_manager.h symbol_table.cpp symbol_table.h - tconv_seq_proof_generator.cpp - tconv_seq_proof_generator.h term_canonize.cpp term_canonize.h term_context.cpp @@ -97,8 +66,6 @@ libcvc5_add_sources( term_context_node.h term_context_stack.cpp term_context_stack.h - term_conversion_proof_generator.cpp - term_conversion_proof_generator.h type_checker.h type_matcher.cpp type_matcher.h diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 2f3a49ac2..5542cfcf3 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,7 +18,7 @@ #include "expr/node_manager.h" #include "options/smt_options.h" -#include "expr/lazy_proof.h" +#include "proof/lazy_proof.h" #include "smt/preprocess_proof_generator.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index bb8e594d7..af88d5164 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -22,7 +22,7 @@ #include <vector> #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 7f6106e3a..de16cc49a 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -21,7 +21,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index 729252dd6..2312c38ed 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace preprocessing { diff --git a/src/expr/buffered_proof_generator.cpp b/src/proof/buffered_proof_generator.cpp index 2cbbd7e91..d6f54fb34 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/proof/buffered_proof_generator.cpp @@ -13,10 +13,10 @@ * Implementation of a proof generator for buffered proof steps. */ -#include "expr/buffered_proof_generator.h" +#include "proof/buffered_proof_generator.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" +#include "proof/proof.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/buffered_proof_generator.h b/src/proof/buffered_proof_generator.h index 2e1ef6c53..9d13faff4 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/proof/buffered_proof_generator.h @@ -15,11 +15,11 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H -#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H +#define CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -28,8 +28,8 @@ class ProofStep; /** * The proof generator for buffered steps. This class is a context-dependent - * mapping from formulas to proof steps. It does not generate ProofNodes until it - * is asked to provide a proof for a given fact. + * mapping from formulas to proof steps. It does not generate ProofNodes until + * it is asked to provide a proof for a given fact. */ class BufferedProofGenerator : public ProofGenerator { @@ -61,4 +61,4 @@ class BufferedProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/proof/conv_proof_generator.cpp index 0e0ed3165..3635f3dea 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/proof/conv_proof_generator.cpp @@ -13,15 +13,15 @@ * Implementation of term conversion proof generator utility. */ -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" #include <sstream> -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "expr/term_context.h" #include "expr/term_context_stack.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" using namespace cvc5::kind; @@ -232,7 +232,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f) } std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f); Trace("tconv-pf-gen") << "... success" << std::endl; - Assert (pfn!=nullptr); + Assert(pfn != nullptr); Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl; return pfn; } diff --git a/src/expr/term_conversion_proof_generator.h b/src/proof/conv_proof_generator.h index 70e606db4..f23a661ae 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/proof/conv_proof_generator.h @@ -15,12 +15,12 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H -#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__CONV_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -174,7 +174,7 @@ class TConvProofGenerator : public ProofGenerator uint32_t tctx = 0); /** Has rewrite step for term t */ bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; - /** + /** * Get rewrite step for term t, returns the s provided in a call to * addRewriteStep if one exists, or null otherwise. */ @@ -253,4 +253,4 @@ class TConvProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__CONV_PROOF_GENERATOR_H */ diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp index 00e961628..65a7e462b 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/proof/conv_seq_proof_generator.cpp @@ -13,11 +13,11 @@ * Term conversion sequence proof generator utility. */ -#include "expr/tconv_seq_proof_generator.h" +#include "proof/conv_seq_proof_generator.h" #include <sstream> -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/tconv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h index bc067f60a..8d4417134 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/proof/conv_seq_proof_generator.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H -#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "theory/trust_node.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { @@ -86,7 +86,7 @@ class TConvSeqProofGenerator : public ProofGenerator * generator, or one of the component proof generators, if only one step * rewrote. In the former case, all steps are registered to this class. * Using a component generator is an optimization that saves having to - * save the conversion steps or use this class. For example, if we have 2 + * save the conversion steps or use this class. For example, if we have 2 * term conversion components, and call this method on: * { a, b, c } * then this method calls: @@ -118,4 +118,4 @@ class TConvSeqProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 4ba409d6d..ca85aadd3 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -17,9 +17,9 @@ #include <sstream> -#include "expr/proof_checker.h" -#include "expr/proof_node_manager.h" #include "printer/smt2/smt2_printer.h" +#include "proof/proof_checker.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" namespace cvc5 { diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 6e6785080..0027d145a 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -20,7 +20,7 @@ #include <iostream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { namespace proof { diff --git a/src/theory/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index c9a8823aa..34ff4fa75 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -13,11 +13,11 @@ * Implementation of the abstract proof generator class. */ -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { @@ -122,8 +122,9 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc, return mkTrustNode(pfs->getResult(), pfs, isConflict); } -TrustNode EagerProofGenerator::mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf) +TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, + Node b, + std::shared_ptr<ProofNode> pf) { if (pf == nullptr) { diff --git a/src/theory/eager_proof_generator.h b/src/proof/eager_proof_generator.h index c0b368e6e..ada48d893 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/proof/eager_proof_generator.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H -#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H +#define CVC5__PROOF__EAGER_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_rule.h" -#include "theory/trust_node.h" +#include "proof/proof_generator.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" namespace cvc5 { @@ -159,8 +159,7 @@ class EagerProofGenerator : public ProofGenerator * @return The trust node corresponding to the fact that this generator has * a proof of a = b */ - TrustNode mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf); + TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> pf); //--------------------------------------- common proofs /** * This returns the trust node corresponding to the splitting lemma @@ -195,4 +194,4 @@ class EagerProofGenerator : public ProofGenerator } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/expr/lazy_proof.cpp b/src/proof/lazy_proof.cpp index 8a54637fa..d7b62a8dc 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -13,11 +13,11 @@ * Implementation of lazy proof utility. */ -#include "expr/lazy_proof.h" +#include "proof/lazy_proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" using namespace cvc5::kind; @@ -178,8 +178,7 @@ void LazyCDProof::addLazyStep(Node expected, } } -ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, - bool& isSym) +ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym) { isSym = false; NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); diff --git a/src/expr/lazy_proof.h b/src/proof/lazy_proof.h index efcda94bd..b566e408e 100644 --- a/src/expr/lazy_proof.h +++ b/src/proof/lazy_proof.h @@ -15,10 +15,10 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__LAZY_PROOF_H -#define CVC5__EXPR__LAZY_PROOF_H +#ifndef CVC5__PROOF__LAZY_PROOF_H +#define CVC5__PROOF__LAZY_PROOF_H -#include "expr/proof.h" +#include "proof/proof.h" namespace cvc5 { @@ -107,4 +107,4 @@ class LazyCDProof : public CDProof } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_H */ diff --git a/src/expr/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp index 3ce2212be..4c1b19ffe 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/proof/lazy_proof_chain.cpp @@ -13,14 +13,14 @@ * Implementation of lazy proof utility. */ -#include "expr/lazy_proof_chain.h" +#include "proof/lazy_proof_chain.h" -#include "expr/proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h index 1abb3f84e..4315ee87a 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/proof/lazy_proof_chain.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H -#define CVC5__EXPR__LAZY_PROOF_CHAIN_H +#ifndef CVC5__PROOF__LAZY_PROOF_CHAIN_H +#define CVC5__PROOF__LAZY_PROOF_CHAIN_H #include <vector> #include "context/cdhashmap.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -151,4 +151,4 @@ class LazyCDProofChain : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_CHAIN_H */ diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp index 3fd3795c1..a50b9efd4 100644 --- a/src/theory/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -13,14 +13,14 @@ * Implementation of the lazy tree proof generator class. */ -#include "theory/lazy_tree_proof_generator.h" +#include "proof/lazy_tree_proof_generator.h" #include <iostream> #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/theory/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h index 7ab921a70..8b8d344e9 100644 --- a/src/theory/lazy_tree_proof_generator.h +++ b/src/proof/lazy_tree_proof_generator.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H -#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H +#define CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H #include <iostream> #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/expr/proof.cpp b/src/proof/proof.cpp index 289a5be5b..a100be990 100644 --- a/src/expr/proof.cpp +++ b/src/proof/proof.cpp @@ -13,11 +13,11 @@ * Implementation of proof. */ -#include "expr/proof.h" +#include "proof/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" using namespace cvc5::kind; diff --git a/src/expr/proof.h b/src/proof/proof.h index 496815938..2c57e0a2e 100644 --- a/src/expr/proof.h +++ b/src/proof/proof.h @@ -15,15 +15,15 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_H -#define CVC5__EXPR__PROOF_H +#ifndef CVC5__PROOF__PROOF_H +#define CVC5__PROOF__PROOF_H #include <vector> #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_step_buffer.h" +#include "proof/proof_generator.h" +#include "proof/proof_step_buffer.h" namespace cvc5 { @@ -275,4 +275,4 @@ class CDProof : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_MANAGER_H */ +#endif /* CVC5__PROOF__PROOF_MANAGER_H */ diff --git a/src/expr/proof_checker.cpp b/src/proof/proof_checker.cpp index 69f880ed5..7a2e5293e 100644 --- a/src/expr/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -13,11 +13,11 @@ * Implementation of proof checker. */ -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" -#include "expr/proof_node.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" +#include "proof/proof_node.h" #include "smt/smt_statistics_registry.h" using namespace cvc5::kind; @@ -78,7 +78,7 @@ Node ProofRuleChecker::mkKindNode(Kind k) ProofCheckerStatistics::ProofCheckerStatistics() : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>( - "ProofCheckerStatistics::ruleChecks")), + "ProofCheckerStatistics::ruleChecks")), d_totalRuleChecks(smtStatisticsRegistry().registerInt( "ProofCheckerStatistics::totalRuleChecks")) { diff --git a/src/expr/proof_checker.h b/src/proof/proof_checker.h index e778f687e..ac5531bf4 100644 --- a/src/expr/proof_checker.h +++ b/src/proof/proof_checker.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_CHECKER_H -#define CVC5__EXPR__PROOF_CHECKER_H +#ifndef CVC5__PROOF__PROOF_CHECKER_H +#define CVC5__PROOF__PROOF_CHECKER_H #include <map> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -203,4 +203,4 @@ class ProofChecker } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_CHECKER_H */ +#endif /* CVC5__PROOF__PROOF_CHECKER_H */ diff --git a/src/expr/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp index e89bd6692..774b25ef6 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/proof/proof_ensure_closed.cpp @@ -13,15 +13,15 @@ * Implementation of debug checks for ensuring proofs are closed. */ -#include "expr/proof_ensure_closed.h" +#include "proof/proof_ensure_closed.h" #include <sstream> -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "options/smt_options.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" namespace cvc5 { diff --git a/src/expr/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h index 3d126a4a1..cacfeeeed 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/proof/proof_ensure_closed.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H -#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H +#ifndef CVC5__PROOF__PROOF_ENSURE_CLOSED_H +#define CVC5__PROOF__PROOF_ENSURE_CLOSED_H #include "expr/node.h" @@ -70,4 +70,4 @@ void pfnEnsureClosedWrt(ProofNode* pn, const char* ctx); } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */ +#endif /* CVC5__PROOF__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.cpp b/src/proof/proof_generator.cpp index 7c034c10d..bbfde7986 100644 --- a/src/expr/proof_generator.cpp +++ b/src/proof/proof_generator.cpp @@ -13,14 +13,14 @@ * Implementation of proof generator utility. */ -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" #include <sstream> -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/smt_options.h" +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" namespace cvc5 { diff --git a/src/expr/proof_generator.h b/src/proof/proof_generator.h index 2e87ab756..a8fe43909 100644 --- a/src/expr/proof_generator.h +++ b/src/proof/proof_generator.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_GENERATOR_H -#define CVC5__EXPR__PROOF_GENERATOR_H +#ifndef CVC5__PROOF__PROOF_GENERATOR_H +#define CVC5__PROOF__PROOF_GENERATOR_H #include "expr/node.h" @@ -110,4 +110,4 @@ class ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node.cpp b/src/proof/proof_node.cpp index 92daad8ed..e3affb306 100644 --- a/src/expr/proof_node.cpp +++ b/src/proof/proof_node.cpp @@ -13,10 +13,10 @@ * Implementation of proof node utility. */ -#include "expr/proof_node.h" +#include "proof/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_to_sexpr.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_to_sexpr.h" namespace cvc5 { diff --git a/src/expr/proof_node.h b/src/proof/proof_node.h index f8d71f703..db82cc63d 100644 --- a/src/expr/proof_node.h +++ b/src/proof/proof_node.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_H -#define CVC5__EXPR__PROOF_NODE_H +#ifndef CVC5__PROOF__PROOF_NODE_H +#define CVC5__PROOF__PROOF_NODE_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -142,4 +142,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn); } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_H */ +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/expr/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp index 4bb35b5dc..82ccc034f 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/proof/proof_node_algorithm.cpp @@ -13,9 +13,9 @@ * Implementation of proof node algorithm utilities. */ -#include "expr/proof_node_algorithm.h" +#include "proof/proof_node_algorithm.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { namespace expr { diff --git a/src/expr/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h index 4c89dd4bc..1ccefb0a2 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/proof/proof_node_algorithm.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H -#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H +#ifndef CVC5__PROOF__PROOF_NODE_ALGORITHM_H +#define CVC5__PROOF__PROOF_NODE_ALGORITHM_H #include <vector> @@ -73,4 +73,4 @@ bool containsSubproof(ProofNode* pn, } // namespace expr } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */ +#endif /* CVC5__PROOF__PROOF_NODE_ALGORITHM_H */ diff --git a/src/expr/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index c2c72f35d..cf19eebdf 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -13,23 +13,22 @@ * Implementation of proof node manager. */ -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include <sstream> -#include "expr/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" #include "theory/rewriter.h" using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) - : d_checker(pc) +ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); } diff --git a/src/expr/proof_node_manager.h b/src/proof/proof_node_manager.h index 853d22de7..2fa7ed3e9 100644 --- a/src/expr/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H -#define CVC5__EXPR__PROOF_NODE_MANAGER_H +#ifndef CVC5__PROOF__PROOF_NODE_MANAGER_H +#define CVC5__PROOF__PROOF_NODE_MANAGER_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -203,4 +203,4 @@ class ProofNodeManager } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_H */ +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp index 033232959..85fc2395e 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/proof/proof_node_to_sexpr.cpp @@ -13,13 +13,13 @@ * Implementation of proof node to s-expression. */ -#include "expr/proof_node_to_sexpr.h" +#include "proof/proof_node_to_sexpr.h" #include <iostream> #include <sstream> -#include "expr/proof_node.h" #include "options/proof_options.h" +#include "proof/proof_node.h" using namespace cvc5::kind; diff --git a/src/expr/proof_node_to_sexpr.h b/src/proof/proof_node_to_sexpr.h index d4cca8eae..c358f3445 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/proof/proof_node_to_sexpr.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H -#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H +#ifndef CVC5__PROOF__PROOF_NODE_TO_SEXPR_H +#define CVC5__PROOF__PROOF_NODE_TO_SEXPR_H #include <map> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -67,4 +67,4 @@ class ProofNodeToSExpr } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_RULE_H */ +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/expr/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp index e2fd0c566..2bdb54a45 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/proof/proof_node_updater.cpp @@ -13,12 +13,12 @@ * Implementation of a utility for updating proof nodes. */ -#include "expr/proof_node_updater.h" +#include "proof/proof_node_updater.h" -#include "expr/lazy_proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" +#include "proof/lazy_proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/proof_node_updater.h b/src/proof/proof_node_updater.h index 215c61210..6b8841e67 100644 --- a/src/expr/proof_node_updater.h +++ b/src/proof/proof_node_updater.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H -#define CVC5__EXPR__PROOF_NODE_UPDATER_H +#ifndef CVC5__PROOF__PROOF_NODE_UPDATER_H +#define CVC5__PROOF__PROOF_NODE_UPDATER_H #include <map> #include <memory> #include "expr/node.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { diff --git a/src/expr/proof_rule.cpp b/src/proof/proof_rule.cpp index f4e8078dc..0cefe1209 100644 --- a/src/expr/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -13,7 +13,7 @@ * Implementation of proof rule. */ -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" #include <iostream> diff --git a/src/expr/proof_rule.h b/src/proof/proof_rule.h index 9771dda31..107285cc3 100644 --- a/src/expr/proof_rule.h +++ b/src/proof/proof_rule.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_RULE_H -#define CVC5__EXPR__PROOF_RULE_H +#ifndef CVC5__PROOF__PROOF_RULE_H +#define CVC5__PROOF__PROOF_RULE_H #include <iosfwd> @@ -1450,4 +1450,4 @@ struct PfRuleHashFunction } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_RULE_H */ +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/expr/proof_set.h b/src/proof/proof_set.h index 5ea9c1021..4015e0466 100644 --- a/src/expr/proof_set.h +++ b/src/proof/proof_set.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_SET_H -#define CVC5__EXPR__PROOF_SET_H +#ifndef CVC5__PROOF__PROOF_SET_H +#define CVC5__PROOF__PROOF_SET_H #include <memory> #include "context/cdlist.h" #include "context/context.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" namespace cvc5 { @@ -73,4 +73,4 @@ class CDProofSet } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp index 84cfc040c..309802505 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/proof/proof_step_buffer.cpp @@ -13,9 +13,9 @@ * Implementation of proof step and proof step buffer utilities. */ -#include "expr/proof_step_buffer.h" +#include "proof/proof_step_buffer.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" using namespace cvc5::kind; diff --git a/src/expr/proof_step_buffer.h b/src/proof/proof_step_buffer.h index b9350cf45..4c1bfa8a3 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/proof/proof_step_buffer.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H -#define CVC5__EXPR__PROOF_STEP_BUFFER_H +#ifndef CVC5__PROOF__PROOF_STEP_BUFFER_H +#define CVC5__PROOF__PROOF_STEP_BUFFER_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -95,4 +95,4 @@ class ProofStepBuffer } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */ +#endif /* CVC5__PROOF__PROOF_STEP_BUFFER_H */ diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp index 667c8d114..f00c664c8 100644 --- a/src/theory/theory_proof_step_buffer.cpp +++ b/src/proof/theory_proof_step_buffer.cpp @@ -13,9 +13,9 @@ * Implementation of theory proof step buffer utility. */ -#include "theory/theory_proof_step_buffer.h" +#include "proof/theory_proof_step_buffer.h" -#include "expr/proof.h" +#include "proof/proof.h" using namespace cvc5::kind; diff --git a/src/theory/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h index 1832ddb08..fc2e25e5a 100644 --- a/src/theory/theory_proof_step_buffer.h +++ b/src/proof/theory_proof_step_buffer.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H -#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H +#ifndef CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H +#define CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H #include <vector> #include "expr/node.h" -#include "expr/proof_step_buffer.h" +#include "proof/proof_step_buffer.h" #include "theory/builtin/proof_checker.h" namespace cvc5 { @@ -117,4 +117,4 @@ class TheoryProofStepBuffer : public ProofStepBuffer } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H */ +#endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */ diff --git a/src/theory/trust_node.cpp b/src/proof/trust_node.cpp index 4086d6e86..d99e6de51 100644 --- a/src/theory/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -13,10 +13,10 @@ * Implementation of the trust node utility. */ -#include "theory/trust_node.h" +#include "proof/trust_node.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_generator.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_generator.h" namespace cvc5 { namespace theory { diff --git a/src/theory/trust_node.h b/src/proof/trust_node.h index 0a4f20c34..200dececd 100644 --- a/src/theory/trust_node.h +++ b/src/proof/trust_node.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__TRUST_NODE_H -#define CVC5__THEORY__TRUST_NODE_H +#ifndef CVC5__PROOF__TRUST_NODE_H +#define CVC5__PROOF__TRUST_NODE_H #include "expr/node.h" @@ -75,8 +75,8 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk); * provided, is capable of proving the given conflict or lemma, or an assertion * failure occurs. Otherwise an assertion error is given. * - * While this is not enforced, a `TrustNode` generally encapsulates a **closed** proof - * of the formula: one without free assumptions. + * While this is not enforced, a `TrustNode` generally encapsulates a **closed** + * proof of the formula: one without free assumptions. */ class TrustNode { @@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& out, TrustNode n); } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__TRUST_NODE_H */ +#endif /* CVC5__PROOF__TRUST_NODE_H */ 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 { diff --git a/src/smt/env.cpp b/src/smt/env.cpp index f9e2a8458..647981ab3 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -18,9 +18,9 @@ #include "context/context.h" #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" #include "options/base_options.h" #include "printer/printer.h" +#include "proof/conv_proof_generator.h" #include "smt/dump_manager.h" #include "smt/smt_engine_stats.h" #include "theory/rewriter.h" diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 91287e5f9..293c46906 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -19,8 +19,8 @@ #include <utility> #include "expr/node_manager_attributes.h" -#include "expr/term_conversion_proof_generator.h" #include "preprocessing/assertion_pipeline.h" +#include "proof/conv_proof_generator.h" #include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 801622e27..ba89a1063 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -21,7 +21,7 @@ #include <unordered_map> #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 3ae03e58f..3f657db63 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -18,10 +18,10 @@ #include <sstream> -#include "expr/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 140a7c91a..347f4af3b 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -19,11 +19,11 @@ #define CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/lazy_proof.h" -#include "expr/proof.h" -#include "expr/proof_set.h" -#include "expr/proof_generator.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_set.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 0968aa1f9..ad1e40c77 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -15,13 +15,13 @@ #include "smt/proof_manager.h" -#include "expr/proof_checker.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" #include "options/smt_options.h" #include "proof/dot/dot_printer.h" +#include "proof/proof_checker.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" #include "smt/assertions.h" #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index f98d1d727..62e18c3b2 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -15,11 +15,11 @@ #include "smt/proof_post_processor.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" +#include "proof/proof_node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/builtin/proof_checker.h" diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 72fa3581d..f9e93fa91 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -22,7 +22,7 @@ #include <sstream> #include <unordered_set> -#include "expr/proof_node_updater.h" +#include "proof/proof_node_updater.h" #include "smt/witness_form.h" #include "util/statistics_stats.h" diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index eaf5cf82f..3bb998688 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -17,12 +17,12 @@ #include <vector> #include "expr/attribute.h" -#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/term_context_stack.h" -#include "expr/term_conversion_proof_generator.h" #include "options/smt_options.h" +#include "proof/conv_proof_generator.h" +#include "proof/lazy_proof.h" using namespace std; diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 6a3a1c019..c2b1f27f3 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -24,7 +24,7 @@ #include "context/context.h" #include "expr/node.h" #include "expr/term_context.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" #include "util/hash.h" namespace cvc5 { diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index df8f2f9d9..ba2c07326 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -15,7 +15,7 @@ #include "unsat_core_manager.h" -#include "expr/proof_node_algorithm.h" +#include "proof/proof_node_algorithm.h" #include "smt/assertions.h" namespace cvc5 { diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index dcd246f2e..e064b83a7 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -20,7 +20,7 @@ #include "context/cdlist.h" #include "expr/node.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 980cbcadb..8522d41f0 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -20,9 +20,9 @@ #include <unordered_set> -#include "expr/proof.h" -#include "expr/proof_generator.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" namespace cvc5 { namespace smt { diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index f343ce56a..33860d2d9 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -25,12 +25,12 @@ #include "base/cvc5config.h" #include "base/output.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" -#include "theory/eager_proof_generator.h" #ifdef CVC5_USE_GLPK #include "theory/arith/partial_model.h" diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 2edc7b210..0c0a4959d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -18,8 +18,8 @@ #include "theory/arith/callbacks.h" -#include "expr/proof_node.h" #include "expr/skolem_manager.h" +#include "proof/proof_node.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 3d5e7270b..96272f939 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -19,8 +19,9 @@ #include "theory/arith/congruence_manager.h" #include "base/output.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "options/arith_options.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/constraint.h" @@ -29,7 +30,6 @@ #include "theory/rewriter.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" -#include "options/arith_options.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index e45b7bf29..8ada48cfe 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,11 +24,11 @@ #include "context/cdlist.h" #include "context/cdmaybe.h" #include "context/cdtrail_queue.h" +#include "proof/trust_node.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" #include "util/statistics_stats.h" diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 15dfe4791..d8fc1c578 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -22,16 +22,15 @@ #include <unordered_set> #include "base/output.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" -#include "theory/eager_proof_generator.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/rewriter.h" - using namespace std; using namespace cvc5::kind; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 0d3c96f89..fce071e6e 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -86,12 +86,12 @@ #include "context/cdlist.h" #include "context/cdqueue.h" #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { 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" diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index f39be2c59..7b4e920fb 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -19,8 +19,8 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" -#include "expr/term_conversion_proof_generator.h" #include "options/arith_options.h" +#include "proof/conv_proof_generator.h" #include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 829601827..27a3d293e 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -19,7 +19,7 @@ #include "expr/node.h" #include "expr/skolem_manager.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 402656154..8fa9f21c1 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARITH__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/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1843ddb8a..5c4678cb4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -15,9 +15,9 @@ #include "theory/arith/theory_arith.h" -#include "expr/proof_checker.h" -#include "expr/proof_rule.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" +#include "proof/proof_rule.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/infer_bounds.h" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 911954a5a..d12553e90 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,13 +33,13 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_rule.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "preprocessing/util/ite_utilities.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_rule.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e029e3c41..e3094ae88 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "proof/trust_node.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" @@ -47,7 +48,6 @@ #include "theory/arith/proof_checker.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 93feb0a53..9b219c9b7 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H #include "expr/node.h" -#include "expr/proof_rule.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_rule.h" #include "theory/theory_inference_manager.h" namespace cvc5 { diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index 9064dbfca..0b7bef163 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARRAYS__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/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9b5676d65..0bdccfd17 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -20,9 +20,9 @@ #include "expr/kind.h" #include "expr/node_algorithm.h" -#include "expr/proof_checker.h" #include "options/arrays_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/arrays/skolem_cache.h" diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index d5917f91c..c2aa9eb1e 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -15,7 +15,7 @@ #include "theory/bags/theory_bags.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "theory/bags/normal_form.h" #include "theory/rewriter.h" diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 7920f5b7f..2fa2890c2 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -20,10 +20,10 @@ #include <vector> #include "expr/node_algorithm.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" -#include "theory/eager_proof_generator.h" #include "theory/theory.h" #include "util/hash.h" #include "util/utility.h" diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 1d4f6e9ee..74e1a7cd8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -26,9 +26,9 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" -#include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof_chain.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index 47a1ce633..114ab2e9b 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__BOOLEANS__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/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index d1f8bb854..f7e788e9a 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -17,8 +17,8 @@ #include <sstream> -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index 624a17f2f..0bed57078 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -21,7 +21,7 @@ #include <memory> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index bac2be70c..3aac5ecfb 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,7 +18,7 @@ #include <stack> #include <vector> -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index dd6bf82e7..892fc7a4b 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BUILTIN__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" #include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index c5bd77e36..80c5dba3d 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -16,7 +16,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 6082a7128..a55adaace 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -16,8 +16,8 @@ #include <unordered_set> -#include "expr/term_conversion_proof_generator.h" #include "options/proof_options.h" +#include "proof/conv_proof_generator.h" #include "theory/theory_model.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 3da08f868..31d9443c8 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -21,12 +21,12 @@ #include <unordered_map> #include "context/cdqueue.h" +#include "proof/eager_proof_generator.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" -#include "theory/eager_proof_generator.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 3faad29a9..a16bf7eb8 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -15,7 +15,7 @@ #include "theory/bv/bv_solver_simple.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h index 674678ff8..c89dd359c 100644 --- a/src/theory/bv/proof_checker.h +++ b/src/theory/bv/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BV__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" #include "theory/bv/bitblast/simple_bitblaster.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c5ab08f0c..22b05b026 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -15,9 +15,9 @@ #include "theory/bv/theory_bv.h" -#include "expr/proof_checker.h" #include "options/bv_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_lazy.h" diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 33300ead8..2b35fb97d 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -16,8 +16,8 @@ #include "theory/combination_engine.h" #include "expr/node_visitor.h" +#include "proof/eager_proof_generator.h" #include "theory/care_graph.h" -#include "theory/eager_proof_generator.h" #include "theory/ee_manager_distributed.h" #include "theory/model_manager.h" #include "theory/model_manager_distributed.h" diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 5ab8a563f..19f396a56 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -15,8 +15,8 @@ #include "theory/datatypes/infer_proof_cons.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index f8e7eea09..6c1663a09 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" #include "theory/datatypes/inference.h" namespace cvc5 { diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index db1d2b4b0..2dac0d7aa 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -19,9 +19,9 @@ #define CVC5__THEORY__DATATYPES__INFERENCE_H #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/theory_inference.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 393813590..014255a7c 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -17,8 +17,8 @@ #include "expr/dtype.h" #include "options/datatypes_options.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" -#include "theory/eager_proof_generator.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_state.h" diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index 76fcee411..5949441d8 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__DATATYPES__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/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f9d08dfc2..dc57e4165 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -21,12 +21,12 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" diff --git a/src/theory/fp/fp_expand_defs.h b/src/theory/fp/fp_expand_defs.h index a9edc8b02..8240f1f8e 100644 --- a/src/theory/fp/fp_expand_defs.h +++ b/src/theory/fp/fp_expand_defs.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 8e802f875..b681dad17 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -18,8 +18,8 @@ #ifndef CVC5__THEORY__OUTPUT_CHANNEL_H #define CVC5__THEORY__OUTPUT_CHANNEL_H +#include "proof/trust_node.h" #include "theory/incomplete_id.h" -#include "theory/trust_node.h" #include "util/resource_manager.h" namespace cvc5 { 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" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 1094d5920..eeb2f166d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -15,8 +15,8 @@ #include "theory/rewriter.h" -#include "expr/term_conversion_proof_generator.h" #include "options/theory_options.h" +#include "proof/conv_proof_generator.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 87f25341e..f88596ffe 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -22,7 +22,7 @@ #include <vector> #include "context/cdhashmap.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/sets/inference_manager.h" #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 40f6080e5..b684ff56f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" #include "theory/ee_setup_info.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" #include "util/statistics_stats.h" diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index 2cb1c6738..277daf88c 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__SKOLEM_LEMMA_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { 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" diff --git a/src/theory/theory.h b/src/theory/theory.h index 8f69d4cb2..d71348ce3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,12 +28,12 @@ #include "context/context.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_stats.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index abbca451a..676351dd5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -20,15 +20,15 @@ #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" -#include "expr/lazy_proof.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" -#include "expr/proof_checker.h" -#include "expr/proof_ensure_closed.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" +#include "proof/lazy_proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_ensure_closed.h" #include "prop/prop_engine.h" #include "smt/dump.h" #include "smt/env.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6887959ed..ffcaf392f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -25,6 +25,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/atom_requests.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" @@ -32,7 +33,6 @@ #include "theory/sort_inference.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" -#include "theory/trust_node.h" #include "theory/trust_substitutions.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 609d7ae8a..f10716bd9 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -17,7 +17,7 @@ #include <sstream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" using namespace cvc5::kind; diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 48969aa21..ab0f616fe 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 2cb7d9d30..06806f8d4 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/output_channel.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 65bd160fc..230c23424 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -15,8 +15,8 @@ #include "theory/theory_preprocessor.h" -#include "expr/lazy_proof.h" #include "expr/skolem_manager.h" +#include "proof/lazy_proof.h" #include "smt/logic_exception.h" #include "theory/logic_info.h" #include "theory/rewriter.h" diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 58dd763e0..6015f2b07 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -22,13 +22,13 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/tconv_seq_proof_generator.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/conv_seq_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/trust_node.h" #include "smt/term_formula_removal.h" #include "theory/skolem_lemma.h" -#include "theory/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index 031e32db4..eca1e4e56 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -21,7 +21,7 @@ #define CVC5__THEORY__THEORY_REWRITER_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 136992fbe..2a6997d1d 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -21,14 +21,14 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_set.h" -#include "expr/term_conversion_proof_generator.h" -#include "theory/eager_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_set.h" +#include "proof/theory_proof_step_buffer.h" +#include "proof/trust_node.h" #include "theory/substitutions.h" -#include "theory/theory_proof_step_buffer.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index c63f8b51d..fbed7ffb5 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -16,9 +16,9 @@ #include "theory/uf/eq_proof.h" #include "base/configuration.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" #include "options/uf_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h index 55f7db3ba..caeda828e 100644 --- a/src/theory/uf/proof_checker.h +++ b/src/theory/uf/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__UF__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/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index ab36cd9df..b4522d9df 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -15,9 +15,9 @@ #include "theory/uf/proof_equality_engine.h" -#include "expr/lazy_proof_chain.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/lazy_proof_chain.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 4ca13d93f..0c093d4b2 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" -#include "expr/buffered_proof_generator.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "theory/eager_proof_generator.h" +#include "proof/buffered_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" namespace cvc5 { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9cf47bab3..1afb8cc31 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -21,11 +21,11 @@ #include <sstream> #include "expr/node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 1aed7ce3f..a81deabc2 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -19,8 +19,8 @@ #include "expr/dtype_cons.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "expr/proof_checker.h" #include "expr/skolem_manager.h" +#include "proof/proof_checker.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index 7fdf44298..669857e96 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -20,8 +20,8 @@ #include <string> #include <thread> -#include "expr/proof_rule.h" #include "lib/clock_gettime.h" +#include "proof/proof_rule.h" #include "test.h" #include "util/statistics_registry.h" #include "util/statistics_stats.h" |