diff options
Diffstat (limited to 'src/preprocessing')
78 files changed, 201 insertions, 201 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index ab3e950b9..92027a303 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -23,7 +23,7 @@ #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { AssertionPipeline::AssertionPipeline() @@ -212,4 +212,4 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) } } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 454606315..aa4ffbca2 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; namespace smt { @@ -198,6 +198,6 @@ class AssertionPipeline }; /* class AssertionPipeline */ } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index a67861664..a19994ad9 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -32,10 +32,10 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -using namespace CVC5; -using namespace CVC5::theory; +using namespace cvc5; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -336,4 +336,4 @@ PreprocessingPassResult Ackermann::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index e177b4270..14f8f713f 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -33,7 +33,7 @@ #include "theory/logic_info.h" #include "theory/substitutions.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -82,6 +82,6 @@ class Ackermann : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */ diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 16f06540e..12f3375b0 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -23,7 +23,7 @@ #include "theory/rewriter.h" #include "theory/substitutions.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -63,4 +63,4 @@ PreprocessingPassResult ApplySubsts::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index 6345f35dd..d94943dc3 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -22,7 +22,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { class PreprocessingPassContext; @@ -46,6 +46,6 @@ class ApplySubsts : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 042bc3e01..df8e93bc7 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -26,10 +26,10 @@ #include "theory/rewriter.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics() @@ -422,4 +422,4 @@ BoolToBV::Statistics::~Statistics() } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 885c57302..1245dbd34 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -23,7 +23,7 @@ #include "preprocessing/preprocessing_pass.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -121,6 +121,6 @@ class BoolToBV : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index 045b4295b..b7a9e9c69 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -32,11 +32,11 @@ #include "theory/rewriter.h" #include "theory/theory_engine.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; BvAbstraction::BvAbstraction(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-abstraction"){}; @@ -60,4 +60,4 @@ PreprocessingPassResult BvAbstraction::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index b16a2f973..d699b288f 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -28,7 +28,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -44,6 +44,6 @@ class BvAbstraction : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index 15b7662c4..54f967bfc 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -22,7 +22,7 @@ #include "theory/theory_engine.h" #include "theory/theory_model.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -47,4 +47,4 @@ PreprocessingPassResult BvEagerAtoms::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index a3c7a424a..e0b53ad1b 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -22,7 +22,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -38,6 +38,6 @@ class BvEagerAtoms : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 2ec12256a..7bd0e7715 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -28,11 +28,11 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -using namespace CVC5; -using namespace CVC5::theory; -using namespace CVC5::theory::bv; +using namespace cvc5; +using namespace cvc5::theory; +using namespace cvc5::theory::bv; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -704,7 +704,7 @@ PreprocessingPassResult BVGauss::applyInternal( { Node a = assertions.back(); assertions.pop_back(); - CVC5::Kind k = a.getKind(); + cvc5::Kind k = a.getKind(); if (k == kind::AND) { @@ -800,4 +800,4 @@ PreprocessingPassResult BVGauss::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index d06071867..e75b41868 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -104,6 +104,6 @@ class BVGauss : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index c611c8af3..fb6a123dd 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -25,12 +25,12 @@ #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; -using namespace CVC5::theory; +using namespace cvc5::theory; namespace { @@ -103,4 +103,4 @@ PreprocessingPassResult BvIntroPow2::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 98e1efc1d..c51383d2c 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -23,7 +23,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class BvIntroPow2 : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 5153f3b7f..9f219e7a4 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -30,12 +30,12 @@ #include "theory/rewriter.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; BVToBool::BVToBool(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-bool"), @@ -310,4 +310,4 @@ BVToBool::Statistics::~Statistics() } // passes } // Preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 45fa4a5df..b6b847140 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -23,7 +23,7 @@ #include "preprocessing/preprocessing_pass.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -73,6 +73,6 @@ class BVToBool : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index f7a87d51f..510d35419 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -33,13 +33,13 @@ #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; -using namespace CVC5::theory::bv; +using namespace cvc5::theory; +using namespace cvc5::theory::bv; namespace { @@ -1046,4 +1046,4 @@ Node BVToInt::createBVNotNode(Node n, uint64_t bvsize) } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index bc949bff2..c0d96d462 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -73,7 +73,7 @@ #include "preprocessing/preprocessing_pass.h" #include "theory/arith/nl/iand_utils.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -285,6 +285,6 @@ class BVToInt : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */ diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 245c889d3..38519e96b 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "theory/quantifiers/extended_rewrite.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -43,4 +43,4 @@ PreprocessingPassResult ExtRewPre::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index 60ab6af98..8fabecbaa 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class ExtRewPre : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index c1a995469..307be46bf 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -22,11 +22,11 @@ #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "foreign-theory-rewrite"), d_cache(preprocContext->getUserContext()){}; @@ -149,4 +149,4 @@ PreprocessingPassResult ForeignTheoryRewrite::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index e50909617..eb228ca67 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.h +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -62,6 +62,6 @@ class ForeignTheoryRewrite : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */ diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index b34df8ca3..c6ea0ee27 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -26,11 +26,11 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::theory; -using namespace CVC5::theory::quantifiers; +using namespace cvc5::kind; +using namespace cvc5::theory; +using namespace cvc5::theory::quantifiers; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -466,4 +466,4 @@ void FunDefFmf::getConstraints(Node n, } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h index 194c520ab..cb461d6e9 100644 --- a/src/preprocessing/passes/fun_def_fmf.h +++ b/src/preprocessing/passes/fun_def_fmf.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -100,6 +100,6 @@ class FunDefFmf : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 60f584225..5cb5663c3 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -21,10 +21,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::theory; +using namespace cvc5::kind; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -124,4 +124,4 @@ PreprocessingPassResult GlobalNegate::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 2e9dbdcb7..263fa636b 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -29,7 +29,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -48,6 +48,6 @@ class GlobalNegate : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 13a59a92d..1bf980c49 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -24,9 +24,9 @@ #include "theory/rewriter.h" #include "theory/uf/theory_uf_rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -539,4 +539,4 @@ TypeNode HoElim::getUSort(TypeNode tn) } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 36aa53acf..ba23a1973 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -150,6 +150,6 @@ class HoElim : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */ diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index bf59a7311..b1f8ad771 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -29,12 +29,12 @@ #include "theory/rewriter.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; @@ -267,4 +267,4 @@ PreprocessingPassResult IntToBV::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index a6eda934f..da9d54229 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -23,7 +23,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class IntToBV : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 91b805004..cae898a7a 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -25,11 +25,11 @@ #include "theory/rewriter.h" #include "theory/theory_preprocessor.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; // TODO (project #42): note this preprocessing pass is deprecated IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext) @@ -79,4 +79,4 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index ceb9af4ac..4c4923647 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -22,7 +22,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class IteRemoval : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 8b9ad9587..0ad4f1abc 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -26,10 +26,10 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC5; -using namespace CVC5::theory; +using namespace cvc5; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -97,7 +97,7 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess, assertionsToPreprocess->resize(before); size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1; intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]); - Node newLast = CVC5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); + Node newLast = cvc5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); assertionsToPreprocess->replace(lastBeforeItes, newLast); Assert(assertionsToPreprocess->size() == before); } @@ -262,4 +262,4 @@ PreprocessingPassResult ITESimp::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index e5ab27620..abb3ec6f5 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -21,7 +21,7 @@ #include "preprocessing/util/ite_utilities.h" #include "util/stats_histogram.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -52,6 +52,6 @@ class ITESimp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index a810d3e19..7c246c3e1 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -30,12 +30,12 @@ #include "theory/theory_model.h" #include "theory/trust_substitutions.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; namespace { @@ -667,4 +667,4 @@ MipLibTrick::Statistics::~Statistics() } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 61bf40040..cad786c6b 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -57,6 +57,6 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index 3bc8ff8dd..838a2a767 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -19,12 +19,12 @@ #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; Node NlExtPurify::purifyNlTerms(TNode n, NodeMap& cache, @@ -140,4 +140,4 @@ PreprocessingPassResult NlExtPurify::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index c9b5c344c..2718639d6 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -51,6 +51,6 @@ class NlExtPurify : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 29e7233c0..e5b0cd39b 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -30,10 +30,10 @@ #include "theory/theory_model.h" #include "theory/trust_substitutions.h" -using namespace CVC5; -using namespace CVC5::theory; +using namespace cvc5; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -491,4 +491,4 @@ Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn) } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index dfaa24a93..679a6216d 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -22,7 +22,7 @@ #include "preprocessing/preprocessing_pass.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { class LazyCDProof; class ProofNodeManager; @@ -97,6 +97,6 @@ class NonClausalSimp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 5ce7338f3..510281bee 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -24,12 +24,12 @@ #include "theory/arith/normal_form.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; -using namespace CVC5::theory::arith; +using namespace cvc5::theory; +using namespace cvc5::theory::arith; PseudoBooleanProcessor::PseudoBooleanProcessor( PreprocessingPassContext* preprocContext) @@ -418,4 +418,4 @@ void PseudoBooleanProcessor::clear() } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 6e1b426bf..47a1eb7dc 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -31,7 +31,7 @@ #include "util/maybe.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -110,6 +110,6 @@ class PseudoBooleanProcessor : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index b296f9c17..8251183dd 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -35,11 +35,11 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC5::theory; -using namespace CVC5::theory::quantifiers; -using namespace CVC5::kind; +using namespace cvc5::theory; +using namespace cvc5::theory::quantifiers; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -568,4 +568,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } // passes } // preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 51b3c7951..4b5b21a5d 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -91,6 +91,6 @@ class QuantifierMacros : public PreprocessingPass } // passes } // preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 15f0fc54b..92b2c8aae 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -24,12 +24,12 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "quantifiers-preprocess"){}; @@ -58,4 +58,4 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index b9ea842cb..6aa5c58f0 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -24,7 +24,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -40,6 +40,6 @@ class QuantifiersPreprocess : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index bc8ba0b79..c80d55d3d 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -24,12 +24,12 @@ #include "theory/rewriter.h" #include "theory/theory_model.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq) { @@ -213,4 +213,4 @@ PreprocessingPassResult RealToInt::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index 5579e3faf..d961f10f2 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -45,6 +45,6 @@ class RealToInt : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index 35c2e9926..e5ff22d4f 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -19,11 +19,11 @@ #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; Rewrite::Rewrite(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "rewrite"){}; @@ -42,4 +42,4 @@ PreprocessingPassResult Rewrite::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 4848c8a98..50443c2c6 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -37,7 +37,7 @@ class Rewrite : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */ diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 6100e0762..8c130768d 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -25,12 +25,12 @@ #include "theory/rewriter.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; namespace { @@ -124,4 +124,4 @@ PreprocessingPassResult SepSkolemEmp::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 11e7bec24..a5b4120cb 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -20,7 +20,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -36,6 +36,6 @@ class SepSkolemEmp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 07c5e7cc5..cb8818f96 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -91,4 +91,4 @@ PreprocessingPassResult SortInferencePass::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index 5874b4363..167697206 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -17,7 +17,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -38,6 +38,6 @@ class SortInferencePass : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 1cc2ce06f..028322c1e 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -23,7 +23,7 @@ #include "theory/rewriter.h" #include "theory/theory_engine.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -57,4 +57,4 @@ PreprocessingPassResult StaticLearning::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index 67bf053f9..8f83e60b5 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -20,7 +20,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -36,6 +36,6 @@ class StaticLearning : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 775a09441..ea12010b0 100644 --- a/src/preprocessing/passes/strings_eager_pp.cpp +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -18,9 +18,9 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_preprocess.h" -using namespace CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -57,4 +57,4 @@ PreprocessingPassResult StringsEagerPp::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index 3af59766c..b4058a659 100644 --- a/src/preprocessing/passes/strings_eager_pp.h +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -19,7 +19,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class StringsEagerPp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */ diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index f05afe54f..a0d4ed91e 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -27,10 +27,10 @@ #include "theory/smt_engine_subsolver.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::theory; +using namespace cvc5::kind; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -345,4 +345,4 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index b31e5ca7c..094788adc 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -20,7 +20,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -63,6 +63,6 @@ class SygusInference : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 7213dc8a8..b2333b30e 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -30,9 +30,9 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -474,4 +474,4 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index eb52688e7..016395029 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -18,7 +18,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -71,6 +71,6 @@ class SynthRewRulesPass : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 7112dd50f..8e79a7b09 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -24,11 +24,11 @@ #include "theory/rewriter.h" #include "theory/theory_engine.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { -using namespace CVC5::theory; +using namespace cvc5::theory; TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "theory-preprocess"){}; @@ -72,4 +72,4 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index bd450840e..cc74792d1 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class TheoryPreprocess : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index c70458b91..c5a73f89b 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -18,9 +18,9 @@ #include "preprocessing/preprocessing_pass_context.h" #include "theory/theory_engine.h" -using namespace CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -116,4 +116,4 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index 626efe8e3..f6651d39c 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { @@ -51,6 +51,6 @@ class TheoryRewriteEq : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */ diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 502889dd3..9a9aaa366 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -26,12 +26,12 @@ #include "theory/logic_info.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC5::theory; +using namespace cvc5::theory; UnconstrainedSimplifier::UnconstrainedSimplifier( PreprocessingPassContext* preprocContext) @@ -880,4 +880,4 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index da368de51..5416abf51 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -29,7 +29,7 @@ #include "theory/substitutions.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; } @@ -72,6 +72,6 @@ class UnconstrainedSimplifier : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 127b22758..f9effecba 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -24,7 +24,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { PreprocessingPassResult PreprocessingPass::apply( @@ -70,4 +70,4 @@ PreprocessingPass::~PreprocessingPass() { } } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index f112d5f54..7f65129f8 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -36,7 +36,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { class AssertionPipeline; @@ -81,6 +81,6 @@ class PreprocessingPass { }; } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */ diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 3c64ce301..fdcbbb466 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -18,7 +18,7 @@ #include "expr/node_algorithm.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( @@ -61,4 +61,4 @@ ProofNodeManager* PreprocessingPassContext::getProofNodeManager() } } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 93563e3a2..17f049748 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -26,7 +26,7 @@ #include "theory/trust_substitutions.h" #include "util/resource_manager.h" -namespace CVC5 { +namespace cvc5 { class SmtEngine; class TheoryEngine; namespace theory::booleans { @@ -106,6 +106,6 @@ class PreprocessingPassContext }; // class PreprocessingPassContext } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index a46ce0205..b9434e63f 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -59,10 +59,10 @@ #include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { -using namespace CVC5::preprocessing::passes; +using namespace cvc5::preprocessing::passes; PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance() { @@ -158,4 +158,4 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() } } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index 4843b810b..bd9e724da 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -23,7 +23,7 @@ #include <string> #include <unordered_map> -namespace CVC5 { +namespace cvc5 { namespace preprocessing { class PreprocessingPass; @@ -94,6 +94,6 @@ class PreprocessingPassRegistry { }; // class PreprocessingPassRegistry } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */ diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 2b215f9b4..a3ad701a8 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -28,7 +28,7 @@ #include "theory/theory.h" using namespace std; -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace util { @@ -1909,4 +1909,4 @@ ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew( } // namespace util } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index ff58bbacf..059bac45c 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -31,7 +31,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { class AssertionPipeline; @@ -417,6 +417,6 @@ class ITECareSimplifier } // namespace util } // namespace preprocessing -} // namespace CVC5 +} // namespace cvc5 #endif |