diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/preprocessing/passes | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/preprocessing/passes')
68 files changed, 182 insertions, 184 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 198ce6f1f..a67861664 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 CVC4; -using namespace CVC4::theory; +using namespace CVC5; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -336,4 +336,4 @@ PreprocessingPassResult Ackermann::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index f74d8cb27..e177b4270 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -82,6 +82,6 @@ class Ackermann : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 f706ea7e3..16f06540e 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -63,4 +63,4 @@ PreprocessingPassResult ApplySubsts::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index 7f206387f..6345f35dd 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 CVC4 { +namespace CVC5 { namespace preprocessing { class PreprocessingPassContext; @@ -46,6 +46,6 @@ class ApplySubsts : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 62c747bc3..042bc3e01 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 357acd374..885c57302 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -121,6 +121,6 @@ class BoolToBV : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 539cc3b36..045b4295b 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index 3e04aa6e1..b16a2f973 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -44,6 +44,6 @@ class BvAbstraction : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 2158a7299..15b7662c4 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -47,4 +47,4 @@ PreprocessingPassResult BvEagerAtoms::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 6fe17115e..a3c7a424a 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -38,6 +38,6 @@ class BvEagerAtoms : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 e1e4b20a2..2ec12256a 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 CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; +using namespace CVC5; +using namespace CVC5::theory; +using namespace CVC5::theory::bv; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -704,7 +704,7 @@ PreprocessingPassResult BVGauss::applyInternal( { Node a = assertions.back(); assertions.pop_back(); - CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index c677a0f87..d06071867 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -104,6 +104,6 @@ class BVGauss : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index 08fe0cbc9..c611c8af3 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; -using namespace CVC4::theory; +using namespace CVC5::theory; namespace { @@ -100,8 +100,7 @@ PreprocessingPassResult BvIntroPow2::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } +} // namespace passes +} // namespace preprocessing -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 870eacf04..98e1efc1d 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class BvIntroPow2 : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 014ddc170..5153f3b7f 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; +using namespace CVC5::theory; BVToBool::BVToBool(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-bool"), @@ -310,4 +310,4 @@ BVToBool::Statistics::~Statistics() } // passes } // Preprocessing -} // CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 17d02c82a..45fa4a5df 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -73,6 +73,6 @@ class BVToBool : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 f5e81bb9c..f7a87d51f 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index 21587a6b4..bc949bff2 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -285,6 +285,6 @@ class BVToInt : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 78898a3dc..245c889d3 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -43,4 +43,4 @@ PreprocessingPassResult ExtRewPre::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index 0b921ad46..60ab6af98 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class ExtRewPre : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 b4e6107cc..c1a995469 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index c693a1192..e50909617 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -62,6 +62,6 @@ class ForeignTheoryRewrite : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 312437c38..b34df8ca3 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 CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; +using namespace CVC5::kind; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -466,4 +466,4 @@ void FunDefFmf::getConstraints(Node n, } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h index 90f3829f6..194c520ab 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -100,6 +100,6 @@ class FunDefFmf : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 364e44e09..60f584225 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 CVC4::kind; -using namespace CVC4::theory; +using namespace CVC5::kind; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -124,4 +124,4 @@ PreprocessingPassResult GlobalNegate::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 857664838..2e9dbdcb7 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -48,6 +48,6 @@ class GlobalNegate : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 284fbc72b..13a59a92d 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -539,4 +539,4 @@ TypeNode HoElim::getUSort(TypeNode tn) } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index d7a0de599..36aa53acf 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -150,6 +150,6 @@ class HoElim : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 e857b7b61..bf59a7311 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 774d8cb46..a6eda934f 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class IntToBV : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 afa1d3ba2..91b805004 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 3881eab2d..ceb9af4ac 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class IteRemoval : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 e298b39e2..8b9ad9587 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 CVC4; -using namespace CVC4::theory; +using namespace CVC5; +using namespace CVC5::theory; -namespace CVC4 { +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 = CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 110ce6057..e5ab27620 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -52,6 +52,6 @@ class ITESimp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f6ae77bc2..a810d3e19 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; +using namespace CVC5::theory; namespace { @@ -667,4 +667,4 @@ MipLibTrick::Statistics::~Statistics() } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 66622d06a..61bf40040 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -57,6 +57,6 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 1f85f0caf..3bc8ff8dd 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; +using namespace CVC5::theory; Node NlExtPurify::purifyNlTerms(TNode n, NodeMap& cache, @@ -140,4 +140,4 @@ PreprocessingPassResult NlExtPurify::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index c49336308..c9b5c344c 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -51,6 +51,6 @@ class NlExtPurify : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 b03d21dd9..29e7233c0 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 CVC4; -using namespace CVC4::theory; +using namespace CVC5; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -491,4 +491,4 @@ Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn) } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 27fac3f60..dfaa24a93 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 CVC4 { +namespace CVC5 { class LazyCDProof; class ProofNodeManager; @@ -97,6 +97,6 @@ class NonClausalSimp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index bc410a70a..5ce7338f3 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::theory; -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 84f7f7f31..6e1b426bf 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -110,6 +110,6 @@ class PseudoBooleanProcessor : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 f0b51e6a5..b296f9c17 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 CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -568,4 +568,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } // passes } // preprocessing -} // CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 3d6a56396..51b3c7951 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -91,6 +91,6 @@ class QuantifierMacros : public PreprocessingPass } // passes } // preprocessing -} // CVC4 +} // 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 af1eb5071..15f0fc54b 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 1c0125217..b9ea842cb 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -40,6 +40,6 @@ class QuantifiersPreprocess : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 9c58250e3..bc8ba0b79 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index 7bfdfd428..5579e3faf 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -45,6 +45,6 @@ class RealToInt : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 f1a4ec283..35c2e9926 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -19,12 +19,11 @@ #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::theory; - +using namespace CVC5::theory; Rewrite::Rewrite(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "rewrite"){}; @@ -43,4 +42,4 @@ PreprocessingPassResult Rewrite::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 22400911f..4848c8a98 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -21,7 +21,7 @@ #include "preprocessing/preprocessing_pass.h" -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -37,7 +37,7 @@ class Rewrite : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 381282b38..6100e0762 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; +using namespace CVC5::theory; namespace { @@ -124,4 +124,4 @@ PreprocessingPassResult SepSkolemEmp::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 51e421505..11e7bec24 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -36,6 +36,6 @@ class SepSkolemEmp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 6e399bcca..07c5e7cc5 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -91,4 +91,4 @@ PreprocessingPassResult SortInferencePass::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index 74ae0bd2b..5874b4363 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -38,6 +38,6 @@ class SortInferencePass : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 7b49de141..1cc2ce06f 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -57,4 +57,4 @@ PreprocessingPassResult StaticLearning::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index e9c5d70f5..67bf053f9 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -36,6 +36,6 @@ class StaticLearning : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 08f6a8de3..775a09441 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 CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -57,4 +57,4 @@ PreprocessingPassResult StringsEagerPp::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index 16324368e..3af59766c 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -39,6 +39,6 @@ class StringsEagerPp : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 ff60173ed..f05afe54f 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 CVC4::kind; -using namespace CVC4::theory; +using namespace CVC5::kind; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -345,4 +345,4 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index f9d8bf9dd..b31e5ca7c 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -63,6 +63,6 @@ class SygusInference : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 bf84ee76e..7213dc8a8 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -474,4 +474,4 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 82adde0d6..eb52688e7 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -71,6 +71,6 @@ class SynthRewRulesPass : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 1a6abd723..7112dd50f 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { -using namespace CVC4::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 CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index fe5dcbd7c..bd450840e 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -37,6 +37,6 @@ class TheoryPreprocess : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 79338d63b..c70458b91 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 CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -116,4 +116,4 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index ada99a7cb..626efe8e3 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { @@ -51,6 +51,6 @@ class TheoryRewriteEq : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // 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 cf2e96c79..502889dd3 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace passes { using namespace std; -using namespace CVC4::theory; +using namespace CVC5::theory; UnconstrainedSimplifier::UnconstrainedSimplifier( PreprocessingPassContext* preprocContext) @@ -880,4 +880,4 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 5609273da..da368de51 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 CVC4 { +namespace CVC5 { namespace context { class Context; } @@ -72,6 +72,6 @@ class UnconstrainedSimplifier : public PreprocessingPass } // namespace passes } // namespace preprocessing -} // namespace CVC4 +} // namespace CVC5 #endif |