diff options
Diffstat (limited to 'src/theory/strings')
62 files changed, 231 insertions, 231 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 36ead8685..a1b2c487f 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -866,4 +866,4 @@ bool ArithEntail::inferZerosInSumGeq(Node x, } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 22011d51b..1726dac0b 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -175,6 +175,6 @@ class ArithEntail } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index b9802b9a5..4cf8c897e 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -760,4 +760,4 @@ Node BaseSolver::TermIndex::add(TNode n, } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 43cb63b47..4ad5c3dec 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -243,6 +243,6 @@ class BaseSolver } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 8593a1e36..6a461cb7a 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -2651,4 +2651,4 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 53bb167c4..7392659c5 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -523,6 +523,6 @@ class CoreSolver } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 e2cb01408..3d23a95a0 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -148,4 +148,4 @@ void EagerSolver::notifyFact(TNode atom, } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h index 49545e622..1d4682c49 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -63,6 +63,6 @@ class EagerSolver } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 0bb2defb6..be2d402a1 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -139,4 +139,4 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index a00cd49ea..23d566ef1 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -76,6 +76,6 @@ class EqcInfo } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 ab7c1d0ac..39bcb8f53 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -724,4 +724,4 @@ bool StringsExtfCallback::getCurrentSubstitution( } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 4b63f261a..3cfe2309c 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -227,6 +227,6 @@ class StringsExtfCallback : public ExtTheoryCallback } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 5e2006f65..bce30096f 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -90,4 +90,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 9c228c197..45a5da2d6 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -131,6 +131,6 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii); } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 c600ce31d..3005fcd19 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -1042,4 +1042,4 @@ std::string InferProofCons::identify() const } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 7d7d7e54a..677ba2e22 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -130,6 +130,6 @@ class InferProofCons : public ProofGenerator } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 15e608ef1..ff3803b7e 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -377,4 +377,4 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 1e57afe79..cb5560f2b 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -271,6 +271,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 6f366d6d7..33e94d3e6 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -4,11 +4,11 @@ # src/theory/builtin/kinds. # -theory THEORY_STRINGS ::CVC5::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 ::CVC5::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(::CVC5::String())" \ + "NodeManager::currentNM()->mkConst(::cvc5::String())" \ "util/string.h" \ "String type" @@ -54,31 +54,31 @@ sort REGEXP_TYPE \ "RegExp type" enumerator STRING_TYPE \ - "::CVC5::theory::strings::StringEnumerator" \ + "::cvc5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::CVC5::String \ - ::CVC5::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 \ - "::CVC5::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ + "::cvc5::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ "theory/strings/theory_strings_type_rules.h" well-founded SEQUENCE_TYPE \ - "::CVC5::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ - "::CVC5::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 \ - "::CVC5::theory::strings::SequenceEnumerator" \ + "::cvc5::theory::strings::SequenceEnumerator" \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::CVC5::Sequence \ - ::CVC5::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 \ - ::CVC5::RegExpRepeat \ - ::CVC5::RegExpRepeatHashFunction \ + ::cvc5::RegExpRepeat \ + ::cvc5::RegExpRepeatHashFunction \ "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the CVC5::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 \ - ::CVC5::RegExpLoop \ - ::CVC5::RegExpLoopHashFunction \ + ::cvc5::RegExpLoop \ + ::cvc5::RegExpLoopHashFunction \ "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the CVC5::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 ::CVC5::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 ::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 +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 ::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 +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 c139a5da7..ed111b4ac 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -185,4 +185,4 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi, } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h index 65d4b3f78..fda691844 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -168,6 +168,6 @@ class NormalForm } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 bf82d16ce..236607840 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -517,4 +517,4 @@ Node StringProofRuleChecker::checkInternal(PfRule id, } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index c55386140..ab971f62f 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -44,6 +44,6 @@ class StringProofRuleChecker : public ProofRuleChecker } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 5dbe02230..4493d6c6c 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -613,4 +613,4 @@ bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 3ffa9566e..f43aacdcd 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -85,6 +85,6 @@ class RegExpElimination } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 94c740742..cc4027aad 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -105,7 +105,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren, else if (xc.isConst()) { // check for constants - CVC5::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()); - CVC5::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(CVC5::String& s, +bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, unsigned index_start, TNode r) { @@ -358,7 +358,7 @@ bool RegExpEntail::testConstStringInRegExp(CVC5::String& s, { case STRING_TO_REGEXP: { - CVC5::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(CVC5::String& s, { for (vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) { - CVC5::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(CVC5::String& s, { for (unsigned i = s.size() - index_start; i > 0; --i) { - CVC5::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(CVC5::String& s, uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt(); for (unsigned len = s.size() - index_start; len >= 1; len--) { - CVC5::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(CVC5::String& s, } else { - Node num2 = nm->mkConst(CVC5::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(CVC5::String& s, } for (unsigned len = 1; len <= s.size() - index_start; len++) { - CVC5::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(CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index 3e14d4ed0..fcad7e2ab 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 CVC5 { +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(CVC5::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 CVC5 +} // 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 5481a0c6d..1bb85ee81 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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(::CVC5::Rational(0))), - d_one(NodeManager::currentNM()->mkConst(::CVC5::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,7 @@ int RegExpOpr::delta( Node r, Node &exp ) { } // 0-unknown, 1-yes, 2-no -int RegExpOpr::derivativeS(Node r, CVC5::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; @@ -302,8 +302,8 @@ int RegExpOpr::derivativeS(Node r, CVC5::String c, Node& retNode) break; } case kind::REGEXP_RANGE: { - CVC5::String a = r[0].getConst<String>(); - CVC5::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; } @@ -521,7 +521,7 @@ int RegExpOpr::derivativeS(Node r, CVC5::String c, Node& retNode) return ret; } -Node RegExpOpr::derivativeSingle(Node r, CVC5::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; @@ -555,8 +555,8 @@ Node RegExpOpr::derivativeSingle(Node r, CVC5::String c) break; } case kind::REGEXP_RANGE: { - CVC5::String a = r[0].getConst<String>(); - CVC5::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; } @@ -1314,7 +1314,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > std::map< PairNodes, Node > cache2(cache); cache2[p] = NodeManager::currentNM()->mkNode( kind::REGEXP_RV, - NodeManager::currentNM()->mkConst(CVC5::Rational(cnt))); + NodeManager::currentNM()->mkConst(cvc5::Rational(cnt))); rt = intersectInternal(r1l, r2l, cache2, cnt+1); cacheX[ pp ] = rt; } @@ -1619,4 +1619,4 @@ Node RegExpOpr::getExistsForRegExpConcatMem(Node mem) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 27324d971..b660e5c49 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -55,7 +55,7 @@ enum RegExpConstType }; class RegExpOpr { - typedef std::pair<Node, CVC5::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, CVC5::String c, Node& retNode); - Node derivativeSingle(Node r, CVC5::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. @@ -209,6 +209,6 @@ class RegExpOpr { } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 861f7c694..2d4404c10 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +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(::CVC5::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; } -CVC5::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; - CVC5::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) { - CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index d35a822a7..440d0fcb7 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 CVC5 { +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); - CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index cdf41d9ad..41b972514 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -224,4 +224,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index af9b636cf..37ef61bee 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -239,6 +239,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 9cec9ad40..302f7dc0b 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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(); - CVC5::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] - CVC5::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]; - CVC5::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(CVC5::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()) { - CVC5::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()) { - CVC5::Rational rMaxInt(CVC5::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(::CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 750589f72..eda8bc1df 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -296,6 +296,6 @@ class SequencesRewriter : public TheoryRewriter } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 919b950ab..e0d14f93e 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -63,4 +63,4 @@ SequencesStatistics::~SequencesStatistics() } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 417f79046..5bd48e877 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -99,6 +99,6 @@ class SequencesStatistics } } -} // namespace CVC5 +} // 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 5e2d8981d..ad36b8edd 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -291,4 +291,4 @@ Node SkolemCache::mkIndexVar(Node t) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index b6deea6eb..5c5fc8d57 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -211,6 +211,6 @@ class SkolemCache } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 00bb39d5c..39fe6dd11 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -223,4 +223,4 @@ void SolverState::separateByLength( } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 8c5d29196..e54a5e7b1 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -161,6 +161,6 @@ class SolverState : public TheoryState } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */ diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp index 56c1cbe98..54f8e43f8 100644 --- a/src/theory/strings/strategy.cpp +++ b/src/theory/strings/strategy.cpp @@ -16,7 +16,7 @@ #include "options/strings_options.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -158,4 +158,4 @@ void Strategy::initializeStrategy() } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h index 4c2e587c9..1eb2fe902 100644 --- a/src/theory/strings/strategy.h +++ b/src/theory/strings/strategy.h @@ -22,7 +22,7 @@ #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -111,6 +111,6 @@ class Strategy } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 926a43159..62ba41743 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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(CVC5::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(CVC5::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 - CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h index 16643332a..cce0bf05b 100644 --- a/src/theory/strings/strings_entail.h +++ b/src/theory/strings/strings_entail.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -379,6 +379,6 @@ class StringsEntail } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 11a743d0d..e543f173c 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -102,4 +102,4 @@ std::string StringsFmf::StringSumLengthDecisionStrategy::identify() const } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h index 1ef610289..a2496dec3 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -106,6 +106,6 @@ class StringsFmf } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 d41a86c18..1a7ca7f6a 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -324,4 +324,4 @@ Node StringsRewriter::rewriteStringIsDigit(Node n) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index 226a66b34..e7ad40d51 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -103,6 +103,6 @@ class StringsRewriter : public SequencesRewriter } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 d82a2333e..4f5c09b5e 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 2f03647fd..1eb000e09 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -279,6 +279,6 @@ class TermRegistry } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 03d93f8f4..5bd92267e 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 CVC5::context; -using namespace CVC5::kind; +using namespace cvc5::context; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -1088,4 +1088,4 @@ std::string TheoryStrings::debugPrintStringsEqc() } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 94a96fc33..e1fc20d29 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -301,6 +301,6 @@ class TheoryStrings : public Theory { } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 f89ffa5fa..8deba50ca 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 CVC5; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -1028,4 +1028,4 @@ Node StringsPreprocess::mkForallInternal(Node bvl, Node body) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index acf9edad7..7c8c4308c 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -104,6 +104,6 @@ class StringsPreprocess { } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 32605f0f1..0892af4de 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -426,6 +426,6 @@ struct SequenceProperties } // namespace strings } // namespace theory -} // namespace CVC5 +} // 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 821319df5..510214e0f 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { namespace utils { @@ -423,4 +423,4 @@ unsigned getLoopMinOccurrences(TNode node) } // namespace utils } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index e720ce0b2..e3c85d562 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { namespace utils { @@ -220,6 +220,6 @@ unsigned getLoopMinOccurrences(TNode node); } // namespace utils } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 7b89e970e..146cf434f 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -271,4 +271,4 @@ bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); } } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 7d340be64..644fe1092 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -199,6 +199,6 @@ class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator> } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index d2e809571..612acb80a 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -486,4 +486,4 @@ Node Word::reverse(TNode x) } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 090c36be3..6cf073cc1 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 CVC5 { +namespace cvc5 { namespace theory { namespace strings { @@ -165,6 +165,6 @@ class Word } // namespace strings } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif |