diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/theory/quantifiers | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/quantifiers')
236 files changed, 757 insertions, 757 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index ac52338a9..eb977960b 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -110,4 +110,4 @@ Node AlphaEquivalence::reduceQuantifier(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 48d667325..822b674e2 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -101,6 +101,6 @@ class AlphaEquivalence } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index d81e23056..c4bd2c083 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -442,4 +442,4 @@ Node BvInverter::solveBvLit(Node sv, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index fa7d4b073..c033b26d7 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -24,7 +24,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -128,6 +128,6 @@ class BvInverter } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 f951b29df..459c3f93f 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index af7343739..c6400bd60 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index a0b9b20f4..1319e5c38 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -294,6 +294,6 @@ void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) d_ext_rewrite = er; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 321880dc0..396ef0d03 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -126,8 +126,8 @@ class CandidateRewriteDatabase : public ExprMiner std::unordered_map<Node, Node, NodeHashFunction> d_add_term_cache; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 aca65fd83..0ab85ccf7 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -277,4 +277,4 @@ bool CandidateRewriteFilter::notify(Node s, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index 6df804dff..faf675bcb 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -171,6 +171,6 @@ class CandidateRewriteFilter } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 b0a5688b2..29881a3a4 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1036,4 +1036,4 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 00b23307e..e6cfa31c6 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class ArithInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 1c60058ff..2c163421e 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -759,4 +759,4 @@ void BvInstantiatorPreprocess::collectExtracts( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 743a27af3..4bfda133e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 c0ef3561f..85faea4b1 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace utils { @@ -342,4 +342,4 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 13b86cff4..576d68d06 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -104,5 +104,5 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index c9bc63308..bb81d2790 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 97cb7a4ee..c0386465d 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -91,6 +91,6 @@ class DtInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 5c6a932fd..118c505fc 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1636,6 +1636,6 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci, return ci->constructInstantiationInc(pv, n, pv_prop, sf); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 800398fb9..03161399c 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -820,8 +820,8 @@ class InstantiatorPreprocess } }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 59b4cc7bd..d6a504713 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -546,4 +546,4 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index e0496a462..a5b79fb00 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -215,6 +215,6 @@ class InstStrategyCegqi : public QuantifiersModule } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 0e938ddae..9efc0ec31 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -152,4 +152,4 @@ Node NestedQe::doQe(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index 21a49424a..29df5d16b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -81,6 +81,6 @@ class NestedQe } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index 912fee2fd..1a7431038 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -296,4 +296,4 @@ bool VtsTermCache::containsVtsInfinity(Node n, bool isFree) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 4f18933ec..53c198213 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 CVC4 { +namespace CVC5 { namespace theory { /** Attribute to mark Skolems as virtual terms */ @@ -140,6 +140,6 @@ class VtsTermCache } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 c095e3864..ffe06a7ad 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 CVC4; -using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; +using namespace CVC5; +using namespace CVC5::kind; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; using namespace std; -namespace CVC4 { +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 diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index b1a1ddf2b..cc3314f82 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -466,6 +466,6 @@ private: //information about ground equivalence classes } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index cf3f5fa2f..6e7601072 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -181,6 +181,6 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) return f; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index e4abdbe76..79b4824b4 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -117,8 +117,8 @@ class DynamicRewriter NodeList d_rewrites; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 60350f882..4c9da3632 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -348,4 +348,4 @@ Node CandidateGeneratorSelector::getNextCandidate() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 45eec1d4c..b21a96225 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -240,9 +240,9 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE Node d_ufOp; }; -}/* CVC4::theory::inst namespace */ +} // namespace inst } // namespace quantifiers -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // 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 a267246a8..14f514b73 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -526,4 +526,4 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index d3489783c..66b374ea8 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -275,6 +275,6 @@ class HigherOrderTrigger : public Trigger } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 06d17dea4..2f415779a 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index b277ec180..b0d937120 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -117,6 +117,6 @@ protected: } // namespace inst } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 04b8a3fcf..79b6927f7 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -673,4 +673,4 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 375fe73e1..32d6e38f1 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -325,6 +325,6 @@ class InstMatchGenerator : public IMGenerator { } // namespace inst } } -} +} // 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 fe0fa8082..6ac910e2e 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -315,4 +315,4 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 1e25baea4..644a47bee 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -103,6 +103,6 @@ class InstMatchGeneratorMulti : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 18708092a..94b7921ed 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // 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 b46960400..00a372c8f 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -85,6 +85,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 ab30b4b2d..7d7b3e1c0 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -198,4 +198,4 @@ int InstMatchGeneratorSimple::getActiveScore() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 6ae2f915b..8361628da 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -100,6 +100,6 @@ class InstMatchGeneratorSimple : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index 5e9899ec3..a56e7efeb 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -44,4 +44,4 @@ options::UserPatMode InstStrategy::getInstUserPatMode() const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 9d304368c..0537d92ce 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 45d5f13a7..c62a034e4 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 CVC4::kind; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -686,6 +686,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 a17e7bbb5..bc52d605c 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -111,7 +111,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy QuantRelevance* d_quant_rel; }; /* class InstStrategyAutoGenTriggers */ } -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // 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 a15baa5e4..4b0d619bc 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 CVC4::kind; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -175,4 +175,4 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 821d7de77..1bb50af7b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -64,6 +64,6 @@ class InstStrategyUserPatterns : public InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 52bf58263..94054b8f9 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 CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::context; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -272,4 +272,4 @@ bool InstantiationEngine::shouldProcess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index c5a82d114..8dface27e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -73,8 +73,8 @@ class InstantiationEngine : public QuantifiersModule { std::unique_ptr<QuantRelevance> d_quant_rel; }; /* class InstantiationEngine */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 7ab54fcfe..467ed46be 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -729,4 +729,4 @@ void PatternTermSelector::getTriggerVariables(Node n, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index 9cbf4cf5e..6f26f2cec 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -192,6 +192,6 @@ class PatternTermSelector } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index c739623bc..234940b54 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 5dd8db452..c6d3b3cd5 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -219,6 +219,6 @@ class Trigger { } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 fae7a10a0..327d2bba1 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -185,4 +185,4 @@ bool TriggerDatabase::mkTriggerTerms(Node q, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 21df0e536..2c28c77bc 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -105,6 +105,6 @@ class TriggerDatabase } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 4bc74dd96..1f3ca0577 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 5bf7e8099..603a1ab77 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -124,6 +124,6 @@ class TriggerTermInfo } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp index 04e9dabb0..c8a13d447 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index ad221ee21..355ad6c31 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -58,6 +58,6 @@ class TriggerTrie } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 45c9e20d7..e2dd3f37d 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index d85a20189..6ee179e91 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -53,6 +53,6 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 48e5682f2..7846a60bd 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -185,6 +185,6 @@ int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) return quantifiers::TermUtil::getTermDepth(n); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 887c54f42..d863c830b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -88,8 +88,8 @@ class EqualityQuery : public QuantifiersUtil int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn); }; /* EqualityQuery */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 71d5d7a7a..20f3afe63 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -104,4 +104,4 @@ Result ExprMiner::doCheck(Node query) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 67ab2b768..7046dad83 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -90,6 +90,6 @@ class ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 6a77d8e45..867e6748a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -165,4 +165,4 @@ bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index eb2a01fac..6e775f586 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -118,6 +118,6 @@ class ExpressionMinerManager } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 9c6dd3964..01d573607 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1724,6 +1724,6 @@ void ExtendedRewriter::debugExtendedRewrite(Node n, } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 0c4d0a1b3..f04f9eaae 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -248,8 +248,8 @@ class ExtendedRewriter //--------------------------------------end theory-specific top-level calls }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 fd84dc500..bbd6443fa 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -361,6 +361,6 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) return n.getAttribute(ModelBasisArgAttribute()); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index b86abd960..7a578a33a 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -194,8 +194,8 @@ class FirstOrderModel : public TheoryModel void computeModelBasisArgAttribute(Node n); };/* class FirstOrderModel */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 9324ce36a..6044de049 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -28,11 +28,11 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4; +using namespace CVC5; using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; +using namespace CVC5::kind; BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node r, diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 30589d40d..f2abf743a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -26,7 +26,7 @@ #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_bound_inference.h" -namespace CVC4 { +namespace CVC5 { namespace theory { class RepSetIterator; @@ -238,6 +238,6 @@ private: } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index 9577e296b..7c9aacd76 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -18,9 +18,9 @@ #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -156,4 +156,4 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix) } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index d8ae054ad..86665aef4 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/first_order_model.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -54,6 +54,6 @@ class FirstOrderModelFmc : public FirstOrderModel } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index fcbd8e83f..3a7209f00 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -28,10 +28,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -1375,4 +1375,4 @@ bool FullModelChecker::isHandled(Node q) const } // namespace fmcheck } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 972c977e8..19ecc8ddc 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -20,7 +20,7 @@ #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/model_builder.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace fmcheck { @@ -184,9 +184,9 @@ protected: bool isHandled(Node q) const; };/* class FullModelChecker */ -}/* CVC4::theory::quantifiers::fmcheck namespace */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace fmcheck +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index f30f811d5..17935f6b4 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -22,11 +22,11 @@ #include "theory/quantifiers/quantifiers_state.h" using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; +using namespace CVC5; +using namespace CVC5::kind; +using namespace CVC5::context; +using namespace CVC5::theory; +using namespace CVC5::theory::quantifiers; QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr, diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index af5dee3cf..2b102c0a8 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/theory_model_builder.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -71,8 +71,8 @@ class QModelBuilder : public TheoryEngineModelBuilder quantifiers::QuantifiersInferenceManager& d_qim; }; -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index f3807aa9e..9943744f7 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -343,4 +343,4 @@ void ModelEngine::debugPrint( const char* c ){ } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index caafe3840..078894de6 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/theory_model.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -69,8 +69,8 @@ private: QModelBuilder* d_builder; };/* class ModelEngine */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 661d45a9f..326de79fa 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -252,4 +252,4 @@ bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h index d9af82f21..be4070840 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -70,6 +70,6 @@ class FunDefEvaluator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/index_trie.cpp b/src/theory/quantifiers/index_trie.cpp index 728d51fc3..444882729 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -114,4 +114,4 @@ IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n, } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h index b77095181..4ac754252 100644 --- a/src/theory/quantifiers/index_trie.h +++ b/src/theory/quantifiers/index_trie.h @@ -21,7 +21,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -106,5 +106,5 @@ class IndexTrie } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 c215a1700..3db8db74e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -101,5 +101,5 @@ bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n) } } // namespace quantifiers -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 6e6796bb1..9ff507917 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -88,7 +88,7 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { } } // namespace quantifiers -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // 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 756550828..879eb8479 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 CVC4::context; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -368,5 +368,5 @@ bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs, } } // namespace quantifiers -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 5164f1820..da8858e8a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -223,7 +223,7 @@ class InstMatchTrieOrdered }; } // namespace quantifiers -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace theory +} // 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 16d92d405..c2ee94d1e 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -220,4 +220,4 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index d570e3039..05e5f7352 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -114,8 +114,8 @@ class InstStrategyEnum : public QuantifiersModule int32_t d_fullSaturateLimit; }; /* class InstStrategyEnum */ -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 21faaa13f..4f878c79b 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -758,6 +758,6 @@ Instantiate::Statistics::~Statistics() smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 94e16b526..3fb194589 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 CVC4 { +namespace CVC5 { class LazyCDProof; @@ -359,8 +359,8 @@ class Instantiate : public QuantifiersUtil std::unique_ptr<CDProof> d_pfInst; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 f38a5f9a8..1c3a0bcac 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index 91d2e284c..da8d5c3b5 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC4 { +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 CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */ diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index fa24275b1..6a32969e3 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -4,12 +4,12 @@ # src/theory/builtin/kinds. # -theory THEORY_QUANTIFIERS ::CVC4::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 ::CVC4::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 ::CVC4::theory::quantifiers::QuantifierTypeRule -typerule EXISTS ::CVC4::theory::quantifiers::QuantifierTypeRule -typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule -typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule - -typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule -typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_POOL ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule -typerule INST_ADD_TO_POOL ::CVC4::theory::quantifiers::QuantifierAnnotationTypeRule -typerule SKOLEM_ADD_TO_POOL ::CVC4::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 3b1abb168..1b706d904 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -154,6 +154,6 @@ void LazyTrieMulti::clear() d_rep_to_class.clear(); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index de53e738c..2d92b13fd 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -166,8 +166,8 @@ class LazyTrieMulti LazyTrie d_trie; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 afbc9efca..572c631e1 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -123,4 +123,4 @@ Node QuantifiersProofRuleChecker::checkInternal( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index 7d2f1baf1..da78daf90 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -44,6 +44,6 @@ class QuantifiersProofRuleChecker : public ProofRuleChecker } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 45c2b5e42..6d7e2e9cd 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -127,4 +127,4 @@ bool QuantifiersBoundInference::getBoundElements( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index 58b4e3db9..62ac0ea58 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 CVC4 { +namespace CVC5 { namespace theory { class RepSetIterator; @@ -122,6 +122,6 @@ class QuantifiersBoundInference } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 c71964565..5fa617670 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -2349,6 +2349,6 @@ bool QuantConflictFind::isPropagatingInstance(Node n) const return true; } -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 7778da4d0..ef605a48a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -311,8 +311,8 @@ public: std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index 156dd54fe..811dc8642 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { QuantifiersModule::QuantifiersModule( @@ -75,4 +75,4 @@ quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry() } } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index fe518d61f..53fb55aa0 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { class TermDb; @@ -174,6 +174,6 @@ class QuantifiersModule }; /* class QuantifiersModule */ } // namespace theory -} // namespace CVC4 +} // 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 2a20800c2..2ce79d285 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -60,6 +60,6 @@ size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const return it->second.size(); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 66a31b58d..73b62489e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -61,8 +61,8 @@ class QuantRelevance : public QuantifiersUtil void computeSymbols(Node n, std::vector<Node>& syms); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 f29e2e224..2a70e5d4e 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -86,4 +86,4 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index 30dbd520b..7e8f5d386 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -67,6 +67,6 @@ class QRepBoundExt : public RepBoundExt } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 cb4e4d8b6..85fb291f0 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -207,4 +207,4 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index e7468dd34..eb85a2c28 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -73,6 +73,6 @@ class QuantDSplit : public QuantifiersModule { } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 45fe078d5..841778a89 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ @@ -130,5 +130,5 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, } } -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index d536fa84d..f41f394e8 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 CVC4 { +namespace CVC5 { namespace theory { /** Quantifiers utility @@ -78,6 +78,6 @@ public: }; } -} +} // 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 30b3ebcbe..8c068e06c 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -376,6 +376,6 @@ void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level) } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index ab1f7369e..4f7f1e22c 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 CVC4 { +namespace CVC5 { namespace theory { /** Attribute true for function definition quantifiers */ @@ -244,6 +244,6 @@ class QuantAttributes } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index b25c1aed3..687e17e4a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -53,4 +53,4 @@ void QuantifiersInferenceManager::doPending() } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index f16f91f04..afe8dd40a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -59,6 +59,6 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 9c8a4c7d0..e39e38ea7 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -122,4 +122,4 @@ void QuantifiersModules::initialize(QuantifiersState& qs, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index e58fcb8d5..71928502d 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -45,7 +45,8 @@ namespace quantifiers { */ class QuantifiersModules { - friend class ::CVC4::theory::QuantifiersEngine; + friend class ::CVC5::theory::QuantifiersEngine; + public: QuantifiersModules(); ~QuantifiersModules(); @@ -93,6 +94,6 @@ class QuantifiersModules } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 daaaea0ad..3cd59c834 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index f2d3f085e..a3dffb063 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersModule; @@ -129,6 +129,6 @@ class QuantifiersRegistry : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 4b7aba7d3..d31b22f88 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -2028,6 +2028,6 @@ TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) return TrustNode::null(); } -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 3c83aef03..7bbe32da7 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -301,8 +301,8 @@ public: bool marked = false); }; /* class QuantifiersRewriter */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 be691ae27..5e3bb3ba3 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -160,4 +160,4 @@ QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 6b4daec61..0f1c13659 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -86,6 +86,6 @@ class QuantifiersState : public TheoryState } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 4567a6d4f..e922c7080 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -61,4 +61,4 @@ QuantifiersStatistics::~QuantifiersStatistics() } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 1fa053484..9f2678796 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -47,6 +47,6 @@ class QuantifiersStatistics } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 61ad4b87f..0860549ba 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -425,4 +425,4 @@ void QueryGenerator::findQueries( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 570226f85..a847a184b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -116,6 +116,6 @@ class QueryGenerator : public ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 8210c5e8a..3e25f4073 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8fbd70f3e..56b728b34 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -168,9 +168,8 @@ class RelevantDomain : public QuantifiersUtil void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ); };/* class RelevantDomain */ - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 72a1a2856..1dbc24280 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 CVC4; -using namespace CVC4::kind; +using namespace CVC5; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -613,6 +613,6 @@ void SingleInvocationPartition::debugPrint(const char* c) Trace(c) << std::endl; } -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 6c55dc959..6feff4169 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -290,8 +290,8 @@ class SingleInvocationPartition Node getConjunct(int index); }; -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // 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 9d6d30790..3767fac61 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -397,6 +397,6 @@ void Skolemize::getSkolemTermVectors( bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 3770cc223..d0a889ace 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 CVC4 { +namespace CVC5 { class DTypeConstructor; @@ -155,8 +155,8 @@ class Skolemize std::unique_ptr<EagerProofGenerator> d_epg; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 c66b83170..3b00f5081 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -103,4 +103,4 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 212b3c7dd..cea5eb74e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -70,6 +70,6 @@ class SolutionFilterStrength : public ExprMiner } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 c9b2559c1..0acd7e718 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -548,4 +548,4 @@ bool CegSingleInv::solveTrivial(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 8a2ed3a71..e2f399ffd 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -176,8 +176,8 @@ class CegSingleInv //-------------- end decomposed conjecture }; -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 9022a9ba0..d980db887 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -704,6 +704,6 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, return false; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 9d91a3d66..a12133d23 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -225,8 +225,8 @@ class Cegis : public SygusModule //---------------------------------end for symbolic constructors }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 a21632bb3..26ad62c90 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -861,4 +861,4 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 5b8be444e..59bf53317 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 CVC4 { +namespace CVC5 { class SmtEngine; @@ -399,6 +399,6 @@ class CegisCoreConnective : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 75e4c2465..bcd9fa67a 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -686,4 +686,4 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index e450c3fa7..e00370f2a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -333,6 +333,6 @@ class CegisUnif : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index d4838de7a..17f2a0c16 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -621,4 +621,4 @@ bool EnumStreamConcrete::increment() Node EnumStreamConcrete::getCurrent() { return d_currTerm; } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 46b51c443..c7e4720d2 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -299,6 +299,6 @@ class EnumStreamConcrete : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index 4508e0a09..5056fb96d 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 CVC4; -using namespace CVC4::kind; +using namespace CVC5; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -119,4 +119,4 @@ void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 35adb889c..97ec38ab5 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -160,6 +160,6 @@ class ExampleEvalCache } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp index 7219b8f4b..12e4f073e 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 CVC4; -using namespace CVC4::kind; +using namespace CVC5; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -275,4 +275,4 @@ bool ExampleInfer::hasExamplesOut(Node f) const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 61c0327b7..0e5ee25ac 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -157,6 +157,6 @@ class ExampleInfer } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp index 22b0cb121..4cb9bd345 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -84,4 +84,4 @@ Node EmeEvalTds::eval(TNode n, } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 088036945..9af07caba 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -118,6 +118,6 @@ class EmeEvalTds : public EmeEval } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp index 25aac1e93..7d4a41f2d 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -97,4 +97,4 @@ void RConsObligationInfo::printCandSols( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index 5ebddd794..e05422b59 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -145,6 +145,6 @@ class RConsObligationInfo } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 d24c4d25d..37b136a1c 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -69,4 +69,4 @@ Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index 432d07687..c2bce5720 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -97,6 +97,6 @@ class RConsTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 7bdc4ff9d..71853fc76 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -187,4 +187,4 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index 85f4ff60b..ffcefd38b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class SygusAbduct } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 4f870830e..c786d2668 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1214,4 +1214,4 @@ bool SygusEnumerator::TermEnumMasterFv::increment() } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index cbf24ada1..a0d1c9b62 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -506,6 +506,6 @@ class SygusEnumerator : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 1b3404757..51814b07c 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -55,4 +55,4 @@ bool EnumValGeneratorBasic::increment() } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index b6a56b6e3..c57d6f814 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -65,6 +65,6 @@ class EnumValGeneratorBasic : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 92d77adff..3e87ccfc7 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -333,4 +333,4 @@ Node SygusEvalUnfold::unfold(Node en) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index f39092a04..d5e47edbc 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -154,6 +154,6 @@ class SygusEvalUnfold } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 9025b1a51..26fab8535 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -355,6 +355,6 @@ void SygusExplain::getExplanationFor(Node n, getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 262062f14..1b1db568f 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -239,8 +239,8 @@ class SygusExplain int& sz); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 7645cc237..554f587c7 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1620,6 +1620,6 @@ bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const return true; } -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 0bd471922..a39540452 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 CVC4 { +namespace CVC5 { namespace theory { /** @@ -264,8 +264,8 @@ public: //---------------- end grammar construction }; -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 964d64655..fa67e17c4 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -536,4 +536,4 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index bb4bb6384..8c057d2c5 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SygusGrammarNorm } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 3a4596a1e..8e6f4fbae 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -174,6 +174,6 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds, } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 565aafe28..25256a68c 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -116,8 +116,8 @@ class SygusRedundantCons std::vector<Node>& terms); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 2335a3a28..1c856ffa2 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -358,4 +358,4 @@ bool SygusInterpol::solveInterpolation(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 07bdde2a8..34517b6e6 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { /** @@ -213,6 +213,6 @@ class SygusInterpol } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 1740ecc3d..7e6c5ab6c 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -259,6 +259,6 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, return d_isUniversal; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 0f8c22f72..88e45df45 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -296,8 +296,8 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest bool d_isUniversal; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 870363c07..8dac30c7e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -25,6 +25,6 @@ SygusModule::SygusModule(QuantifiersInferenceManager& qim, { } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 9c543c6b6..32f404005 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -155,8 +155,8 @@ class SygusModule SynthConjecture* d_parent; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 170cf6fd7..25068eb7d 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 CVC4; -using namespace CVC4::kind; +using namespace CVC5; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -258,4 +258,4 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, } } -} +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index cbd307cab..c63dcf697 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -166,8 +166,8 @@ class SygusPbe : public SygusModule std::map<Node, Node> d_enum_to_candidate; }; -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index e58c209d4..dfb0a0f7c 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -802,6 +802,6 @@ void SynthConjectureProcess::getComponentVector(Kind k, } } -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index de136d546..0b07db89b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -356,8 +356,8 @@ class SynthConjectureProcess void getComponentVector(Kind k, Node n, std::vector<Node>& args); }; -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index c8582cce5..72ce3f1ab 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -144,4 +144,4 @@ Node SygusQePreproc::preprocess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 4cfa8a624..49f81df02 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -45,6 +45,6 @@ class SygusQePreproc } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 bd0f7c4dd..723d924f8 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ void SygusReconstruct::printPool( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 2d55c3f3d..0512fe643 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -307,6 +307,6 @@ class SygusReconstruct : public expr::NotifyMatch } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 a7d352740..2d7dfc4bc 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -619,6 +619,6 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, return true; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 78c17280c..1e7eeb9fc 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 CVC4 { +namespace CVC5 { class LogicInfo; @@ -207,8 +207,8 @@ class SygusRepairConst bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 cd75a1e5e..da08ec1b5 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -60,4 +60,4 @@ SygusStatistics::~SygusStatistics() } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 0824e846f..d89fa0eca 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -53,6 +53,6 @@ class SygusStatistics } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index e590f704f..8eb13fef8 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -134,6 +134,6 @@ void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol) } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index ca5eb0a73..153c4603b 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -191,8 +191,8 @@ class SygusUnif Node getMinimalTerm(const std::vector<Node>& terms); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 813aaa2b5..be24cb9e7 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1675,6 +1675,6 @@ Node SygusUnifIo::constructBestConditional(Node ce, return conds[bestIndex]; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index d7b0e231c..5d4f7fb7d 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -466,8 +466,8 @@ class SygusUnifIo : public SygusUnif const std::vector<Node>& conds) override; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 8859ba72b..436678aa9 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1207,4 +1207,4 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 4c40e39db..82f2a80d2 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -443,6 +443,6 @@ class SygusUnifRl : public SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 3a61c5635..5551be630 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1048,6 +1048,6 @@ void SygusUnifStrategy::indent(const char* c, int ind) } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index a1d34ad4e..c9d6e5d96 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -426,8 +426,8 @@ class SygusUnifStrategy //------------------------------ end strategy registration }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 04acad0e6..ec5edd640 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -179,4 +179,4 @@ TypeNode SygusUtils::getSygusTypeForSynthFun(Node f) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 41cdb85b2..2646dd1c8 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -110,6 +110,6 @@ class SygusUtils } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 72e69afae..0bfa73048 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 CVC4::kind; +using namespace CVC5::kind; using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1353,4 +1353,4 @@ ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e) } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index efb559889..e39f65d80 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SynthConjecture } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 811730d4a..4f1a0bbbb 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -290,4 +290,4 @@ void SynthEngine::preregisterAssertion(Node n) } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 813981395..30f9c181e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -115,6 +115,6 @@ class SynthEngine : public QuantifiersModule } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 5cfc09d7c..84fcafd05 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -203,4 +203,4 @@ Node SygusTemplateInfer::getTemplateArg(Node prog) const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index a00239df9..be35025bd 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -71,6 +71,6 @@ class SygusTemplateInfer } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index e7bbc947a..f50e222ff 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1089,6 +1089,6 @@ bool TermDbSygus::isEvaluationPoint(Node n) const return true; } -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index f2188469e..0bd0c636a 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -465,8 +465,8 @@ class TermDbSygus { }; -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 543d5e7f0..0b5946176 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -585,4 +585,4 @@ Node TransitionInference::constructFormulaTrace(DetTrace& dt) const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index aa060de4e..aed003357 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -332,6 +332,6 @@ class TransitionInference } // namespace quantifiers } // namespace theory -} /* namespace CVC4 */ +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 9266a3f9d..19dff9936 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ bool SygusTypeInfo::isSubclassVarTrivial() const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 7b45d115b..cc78fc526 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -253,6 +253,6 @@ class SygusTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 93162b50e..064543af8 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -49,4 +49,4 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 020c8d086..a60afda23 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -48,6 +48,6 @@ class TypeNodeIdTrie } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 8732f1715..0b1d91684 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -553,4 +553,4 @@ void SygusInst::addCeLemma(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 402846e87..08fc5ccb3 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 CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -147,6 +147,6 @@ class SygusInst : public QuantifiersModule } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index ea530da67..2b89c0c7c 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -843,6 +843,6 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index a51f1e015..65843dc63 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -318,8 +318,8 @@ class SygusSampler : public LazyTrieEvaluator void registerSygusType(TypeNode tn); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 2d857a4d3..d6d7933cb 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1230,6 +1230,6 @@ Node TermDb::getHoTypeMatchPredicate(TypeNode tn) return k; } -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index bafaa8bdd..d0812d1d1 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -420,8 +420,8 @@ class TermDb : public QuantifiersUtil { //------------------------------end higher-order term indexing };/* class TermDb */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 0b1b1cdae..2945750c1 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -73,6 +73,6 @@ bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom) return true; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index 9cd57bfd0..fa7eaf63e 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -69,8 +69,8 @@ class TermEnumeration std::vector<TypeEnumerator> d_typ_enum; }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 74dad6cc7..cf33f0a41 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -134,4 +134,4 @@ bool TermRegistry::useFmcModel() const { return d_useFmcModel; } } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index d70b7acf8..e4e4a7e9f 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -99,6 +99,6 @@ class TermRegistry } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 209196110..546f6aa6c 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h index 28831baf5..b15ab2212 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -94,5 +94,5 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // 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 daf291d18..41e06a708 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -599,6 +599,6 @@ bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok) return false; } -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 6fd9d32d6..1ac6ca495 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 CVC4 { +namespace CVC5 { namespace theory { // attribute for "contains instantiation constants from" @@ -204,8 +204,8 @@ public: static Node mkTypeConst(TypeNode tn, bool pol); };/* class TermUtil */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 ace7b79ff..d89abf076 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 CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 91f12c0ed..6af0e8648 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -96,8 +96,8 @@ class TheoryQuantifiers : public Theory { std::unique_ptr<QuantifiersEngine> d_qengine; };/* class TheoryQuantifiers */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // 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 6758cde28..e990f5320 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 CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -129,8 +129,8 @@ struct QuantifierInstPatternListTypeRule { } };/* struct QuantifierInstPatternListTypeRule */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ |