diff options
Diffstat (limited to 'src/theory/strings/strings_entail.cpp')
| -rw-r--r-- | src/theory/strings/strings_entail.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
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 |