diff options
Diffstat (limited to 'src/theory/strings')
62 files changed, 253 insertions, 249 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index f8abc9aef..36ead8685 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -22,9 +22,9 @@ #include "theory/strings/word.h" #include "theory/theory.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -866,4 +866,4 @@ bool ArithEntail::inferZerosInSumGeq(Node x, } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index cd933ad26..22011d51b 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -175,6 +175,6 @@ class ArithEntail } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 8a8abbf81..b9802b9a5 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -22,10 +22,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -760,4 +760,4 @@ Node BaseSolver::TermIndex::add(TNode n, } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 76273c747..43cb63b47 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -26,7 +26,7 @@ #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -243,6 +243,6 @@ class BaseSolver } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */ diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 3c5bcc98d..8593a1e36 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -26,10 +26,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -2649,6 +2649,6 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii) return true; } -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 94f47f6c3..53bb167c4 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -27,7 +27,7 @@ #include "theory/strings/solver_state.h" #include "theory/strings/term_registry.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -523,6 +523,6 @@ class CoreSolver } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__CORE_SOLVER_H */ diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp index be122f869..e2cb01408 100644 --- a/src/theory/strings/eager_solver.cpp +++ b/src/theory/strings/eager_solver.cpp @@ -16,9 +16,9 @@ #include "theory/strings/theory_strings_utils.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -148,4 +148,4 @@ void EagerSolver::notifyFact(TNode atom, } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h index b30968e0b..49545e622 100644 --- a/src/theory/strings/eager_solver.h +++ b/src/theory/strings/eager_solver.h @@ -23,7 +23,7 @@ #include "theory/strings/eqc_info.h" #include "theory/strings/solver_state.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -63,6 +63,6 @@ class EagerSolver } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__EAGER_SOLVER_H */ diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp index 81515fc54..0bb2defb6 100644 --- a/src/theory/strings/eqc_info.cpp +++ b/src/theory/strings/eqc_info.cpp @@ -18,10 +18,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -139,4 +139,4 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index 842360f5d..a00cd49ea 100644 --- a/src/theory/strings/eqc_info.h +++ b/src/theory/strings/eqc_info.h @@ -23,7 +23,7 @@ #include "context/context.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -76,6 +76,6 @@ class EqcInfo } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */ diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index d721abf71..ab7c1d0ac 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -20,10 +20,10 @@ #include "theory/strings/theory_strings_utils.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -724,4 +724,4 @@ bool StringsExtfCallback::getCurrentSubstitution( } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 10e380e94..4b63f261a 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -32,7 +32,7 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -227,6 +227,6 @@ class StringsExtfCallback : public ExtTheoryCallback } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */ diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 8d276d60e..5e2006f65 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -17,7 +17,7 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -90,4 +90,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index af415ecd9..9c228c197 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -25,7 +25,7 @@ #include "theory/theory_inference.h" #include "util/safe_print.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -131,6 +131,6 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii); } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */ diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index a02566a41..c600ce31d 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -23,9 +23,9 @@ #include "theory/strings/regexp_operation.h" #include "theory/strings/theory_strings_utils.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -1042,4 +1042,4 @@ std::string InferProofCons::identify() const } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 7484959b8..7d7d7e54a 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -28,7 +28,7 @@ #include "theory/theory_proof_step_buffer.h" #include "theory/uf/proof_equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -130,6 +130,6 @@ class InferProofCons : public ProofGenerator } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */ diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0d4839238..15e608ef1 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -21,10 +21,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -377,4 +377,4 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 9fbe10637..1e57afe79 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -35,7 +35,7 @@ #include "theory/theory_inference_manager.h" #include "theory/uf/equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -271,6 +271,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 427e2e4e6..6f366d6d7 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -4,11 +4,11 @@ # src/theory/builtin/kinds. # -theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" +theory THEORY_STRINGS ::CVC5::theory::strings::TheoryStrings "theory/strings/theory_strings.h" properties check parametric presolve -rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" +rewriter ::CVC5::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" typechecker "theory/strings/theory_strings_type_rules.h" @@ -42,7 +42,7 @@ operator STRING_REV 1 "string reverse" sort STRING_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkConst(::CVC4::String())" \ + "NodeManager::currentNM()->mkConst(::CVC5::String())" \ "util/string.h" \ "String type" @@ -54,31 +54,31 @@ sort REGEXP_TYPE \ "RegExp type" enumerator STRING_TYPE \ - "::CVC4::theory::strings::StringEnumerator" \ + "::CVC5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::CVC4::String \ - ::CVC4::strings::StringHashFunction \ + ::CVC5::String \ + ::CVC5::strings::StringHashFunction \ "util/string.h" \ "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" cardinality SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ "theory/strings/theory_strings_type_rules.h" well-founded SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ + "::CVC5::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ "theory/strings/theory_strings_type_rules.h" enumerator SEQUENCE_TYPE \ - "::CVC4::theory::strings::SequenceEnumerator" \ + "::CVC5::theory::strings::SequenceEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::CVC4::Sequence \ - ::CVC4::SequenceHashFunction \ + ::CVC5::Sequence \ + ::CVC5::SequenceHashFunction \ "expr/sequence.h" \ "a sequence of characters" @@ -102,17 +102,17 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::CVC4::RegExpRepeat \ - ::CVC4::RegExpRepeatHashFunction \ + ::CVC5::RegExpRepeat \ + ::CVC5::RegExpRepeatHashFunction \ "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the CVC4::RegExpRepeat class" + "operator for regular expression repeat; payload is an instance of the CVC5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::CVC4::RegExpLoop \ - ::CVC4::RegExpLoopHashFunction \ + ::CVC5::RegExpLoop \ + ::CVC5::RegExpLoopHashFunction \ "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the CVC4::RegExpLoop class" + "operator for regular expression loop; payload is an instance of the CVC5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal @@ -128,7 +128,7 @@ typerule REGEXP_DIFF "SimpleTypeRuleVar<RRegExp, ARegExp>" typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>" -typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule +typerule REGEXP_RANGE ::CVC5::theory::strings::RegExpRangeTypeRule typerule REGEXP_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>" typerule REGEXP_REPEAT "SimpleTypeRule<RRegExp, ARegExp>" typerule REGEXP_LOOP_OP "SimpleTypeRule<RBuiltinOperator>" @@ -141,18 +141,18 @@ typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>" ### operators that apply to both strings and sequences -typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule -typerule STRING_LENGTH ::CVC4::theory::strings::StringStrToIntTypeRule -typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule -typerule STRING_UPDATE ::CVC4::theory::strings::StringUpdateTypeRule -typerule STRING_CHARAT ::CVC4::theory::strings::StringAtTypeRule -typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule -typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule -typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule -typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule -typerule STRING_PREFIX ::CVC4::theory::strings::StringStrToBoolTypeRule -typerule STRING_SUFFIX ::CVC4::theory::strings::StringStrToBoolTypeRule -typerule STRING_REV ::CVC4::theory::strings::StringStrToStrTypeRule +typerule STRING_CONCAT ::CVC5::theory::strings::StringConcatTypeRule +typerule STRING_LENGTH ::CVC5::theory::strings::StringStrToIntTypeRule +typerule STRING_SUBSTR ::CVC5::theory::strings::StringSubstrTypeRule +typerule STRING_UPDATE ::CVC5::theory::strings::StringUpdateTypeRule +typerule STRING_CHARAT ::CVC5::theory::strings::StringAtTypeRule +typerule STRING_STRCTN ::CVC5::theory::strings::StringRelationTypeRule +typerule STRING_STRIDOF ::CVC5::theory::strings::StringIndexOfTypeRule +typerule STRING_STRREPL ::CVC5::theory::strings::StringReplaceTypeRule +typerule STRING_STRREPLALL ::CVC5::theory::strings::StringReplaceTypeRule +typerule STRING_PREFIX ::CVC5::theory::strings::StringStrToBoolTypeRule +typerule STRING_SUFFIX ::CVC5::theory::strings::StringStrToBoolTypeRule +typerule STRING_REV ::CVC5::theory::strings::StringStrToStrTypeRule ### string specific operators @@ -169,9 +169,9 @@ typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" ### sequence specific operators -typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule -typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule -typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule -typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule +typerule CONST_SEQUENCE ::CVC5::theory::strings::ConstSequenceTypeRule +typerule SEQ_UNIT ::CVC5::theory::strings::SeqUnitTypeRule +typerule SEQ_NTH ::CVC5::theory::strings::SeqNthTypeRule +typerule SEQ_NTH_TOTAL ::CVC5::theory::strings::SeqNthTypeRule endtheory diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 5cc101a9f..c139a5da7 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -21,9 +21,9 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -185,4 +185,4 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi, } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h index cadaa2c6e..65d4b3f78 100644 --- a/src/theory/strings/normal_form.h +++ b/src/theory/strings/normal_form.h @@ -21,7 +21,7 @@ #include <vector> #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -168,6 +168,6 @@ class NormalForm } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */ diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 5cae7c69f..bf82d16ce 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -25,9 +25,9 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -517,4 +517,4 @@ Node StringProofRuleChecker::checkInternal(PfRule id, } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index 5f6b779c0..c55386140 100644 --- a/src/theory/strings/proof_checker.h +++ b/src/theory/strings/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -44,6 +44,6 @@ class StringProofRuleChecker : public ProofRuleChecker } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index de67fc9bf..5dbe02230 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -21,9 +21,9 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -613,4 +613,4 @@ bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 9c9733a95..3ffa9566e 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -21,7 +21,7 @@ #include "theory/eager_proof_generator.h" #include "theory/trust_node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -85,6 +85,6 @@ class RegExpElimination } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__REGEXP_ELIM_H */ diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 0e4d6dd8e..94c740742 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -19,9 +19,9 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -105,7 +105,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren, else if (xc.isConst()) { // check for constants - CVC4::String s = xc.getConst<String>(); + CVC5::String s = xc.getConst<String>(); if (Word::isEmpty(xc)) { Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl; @@ -117,7 +117,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren, { std::vector<unsigned> ssVec; ssVec.push_back(t == 0 ? s.back() : s.front()); - CVC4::String ss(ssVec); + CVC5::String ss(ssVec); if (testConstStringInRegExp(ss, 0, rc)) { // strip off one character @@ -345,7 +345,7 @@ bool RegExpEntail::isConstRegExp(TNode t) return true; } -bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, +bool RegExpEntail::testConstStringInRegExp(CVC5::String& s, unsigned index_start, TNode r) { @@ -358,7 +358,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, { case STRING_TO_REGEXP: { - CVC4::String s2 = s.substr(index_start, s.size() - index_start); + CVC5::String s2 = s.substr(index_start, s.size() - index_start); if (r[0].isConst()) { return (s2 == r[0].getConst<String>()); @@ -392,7 +392,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, { for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) { - CVC4::String t = s.substr(index_start + start, vec_k[i]); + CVC5::String t = s.substr(index_start + start, vec_k[i]); if (testConstStringInRegExp(t, 0, r[i])) { start += vec_k[i]; @@ -457,7 +457,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, { for (unsigned i = s.size() - index_start; i > 0; --i) { - CVC4::String t = s.substr(index_start, i); + CVC5::String t = s.substr(index_start, i); if (testConstStringInRegExp(t, 0, r[0])) { if (index_start + i == s.size() @@ -525,7 +525,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); for (unsigned len = s.size() - index_start; len >= 1; len--) { - CVC4::String t = s.substr(index_start, len); + CVC5::String t = s.substr(index_start, len); if (testConstStringInRegExp(t, 0, r[0])) { if (len + index_start == s.size()) @@ -534,7 +534,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, } else { - Node num2 = nm->mkConst(CVC4::Rational(u - 1)); + Node num2 = nm->mkConst(CVC5::Rational(u - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -563,10 +563,10 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, } for (unsigned len = 1; len <= s.size() - index_start; len++) { - CVC4::String t = s.substr(index_start, len); + CVC5::String t = s.substr(index_start, len); if (testConstStringInRegExp(t, 0, r[0])) { - Node num2 = nm->mkConst(CVC4::Rational(l - 1)); + Node num2 = nm->mkConst(CVC5::Rational(l - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -761,4 +761,4 @@ bool RegExpEntail::regExpIncludes(Node r1, Node r2) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index f4359aa76..3e14d4ed0 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -26,7 +26,7 @@ #include "theory/theory_rewriter.h" #include "theory/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -97,7 +97,7 @@ class RegExpEntail * Does the substring of s starting at index_start occur in constant regular * expression r? */ - static bool testConstStringInRegExp(CVC4::String& s, + static bool testConstStringInRegExp(CVC5::String& s, unsigned index_start, TNode r); /** Does regular expression node have (str.to.re "") as a child? */ @@ -127,6 +127,6 @@ class RegExpEntail } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H */ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index ad71e98fd..5481a0c6d 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -25,9 +25,9 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -36,8 +36,8 @@ RegExpOpr::RegExpOpr(SkolemCache* sc) d_false(NodeManager::currentNM()->mkConst(false)), d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY, std::vector<Node>{})), - d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), - d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))), + d_zero(NodeManager::currentNM()->mkConst(::CVC5::Rational(0))), + d_one(NodeManager::currentNM()->mkConst(::CVC5::Rational(1))), d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, std::vector<Node>{})), d_sigma_star( @@ -266,7 +266,8 @@ int RegExpOpr::delta( Node r, Node &exp ) { } // 0-unknown, 1-yes, 2-no -int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { +int RegExpOpr::derivativeS(Node r, CVC5::String c, Node& retNode) +{ Assert(c.size() < 2); Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl; @@ -301,8 +302,8 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { break; } case kind::REGEXP_RANGE: { - CVC4::String a = r[0].getConst<String>(); - CVC4::String b = r[1].getConst<String>(); + CVC5::String a = r[0].getConst<String>(); + CVC5::String b = r[1].getConst<String>(); retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp; break; } @@ -520,7 +521,8 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { return ret; } -Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { +Node RegExpOpr::derivativeSingle(Node r, CVC5::String c) +{ Assert(c.size() < 2); Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl; Node retNode = d_emptyRegexp; @@ -553,8 +555,8 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { break; } case kind::REGEXP_RANGE: { - CVC4::String a = r[0].getConst<String>(); - CVC4::String b = r[1].getConst<String>(); + CVC5::String a = r[0].getConst<String>(); + CVC5::String b = r[1].getConst<String>(); retNode = (a <= c && c <= b) ? d_emptySingleton : d_emptyRegexp; break; } @@ -1310,7 +1312,9 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > rt = itr2->second; } else { std::map< PairNodes, Node > cache2(cache); - cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt))); + cache2[p] = NodeManager::currentNM()->mkNode( + kind::REGEXP_RV, + NodeManager::currentNM()->mkConst(CVC5::Rational(cnt))); rt = intersectInternal(r1l, r2l, cache2, cnt+1); cacheX[ pp ] = rt; } @@ -1613,6 +1617,6 @@ Node RegExpOpr::getExistsForRegExpConcatMem(Node mem) return eform; } -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 8c0cd6c14..27324d971 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -28,7 +28,7 @@ #include "theory/strings/skolem_cache.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -55,7 +55,7 @@ enum RegExpConstType }; class RegExpOpr { - typedef std::pair< Node, CVC4::String > PairNodeStr; + typedef std::pair<Node, CVC5::String> PairNodeStr; typedef std::set< Node > SetNodes; typedef std::pair< Node, Node > PairNodes; @@ -171,8 +171,8 @@ class RegExpOpr { * - delta( (re.union (re.* "A") R) ) returns 1. */ int delta( Node r, Node &exp ); - int derivativeS( Node r, CVC4::String c, Node &retNode ); - Node derivativeSingle( Node r, CVC4::String c ); + int derivativeS(Node r, CVC5::String c, Node& retNode); + Node derivativeSingle(Node r, CVC5::String c); /** * Returns the regular expression intersection of r1 and r2. If r1 or r2 is * not constant, then this method returns null. @@ -207,8 +207,8 @@ class RegExpOpr { SkolemCache* d_sc; }; -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index f252196d8..861f7c694 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -25,10 +25,10 @@ #include "theory/theory_model.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -48,7 +48,7 @@ RegExpSolver::RegExpSolver(SolverState& s, d_processed_memberships(s.getSatContext()), d_regexp_opr(skc) { - d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String("")); + d_emptyString = NodeManager::currentNM()->mkConst(::CVC5::String("")); std::vector<Node> nvec; d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY, nvec); d_true = NodeManager::currentNM()->mkConst(true); @@ -582,7 +582,7 @@ bool RegExpSolver::checkPDerivative( return true; } -CVC4::String RegExpSolver::getHeadConst(Node x) +CVC5::String RegExpSolver::getHeadConst(Node x) { if (x.isConst()) { @@ -606,7 +606,7 @@ bool RegExpSolver::deriveRegExp(Node x, Assert(x != d_emptyString); Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x << ", r= " << r << std::endl; - CVC4::String s = getHeadConst(x); + CVC5::String s = getHeadConst(x); // only allow RE_DERIVE for concrete constant regular expressions if (!s.empty() && d_regexp_opr.getRegExpConstType(r) == RE_C_CONRETE_CONSTANT) { @@ -615,7 +615,7 @@ bool RegExpSolver::deriveRegExp(Node x, bool flag = true; for (unsigned i = 0; i < s.size(); ++i) { - CVC4::String c = s.substr(i, 1); + CVC5::String c = s.substr(i, 1); Node dc2; int rt = d_regexp_opr.derivativeS(dc, c, dc2); dc = dc2; @@ -706,4 +706,4 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 50e58140d..d35a822a7 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -31,7 +31,7 @@ #include "theory/strings/solver_state.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -137,7 +137,7 @@ class RegExpSolver Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp); Node getMembership(Node n, bool isPos, unsigned i); unsigned getNumMemberships(Node n, bool isPos); - CVC4::String getHeadConst(Node x); + CVC5::String getHeadConst(Node x); bool deriveRegExp(Node x, Node r, Node atom, std::vector<Node>& ant); Node getNormalSymRegExp(Node r, std::vector<Node>& nf_exp); // regular expression memberships @@ -154,6 +154,6 @@ class RegExpSolver } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index 9788bc173..cdf41d9ad 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -224,4 +224,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 26e3629ff..af9b636cf 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -239,6 +239,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__REWRITES_H */ diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index c54cdfb50..9cec9ad40 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -27,9 +27,9 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -1028,7 +1028,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node) return returnRewrite(node, r, Rewrite::RE_LOOP_STAR); } NodeManager* nm = NodeManager::currentNM(); - CVC4::Rational rMaxInt(String::maxSize()); + CVC5::Rational rMaxInt(String::maxSize()); uint32_t l = utils::getLoopMinOccurrences(node); std::vector<Node> vec_nodes; for (unsigned i = 0; i < l; i++) @@ -1141,7 +1141,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) else if (x.isConst() && RegExpEntail::isConstRegExp(r)) { // test whether x in node[1] - CVC4::String s = x.getConst<String>(); + CVC5::String s = x.getConst<String>(); bool test = RegExpEntail::testConstStringInRegExp(s, 0, r); Node retNode = NodeManager::currentNM()->mkConst(test); return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL); @@ -1571,7 +1571,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) if (node[1].isConst() && node[2].isConst()) { Node s = node[0]; - CVC4::Rational rMaxInt(String::maxSize()); + CVC5::Rational rMaxInt(String::maxSize()); uint32_t start; if (node[1].getConst<Rational>() > rMaxInt) { @@ -1628,7 +1628,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } } - Node zero = nm->mkConst(CVC4::Rational(0)); + Node zero = nm->mkConst(CVC5::Rational(0)); // if entailed non-positive length or negative start point if (ArithEntail::check(zero, node[1], true)) @@ -1858,7 +1858,7 @@ Node SequencesRewriter::rewriteUpdate(Node node) // rewriting for constant arguments if (node[1].isConst()) { - CVC4::Rational rMaxInt(String::maxSize()); + CVC5::Rational rMaxInt(String::maxSize()); if (node[1].getConst<Rational>() > rMaxInt) { // start beyond the maximum size of strings @@ -2266,7 +2266,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) utils::getConcat(node[0], children0); if (children0[0].isConst() && node[1].isConst() && node[2].isConst()) { - CVC4::Rational rMaxInt(CVC4::String::maxSize()); + CVC5::Rational rMaxInt(CVC5::String::maxSize()); if (node[2].getConst<Rational>() > rMaxInt) { // We know that, due to limitations on the size of string constants @@ -3230,7 +3230,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node val; if (isPrefix) { - val = NodeManager::currentNM()->mkConst(::CVC4::Rational(0)); + val = NodeManager::currentNM()->mkConst(::CVC5::Rational(0)); } else { @@ -3396,4 +3396,4 @@ Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 9f5b002af..750589f72 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -26,7 +26,7 @@ #include "theory/strings/strings_entail.h" #include "theory/theory_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -296,6 +296,6 @@ class SequencesRewriter : public TheoryRewriter } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H */ diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index c679bc414..919b950ab 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -63,4 +63,4 @@ SequencesStatistics::~SequencesStatistics() } } -} +} // namespace CVC5 diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 1a0e94cdb..417f79046 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -23,7 +23,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -99,6 +99,6 @@ class SequencesStatistics } } -} +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__SEQUENCES_STATS_H */ diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 3ddcdbf71..5e2d8981d 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -23,9 +23,9 @@ #include "theory/strings/word.h" #include "util/rational.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -291,4 +291,4 @@ Node SkolemCache::mkIndexVar(Node t) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index e4a9ef17e..b6deea6eb 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -24,7 +24,7 @@ #include "expr/node.h" #include "expr/skolem_manager.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -211,6 +211,6 @@ class SkolemCache } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 456cd492b..00bb39d5c 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -19,10 +19,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -223,4 +223,4 @@ void SolverState::separateByLength( } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index e9786526c..8c5d29196 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -29,7 +29,7 @@ #include "theory/uf/equality_engine.h" #include "theory/valuation.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -161,6 +161,6 @@ class SolverState : public TheoryState } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */ diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp index 2e2e8bc22..56c1cbe98 100644 --- a/src/theory/strings/strategy.cpp +++ b/src/theory/strings/strategy.cpp @@ -16,7 +16,7 @@ #include "options/strings_options.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -158,4 +158,4 @@ void Strategy::initializeStrategy() } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h index fde01878d..4c2e587c9 100644 --- a/src/theory/strings/strategy.h +++ b/src/theory/strings/strategy.h @@ -22,7 +22,7 @@ #include "theory/theory.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -111,6 +111,6 @@ class Strategy } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__STRATEGY_H */ diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index f4c91d39f..926a43159 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -21,9 +21,9 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -117,7 +117,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1, Assert(dir == 1 || dir == -1); Assert(nr.empty()); NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(CVC4::Rational(0)); + Node zero = nm->mkConst(CVC5::Rational(0)); bool ret = false; bool success = true; unsigned sindex = 0; @@ -139,7 +139,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1, Assert(ArithEntail::check(curr, true)); Node s = n1[sindex_use]; size_t slen = Word::getLength(s); - Node ncl = nm->mkConst(CVC4::Rational(slen)); + Node ncl = nm->mkConst(CVC5::Rational(slen)); Node next_s = nm->mkNode(MINUS, lowerBound, ncl); next_s = Rewriter::rewrite(next_s); Assert(next_s.isConst()); @@ -602,7 +602,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1, if (n2[index1].isConst()) { Assert(n2[index1].getType().isString()); // string-only - CVC4::String t = n2[index1].getConst<String>(); + CVC5::String t = n2[index1].getConst<String>(); if (n1.size() == 1) { // if n1.size()==1, then if n2[index1] is not a number, we can drop @@ -993,4 +993,4 @@ Node StringsEntail::inferEqsFromContains(Node x, Node y) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h index d5f4ac0d4..16643332a 100644 --- a/src/theory/strings/strings_entail.h +++ b/src/theory/strings/strings_entail.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -379,6 +379,6 @@ class StringsEntail } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__STRING_ENTAIL_H */ diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index 0ce83dbd0..11a743d0d 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -16,10 +16,10 @@ #include "theory/strings/strings_fmf.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -102,4 +102,4 @@ std::string StringsFmf::StringSumLengthDecisionStrategy::identify() const } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h index 6832da5a7..1ef610289 100644 --- a/src/theory/strings/strings_fmf.h +++ b/src/theory/strings/strings_fmf.h @@ -25,7 +25,7 @@ #include "theory/strings/term_registry.h" #include "theory/valuation.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -106,6 +106,6 @@ class StringsFmf } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */ diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 33e7cd895..d41a86c18 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -19,9 +19,9 @@ #include "theory/strings/theory_strings_utils.h" #include "util/rational.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -324,4 +324,4 @@ Node StringsRewriter::rewriteStringIsDigit(Node n) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index 1398d4703..226a66b34 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/strings/sequences_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -103,6 +103,6 @@ class StringsRewriter : public SequencesRewriter } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */ diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index f24fe12e5..d82a2333e 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -24,10 +24,10 @@ #include "theory/strings/word.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -618,4 +618,4 @@ void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index cb1b50816..2f03647fd 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -28,7 +28,7 @@ #include "theory/strings/solver_state.h" #include "theory/uf/equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -279,6 +279,6 @@ class TermRegistry } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__TERM_REGISTRY_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7a8b44625..03d93f8f4 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -29,10 +29,10 @@ #include "theory/valuation.h" using namespace std; -using namespace CVC4::context; -using namespace CVC4::kind; +using namespace CVC5::context; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -1086,6 +1086,6 @@ std::string TheoryStrings::debugPrintStringsEqc() return ss.str(); } -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index f35c67da6..94a96fc33 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -46,7 +46,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -299,8 +299,8 @@ class TheoryStrings : public Theory { Strategy d_strat; };/* class TheoryStrings */ -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d6fa91f34..f89ffa5fa 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -26,10 +26,10 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" -using namespace CVC4; -using namespace CVC4::kind; +using namespace CVC5; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -1026,6 +1026,6 @@ Node StringsPreprocess::mkForallInternal(Node bvl, Node body) return nm->mkNode(FORALL, bvl, body, ipl); } -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index a947c6da6..acf9edad7 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -27,7 +27,7 @@ #include "theory/theory.h" #include "util/hash.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -102,8 +102,8 @@ class StringsPreprocess { static Node mkForallInternal(Node bvl, Node body); }; -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__PREPROCESS_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index fd5d2611e..32605f0f1 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -22,7 +22,7 @@ #include "expr/sequence.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -424,8 +424,8 @@ struct SequenceProperties } }; /* struct SequenceProperties */ -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 73cdf1ddb..821319df5 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -24,9 +24,9 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/word.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { namespace utils { @@ -423,4 +423,4 @@ unsigned getLoopMinOccurrences(TNode node) } // namespace utils } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index 6b53a102d..e720ce0b2 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -23,7 +23,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { namespace utils { @@ -220,6 +220,6 @@ unsigned getLoopMinOccurrences(TNode node); } // namespace utils } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 5def8ec4b..7b89e970e 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -17,7 +17,7 @@ #include "theory/strings/theory_strings_utils.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -271,4 +271,4 @@ bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); } } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 02d3e7f41..7d340be64 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -23,7 +23,7 @@ #include "expr/type_node.h" #include "theory/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -197,8 +197,8 @@ class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator> SeqEnumLen d_wenum; }; /* class SequenceEnumerator */ -}/* CVC4::theory::strings namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace strings +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 0c743dd93..d2e809571 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -17,9 +17,9 @@ #include "expr/sequence.h" #include "util/string.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -486,4 +486,4 @@ Node Word::reverse(TNode x) } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 1b2c94af5..090c36be3 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace strings { @@ -165,6 +165,6 @@ class Word } // namespace strings } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif |