src/theory/strings/extf_solver.cpp

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