diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/quantifiers/sygus | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/theory/quantifiers/sygus')
78 files changed, 194 insertions, 194 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 0acd7e718..5e9f2d591 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -32,9 +32,9 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -548,4 +548,4 @@ bool CegSingleInv::solveTrivial(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index e2f399ffd..ca83bf973 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/sygus_stats.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -178,6 +178,6 @@ class CegSingleInv } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index d980db887..52adc1972 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -24,10 +24,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -706,4 +706,4 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index a12133d23..f728d3d7e 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus_sampler.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -227,6 +227,6 @@ class Cegis : public SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 26ad62c90..6e47c2d89 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -28,9 +28,9 @@ #include "theory/smt_engine_subsolver.h" #include "util/random.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -861,4 +861,4 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 59bf53317..2abce835a 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { class SmtEngine; @@ -399,6 +399,6 @@ class CegisCoreConnective : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index bcd9fa67a..9a5c6146d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -21,9 +21,9 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -686,4 +686,4 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index e00370f2a..a543bfda0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -333,6 +333,6 @@ class CegisUnif : public Cegis } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 17f2a0c16..2bf8b4611 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -24,9 +24,9 @@ #include <numeric> // for std::iota -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -621,4 +621,4 @@ bool EnumStreamConcrete::increment() Node EnumStreamConcrete::getCurrent() { return d_currTerm; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index c7e4720d2..a72481a38 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -299,6 +299,6 @@ class EnumStreamConcrete : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index 5056fb96d..aea6cb9ef 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.cpp +++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp @@ -17,10 +17,10 @@ #include "theory/quantifiers/sygus/example_min_eval.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -119,4 +119,4 @@ void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 97ec38ab5..1a70369a5 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -20,7 +20,7 @@ #include "expr/node_trie.h" #include "theory/quantifiers/sygus/example_infer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -160,6 +160,6 @@ class ExampleEvalCache } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp index 12e4f073e..9dc99cab1 100644 --- a/src/theory/quantifiers/sygus/example_infer.cpp +++ b/src/theory/quantifiers/sygus/example_infer.cpp @@ -17,10 +17,10 @@ #include "theory/quantifiers/quant_util.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -275,4 +275,4 @@ bool ExampleInfer::hasExamplesOut(Node f) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 0e5ee25ac..dd2bf8a0a 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -157,6 +157,6 @@ class ExampleInfer } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp index 4cb9bd345..5b3ccec4f 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.cpp +++ b/src/theory/quantifiers/sygus/example_min_eval.cpp @@ -18,7 +18,7 @@ #include "expr/node_algorithm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -84,4 +84,4 @@ Node EmeEvalTds::eval(TNode n, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 9af07caba..2105faf2b 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.h +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "expr/node_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -118,6 +118,6 @@ class EmeEvalTds : public EmeEval } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp index 7d4a41f2d..6db446dbb 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp @@ -17,7 +17,7 @@ #include "expr/node_algorithm.h" #include "theory/datatypes/sygus_datatype_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -97,4 +97,4 @@ void RConsObligationInfo::printCandSols( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index e05422b59..3bded2a90 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -145,6 +145,6 @@ class RConsObligationInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index 37b136a1c..97ae4878d 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -16,7 +16,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -69,4 +69,4 @@ Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; } } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index c2bce5720..974897023 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -97,6 +97,6 @@ class RConsTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 71853fc76..8df45320f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -29,9 +29,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -187,4 +187,4 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index ffcefd38b..634a9a4bd 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class SygusAbduct } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index c786d2668..82d0c6c62 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -24,9 +24,9 @@ #include "theory/quantifiers/sygus/type_node_id_trie.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1214,4 +1214,4 @@ bool SygusEnumerator::TermEnumMasterFv::increment() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index a0d1c9b62..f1ef115f8 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -506,6 +506,6 @@ class SygusEnumerator : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp index 51814b07c..e9f41c916 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp @@ -15,10 +15,10 @@ #include "options/datatypes_options.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -55,4 +55,4 @@ bool EnumValGeneratorBasic::increment() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index c57d6f814..1f489eafc 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -65,6 +65,6 @@ class EnumValGeneratorBasic : public EnumValGenerator } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 3e87ccfc7..5dbd7655f 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -22,10 +22,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; -using namespace CVC5::context; +using namespace cvc5::kind; +using namespace cvc5::context; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -333,4 +333,4 @@ Node SygusEvalUnfold::unfold(Node en) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index d5e47edbc..628f01c40 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/sygus_invariance.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -154,6 +154,6 @@ class SygusEvalUnfold } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 26fab8535..95acce626 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -21,10 +21,10 @@ #include "theory/quantifiers/sygus/sygus_invariance.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -357,4 +357,4 @@ void SygusExplain::getExplanationFor(Node n, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 1b1db568f..477857794 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -241,6 +241,6 @@ class SygusExplain } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 554f587c7..1c96b1346 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -30,9 +30,9 @@ #include "theory/rewriter.h" #include "theory/strings/word.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1622,4 +1622,4 @@ bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index a39540452..56f469fef 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -25,7 +25,7 @@ #include "expr/node.h" #include "expr/sygus_datatype.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** @@ -266,6 +266,6 @@ public: } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index fa67e17c4..8a2ad109d 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -31,9 +31,9 @@ #include <numeric> // for std::iota -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -536,4 +536,4 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 8c057d2c5..eda34a251 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -25,7 +25,7 @@ #include "expr/sygus_datatype.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SygusGrammarNorm } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 8e6f4fbae..a8ada94ed 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -176,4 +176,4 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 25256a68c..2144102e0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -118,6 +118,6 @@ class SygusRedundantCons } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 1c856ffa2..fe286d15c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -27,7 +27,7 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -358,4 +358,4 @@ bool SygusInterpol::solveInterpolation(const std::string& name, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 34517b6e6..c63d096b8 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -23,7 +23,7 @@ #include "expr/type_node.h" #include "smt/smt_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { /** @@ -213,6 +213,6 @@ class SygusInterpol } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 7e6c5ab6c..22ef38b0d 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -19,10 +19,10 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -261,4 +261,4 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 88e45df45..df2e189e3 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -298,6 +298,6 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 8dac30c7e..3f2bea9cb 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -27,4 +27,4 @@ SygusModule::SygusModule(QuantifiersInferenceManager& qim, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 32f404005..90460eeed 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -157,6 +157,6 @@ class SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 25068eb7d..b54b1c940 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/term_util.h" #include "util/random.h" -using namespace CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -258,4 +258,4 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index c63dcf697..a56a22838 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -19,7 +19,7 @@ #include "theory/quantifiers/sygus/sygus_module.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -168,6 +168,6 @@ class SygusPbe : public SygusModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index dfb0a0f7c..822d19f29 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -804,4 +804,4 @@ void SynthConjectureProcess::getComponentVector(Kind k, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 0b07db89b..6f6e25d0c 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -26,7 +26,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -358,6 +358,6 @@ class SynthConjectureProcess } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 72ce3f1ab..1b3a52db8 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -19,9 +19,9 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -144,4 +144,4 @@ Node SygusQePreproc::preprocess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 49f81df02..26bbf2f92 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -45,6 +45,6 @@ class SygusQePreproc } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 723d924f8..55e8c922d 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -19,9 +19,9 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ void SygusReconstruct::printPool( } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 0512fe643..1f9037a26 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/sygus/rcons_obligation_info.h" #include "theory/quantifiers/sygus/rcons_type_info.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -307,6 +307,6 @@ class SygusReconstruct : public expr::NotifyMatch } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 2d7dfc4bc..179798222 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -29,9 +29,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -621,4 +621,4 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 1e7eeb9fc..b79fa4177 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -20,7 +20,7 @@ #include <unordered_set> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class LogicInfo; @@ -209,6 +209,6 @@ class SygusRepairConst } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index da08ec1b5..11dec3e61 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -17,7 +17,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -60,4 +60,4 @@ SygusStatistics::~SygusStatistics() } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index d89fa0eca..7a8ae8ce9 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -19,7 +19,7 @@ #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -53,6 +53,6 @@ class SygusStatistics } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 8eb13fef8..2d72b4fab 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -19,9 +19,9 @@ #include "util/random.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -136,4 +136,4 @@ void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 153c4603b..1ed81194a 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/sygus_unif_strat.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -193,6 +193,6 @@ class SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index be24cb9e7..9dfac1d68 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -26,9 +26,9 @@ #include <math.h> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1677,4 +1677,4 @@ Node SygusUnifIo::constructBestConditional(Node ce, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 5d4f7fb7d..825e5741d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -20,7 +20,7 @@ #include <map> #include "theory/quantifiers/sygus/sygus_unif.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -468,6 +468,6 @@ class SygusUnifIo : public SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 436678aa9..c3cff70d9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -24,9 +24,9 @@ #include <math.h> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1207,4 +1207,4 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 82f2a80d2..51c49cbef 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/lazy_trie.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -443,6 +443,6 @@ class SygusUnifRl : public SygusUnif } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 5551be630..24bcb1eab 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -24,9 +24,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1050,4 +1050,4 @@ void SygusUnifStrategy::indent(const char* c, int ind) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index c9d6e5d96..2508fdc9b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -20,7 +20,7 @@ #include <map> #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -428,6 +428,6 @@ class SygusUnifStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index ec5edd640..6c14aaa80 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -179,4 +179,4 @@ TypeNode SygusUtils::getSygusTypeForSynthFun(Node f) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 2646dd1c8..0ec497789 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.h +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/subs.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -110,6 +110,6 @@ class SygusUtils } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0bfa73048..f7566e7a2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -37,10 +37,10 @@ #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC5::kind; +using namespace cvc5::kind; using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1353,4 +1353,4 @@ ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index e39f65d80..7fd1ae4b3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -32,7 +32,7 @@ #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/template_infer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -426,6 +426,6 @@ class SynthConjecture } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 4f1a0bbbb..3d5406f27 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_registry.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -290,4 +290,4 @@ void SynthEngine::preregisterAssertion(Node n) } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 30f9c181e..a5fde8476 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -115,6 +115,6 @@ class SynthEngine : public QuantifiersModule } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 84fcafd05..875b25370 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers/term_util.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -203,4 +203,4 @@ Node SygusTemplateInfer::getTemplateArg(Node prog) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index be35025bd..1ab97b651 100644 --- a/src/theory/quantifiers/sygus/template_infer.h +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/transition_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -71,6 +71,6 @@ class SygusTemplateInfer } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index f50e222ff..34a81467a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -30,9 +30,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -1091,4 +1091,4 @@ bool TermDbSygus::isEvaluationPoint(Node n) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 0bd0c636a..fb7e38ff8 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -28,7 +28,7 @@ #include "theory/quantifiers/sygus/type_info.h" #include "theory/quantifiers/term_database.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -467,6 +467,6 @@ class TermDbSygus { } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 0b5946176..7ee2f2ec6 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -585,4 +585,4 @@ Node TransitionInference::constructFormulaTrace(DetTrace& dt) const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index aed003357..8ddc1a320 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -27,7 +27,7 @@ #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/single_inv_partition.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -332,6 +332,6 @@ class TransitionInference } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 19dff9936..fdc8ca6a3 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -22,9 +22,9 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus/type_node_id_trie.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -488,4 +488,4 @@ bool SygusTypeInfo::isSubclassVarTrivial() const } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index cc78fc526..79413a03c 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -253,6 +253,6 @@ class SygusTypeInfo } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */ diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.cpp b/src/theory/quantifiers/sygus/type_node_id_trie.cpp index 064543af8..a2c7b264d 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.cpp +++ b/src/theory/quantifiers/sygus/type_node_id_trie.cpp @@ -14,9 +14,9 @@ #include "theory/quantifiers/sygus/type_node_id_trie.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -49,4 +49,4 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign, } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h index a60afda23..6311cbabe 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace quantifiers { @@ -48,6 +48,6 @@ class TypeNodeIdTrie } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */ |