diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
34 files changed, 93 insertions, 93 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 60350f882..4c9da3632 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -24,9 +24,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -348,4 +348,4 @@ Node CandidateGeneratorSelector::getNextCandidate() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 45eec1d4c..b21a96225 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -20,7 +20,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -240,9 +240,9 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE Node d_ufOp; }; -}/* CVC4::theory::inst namespace */ +} // namespace inst } // namespace quantifiers -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index a267246a8..14f514b73 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -25,9 +25,9 @@ #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -526,4 +526,4 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index d3489783c..66b374ea8 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -275,6 +275,6 @@ class HigherOrderTrigger : public Trigger } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp index 06d17dea4..2f415779a 100644 --- a/src/theory/quantifiers/ematching/im_generator.cpp +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/ematching/trigger.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -36,4 +36,4 @@ bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index b277ec180..b0d937120 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -22,7 +22,7 @@ #include "theory/inference_id.h" #include "theory/quantifiers/inst_match.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -117,6 +117,6 @@ protected: } // namespace inst } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 04b8a3fcf..79b6927f7 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -29,9 +29,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -673,4 +673,4 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 375fe73e1..32d6e38f1 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/ematching/im_generator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -325,6 +325,6 @@ class InstMatchGenerator : public IMGenerator { } // namespace inst } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index fe0fa8082..6ac910e2e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -18,9 +18,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/uf/equality_engine_iterator.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -315,4 +315,4 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 1e25baea4..644a47bee 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/inst_match_trie.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -103,6 +103,6 @@ class InstMatchGeneratorMulti : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 18708092a..94b7921ed 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -17,9 +17,9 @@ #include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -175,4 +175,4 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index b46960400..00a372c8f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -85,6 +85,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index ab30b4b2d..7d7b3e1c0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -21,9 +21,9 @@ #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -198,4 +198,4 @@ int InstMatchGeneratorSimple::getActiveScore() } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 6ae2f915b..8361628da 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -23,7 +23,7 @@ #include "expr/node_trie.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -100,6 +100,6 @@ class InstMatchGeneratorSimple : public IMGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp index 5e9899ec3..a56e7efeb 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers/quantifiers_state.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -44,4 +44,4 @@ options::UserPatMode InstStrategy::getInstUserPatMode() const } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 9d304368c..0537d92ce 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -22,7 +22,7 @@ #include "options/quantifiers_options.h" #include "theory/theory.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -85,6 +85,6 @@ class InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 45d5f13a7..c62a034e4 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -22,10 +22,10 @@ #include "theory/quantifiers/quantifiers_state.h" #include "util/random.h" -using namespace CVC4::kind; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -686,6 +686,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { } } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index a17e7bbb5..bc52d605c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_relevance.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -111,7 +111,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy QuantRelevance* d_quant_rel; }; /* class InstStrategyAutoGenTriggers */ } -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index a15baa5e4..4b0d619bc 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -18,10 +18,10 @@ #include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quantifiers_state.h" -using namespace CVC4::kind; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -175,4 +175,4 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 821d7de77..1bb50af7b 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -23,7 +23,7 @@ #include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -64,6 +64,6 @@ class InstStrategyUserPatterns : public InstStrategy } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 52bf58263..94054b8f9 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -23,11 +23,11 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory::quantifiers::inst; +using namespace CVC5::kind; +using namespace CVC5::context; +using namespace CVC5::theory::quantifiers::inst; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -272,4 +272,4 @@ bool InstantiationEngine::shouldProcess(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index c5a82d114..8dface27e 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_relevance.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -73,8 +73,8 @@ class InstantiationEngine : public QuantifiersModule { std::unique_ptr<QuantRelevance> d_quant_rel; }; /* class InstantiationEngine */ -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 7ab54fcfe..467ed46be 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -20,9 +20,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -729,4 +729,4 @@ void PatternTermSelector::getTriggerVariables(Node n, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index 9cbf4cf5e..6f26f2cec 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -23,7 +23,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -192,6 +192,6 @@ class PatternTermSelector } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index c739623bc..234940b54 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -32,9 +32,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/valuation.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -229,4 +229,4 @@ void Trigger::debugPrint(const char* c) const } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 5dd8db452..c6d3b3cd5 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/inference_id.h" -namespace CVC4 { +namespace CVC5 { namespace theory { class QuantifiersEngine; @@ -219,6 +219,6 @@ class Trigger { } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp index fae7a10a0..327d2bba1 100644 --- a/src/theory/quantifiers/ematching/trigger_database.cpp +++ b/src/theory/quantifiers/ematching/trigger_database.cpp @@ -18,7 +18,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_util.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -185,4 +185,4 @@ bool TriggerDatabase::mkTriggerTerms(Node q, } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 21df0e536..2c28c77bc 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/trigger_trie.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -105,6 +105,6 @@ class TriggerDatabase } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */ diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 4bc74dd96..1f3ca0577 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/term_util.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -114,4 +114,4 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 5bf7e8099..603a1ab77 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -124,6 +124,6 @@ class TriggerTermInfo } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp index 04e9dabb0..c8a13d447 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.cpp +++ b/src/theory/quantifiers/ematching/trigger_trie.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/ematching/trigger_trie.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -74,4 +74,4 @@ void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index ad221ee21..355ad6c31 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/trigger.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -58,6 +58,6 @@ class TriggerTrie } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */ diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 45c9e20d7..e2dd3f37d 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -16,9 +16,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -81,4 +81,4 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m) } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index d85a20189..6ee179e91 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace inst { @@ -53,6 +53,6 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator } // namespace inst } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif |