src/theory/strings/extf_solver.cpp

   1 /*********************                                                        */
   2 /*! \file ext_solver.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Implementation of solver for extended functions of theory of strings.
  13  **/
  14
  15 #include "theory/strings/extf_solver.h"
  16
  17 #include "options/strings_options.h"
  18 #include "theory/strings/sequences_rewriter.h"
  19 #include "theory/strings/theory_strings_preprocess.h"
  20 #include "theory/strings/theory_strings_utils.h"
  21
  22 using namespace std;
  23 using namespace CVC4::context;
  24 using namespace CVC4::kind;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace strings {
  29
  30 ExtfSolver::ExtfSolver(context::Context* c,
  31                        context::UserContext* u,
  32                        SolverState& s,
  33                        InferenceManager& im,
  34                        SkolemCache& skc,
  35                        StringsRewriter& rewriter,
  36                        BaseSolver& bs,
  37                        CoreSolver& cs,
  38                        ExtTheory* et,
  39                        SequencesStatistics& statistics)
  40     : d_state(s),
  41       d_im(im),
  42       d_skCache(skc),
  43       d_rewriter(rewriter),
  44       d_bsolver(bs),
  45       d_csolver(cs),
  46       d_extt(et),
  47       d_statistics(statistics),
  48       d_preproc(&skc, u, statistics),
  49       d_hasExtf(c, false),
  50       d_extfInferCache(c)
  51 {
  52   d_extt->addFunctionKind(kind::STRING_SUBSTR);
  53   d_extt->addFunctionKind(kind::STRING_STRIDOF);
  54   d_extt->addFunctionKind(kind::STRING_ITOS);
  55   d_extt->addFunctionKind(kind::STRING_STOI);
  56   d_extt->addFunctionKind(kind::STRING_STRREPL);
  57   d_extt->addFunctionKind(kind::STRING_STRREPLALL);
  58   d_extt->addFunctionKind(kind::STRING_STRCTN);
  59   d_extt->addFunctionKind(kind::STRING_IN_REGEXP);
  60   d_extt->addFunctionKind(kind::STRING_LEQ);
  61   d_extt->addFunctionKind(kind::STRING_TO_CODE);
  62   d_extt->addFunctionKind(kind::STRING_TOLOWER);
  63   d_extt->addFunctionKind(kind::STRING_TOUPPER);
  64   d_extt->addFunctionKind(kind::STRING_REV);
  65
  66   d_true = NodeManager::currentNM()->mkConst(true);
  67   d_false = NodeManager::currentNM()->mkConst(false);
  68 }
  69
  70 ExtfSolver::~ExtfSolver() {}
  71
  72 bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
  73 {
  74   Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
  75   if (!d_extfInfoTmp[n].d_modelActive)
  76   {
  77     // n is not active in the model, no need to reduce
  78     return false;
  79   }
  80   // determine the effort level to process the extf at
  81   // 0 - at assertion time, 1+ - after no other reduction is applicable
  82   int r_effort = -1;
  83   // polarity : 1 true, -1 false, 0 neither
  84   int pol = 0;
  85   Kind k = n.getKind();
  86   if (n.getType().isBoolean() && !d_extfInfoTmp[n].d_const.isNull())
  87   {
  88     pol = d_extfInfoTmp[n].d_const.getConst<bool>() ? 1 : -1;
  89   }
  90   if (k == STRING_STRCTN)
  91   {
  92     if (pol == 1)
  93     {
  94       r_effort = 1;
  95     }
  96     else if (pol == -1)
  97     {
  98       if (effort == 2)
  99       {
 100         Node x = n[0];
 101         Node s = n[1];
 102         std::vector<Node> lexp;
 103         Node lenx = d_state.getLength(x, lexp);
 104         Node lens = d_state.getLength(s, lexp);
 105         if (d_state.areEqual(lenx, lens))
 106         {
 107           Trace("strings-extf-debug")
 108               << "  resolve extf : " << n
 109               << " based on equal lengths disequality." << std::endl;
 110           // We can reduce negative contains to a disequality when lengths are
 111           // equal. In other words, len( x ) = len( s ) implies
 112           //   ~contains( x, s ) reduces to x != s.
 113           if (!d_state.areDisequal(x, s))
 114           {
 115             // len( x ) = len( s ) ^ ~contains( x, s ) => x != s
 116             lexp.push_back(lenx.eqNode(lens));
 117             lexp.push_back(n.negate());
 118             Node xneqs = x.eqNode(s).negate();
 119             d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
 120           }
 121           // this depends on the current assertions, so we set that this
 122           // inference is context-dependent.
 123           isCd = true;
 124           return true;
 125         }
 126         else
 127         {
 128           r_effort = 2;
 129         }
 130       }
 131     }
 132   }
 133   else
 134   {
 135     if (k == STRING_SUBSTR)
 136     {
 137       r_effort = 1;
 138     }
 139     else if (k != STRING_IN_REGEXP)
 140     {
 141       r_effort = 2;
 142     }
 143   }
 144   if (effort != r_effort)
 145   {
 146     // not the right effort level to reduce
 147     return false;
 148   }
 149   Node c_n = pol == -1 ? n.negate() : n;
 150   Trace("strings-process-debug")
 151       << "Process reduction for " << n << ", pol = " << pol << std::endl;
 152   if (k == STRING_STRCTN && pol == 1)
 153   {
 154     Node x = n[0];
 155     Node s = n[1];
 156     // positive contains reduces to a equality
 157     Node sk1 =
 158         d_skCache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1");
 159     Node sk2 =
 160         d_skCache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2");
 161     Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2)));
 162     std::vector<Node> exp_vec;
 163     exp_vec.push_back(n);
 164     d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true);
 165     Trace("strings-extf-debug")
 166         << "  resolve extf : " << n << " based on positive contain reduction."
 167         << std::endl;
 168     Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
 169                                << " => " << eq << std::endl;
 170     // context-dependent because it depends on the polarity of n itself
 171     isCd = true;
 172   }
 173   else if (k != kind::STRING_TO_CODE)
 174   {
 175     NodeManager* nm = NodeManager::currentNM();
 176     Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF
 177            || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL
 178            || k == STRING_STRREPLALL || k == STRING_LEQ || k == STRING_TOLOWER
 179            || k == STRING_TOUPPER || k == STRING_REV);
 180     std::vector<Node> new_nodes;
 181     Node res = d_preproc.simplify(n, new_nodes);
 182     Assert(res != n);
 183     new_nodes.push_back(res.eqNode(n));
 184     Node nnlem =
 185         new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes);
 186     nnlem = Rewriter::rewrite(nnlem);
 187     Trace("strings-red-lemma")
 188         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
 189     Trace("strings-red-lemma") << "...from " << n << std::endl;
 190     d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
 191     Trace("strings-extf-debug")
 192         << "  resolve extf : " << n << " based on reduction." << std::endl;
 193     isCd = false;
 194   }
 195   return true;
 196 }
 197
 198 void ExtfSolver::checkExtfReductions(int effort)
 199 {
 200   // Notice we don't make a standard call to ExtTheory::doReductions here,
 201   // since certain optimizations like context-dependent reductions and
 202   // stratifying effort levels are done in doReduction below.
 203   std::vector<Node> extf = d_extt->getActive();
 204   Trace("strings-process") << "  checking " << extf.size() << " active extf"
 205                            << std::endl;
 206   for (const Node& n : extf)
 207   {
 208     Assert(!d_state.isInConflict());
 209     Trace("strings-process")
 210         << "  check " << n
 211         << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
 212     // whether the reduction was context-dependent
 213     bool isCd = false;
 214     bool ret = doReduction(effort, n, isCd);
 215     if (ret)
 216     {
 217       d_extt->markReduced(n, isCd);
 218       if (d_im.hasProcessed())
 219       {
 220         return;
 221       }
 222     }
 223   }
 224 }
 225
 226 void ExtfSolver::checkExtfEval(int effort)
 227 {
 228   Trace("strings-extf-list")
 229       << "Active extended functions, effort=" << effort << " : " << std::endl;
 230   d_extfInfoTmp.clear();
 231   NodeManager* nm = NodeManager::currentNM();
 232   bool has_nreduce = false;
 233   std::vector<Node> terms = d_extt->getActive();
 234   for (const Node& n : terms)
 235   {
 236     // Setup information about n, including if it is equal to a constant.
 237     ExtfInfoTmp& einfo = d_extfInfoTmp[n];
 238     Node r = d_state.getRepresentative(n);
 239     einfo.d_const = d_bsolver.getConstantEqc(r);
 240     // Get the current values of the children of n.
 241     // Notice that we look up the value of the direct children of n, and not
 242     // their free variables. In other words, given a term:
 243     //   t = (str.replace "B" (str.replace x "A" "B") "C")
 244     // we may build the explanation that:
 245     //   ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C")
 246     // instead of basing this on the free variable x:
 247     //   (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C")
 248     // Although both allow us to infer t = "C", it is important to use the
 249     // first kind of inference since it ensures that its subterms have the
 250     // expected values. Otherwise, we may in rare cases fail to realize that
 251     // the subterm (str.replace x "A" "B") does not currently have the correct
 252     // value, say in this example that (str.replace x "A" "B") != "B".
 253     std::vector<Node> exp;
 254     std::vector<Node> schildren;
 255     bool schanged = false;
 256     for (const Node& nc : n)
 257     {
 258       Node sc = getCurrentSubstitutionFor(effort, nc, exp);
 259       schildren.push_back(sc);
 260       schanged = schanged || sc != nc;
 261     }
 262     // If there is information involving the children, attempt to do an
 263     // inference and/or mark n as reduced.
 264     Node to_reduce;
 265     if (schanged)
 266     {
 267       Node sn = nm->mkNode(n.getKind(), schildren);
 268       Trace("strings-extf-debug")
 269           << "Check extf " << n << " == " << sn
 270           << ", constant = " << einfo.d_const << ", effort=" << effort << "..."
 271           << std::endl;
 272       einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
 273       // inference is rewriting the substituted node
 274       Node nrc = Rewriter::rewrite(sn);
 275       // if rewrites to a constant, then do the inference and mark as reduced
 276       if (nrc.isConst())
 277       {
 278         if (effort < 3)
 279         {
 280           d_extt->markReduced(n);
 281           Trace("strings-extf-debug")
 282               << "  resolvable by evaluation..." << std::endl;
 283           std::vector<Node> exps;
 284           // The following optimization gets the "symbolic definition" of
 285           // an extended term. The symbolic definition of a term t is a term
 286           // t' where constants are replaced by their corresponding proxy
 287           // variables.
 288           // For example, if lsym is a proxy variable for "", then
 289           // str.replace( lsym, lsym, lsym ) is the symbolic definition for
 290           // str.replace( "", "", "" ). It is generally better to use symbolic
 291           // definitions when doing cd-rewriting for the purpose of minimizing
 292           // clauses, e.g. we infer the unit equality:
 293           //    str.replace( lsym, lsym, lsym ) == ""
 294           // instead of making this inference multiple times:
 295           //    x = "" => str.replace( x, x, x ) == ""
 296           //    y = "" => str.replace( y, y, y ) == ""
 297           Trace("strings-extf-debug")
 298               << "  get symbolic definition..." << std::endl;
 299           Node nrs;
 300           // only use symbolic definitions if option is set
 301           if (options::stringInferSym())
 302           {
 303             nrs = d_im.getSymbolicDefinition(sn, exps);
 304           }
 305           if (!nrs.isNull())
 306           {
 307             Trace("strings-extf-debug")
 308                 << "  rewrite " << nrs << "..." << std::endl;
 309             Node nrsr = Rewriter::rewrite(nrs);
 310             // ensure the symbolic form is not rewritable
 311             if (nrsr != nrs)
 312             {
 313               // we cannot use the symbolic definition if it rewrites
 314               Trace("strings-extf-debug")
 315                   << "  symbolic definition is trivial..." << std::endl;
 316               nrs = Node::null();
 317             }
 318           }
 319           else
 320           {
 321             Trace("strings-extf-debug")
 322                 << "  could not infer symbolic definition." << std::endl;
 323           }
 324           Node conc;
 325           if (!nrs.isNull())
 326           {
 327             Trace("strings-extf-debug")
 328                 << "  symbolic def : " << nrs << std::endl;
 329             if (!d_state.areEqual(nrs, nrc))
 330             {
 331               // infer symbolic unit
 332               if (n.getType().isBoolean())
 333               {
 334                 conc = nrc == d_true ? nrs : nrs.negate();
 335               }
 336               else
 337               {
 338                 conc = nrs.eqNode(nrc);
 339               }
 340               einfo.d_exp.clear();
 341             }
 342           }
 343           else
 344           {
 345             if (!d_state.areEqual(n, nrc))
 346             {
 347               if (n.getType().isBoolean())
 348               {
 349                 if (d_state.areEqual(n, nrc == d_true ? d_false : d_true))
 350                 {
 351                   einfo.d_exp.push_back(nrc == d_true ? n.negate() : n);
 352                   conc = d_false;
 353                 }
 354                 else
 355                 {
 356                   conc = nrc == d_true ? n : n.negate();
 357                 }
 358               }
 359               else
 360               {
 361                 conc = n.eqNode(nrc);
 362               }
 363             }
 364           }
 365           if (!conc.isNull())
 366           {
 367             Trace("strings-extf")
 368                 << "  resolve extf : " << sn << " -> " << nrc << std::endl;
 369             Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
 370             d_im.sendInference(einfo.d_exp, conc, inf, true);
 371             d_statistics.d_cdSimplifications << n.getKind();
 372             if (d_state.isInConflict())
 373             {
 374               Trace("strings-extf-debug") << "  conflict, return." << std::endl;
 375               return;
 376             }
 377           }
 378         }
 379         else
 380         {
 381           // check if it is already equal, if so, mark as reduced. Otherwise, do
 382           // nothing.
 383           if (d_state.areEqual(n, nrc))
 384           {
 385             Trace("strings-extf")
 386                 << "  resolved extf, since satisfied by model: " << n
 387                 << std::endl;
 388             einfo.d_modelActive = false;
 389           }
 390         }
 391       }
 392       else
 393       {
 394         // if this was a predicate which changed after substitution + rewriting
 395         if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n)
 396         {
 397           bool pol = einfo.d_const == d_true;
 398           Node nrcAssert = pol ? nrc : nrc.negate();
 399           Node nAssert = pol ? n : n.negate();
 400           Assert(effort < 3);
 401           einfo.d_exp.push_back(nAssert);
 402           Trace("strings-extf-debug") << "  decomposable..." << std::endl;
 403           Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc
 404                                 << ", const = " << einfo.d_const << std::endl;
 405           // We send inferences internal here, which may help show unsat.
 406           // However, we do not make a determination whether n can be marked
 407           // reduced since this argument may be circular: we may infer than n
 408           // can be reduced to something else, but that thing may argue that it
 409           // can be reduced to n, in theory.
 410           Inference infer =
 411               effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N;
 412           d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
 413         }
 414         to_reduce = nrc;
 415       }
 416     }
 417     else
 418     {
 419       to_reduce = n;
 420     }
 421     // if not reduced
 422     if (!to_reduce.isNull())
 423     {
 424       Assert(effort < 3);
 425       if (effort == 1)
 426       {
 427         Trace("strings-extf")
 428             << "  cannot rewrite extf : " << to_reduce << std::endl;
 429       }
 430       checkExtfInference(n, to_reduce, einfo, effort);
 431       if (Trace.isOn("strings-extf-list"))
 432       {
 433         Trace("strings-extf-list") << "  * " << to_reduce;
 434         if (!einfo.d_const.isNull())
 435         {
 436           Trace("strings-extf-list") << ", const = " << einfo.d_const;
 437         }
 438         if (n != to_reduce)
 439         {
 440           Trace("strings-extf-list") << ", from " << n;
 441         }
 442         Trace("strings-extf-list") << std::endl;
 443       }
 444       if (d_extt->isActive(n) && einfo.d_modelActive)
 445       {
 446         has_nreduce = true;
 447       }
 448     }
 449   }
 450   d_hasExtf = has_nreduce;
 451 }
 452
 453 void ExtfSolver::checkExtfInference(Node n,
 454                                     Node nr,
 455                                     ExtfInfoTmp& in,
 456                                     int effort)
 457 {
 458   if (in.d_const.isNull())
 459   {
 460     return;
 461   }
 462   NodeManager* nm = NodeManager::currentNM();
 463   Trace("strings-extf-infer") << "checkExtfInference: " << n << " : " << nr
 464                               << " == " << in.d_const << std::endl;
 465
 466   // add original to explanation
 467   if (n.getType().isBoolean())
 468   {
 469     // if Boolean, it's easy
 470     in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate());
 471   }
 472   else
 473   {
 474     // otherwise, must explain via base node
 475     Node r = d_state.getRepresentative(n);
 476     // explain using the base solver
 477     d_bsolver.explainConstantEqc(n, r, in.d_exp);
 478   }
 479
 480   // d_extfInferCache stores whether we have made the inferences associated
 481   // with a node n,
 482   // this may need to be generalized if multiple inferences apply
 483
 484   if (nr.getKind() == STRING_STRCTN)
 485   {
 486     Assert(in.d_const.isConst());
 487     bool pol = in.d_const.getConst<bool>();
 488     if ((pol && nr[1].getKind() == STRING_CONCAT)
 489         || (!pol && nr[0].getKind() == STRING_CONCAT))
 490     {
 491       // If str.contains( x, str.++( y1, ..., yn ) ),
 492       //   we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
 493       // The following recognizes two situations related to the above reasoning:
 494       // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
 495       // (2) If str.contains( x, yj ) already holds for some j, then the term
 496       // str.contains( x, yj ) is irrelevant since it is satisfied by all models
 497       // for str.contains( x, str.++( y1, ..., yn ) ).
 498
 499       // Notice that the dual of the above reasoning also holds, i.e.
 500       // If ~str.contains( str.++( x1, ..., xn ), y ),
 501       //   we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
 502       // This is also handled here.
 503       if (d_extfInferCache.find(nr) == d_extfInferCache.end())
 504       {
 505         d_extfInferCache.insert(nr);
 506
 507         int index = pol ? 1 : 0;
 508         std::vector<Node> children;
 509         children.push_back(nr[0]);
 510         children.push_back(nr[1]);
 511         for (const Node& nrc : nr[index])
 512         {
 513           children[index] = nrc;
 514           Node conc = nm->mkNode(STRING_STRCTN, children);
 515           conc = Rewriter::rewrite(pol ? conc : conc.negate());
 516           // check if it already (does not) hold
 517           if (d_state.hasTerm(conc))
 518           {
 519             if (d_state.areEqual(conc, d_false))
 520             {
 521               // we are in conflict
 522               d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
 523             }
 524             else if (d_extt->hasFunctionKind(conc.getKind()))
 525             {
 526               // can mark as reduced, since model for n implies model for conc
 527               d_extt->markReduced(conc);
 528             }
 529           }
 530         }
 531       }
 532     }
 533     else
 534     {
 535       if (std::find(d_extfInfoTmp[nr[0]].d_ctn[pol].begin(),
 536                     d_extfInfoTmp[nr[0]].d_ctn[pol].end(),
 537                     nr[1])
 538           == d_extfInfoTmp[nr[0]].d_ctn[pol].end())
 539       {
 540         Trace("strings-extf-debug") << "  store contains info : " << nr[0]
 541                                     << " " << pol << " " << nr[1] << std::endl;
 542         // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
 543         d_extfInfoTmp[nr[0]].d_ctn[pol].push_back(nr[1]);
 544         d_extfInfoTmp[nr[0]].d_ctnFrom[pol].push_back(n);
 545         // Do transistive closure on contains, e.g.
 546         // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
 547
 548         // The following infers new (negative) contains based on the above
 549         // reasoning, provided that ~contains( t, r ) does not
 550         // already hold in the current context. We test this by checking that
 551         // contains( t, r ) is not already asserted false in the current
 552         // context. We also handle the case where contains( t, r ) is equivalent
 553         // to t = r, in which case we check that t != r does not already hold
 554         // in the current context.
 555
 556         // Notice that form of the above inference is enough to find
 557         // conflicts purely due to contains predicates. For example, if we
 558         // have only positive occurrences of contains, then no conflicts due to
 559         // contains predicates are possible and this schema does nothing. For
 560         // example, note that contains( s, t ) and contains( t, r ) implies
 561         // contains( s, r ), which we could but choose not to infer. Instead,
 562         // we prefer being lazy: only if ~contains( s, r ) appears later do we
 563         // infer ~contains( t, r ), which suffices to show a conflict.
 564         bool opol = !pol;
 565         for (unsigned i = 0, size = d_extfInfoTmp[nr[0]].d_ctn[opol].size();
 566              i < size;
 567              i++)
 568         {
 569           Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
 570           Node concOrig =
 571               nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]);
 572           Node conc = Rewriter::rewrite(concOrig);
 573           // For termination concerns, we only do the inference if the contains
 574           // does not rewrite (and thus does not introduce new terms).
 575           if (conc == concOrig)
 576           {
 577             bool do_infer = false;
 578             conc = conc.negate();
 579             bool pol2 = conc.getKind() != NOT;
 580             Node lit = pol2 ? conc : conc[0];
 581             if (lit.getKind() == EQUAL)
 582             {
 583               do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1])
 584                               : !d_state.areDisequal(lit[0], lit[1]);
 585             }
 586             else
 587             {
 588               do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false);
 589             }
 590             if (do_infer)
 591             {
 592               std::vector<Node> exp_c;
 593               exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
 594               Node ofrom = d_extfInfoTmp[nr[0]].d_ctnFrom[opol][i];
 595               Assert(d_extfInfoTmp.find(ofrom) != d_extfInfoTmp.end());
 596               exp_c.insert(exp_c.end(),
 597                            d_extfInfoTmp[ofrom].d_exp.begin(),
 598                            d_extfInfoTmp[ofrom].d_exp.end());
 599               d_im.sendInference(exp_c, conc, Inference::CTN_TRANS);
 600             }
 601           }
 602         }
 603       }
 604       else
 605       {
 606         // If we already know that s (does not) contain t, then n is redundant.
 607         // For example, if str.contains( x, y ), str.contains( z, y ), and x=z
 608         // are asserted in the current context, then str.contains( z, y ) is
 609         // satisfied by all models of str.contains( x, y ) ^ x=z and thus can
 610         // be ignored.
 611         Trace("strings-extf-debug") << "  redundant." << std::endl;
 612         d_extt->markReduced(n);
 613       }
 614     }
 615     return;
 616   }
 617
 618   // If it's not a predicate, see if we can solve the equality n = c, where c
 619   // is the constant that extended term n is equal to.
 620   Node inferEq = nr.eqNode(in.d_const);
 621   Node inferEqr = Rewriter::rewrite(inferEq);
 622   Node inferEqrr = inferEqr;
 623   if (inferEqr.getKind() == EQUAL)
 624   {
 625     // try to use the extended rewriter for equalities
 626     inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
 627   }
 628   if (inferEqrr != inferEqr)
 629   {
 630     inferEqrr = Rewriter::rewrite(inferEqrr);
 631     Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
 632                                 << " ...reduces to " << inferEqrr << std::endl;
 633     d_im.sendInternalInference(in.d_exp, inferEqrr, Inference::EXTF_EQ_REW);
 634   }
 635 }
 636
 637 Node ExtfSolver::getCurrentSubstitutionFor(int effort,
 638                                            Node n,
 639                                            std::vector<Node>& exp)
 640 {
 641   if (effort >= 3)
 642   {
 643     // model values
 644     Node mv = d_state.getModel()->getRepresentative(n);
 645     Trace("strings-subs") << "   model val : " << mv << std::endl;
 646     return mv;
 647   }
 648   Node nr = d_state.getRepresentative(n);
 649   Node c = d_bsolver.explainConstantEqc(n, nr, exp);
 650   if (!c.isNull())
 651   {
 652     return c;
 653   }
 654   else if (effort >= 1 && n.getType().isStringLike())
 655   {
 656     Assert(effort < 3);
 657     // normal forms
 658     NormalForm& nfnr = d_csolver.getNormalForm(nr);
 659     Node ns = d_csolver.getNormalString(nfnr.d_base, exp);
 660     Trace("strings-subs") << "   normal eqc : " << ns << " " << nfnr.d_base
 661                           << " " << nr << std::endl;
 662     if (!nfnr.d_base.isNull())
 663     {
 664       d_im.addToExplanation(n, nfnr.d_base, exp);
 665     }
 666     return ns;
 667   }
 668   return n;
 669 }
 670
 671 const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const
 672 {
 673   return d_extfInfoTmp;
 674 }
 675 bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
 676
 677 std::vector<Node> ExtfSolver::getActive(Kind k) const
 678 {
 679   return d_extt->getActive(k);
 680 }
 681
 682 }  // namespace strings
 683 }  // namespace theory
 684 }  // namespace CVC4