src/theory/strings/term_registry.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Morgan Deters
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of term registry for the theory of strings.
  14  */
  15
  16 #include "theory/strings/term_registry.h"
  17
  18 #include "expr/attribute.h"
  19 #include "options/smt_options.h"
  20 #include "options/strings_options.h"
  21 #include "smt/logic_exception.h"
  22 #include "theory/rewriter.h"
  23 #include "theory/strings/inference_manager.h"
  24 #include "theory/strings/theory_strings_utils.h"
  25 #include "theory/strings/word.h"
  26 #include "util/rational.h"
  27 #include "util/string.h"
  28
  29 using namespace std;
  30 using namespace cvc5::context;
  31 using namespace cvc5::kind;
  32
  33 namespace cvc5 {
  34 namespace theory {
  35 namespace strings {
  36
  37 struct StringsProxyVarAttributeId
  38 {
  39 };
  40 typedef expr::Attribute<StringsProxyVarAttributeId, bool>
  41     StringsProxyVarAttribute;
  42
  43 TermRegistry::TermRegistry(SolverState& s,
  44                            SequencesStatistics& statistics,
  45                            ProofNodeManager* pnm)
  46     : d_state(s),
  47       d_im(nullptr),
  48       d_statistics(statistics),
  49       d_hasStrCode(false),
  50       d_functionsTerms(s.getSatContext()),
  51       d_inputVars(s.getUserContext()),
  52       d_preregisteredTerms(s.getSatContext()),
  53       d_registeredTerms(s.getUserContext()),
  54       d_registeredTypes(s.getUserContext()),
  55       d_proxyVar(s.getUserContext()),
  56       d_lengthLemmaTermsCache(s.getUserContext()),
  57       d_epg(pnm ? new EagerProofGenerator(
  58                       pnm,
  59                       s.getUserContext(),
  60                       "strings::TermRegistry::EagerProofGenerator")
  61                 : nullptr)
  62 {
  63   NodeManager* nm = NodeManager::currentNM();
  64   d_zero = nm->mkConst(Rational(0));
  65   d_one = nm->mkConst(Rational(1));
  66   d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
  67   d_cardSize = utils::getAlphabetCardinality();
  68 }
  69
  70 TermRegistry::~TermRegistry() {}
  71
  72 void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
  73
  74 Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
  75 {
  76   NodeManager* nm = NodeManager::currentNM();
  77   Node lemma;
  78   Kind tk = t.getKind();
  79   if (tk == STRING_TO_CODE)
  80   {
  81     // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
  82     Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
  83     Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
  84     Node code_range = nm->mkNode(
  85         AND,
  86         nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
  87         nm->mkNode(
  88             LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
  89     lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
  90   }
  91   else if (tk == STRING_STRIDOF || tk == STRING_INDEXOF_RE)
  92   {
  93     // (and
  94     //   (or (= (f x y n) (- 1)) (>= (f x y n) n))
  95     //   (<= (f x y n) (str.len x)))
  96     //
  97     // where f in { str.indexof, str.indexof_re }
  98     Node l = nm->mkNode(STRING_LENGTH, t[0]);
  99     lemma = nm->mkNode(
 100         AND,
 101         nm->mkNode(
 102             OR, nm->mkConst(Rational(-1)).eqNode(t), nm->mkNode(GEQ, t, t[2])),
 103         nm->mkNode(LEQ, t, l));
 104   }
 105   else if (tk == STRING_STOI)
 106   {
 107     // (>= (str.to_int x) (- 1))
 108     lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
 109   }
 110   else if (tk == STRING_STRCTN)
 111   {
 112     // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
 113     Node sk1 =
 114         sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
 115     Node sk2 =
 116         sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
 117     lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
 118     lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
 119   }
 120   return lemma;
 121 }
 122
 123 Node TermRegistry::lengthPositive(Node t)
 124 {
 125   NodeManager* nm = NodeManager::currentNM();
 126   Node zero = nm->mkConst(Rational(0));
 127   Node emp = Word::mkEmptyWord(t.getType());
 128   Node tlen = nm->mkNode(STRING_LENGTH, t);
 129   Node tlenEqZero = tlen.eqNode(zero);
 130   Node tEqEmp = t.eqNode(emp);
 131   Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
 132   Node caseNEmpty = nm->mkNode(GT, tlen, zero);
 133   // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
 134   return nm->mkNode(OR, caseEmpty, caseNEmpty);
 135 }
 136
 137 void TermRegistry::preRegisterTerm(TNode n)
 138 {
 139   if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
 140   {
 141     return;
 142   }
 143   eq::EqualityEngine* ee = d_state.getEqualityEngine();
 144   d_preregisteredTerms.insert(n);
 145   Trace("strings-preregister")
 146       << "TheoryString::preregister : " << n << std::endl;
 147   // check for logic exceptions
 148   Kind k = n.getKind();
 149   if (!options::stringExp())
 150   {
 151     if (k == STRING_STRIDOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
 152         || k == STRING_STOI || k == STRING_STRREPL || k == STRING_SUBSTR
 153         || k == STRING_STRREPLALL || k == SEQ_NTH || k == STRING_REPLACE_RE
 154         || k == STRING_REPLACE_RE_ALL || k == STRING_STRCTN || k == STRING_LEQ
 155         || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV
 156         || k == STRING_UPDATE)
 157     {
 158       std::stringstream ss;
 159       ss << "Term of kind " << k
 160          << " not supported in default mode, try --strings-exp";
 161       throw LogicException(ss.str());
 162     }
 163   }
 164   if (k == EQUAL)
 165   {
 166     if (n[0].getType().isRegExp())
 167     {
 168       std::stringstream ss;
 169       ss << "Equality between regular expressions is not supported";
 170       throw LogicException(ss.str());
 171     }
 172     ee->addTriggerPredicate(n);
 173     return;
 174   }
 175   else if (k == STRING_IN_REGEXP)
 176   {
 177     d_im->requirePhase(n, true);
 178     ee->addTriggerPredicate(n);
 179     ee->addTerm(n[0]);
 180     ee->addTerm(n[1]);
 181     return;
 182   }
 183   else if (k == STRING_TO_CODE)
 184   {
 185     d_hasStrCode = true;
 186   }
 187   else if (k == REGEXP_RANGE)
 188   {
 189     for (const Node& nc : n)
 190     {
 191       if (!nc.isConst())
 192       {
 193         throw LogicException(
 194             "expecting a constant string term in regexp range");
 195       }
 196       if (nc.getConst<String>().size() != 1)
 197       {
 198         throw LogicException(
 199             "expecting a single constant string term in regexp range");
 200       }
 201     }
 202   }
 203   registerTerm(n, 0);
 204   TypeNode tn = n.getType();
 205   if (tn.isRegExp() && n.isVar())
 206   {
 207     std::stringstream ss;
 208     ss << "Regular expression variables are not supported.";
 209     throw LogicException(ss.str());
 210   }
 211   if (tn.isString())  // string-only
 212   {
 213     // all characters of constants should fall in the alphabet
 214     if (n.isConst())
 215     {
 216       std::vector<unsigned> vec = n.getConst<String>().getVec();
 217       for (unsigned u : vec)
 218       {
 219         if (u >= d_cardSize)
 220         {
 221           std::stringstream ss;
 222           ss << "Characters in string \"" << n
 223              << "\" are outside of the given alphabet.";
 224           throw LogicException(ss.str());
 225         }
 226       }
 227     }
 228     ee->addTerm(n);
 229   }
 230   else if (tn.isBoolean())
 231   {
 232     // All kinds that we do congruence over that may return a Boolean go here
 233     if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH)
 234     {
 235       // Get triggered for both equal and dis-equal
 236       ee->addTriggerPredicate(n);
 237     }
 238   }
 239   else
 240   {
 241     // Function applications/predicates
 242     ee->addTerm(n);
 243   }
 244   // Set d_functionsTerms stores all function applications that are
 245   // relevant to theory combination. Notice that this is a subset of
 246   // the applications whose kinds are function kinds in the equality
 247   // engine. This means it does not include applications of operators
 248   // like re.++, which is not a function kind in the equality engine.
 249   // Concatenation terms do not need to be considered here because
 250   // their arguments have string type and do not introduce any shared
 251   // terms.
 252   if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
 253   {
 254     d_functionsTerms.push_back(n);
 255   }
 256   if (options::stringFMF())
 257   {
 258     if (tn.isStringLike())
 259     {
 260       // Our decision strategy will minimize the length of this term if it is a
 261       // variable but not an internally generated Skolem, or a term that does
 262       // not belong to this theory.
 263       if (n.isVar() ? !d_skCache.isSkolem(n)
 264                     : kindToTheoryId(k) != THEORY_STRINGS)
 265       {
 266         d_inputVars.insert(n);
 267         Trace("strings-preregister") << "input variable: " << n << std::endl;
 268       }
 269     }
 270   }
 271 }
 272
 273 void TermRegistry::registerTerm(Node n, int effort)
 274 {
 275   Trace("strings-register") << "TheoryStrings::registerTerm() " << n
 276                             << ", effort = " << effort << std::endl;
 277   if (d_registeredTerms.find(n) != d_registeredTerms.end())
 278   {
 279     Trace("strings-register") << "...already registered" << std::endl;
 280     return;
 281   }
 282   bool do_register = true;
 283   TypeNode tn = n.getType();
 284   if (!tn.isStringLike())
 285   {
 286     if (options::stringEagerLen())
 287     {
 288       do_register = effort == 0;
 289     }
 290     else
 291     {
 292       do_register = effort > 0 || n.getKind() != STRING_CONCAT;
 293     }
 294   }
 295   if (!do_register)
 296   {
 297     Trace("strings-register") << "...do not register" << std::endl;
 298     return;
 299   }
 300   Trace("strings-register") << "...register" << std::endl;
 301   d_registeredTerms.insert(n);
 302   // ensure the type is registered
 303   registerType(tn);
 304   TrustNode regTermLem;
 305   if (tn.isStringLike())
 306   {
 307     // register length information:
 308     //  for variables, split on empty vs positive length
 309     //  for concat/const/replace, introduce proxy var and state length relation
 310     regTermLem = getRegisterTermLemma(n);
 311   }
 312   else if (n.getKind() != STRING_STRCTN)
 313   {
 314     // we don't send out eager reduction lemma for str.contains currently
 315     Node eagerRedLemma = eagerReduce(n, &d_skCache);
 316     if (!eagerRedLemma.isNull())
 317     {
 318       // if there was an eager reduction, we make the trust node for it
 319       if (d_epg != nullptr)
 320       {
 321         regTermLem = d_epg->mkTrustNode(
 322             eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
 323       }
 324       else
 325       {
 326         regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
 327       }
 328     }
 329   }
 330   if (!regTermLem.isNull())
 331   {
 332     Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
 333                            << std::endl;
 334     Trace("strings-assert")
 335         << "(assert " << regTermLem.getNode() << ")" << std::endl;
 336     d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
 337   }
 338 }
 339
 340 void TermRegistry::registerType(TypeNode tn)
 341 {
 342   if (d_registeredTypes.find(tn) != d_registeredTypes.end())
 343   {
 344     return;
 345   }
 346   d_registeredTypes.insert(tn);
 347   if (tn.isStringLike())
 348   {
 349     // preregister the empty word for the type
 350     Node emp = Word::mkEmptyWord(tn);
 351     if (!d_state.hasTerm(emp))
 352     {
 353       preRegisterTerm(emp);
 354     }
 355   }
 356 }
 357
 358 TrustNode TermRegistry::getRegisterTermLemma(Node n)
 359 {
 360   Assert(n.getType().isStringLike());
 361   NodeManager* nm = NodeManager::currentNM();
 362   // register length information:
 363   //  for variables, split on empty vs positive length
 364   //  for concat/const/replace, introduce proxy var and state length relation
 365   Node lsum;
 366   if (n.getKind() != STRING_CONCAT && !n.isConst())
 367   {
 368     Node lsumb = nm->mkNode(STRING_LENGTH, n);
 369     lsum = Rewriter::rewrite(lsumb);
 370     // can register length term if it does not rewrite
 371     if (lsum == lsumb)
 372     {
 373       registerTermAtomic(n, LENGTH_SPLIT);
 374       return TrustNode::null();
 375     }
 376   }
 377   Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
 378   StringsProxyVarAttribute spva;
 379   sk.setAttribute(spva, true);
 380   Node eq = Rewriter::rewrite(sk.eqNode(n));
 381   d_proxyVar[n] = sk;
 382   // If we are introducing a proxy for a constant or concat term, we do not
 383   // need to send lemmas about its length, since its length is already
 384   // implied.
 385   if (n.isConst() || n.getKind() == STRING_CONCAT)
 386   {
 387     // do not send length lemma for sk.
 388     registerTermAtomic(sk, LENGTH_IGNORE);
 389   }
 390   Node skl = nm->mkNode(STRING_LENGTH, sk);
 391   if (n.getKind() == STRING_CONCAT)
 392   {
 393     std::vector<Node> nodeVec;
 394     for (const Node& nc : n)
 395     {
 396       if (nc.getAttribute(StringsProxyVarAttribute()))
 397       {
 398         Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end());
 399         nodeVec.push_back(d_proxyVarToLength[nc]);
 400       }
 401       else
 402       {
 403         Node lni = nm->mkNode(STRING_LENGTH, nc);
 404         nodeVec.push_back(lni);
 405       }
 406     }
 407     lsum = nm->mkNode(PLUS, nodeVec);
 408     lsum = Rewriter::rewrite(lsum);
 409   }
 410   else if (n.isConst())
 411   {
 412     lsum = nm->mkConst(Rational(Word::getLength(n)));
 413   }
 414   Assert(!lsum.isNull());
 415   d_proxyVarToLength[sk] = lsum;
 416   Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
 417
 418   Node ret = nm->mkNode(AND, eq, ceq);
 419
 420   // it is a simple rewrite to justify this
 421   if (d_epg != nullptr)
 422   {
 423     return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
 424   }
 425   return TrustNode::mkTrustLemma(ret, nullptr);
 426 }
 427
 428 void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
 429 {
 430   if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
 431   {
 432     return;
 433   }
 434   d_lengthLemmaTermsCache.insert(n);
 435
 436   if (s == LENGTH_IGNORE)
 437   {
 438     // ignore it
 439     return;
 440   }
 441   std::map<Node, bool> reqPhase;
 442   TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
 443   if (!lenLem.isNull())
 444   {
 445     Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
 446                            << std::endl;
 447     Trace("strings-assert")
 448         << "(assert " << lenLem.getNode() << ")" << std::endl;
 449     d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
 450   }
 451   for (const std::pair<const Node, bool>& rp : reqPhase)
 452   {
 453     d_im->requirePhase(rp.first, rp.second);
 454   }
 455 }
 456
 457 SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
 458
 459 const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
 460 {
 461   return d_functionsTerms;
 462 }
 463
 464 const context::CDHashSet<Node>& TermRegistry::getInputVars() const
 465 {
 466   return d_inputVars;
 467 }
 468
 469 bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
 470
 471 TrustNode TermRegistry::getRegisterTermAtomicLemma(
 472     Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
 473 {
 474   if (n.isConst())
 475   {
 476     // No need to send length for constant terms. This case may be triggered
 477     // for cases where the skolem cache automatically replaces a skolem by
 478     // a constant.
 479     return TrustNode::null();
 480   }
 481   Assert(n.getType().isStringLike());
 482   NodeManager* nm = NodeManager::currentNM();
 483   Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
 484   Node emp = Word::mkEmptyWord(n.getType());
 485   if (s == LENGTH_GEQ_ONE)
 486   {
 487     Node neq_empty = n.eqNode(emp).negate();
 488     Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
 489     Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
 490     Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
 491                            << std::endl;
 492     Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
 493     return TrustNode::mkTrustLemma(len_geq_one, nullptr);
 494   }
 495
 496   if (s == LENGTH_ONE)
 497   {
 498     Node len_one = n_len.eqNode(d_one);
 499     Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
 500                            << std::endl;
 501     Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
 502     return TrustNode::mkTrustLemma(len_one, nullptr);
 503   }
 504   Assert(s == LENGTH_SPLIT);
 505
 506   // get the positive length lemma
 507   Node lenLemma = lengthPositive(n);
 508   // split whether the string is empty
 509   Node n_len_eq_z = n_len.eqNode(d_zero);
 510   Node n_len_eq_z_2 = n.eqNode(emp);
 511   Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
 512   Node case_emptyr = Rewriter::rewrite(case_empty);
 513   if (!case_emptyr.isConst())
 514   {
 515     // prefer trying the empty case first
 516     // notice that requirePhase must only be called on rewritten literals that
 517     // occur in the CNF stream.
 518     n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
 519     Assert(!n_len_eq_z.isConst());
 520     reqPhase[n_len_eq_z] = true;
 521     n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
 522     Assert(!n_len_eq_z_2.isConst());
 523     reqPhase[n_len_eq_z_2] = true;
 524   }
 525   else
 526   {
 527     // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
 528     // n ---> "". Since this method is only called on non-constants n, it must
 529     // be that n = "" ^ len( n ) = 0 does not rewrite to true.
 530     Assert(!case_emptyr.getConst<bool>());
 531   }
 532
 533   if (d_epg != nullptr)
 534   {
 535     return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
 536   }
 537   return TrustNode::mkTrustLemma(lenLemma, nullptr);
 538 }
 539
 540 Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
 541 {
 542   if (n.getNumChildren() == 0)
 543   {
 544     Node pn = getProxyVariableFor(n);
 545     if (pn.isNull())
 546     {
 547       return Node::null();
 548     }
 549     Node eq = n.eqNode(pn);
 550     eq = Rewriter::rewrite(eq);
 551     if (std::find(exp.begin(), exp.end(), eq) == exp.end())
 552     {
 553       exp.push_back(eq);
 554     }
 555     return pn;
 556   }
 557   std::vector<Node> children;
 558   if (n.getMetaKind() == metakind::PARAMETERIZED)
 559   {
 560     children.push_back(n.getOperator());
 561   }
 562   for (const Node& nc : n)
 563   {
 564     if (n.getType().isRegExp())
 565     {
 566       children.push_back(nc);
 567     }
 568     else
 569     {
 570       Node ns = getSymbolicDefinition(nc, exp);
 571       if (ns.isNull())
 572       {
 573         return Node::null();
 574       }
 575       else
 576       {
 577         children.push_back(ns);
 578       }
 579     }
 580   }
 581   return NodeManager::currentNM()->mkNode(n.getKind(), children);
 582 }
 583
 584 Node TermRegistry::getProxyVariableFor(Node n) const
 585 {
 586   NodeNodeMap::const_iterator it = d_proxyVar.find(n);
 587   if (it != d_proxyVar.end())
 588   {
 589     return (*it).second;
 590   }
 591   return Node::null();
 592 }
 593
 594 Node TermRegistry::ensureProxyVariableFor(Node n)
 595 {
 596   Node proxy = getProxyVariableFor(n);
 597   if (proxy.isNull())
 598   {
 599     registerTerm(n, 0);
 600     proxy = getProxyVariableFor(n);
 601   }
 602   Assert(!proxy.isNull());
 603   return proxy;
 604 }
 605
 606 void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
 607 {
 608   if (n.getKind() == AND)
 609   {
 610     for (const Node& nc : n)
 611     {
 612       removeProxyEqs(nc, unproc);
 613     }
 614     return;
 615   }
 616   Trace("strings-subs-proxy") << "Input : " << n << std::endl;
 617   Node ns = Rewriter::rewrite(n);
 618   if (ns.getKind() == EQUAL)
 619   {
 620     for (size_t i = 0; i < 2; i++)
 621     {
 622       // determine whether this side has a proxy variable
 623       if (ns[i].getAttribute(StringsProxyVarAttribute()))
 624       {
 625         if (getProxyVariableFor(ns[1 - i]) == ns[i])
 626         {
 627           Trace("strings-subs-proxy")
 628               << "...trivial definition via " << ns[i] << std::endl;
 629           // it is a trivial equality, e.g. between a proxy variable
 630           // and its definition
 631           return;
 632         }
 633       }
 634     }
 635   }
 636   if (!n.isConst() || !n.getConst<bool>())
 637   {
 638     Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
 639     unproc.push_back(n);
 640   }
 641 }
 642
 643 }  // namespace strings
 644 }  // namespace theory
 645 }  // namespace cvc5