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/theory/quantifiers | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/theory/quantifiers')
236 files changed, 607 insertions, 607 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index eb977960b..3832508dd 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -15,9 +15,9 @@ #include "theory/quantifiers/alpha_equivalence.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -110,4 +110,4 @@ Node AlphaEquivalence::reduceQuantifier(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 822b674e2..03047c93b 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -21,7 +21,7 @@ #include "expr/term_canonize.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -101,6 +101,6 @@ class AlphaEquivalence } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index c4bd2c083..014e46925 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -442,4 +442,4 @@ Node BvInverter::solveBvLit(Node sv, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index c033b26d7..a187cd36a 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -24,7 +24,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -128,6 +128,6 @@ class BvInverter } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__BV_INVERTER_H */ diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index 459c3f93f..e53e64a94 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -15,9 +15,9 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "theory/bv/theory_bv_utils.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace utils { @@ -2589,4 +2589,4 @@ Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t) } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index c6400bd60..823855d1b 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace utils { @@ -68,5 +68,5 @@ Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t); } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 1319e5c38..526469ef2 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -24,10 +24,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -296,4 +296,4 @@ void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 396ef0d03..45333bc76 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/expr_miner.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -128,6 +128,6 @@ class CandidateRewriteDatabase : public ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 0ab85ccf7..7ada36dc2 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -20,9 +20,9 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -277,4 +277,4 @@ bool CandidateRewriteFilter::notify(Node s, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index faf675bcb..aa31c7845 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -171,6 +171,6 @@ class CandidateRewriteFilter } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 29881a3a4..2a7a95b65 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -25,10 +25,10 @@ #include "util/random.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1036,4 +1036,4 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index e6cfa31c6..a81f5f180 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/cegqi/vts_term_cache.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class ArithInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 2c163421e..bdd6d26ab 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -23,9 +23,9 @@ #include "util/random.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -759,4 +759,4 @@ void BvInstantiatorPreprocess::collectExtracts( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 4bfda133e..9914428ef 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 85faea4b1..030258113 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -17,9 +17,9 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace utils { @@ -342,4 +342,4 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 576d68d06..ac68dc4d5 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -20,7 +20,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -104,5 +104,5 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index bb81d2790..672ed990a 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -20,9 +20,9 @@ #include "theory/datatypes/theory_datatypes_utils.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -180,4 +180,4 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index c0386465d..27bf560cb 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -91,6 +91,6 @@ class DtInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 118c505fc..b9d70768b 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -32,9 +32,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1638,4 +1638,4 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 03161399c..986874266 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -23,7 +23,7 @@ #include "theory/inference_id.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -822,6 +822,6 @@ class InstantiatorPreprocess } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index d6a504713..5e3a64325 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -26,10 +26,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -546,4 +546,4 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index a5b79fb00..6d4ee047f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -26,7 +26,7 @@ #include "theory/quantifiers/quant_module.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -215,6 +215,6 @@ class InstStrategyCegqi : public QuantifiersModule } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 9efc0ec31..d5fabbbd9 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -19,7 +19,7 @@ #include "expr/subs.h" #include "theory/smt_engine_subsolver.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -152,4 +152,4 @@ Node NestedQe::doQe(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index 29df5d16b..e0cccb9c9 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -23,7 +23,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -81,6 +81,6 @@ class NestedQe } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index 1a7431038..1974e7c7c 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -296,4 +296,4 @@ bool VtsTermCache::containsVtsInfinity(Node n, bool isFree) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 53c198213..d56684d43 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -21,7 +21,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** Attribute to mark Skolems as virtual terms */ @@ -140,6 +140,6 @@ class VtsTermCache } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index ffe06a7ad..41d881f2c 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -26,13 +26,13 @@ #include "theory/rewriter.h" #include "util/random.h" -using namespace CVC5; -using namespace CVC5::kind; -using namespace CVC5::theory; -using namespace CVC5::theory::quantifiers; +using namespace cvc5; +using namespace cvc5::kind; +using namespace cvc5::theory; +using namespace cvc5::theory::quantifiers; using namespace std; -namespace CVC5 { +namespace cvc5 { struct sortConjectureScore { std::vector< int > d_scores; @@ -2260,4 +2260,4 @@ unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; } bool ConjectureGenerator::optStatsOnly() { return false; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index cc3314f82..db609a521 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -466,6 +466,6 @@ private: //information about ground equivalence classes } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 6e7601072..fe712e01e 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -17,9 +17,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -183,4 +183,4 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 79b4824b4..9fce59796 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -22,7 +22,7 @@ #include "context/cdlist.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -119,6 +119,6 @@ class DynamicRewriter } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4c9da3632..a3708bdfe 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -24,9 +24,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -348,4 +348,4 @@ Node CandidateGeneratorSelector::getNextCandidate() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index b21a96225..0de57f02f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -20,7 +20,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -243,6 +243,6 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 14f514b73..5a00d41ca 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -25,9 +25,9 @@ #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -526,4 +526,4 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 66b374ea8..12c91be63 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -275,6 +275,6 @@ class HigherOrderTrigger : public Trigger } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp index 2f415779a..9f24faf68 100644 --- a/src/theory/quantifiers/ematching/im_generator.cpp +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/ematching/trigger.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -36,4 +36,4 @@ bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index b0d937120..222e3c078 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -22,7 +22,7 @@ #include "theory/inference_id.h" #include "theory/quantifiers/inst_match.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -117,6 +117,6 @@ protected: } // namespace inst } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 79b6927f7..94e356418 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -29,9 +29,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -673,4 +673,4 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 32d6e38f1..7b440035f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/ematching/im_generator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -325,6 +325,6 @@ class InstMatchGenerator : public IMGenerator { } // namespace inst } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 6ac910e2e..6677a162f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -18,9 +18,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/uf/equality_engine_iterator.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -315,4 +315,4 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 644a47bee..309aa2640 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/inst_match_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -103,6 +103,6 @@ class InstMatchGeneratorMulti : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 94b7921ed..8289ea841 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -17,9 +17,9 @@ #include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -175,4 +175,4 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index 00a372c8f..4d4339bac 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -85,6 +85,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 7d7b3e1c0..b6af066f8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -21,9 +21,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -198,4 +198,4 @@ int InstMatchGeneratorSimple::getActiveScore() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 8361628da..ccc650044 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -23,7 +23,7 @@ #include "expr/node_trie.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -100,6 +100,6 @@ class InstMatchGeneratorSimple : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index a56e7efeb..ad269ac31 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers/quantifiers_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -44,4 +44,4 @@ options::UserPatMode InstStrategy::getInstUserPatMode() const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 0537d92ce..1ce62f170 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -22,7 +22,7 @@ #include "options/quantifiers_options.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index c62a034e4..d298f994d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/quantifiers_state.h" #include "util/random.h" -using namespace CVC5::kind; -using namespace CVC5::theory::quantifiers::inst; +using namespace cvc5::kind; +using namespace cvc5::theory::quantifiers::inst; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -688,4 +688,4 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index bc52d605c..2c765e194 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_relevance.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -112,6 +112,6 @@ class InstStrategyAutoGenTriggers : public InstStrategy }; /* class InstStrategyAutoGenTriggers */ } } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 4b0d619bc..12ad77ef2 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -18,10 +18,10 @@ #include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quantifiers_state.h" -using namespace CVC5::kind; -using namespace CVC5::theory::quantifiers::inst; +using namespace cvc5::kind; +using namespace cvc5::theory::quantifiers::inst; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -175,4 +175,4 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 1bb50af7b..ed247b89a 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -64,6 +64,6 @@ class InstStrategyUserPatterns : public InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 94054b8f9..86abb4986 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -23,11 +23,11 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; -using namespace CVC5::context; -using namespace CVC5::theory::quantifiers::inst; +using namespace cvc5::kind; +using namespace cvc5::context; +using namespace cvc5::theory::quantifiers::inst; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -272,4 +272,4 @@ bool InstantiationEngine::shouldProcess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 8dface27e..bd7388afb 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_relevance.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -75,6 +75,6 @@ class InstantiationEngine : public QuantifiersModule { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 467ed46be..fb5bd49a3 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -729,4 +729,4 @@ void PatternTermSelector::getTriggerVariables(Node n, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index 6f26f2cec..5ac6c1da3 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -23,7 +23,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -192,6 +192,6 @@ class PatternTermSelector } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 234940b54..dd0af2e18 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -32,9 +32,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/valuation.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -229,4 +229,4 @@ void Trigger::debugPrint(const char* c) const } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index c6d3b3cd5..e2ad00561 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/inference_id.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -219,6 +219,6 @@ class Trigger { } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp index 327d2bba1..fa8d2ff52 100644 --- a/src/theory/quantifiers/ematching/trigger_database.cpp +++ b/src/theory/quantifiers/ematching/trigger_database.cpp @@ -18,7 +18,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -185,4 +185,4 @@ bool TriggerDatabase::mkTriggerTerms(Node q, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 2c28c77bc..9cebb6173 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/trigger_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -105,6 +105,6 @@ class TriggerDatabase } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */ diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 1f3ca0577..984e825f0 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -114,4 +114,4 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 603a1ab77..c70257e08 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -124,6 +124,6 @@ class TriggerTermInfo } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp index c8a13d447..7ca925b53 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.cpp +++ b/src/theory/quantifiers/ematching/trigger_trie.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/ematching/trigger_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -74,4 +74,4 @@ void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index 355ad6c31..fe16e3c0f 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -58,6 +58,6 @@ class TriggerTrie } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */ diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index e2dd3f37d..63a9cceae 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -81,4 +81,4 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 6ee179e91..87c4d1e32 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace inst { @@ -53,6 +53,6 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 7846a60bd..77b402843 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -21,10 +21,10 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -187,4 +187,4 @@ int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index d863c830b..988291ed5 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/quant_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -90,6 +90,6 @@ class EqualityQuery : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 20f3afe63..b21252358 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -22,9 +22,9 @@ #include "theory/smt_engine_subsolver.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -104,4 +104,4 @@ Result ExprMiner::doCheck(Node query) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 7046dad83..37d0de6f8 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -25,7 +25,7 @@ #include "smt/smt_engine.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -90,6 +90,6 @@ class ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index 867e6748a..b84968adf 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -16,7 +16,7 @@ #include "options/quantifiers_options.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -165,4 +165,4 @@ bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 6e775f586..d33c9902c 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/solution_filter.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -118,6 +118,6 @@ class ExpressionMinerManager } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 01d573607..092041b15 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -24,10 +24,10 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/theory.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1726,4 +1726,4 @@ void ExtendedRewriter::debugExtendedRewrite(Node n, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index f04f9eaae..0d6ece71e 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -250,6 +250,6 @@ class ExtendedRewriter } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bbd6443fa..eb1e4e96a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -23,10 +23,10 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -363,4 +363,4 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 7a578a33a..ec3b6dd7a 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -22,7 +22,7 @@ #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -196,6 +196,6 @@ class FirstOrderModel : public TheoryModel } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 6044de049..efa3dd160 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 CVC5; +using namespace cvc5; 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; BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node r, diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index f2abf743a..fc6fac92a 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 CVC5 { +namespace cvc5 { namespace theory { class RepSetIterator; @@ -238,6 +238,6 @@ private: } } -} // namespace CVC5 +} // 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 7c9aacd76..515d9fe58 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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 CVC5 +} // 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 86665aef4..d858e24f6 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 CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -54,6 +54,6 @@ class FirstOrderModelFmc : public FirstOrderModel } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // 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 3a7209f00..7dbc10f57 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 CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 19ecc8ddc..586bde226 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 CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -187,6 +187,6 @@ protected: } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // 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 17935f6b4..27eed53f2 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 CVC5; -using namespace CVC5::kind; -using namespace CVC5::context; -using namespace CVC5::theory; -using namespace CVC5::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 2b102c0a8..4a95a8a73 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 CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -73,6 +73,6 @@ class QModelBuilder : public TheoryEngineModelBuilder } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // 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 9943744f7..1c46e425d 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 CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -343,4 +343,4 @@ void ModelEngine::debugPrint( const char* c ){ } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 078894de6..2547f2831 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 CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -71,6 +71,6 @@ private: } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 326de79fa..9a3d465d5 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -252,4 +252,4 @@ bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h index be4070840..fcc30948d 100644 --- a/src/theory/quantifiers/fun_def_evaluator.h +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/evaluator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -70,6 +70,6 @@ class FunDefEvaluator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/index_trie.cpp b/src/theory/quantifiers/index_trie.cpp index 444882729..8c00efb0e 100644 --- a/src/theory/quantifiers/index_trie.cpp +++ b/src/theory/quantifiers/index_trie.cpp @@ -15,7 +15,7 @@ **/ #include "theory/quantifiers/index_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -114,4 +114,4 @@ IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n, } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h index 4ac754252..2c968e107 100644 --- a/src/theory/quantifiers/index_trie.h +++ b/src/theory/quantifiers/index_trie.h @@ -21,7 +21,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -106,5 +106,5 @@ class IndexTrie } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* THEORY__QUANTIFIERS__INDEX_TRIE_H */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 3db8db74e..c2f65ea93 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers/quantifiers_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -102,4 +102,4 @@ bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 9ff507917..e5e8f97cd 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -89,6 +89,6 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 879eb8479..347fe45af 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/term_database.h" #include "theory/uf/equality_engine_iterator.h" -using namespace CVC5::context; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -369,4 +369,4 @@ bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index da8858e8a..ca878c888 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -23,7 +23,7 @@ #include "context/cdo.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -224,6 +224,6 @@ class InstMatchTrieOrdered } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index c2ee94d1e..3e560acaa 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -21,10 +21,10 @@ #include "theory/quantifiers/term_tuple_enumerator.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -220,4 +220,4 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 05e5f7352..7b5cb8e0e 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/quant_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -116,6 +116,6 @@ class InstStrategyEnum : public QuantifiersModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 4f878c79b..62376bff6 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -33,10 +33,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -760,4 +760,4 @@ Instantiate::Statistics::~Statistics() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 3fb194589..b3c056506 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -27,7 +27,7 @@ #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { class LazyCDProof; @@ -361,6 +361,6 @@ class Instantiate : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp index 1c3a0bcac..78bfdf9a4 100644 --- a/src/theory/quantifiers/instantiation_list.cpp +++ b/src/theory/quantifiers/instantiation_list.cpp @@ -17,7 +17,7 @@ #include "options/base_options.h" #include "printer/printer.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist) { @@ -31,4 +31,4 @@ std::ostream& operator<<(std::ostream& out, const SkolemList& skl) return out; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index da8d5c3b5..86dfa0081 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** A list of instantiations for a quantified formula */ struct InstantiationList @@ -53,6 +53,6 @@ struct SkolemList /** Print the skolem list to stream out */ std::ostream& operator<<(std::ostream& out, const SkolemList& skl); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */ diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 6a32969e3..4561226e1 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -4,12 +4,12 @@ # src/theory/builtin/kinds. # -theory THEORY_QUANTIFIERS ::CVC5::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h" +theory THEORY_QUANTIFIERS ::cvc5::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h" typechecker "theory/quantifiers/theory_quantifiers_type_rules.h" properties check presolve -rewriter ::CVC5::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h" +rewriter ::cvc5::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h" operator FORALL 2:3 "universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST" @@ -47,16 +47,16 @@ sort INST_PATTERN_LIST_TYPE \ # a list of instantiation patterns operator INST_PATTERN_LIST 1: "a list of instantiation patterns" -typerule FORALL ::CVC5::theory::quantifiers::QuantifierTypeRule -typerule EXISTS ::CVC5::theory::quantifiers::QuantifierTypeRule -typerule BOUND_VAR_LIST ::CVC5::theory::quantifiers::QuantifierBoundVarListTypeRule -typerule INST_PATTERN_LIST ::CVC5::theory::quantifiers::QuantifierInstPatternListTypeRule - -typerule INST_PATTERN ::CVC5::theory::quantifiers::QuantifierInstPatternTypeRule -typerule INST_NO_PATTERN ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_ATTRIBUTE ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule -typerule SKOLEM_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule +typerule FORALL ::cvc5::theory::quantifiers::QuantifierTypeRule +typerule EXISTS ::cvc5::theory::quantifiers::QuantifierTypeRule +typerule BOUND_VAR_LIST ::cvc5::theory::quantifiers::QuantifierBoundVarListTypeRule +typerule INST_PATTERN_LIST ::cvc5::theory::quantifiers::QuantifierInstPatternListTypeRule + +typerule INST_PATTERN ::cvc5::theory::quantifiers::QuantifierInstPatternTypeRule +typerule INST_NO_PATTERN ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule +typerule INST_ATTRIBUTE ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule +typerule INST_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule +typerule INST_ADD_TO_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule +typerule SKOLEM_ADD_TO_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule endtheory diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 1b706d904..06d1798d5 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/lazy_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -156,4 +156,4 @@ void LazyTrieMulti::clear() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 2d92b13fd..d4437ae75 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -168,6 +168,6 @@ class LazyTrieMulti } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 572c631e1..4be66a703 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -18,9 +18,9 @@ #include "expr/skolem_manager.h" #include "theory/builtin/proof_checker.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -123,4 +123,4 @@ Node QuantifiersProofRuleChecker::checkInternal( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index da78daf90..39e933149 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -44,6 +44,6 @@ class QuantifiersProofRuleChecker : public ProofRuleChecker } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */ diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index 6d7e2e9cd..609bc66a4 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -17,9 +17,9 @@ #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -127,4 +127,4 @@ bool QuantifiersBoundInference::getBoundElements( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index 62ac0ea58..7c15d5146 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -20,7 +20,7 @@ #include <vector> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class RepSetIterator; @@ -122,6 +122,6 @@ class QuantifiersBoundInference } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 5fa617670..94b2f001e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -29,10 +29,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -2351,4 +2351,4 @@ bool QuantConflictFind::isPropagatingInstance(Node n) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index ef605a48a..93e6075a8 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -25,7 +25,7 @@ #include "expr/node_trie.h" #include "theory/quantifiers/quant_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -313,6 +313,6 @@ std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index 811dc8642..2c74b3557 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -14,9 +14,9 @@ #include "theory/quantifiers/quant_module.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { QuantifiersModule::QuantifiersModule( @@ -75,4 +75,4 @@ quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry() } } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 53fb55aa0..e6d5eee76 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { class TermDb; @@ -174,6 +174,6 @@ class QuantifiersModule }; /* class QuantifiersModule */ } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index 2ce79d285..f6a96cda2 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -15,10 +15,10 @@ #include "theory/quantifiers/quant_relevance.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -62,4 +62,4 @@ size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 73b62489e..e6a178c73 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/quant_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -63,6 +63,6 @@ class QuantRelevance : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANT_RELEVANCE_H */ diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index 2a70e5d4e..383091e33 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -17,9 +17,9 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_bound_inference.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -86,4 +86,4 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index 7e8f5d386..6fe0faefa 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -23,7 +23,7 @@ #include "theory/rep_set.h" #include "theory/theory_model.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -67,6 +67,6 @@ class QRepBoundExt : public RepBoundExt } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 85fb291f0..00a8ff08f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/first_order_model.h" #include "options/quantifiers_options.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -207,4 +207,4 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index eb85a2c28..ee961cbbc 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -20,7 +20,7 @@ #include "context/cdo.h" #include "theory/quantifiers/quant_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -73,6 +73,6 @@ class QuantDSplit : public QuantifiersModule { } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 841778a89..cbf29065c 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ @@ -131,4 +131,4 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, } } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f41f394e8..7cd89c7d8 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** Quantifiers utility @@ -78,6 +78,6 @@ public: }; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 8c068e06c..d53ed74be 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -20,10 +20,10 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -378,4 +378,4 @@ void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 4f7f1e22c..2fb294abe 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -22,7 +22,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** Attribute true for function definition quantifiers */ @@ -244,6 +244,6 @@ class QuantAttributes } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 687e17e4a..ff3087b63 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -17,7 +17,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/skolemize.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -53,4 +53,4 @@ void QuantifiersInferenceManager::doPending() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index afe8dd40a..b468e0478 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -20,7 +20,7 @@ #include "theory/inference_manager_buffered.h" #include "theory/quantifiers/quantifiers_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -59,6 +59,6 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */ diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index e39e38ea7..049e72edf 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -18,7 +18,7 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -122,4 +122,4 @@ void QuantifiersModules::initialize(QuantifiersState& qs, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 71928502d..c52da79a7 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -30,7 +30,7 @@ #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus_inst.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -45,7 +45,7 @@ namespace quantifiers { */ class QuantifiersModules { - friend class ::CVC5::theory::QuantifiersEngine; + friend class ::cvc5::theory::QuantifiersEngine; public: QuantifiersModules(); @@ -94,6 +94,6 @@ class QuantifiersModules } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */ diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 3cd59c834..58edc72bd 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -18,7 +18,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/term_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -208,4 +208,4 @@ bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index a3dffb063..383934c15 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -22,7 +22,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersModule; @@ -129,6 +129,6 @@ class QuantifiersRegistry : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d31b22f88..2c91df7a7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -32,10 +32,10 @@ #include "theory/strings/theory_strings_utils.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -2030,4 +2030,4 @@ TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 7bbe32da7..5ea8352d0 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -22,7 +22,7 @@ #include "theory/theory_rewriter.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -303,6 +303,6 @@ public: } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 5e3bb3ba3..927369442 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/uf/equality_engine_iterator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -160,4 +160,4 @@ QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 0f1c13659..623d52289 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -21,7 +21,7 @@ #include "theory/theory.h" #include "theory/theory_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -86,6 +86,6 @@ class QuantifiersState : public TheoryState } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */ diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp index e922c7080..720ae2ee0 100644 --- a/src/theory/quantifiers/quantifiers_statistics.cpp +++ b/src/theory/quantifiers/quantifiers_statistics.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -61,4 +61,4 @@ QuantifiersStatistics::~QuantifiersStatistics() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 9f2678796..9eccf3ce6 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -20,7 +20,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -47,6 +47,6 @@ class QuantifiersStatistics } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */ diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 0860549ba..6abb8bbec 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -24,9 +24,9 @@ #include "util/random.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -425,4 +425,4 @@ void QueryGenerator::findQueries( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index a847a184b..cf10b42da 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/lazy_trie.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -116,6 +116,6 @@ class QueryGenerator : public ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 3e25f4073..6fb27bec4 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -338,4 +338,4 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 56b728b34..807e4c4a2 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -20,7 +20,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -170,6 +170,6 @@ class RelevantDomain : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 1dbc24280..2fe173763 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -20,11 +20,11 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -615,4 +615,4 @@ void SingleInvocationPartition::debugPrint(const char* c) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 6feff4169..604c711ad 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -292,6 +292,6 @@ class SingleInvocationPartition } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 3767fac61..2a19824ac 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -27,9 +27,9 @@ #include "theory/rewriter.h" #include "theory/sort_inference.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -399,4 +399,4 @@ bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index d0a889ace..4c4d770f3 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -26,7 +26,7 @@ #include "theory/eager_proof_generator.h" #include "theory/trust_node.h" -namespace CVC5 { +namespace cvc5 { class DTypeConstructor; @@ -157,6 +157,6 @@ class Skolemize } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 3b00f5081..d7556be40 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -20,9 +20,9 @@ #include "smt/smt_engine_scope.h" #include "util/random.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -103,4 +103,4 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index cea5eb74e..bf3d9bddc 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/lazy_trie.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -70,6 +70,6 @@ class SolutionFilterStrength : public ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 0acd7e718..5e9f2d591 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -32,9 +32,9 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -548,4 +548,4 @@ bool CegSingleInv::solveTrivial(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index e2f399ffd..ca83bf973 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/sygus_stats.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -178,6 +178,6 @@ class CegSingleInv } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index d980db887..52adc1972 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -24,10 +24,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -706,4 +706,4 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index a12133d23..f728d3d7e 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -227,6 +227,6 @@ class Cegis : public SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 26ad62c90..6e47c2d89 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -28,9 +28,9 @@ #include "theory/smt_engine_subsolver.h" #include "util/random.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -861,4 +861,4 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 59bf53317..2abce835a 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { class SmtEngine; @@ -399,6 +399,6 @@ class CegisCoreConnective : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index bcd9fa67a..9a5c6146d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -21,9 +21,9 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -686,4 +686,4 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index e00370f2a..a543bfda0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -333,6 +333,6 @@ class CegisUnif : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 17f2a0c16..2bf8b4611 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -24,9 +24,9 @@ #include <numeric> // for std::iota -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -621,4 +621,4 @@ bool EnumStreamConcrete::increment() Node EnumStreamConcrete::getCurrent() { return d_currTerm; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index c7e4720d2..a72481a38 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -299,6 +299,6 @@ class EnumStreamConcrete : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index 5056fb96d..aea6cb9ef 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.cpp +++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp @@ -17,10 +17,10 @@ #include "theory/quantifiers/sygus/example_min_eval.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -119,4 +119,4 @@ void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 97ec38ab5..1a70369a5 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -20,7 +20,7 @@ #include "expr/node_trie.h" #include "theory/quantifiers/sygus/example_infer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -160,6 +160,6 @@ class ExampleEvalCache } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp index 12e4f073e..9dc99cab1 100644 --- a/src/theory/quantifiers/sygus/example_infer.cpp +++ b/src/theory/quantifiers/sygus/example_infer.cpp @@ -17,10 +17,10 @@ #include "theory/quantifiers/quant_util.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -275,4 +275,4 @@ bool ExampleInfer::hasExamplesOut(Node f) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 0e5ee25ac..dd2bf8a0a 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -157,6 +157,6 @@ class ExampleInfer } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp index 4cb9bd345..5b3ccec4f 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.cpp +++ b/src/theory/quantifiers/sygus/example_min_eval.cpp @@ -18,7 +18,7 @@ #include "expr/node_algorithm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -84,4 +84,4 @@ Node EmeEvalTds::eval(TNode n, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 9af07caba..2105faf2b 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.h +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "expr/node_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -118,6 +118,6 @@ class EmeEvalTds : public EmeEval } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp index 7d4a41f2d..6db446dbb 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp @@ -17,7 +17,7 @@ #include "expr/node_algorithm.h" #include "theory/datatypes/sygus_datatype_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -97,4 +97,4 @@ void RConsObligationInfo::printCandSols( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index e05422b59..3bded2a90 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -145,6 +145,6 @@ class RConsObligationInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index 37b136a1c..97ae4878d 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -16,7 +16,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -69,4 +69,4 @@ Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index c2bce5720..974897023 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -97,6 +97,6 @@ class RConsTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 71853fc76..8df45320f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -29,9 +29,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -187,4 +187,4 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index ffcefd38b..634a9a4bd 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class SygusAbduct } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index c786d2668..82d0c6c62 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -24,9 +24,9 @@ #include "theory/quantifiers/sygus/type_node_id_trie.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1214,4 +1214,4 @@ bool SygusEnumerator::TermEnumMasterFv::increment() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index a0d1c9b62..f1ef115f8 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -506,6 +506,6 @@ class SygusEnumerator : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp index 51814b07c..e9f41c916 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp @@ -15,10 +15,10 @@ #include "options/datatypes_options.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -55,4 +55,4 @@ bool EnumValGeneratorBasic::increment() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index c57d6f814..1f489eafc 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -65,6 +65,6 @@ class EnumValGeneratorBasic : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 3e87ccfc7..5dbd7655f 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -22,10 +22,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -333,4 +333,4 @@ Node SygusEvalUnfold::unfold(Node en) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index d5e47edbc..628f01c40 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/sygus_invariance.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -154,6 +154,6 @@ class SygusEvalUnfold } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 26fab8535..95acce626 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -21,10 +21,10 @@ #include "theory/quantifiers/sygus/sygus_invariance.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -357,4 +357,4 @@ void SygusExplain::getExplanationFor(Node n, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 1b1db568f..477857794 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -241,6 +241,6 @@ class SygusExplain } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 554f587c7..1c96b1346 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -30,9 +30,9 @@ #include "theory/rewriter.h" #include "theory/strings/word.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1622,4 +1622,4 @@ bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index a39540452..56f469fef 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -25,7 +25,7 @@ #include "expr/node.h" #include "expr/sygus_datatype.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** @@ -266,6 +266,6 @@ public: } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index fa67e17c4..8a2ad109d 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -31,9 +31,9 @@ #include <numeric> // for std::iota -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -536,4 +536,4 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 8c057d2c5..eda34a251 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -25,7 +25,7 @@ #include "expr/sygus_datatype.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SygusGrammarNorm } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 8e6f4fbae..a8ada94ed 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -176,4 +176,4 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 25256a68c..2144102e0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -118,6 +118,6 @@ class SygusRedundantCons } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 1c856ffa2..fe286d15c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -27,7 +27,7 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -358,4 +358,4 @@ bool SygusInterpol::solveInterpolation(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 34517b6e6..c63d096b8 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -23,7 +23,7 @@ #include "expr/type_node.h" #include "smt/smt_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { /** @@ -213,6 +213,6 @@ class SygusInterpol } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 7e6c5ab6c..22ef38b0d 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -19,10 +19,10 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -261,4 +261,4 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 88e45df45..df2e189e3 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -298,6 +298,6 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 8dac30c7e..3f2bea9cb 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -27,4 +27,4 @@ SygusModule::SygusModule(QuantifiersInferenceManager& qim, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 32f404005..90460eeed 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -157,6 +157,6 @@ class SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 25068eb7d..b54b1c940 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/term_util.h" #include "util/random.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -258,4 +258,4 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index c63dcf697..a56a22838 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -168,6 +168,6 @@ class SygusPbe : public SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index dfb0a0f7c..822d19f29 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -804,4 +804,4 @@ void SynthConjectureProcess::getComponentVector(Kind k, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 0b07db89b..6f6e25d0c 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -358,6 +358,6 @@ class SynthConjectureProcess } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 72ce3f1ab..1b3a52db8 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -19,9 +19,9 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -144,4 +144,4 @@ Node SygusQePreproc::preprocess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 49f81df02..26bbf2f92 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -45,6 +45,6 @@ class SygusQePreproc } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 723d924f8..55e8c922d 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -19,9 +19,9 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ void SygusReconstruct::printPool( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 0512fe643..1f9037a26 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/sygus/rcons_obligation_info.h" #include "theory/quantifiers/sygus/rcons_type_info.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -307,6 +307,6 @@ class SygusReconstruct : public expr::NotifyMatch } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 2d7dfc4bc..179798222 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -29,9 +29,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -621,4 +621,4 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 1e7eeb9fc..b79fa4177 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -20,7 +20,7 @@ #include <unordered_set> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class LogicInfo; @@ -209,6 +209,6 @@ class SygusRepairConst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index da08ec1b5..11dec3e61 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -17,7 +17,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -60,4 +60,4 @@ SygusStatistics::~SygusStatistics() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index d89fa0eca..7a8ae8ce9 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -19,7 +19,7 @@ #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -53,6 +53,6 @@ class SygusStatistics } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 8eb13fef8..2d72b4fab 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -19,9 +19,9 @@ #include "util/random.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -136,4 +136,4 @@ void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 153c4603b..1ed81194a 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/sygus_unif_strat.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -193,6 +193,6 @@ class SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index be24cb9e7..9dfac1d68 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -26,9 +26,9 @@ #include <math.h> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1677,4 +1677,4 @@ Node SygusUnifIo::constructBestConditional(Node ce, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 5d4f7fb7d..825e5741d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -20,7 +20,7 @@ #include <map> #include "theory/quantifiers/sygus/sygus_unif.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -468,6 +468,6 @@ class SygusUnifIo : public SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 436678aa9..c3cff70d9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -24,9 +24,9 @@ #include <math.h> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1207,4 +1207,4 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 82f2a80d2..51c49cbef 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/lazy_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -443,6 +443,6 @@ class SygusUnifRl : public SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 5551be630..24bcb1eab 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -24,9 +24,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1050,4 +1050,4 @@ void SygusUnifStrategy::indent(const char* c, int ind) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index c9d6e5d96..2508fdc9b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -20,7 +20,7 @@ #include <map> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -428,6 +428,6 @@ class SygusUnifStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index ec5edd640..6c14aaa80 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -179,4 +179,4 @@ TypeNode SygusUtils::getSygusTypeForSynthFun(Node f) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 2646dd1c8..0ec497789 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.h +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/subs.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -110,6 +110,6 @@ class SygusUtils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0bfa73048..f7566e7a2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -37,10 +37,10 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1353,4 +1353,4 @@ ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index e39f65d80..7fd1ae4b3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -32,7 +32,7 @@ #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/template_infer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SynthConjecture } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 4f1a0bbbb..3d5406f27 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_registry.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -290,4 +290,4 @@ void SynthEngine::preregisterAssertion(Node n) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 30f9c181e..a5fde8476 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -115,6 +115,6 @@ class SynthEngine : public QuantifiersModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 84fcafd05..875b25370 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -203,4 +203,4 @@ Node SygusTemplateInfer::getTemplateArg(Node prog) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index be35025bd..1ab97b651 100644 --- a/src/theory/quantifiers/sygus/template_infer.h +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/transition_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -71,6 +71,6 @@ class SygusTemplateInfer } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index f50e222ff..34a81467a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -30,9 +30,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1091,4 +1091,4 @@ bool TermDbSygus::isEvaluationPoint(Node n) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 0bd0c636a..fb7e38ff8 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -28,7 +28,7 @@ #include "theory/quantifiers/sygus/type_info.h" #include "theory/quantifiers/term_database.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -467,6 +467,6 @@ class TermDbSygus { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 0b5946176..7ee2f2ec6 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -585,4 +585,4 @@ Node TransitionInference::constructFormulaTrace(DetTrace& dt) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index aed003357..8ddc1a320 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -27,7 +27,7 @@ #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/single_inv_partition.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -332,6 +332,6 @@ class TransitionInference } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 19dff9936..fdc8ca6a3 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus/type_node_id_trie.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ bool SygusTypeInfo::isSubclassVarTrivial() const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index cc78fc526..79413a03c 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -253,6 +253,6 @@ class SygusTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */ diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.cpp b/src/theory/quantifiers/sygus/type_node_id_trie.cpp index 064543af8..a2c7b264d 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.cpp +++ b/src/theory/quantifiers/sygus/type_node_id_trie.cpp @@ -14,9 +14,9 @@ #include "theory/quantifiers/sygus/type_node_id_trie.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -49,4 +49,4 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h index a60afda23..6311cbabe 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -48,6 +48,6 @@ class TypeNodeIdTrie } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */ diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 0b1d91684..81dc5cecb 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -28,7 +28,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -553,4 +553,4 @@ void SygusInst::addCeLemma(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 08fc5ccb3..35b66437b 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -24,7 +24,7 @@ #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class QuantifiersEngine; @@ -147,6 +147,6 @@ class SygusInst : public QuantifiersModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 2b89c0c7c..5c7797a1a 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -30,7 +30,7 @@ #include "util/random.h" #include "util/sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -845,4 +845,4 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 65843dc63..7350f4845 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -320,6 +320,6 @@ class SygusSampler : public LazyTrieEvaluator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d6d7933cb..64c2fda76 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -28,10 +28,10 @@ #include "theory/rewriter.h" #include "theory/uf/equality_engine.h" -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1232,4 +1232,4 @@ Node TermDb::getHoTypeMatchPredicate(TypeNode tn) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d0812d1d1..2077b3d2d 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -422,6 +422,6 @@ class TermDb : public QuantifiersUtil { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 2945750c1..a13a19a77 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/quant_bound_inference.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -75,4 +75,4 @@ bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index fa7eaf63e..bd545ff50 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -24,7 +24,7 @@ #include "expr/type_node.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -71,6 +71,6 @@ class TermEnumeration } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index cf33f0a41..8317271f9 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -20,7 +20,7 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/quantifiers_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -134,4 +134,4 @@ bool TermRegistry::useFmcModel() const { return d_useFmcModel; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index e4e4a7e9f..79070fae8 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -99,6 +99,6 @@ class TermRegistry } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 546f6aa6c..e4e63787e 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -31,7 +31,7 @@ #include "theory/quantifiers/term_util.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { template <typename T> static CVC4ostream& operator<<(CVC4ostream& out, const std::vector<T>& v) @@ -505,4 +505,4 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h index b15ab2212..4d6eb52f8 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.h +++ b/src/theory/quantifiers/term_tuple_enumerator.h @@ -18,7 +18,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -94,5 +94,5 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* TERM_TUPLE_ENUMERATOR_H_7640 */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 41e06a708..8b1c1aa30 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -22,9 +22,9 @@ #include "theory/strings/word.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -601,4 +601,4 @@ bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 1ac6ca495..d8a881e2e 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -22,7 +22,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { // attribute for "contains instantiation constants from" @@ -206,6 +206,6 @@ public: } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index d89abf076..c3c3fe7b6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/valuation.h" -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -184,4 +184,4 @@ void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::v } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 6af0e8648..21c30390c 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -30,7 +30,7 @@ #include "theory/theory.h" #include "theory/valuation.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -98,6 +98,6 @@ class TheoryQuantifiers : public Theory { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index e990f5320..53c077930 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -131,6 +131,6 @@ struct QuantifierInstPatternListTypeRule { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ |