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