diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
78 files changed, 246 insertions, 246 deletions
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 */ |