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/theory/quantifiers/fmf | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/quantifiers/fmf')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/first_order_model_fmc.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/first_order_model_fmc.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_builder.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_builder.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.h | 8 |
10 files changed, 37 insertions, 37 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 9324ce36a..6044de049 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -28,11 +28,11 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4; +using namespace CVC5; 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; BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node r, diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 30589d40d..f2abf743a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -26,7 +26,7 @@ #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_bound_inference.h" -namespace CVC4 { +namespace CVC5 { namespace theory { class RepSetIterator; @@ -238,6 +238,6 @@ private: } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index 9577e296b..7c9aacd76 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -18,9 +18,9 @@ #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -156,4 +156,4 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix) } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index d8ae054ad..86665aef4 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/first_order_model.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -54,6 +54,6 @@ class FirstOrderModelFmc : public FirstOrderModel } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index fcbd8e83f..3a7209f00 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -28,10 +28,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -1375,4 +1375,4 @@ bool FullModelChecker::isHandled(Node q) const } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 972c977e8..19ecc8ddc 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -20,7 +20,7 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/model_builder.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -184,9 +184,9 @@ protected: bool isHandled(Node q) const; };/* class FullModelChecker */ -}/* CVC4::theory::quantifiers::fmcheck namespace */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace fmcheck +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index f30f811d5..17935f6b4 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -22,11 +22,11 @@ #include "theory/quantifiers/quantifiers_state.h" using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; +using namespace CVC5; +using namespace CVC5::kind; +using namespace CVC5::context; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index af5dee3cf..2b102c0a8 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/theory_model_builder.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -71,8 +71,8 @@ class QModelBuilder : public TheoryEngineModelBuilder quantifiers::QuantifiersInferenceManager& d_qim; }; -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index f3807aa9e..9943744f7 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -343,4 +343,4 @@ void ModelEngine::debugPrint( const char* c ){ } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index caafe3840..078894de6 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/theory_model.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -69,8 +69,8 @@ private: QModelBuilder* d_builder; };/* class ModelEngine */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ |