diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/decision | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_attributes.h | 4 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 4 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 8 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 4 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 10 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 6 |
6 files changed, 18 insertions, 18 deletions
diff --git a/src/decision/decision_attributes.h b/src/decision/decision_attributes.h index be5987e6d..c34abd179 100644 --- a/src/decision/decision_attributes.h +++ b/src/decision/decision_attributes.h @@ -22,7 +22,7 @@ #include "options/decision_weight.h" #include "expr/attribute.h" -namespace CVC5 { +namespace cvc5 { namespace decision { namespace attr { struct DecisionWeightTag {}; @@ -31,6 +31,6 @@ namespace attr { typedef expr::Attribute<attr::DecisionWeightTag, DecisionWeight> DecisionWeightAttr; } // namespace decision -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DECISION__DECISION_ATTRIBUTES_H */ diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 3196336aa..f202037b0 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc, @@ -101,4 +101,4 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 7405498b5..cbb6b897d 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -28,10 +28,10 @@ #include "prop/sat_solver_types.h" #include "util/result.h" -using namespace CVC5::prop; -using namespace CVC5::decision; +using namespace cvc5::prop; +using namespace cvc5::decision; -namespace CVC5 { +namespace cvc5 { class DecisionEngine { @@ -160,6 +160,6 @@ class DecisionEngine { std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; };/* DecisionEngine class */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 6a9353474..4a1828a8f 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -25,7 +25,7 @@ #include "prop/sat_solver_types.h" #include "smt/term_formula_removal.h" -namespace CVC5 { +namespace cvc5 { class DecisionEngine; @@ -66,6 +66,6 @@ public: };/* class ITEDecisionStrategy */ } // namespace decision -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DECISION__DECISION_STRATEGY_H */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index f9f9cb7df..abe7a47a7 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -28,10 +28,10 @@ #include "theory/rewriter.h" #include "util/random.h" -namespace CVC5 { +namespace cvc5 { namespace decision { -JustificationHeuristic::JustificationHeuristic(CVC5::DecisionEngine* de, +JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de, context::UserContext* uc, context::Context* c) : ITEDecisionStrategy(de, c), @@ -66,7 +66,7 @@ JustificationHeuristic::~JustificationHeuristic() smtStatisticsRegistry()->unregisterStat(&d_timestat); } -CVC5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) +cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) { if(options::decisionThreshold() > 0) { bool stopSearchTmp = false; @@ -82,7 +82,7 @@ CVC5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) return getNextThresh(stopSearch, 0); } -CVC5::prop::SatLiteral JustificationHeuristic::getNextThresh( +cvc5::prop::SatLiteral JustificationHeuristic::getNextThresh( bool& stopSearch, DecisionWeight threshold) { Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl; @@ -733,4 +733,4 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node) } } /* namespace decision */ -} // namespace CVC5
\ No newline at end of file +} // namespace cvc5
\ No newline at end of file diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 9ec61d540..06864470e 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -37,7 +37,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { @@ -117,7 +117,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { }; public: - JustificationHeuristic(CVC5::DecisionEngine* de, + JustificationHeuristic(cvc5::DecisionEngine* de, context::UserContext* uc, context::Context* c); @@ -195,6 +195,6 @@ private: };/* class JustificationHeuristic */ }/* namespace decision */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */ |