src/theory/strings/infer_proof_cons.cpp

   1 /*********************                                                        */
   2 /*! \file infer_proof_cons.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-2020 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 inference to proof conversion
  13  **/
  14
  15 #include "theory/strings/infer_proof_cons.h"
  16
  17 #include "expr/skolem_manager.h"
  18 #include "options/smt_options.h"
  19 #include "options/strings_options.h"
  20 #include "theory/builtin/proof_checker.h"
  21 #include "theory/rewriter.h"
  22 #include "theory/strings/regexp_operation.h"
  23 #include "theory/strings/theory_strings_utils.h"
  24
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace strings {
  30
  31 InferProofCons::InferProofCons(context::Context* c,
  32                                ProofNodeManager* pnm,
  33                                SequencesStatistics& statistics)
  34     : d_pnm(pnm), d_lazyFactMap(c), d_statistics(statistics)
  35 {
  36   Assert(d_pnm != nullptr);
  37 }
  38
  39 void InferProofCons::notifyFact(const InferInfo& ii)
  40 {
  41   Node fact = ii.d_conc;
  42   Trace("strings-ipc-debug")
  43       << "InferProofCons::notifyFact: " << ii << std::endl;
  44   if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
  45   {
  46     Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
  47     return;
  48   }
  49   Node symFact = CDProof::getSymmFact(fact);
  50   if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
  51   {
  52     Trace("strings-ipc-debug") << "...duplicate (sym)!" << std::endl;
  53     return;
  54   }
  55   std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
  56   d_lazyFactMap.insert(ii.d_conc, iic);
  57 }
  58
  59 void InferProofCons::convert(Inference infer,
  60                              bool isRev,
  61                              Node conc,
  62                              const std::vector<Node>& exp,
  63                              ProofStep& ps,
  64                              TheoryProofStepBuffer& psb,
  65                              bool& useBuffer)
  66 {
  67   // by default, don't use the buffer
  68   useBuffer = false;
  69   // Must flatten children with respect to AND to be ready to explain.
  70   // We store the index where each flattened vector begins, since some
  71   // explanations are grouped together using AND.
  72   std::vector<size_t> startExpIndex;
  73   for (const Node& ec : exp)
  74   {
  75     // store the index in the flattened vector
  76     startExpIndex.push_back(ps.d_children.size());
  77     utils::flattenOp(AND, ec, ps.d_children);
  78   }
  79   // debug print
  80   if (Trace.isOn("strings-ipc-debug"))
  81   {
  82     Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer
  83                                << (isRev ? " :rev " : " ") << conc << std::endl;
  84     for (const Node& ec : exp)
  85     {
  86       Trace("strings-ipc-debug") << "    e: " << ec << std::endl;
  87     }
  88   }
  89   // try to find a set of proof steps to incorporate into the buffer
  90   psb.clear();
  91   NodeManager* nm = NodeManager::currentNM();
  92   Node nodeIsRev = nm->mkConst(isRev);
  93   switch (infer)
  94   {
  95     // ========================== equal by substitution+rewriting
  96     case Inference::I_NORM_S:
  97     case Inference::I_CONST_MERGE:
  98     case Inference::I_NORM:
  99     case Inference::LEN_NORM:
 100     case Inference::NORMAL_FORM:
 101     case Inference::CODE_PROXY:
 102     {
 103       ps.d_args.push_back(conc);
 104       // will attempt this rule
 105       ps.d_rule = PfRule::MACRO_SR_PRED_INTRO;
 106     }
 107     break;
 108     // ========================== substitution + rewriting
 109     case Inference::RE_NF_CONFLICT:
 110     case Inference::EXTF:
 111     case Inference::EXTF_N:
 112     case Inference::EXTF_D:
 113     case Inference::EXTF_D_N:
 114     case Inference::I_CONST_CONFLICT:
 115     case Inference::UNIT_CONST_CONFLICT:
 116     {
 117       if (!ps.d_children.empty())
 118       {
 119         std::vector<Node> exps(ps.d_children.begin(), ps.d_children.end() - 1);
 120         Node src = ps.d_children[ps.d_children.size() - 1];
 121         if (psb.applyPredTransform(src, conc, exps))
 122         {
 123           useBuffer = true;
 124         }
 125       }
 126       if (!useBuffer)
 127       {
 128         // use the predicate version?
 129         ps.d_args.push_back(conc);
 130         ps.d_rule = PfRule::MACRO_SR_PRED_INTRO;
 131       }
 132     }
 133     break;
 134     // ========================== rewrite pred
 135     case Inference::EXTF_EQ_REW:
 136     case Inference::INFER_EMP:
 137     {
 138       // the last child is the predicate we are operating on, move to front
 139       Node src = ps.d_children[ps.d_children.size() - 1];
 140       std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1);
 141       // start with a default rewrite
 142       Node mainEqSRew = psb.applyPredElim(src, expe);
 143       if (mainEqSRew == conc)
 144       {
 145         useBuffer = true;
 146         break;
 147       }
 148       // may need the "extended equality rewrite"
 149       Node mainEqSRew2 = psb.applyPredElim(
 150           mainEqSRew, {}, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT);
 151       if (mainEqSRew2 == conc)
 152       {
 153         useBuffer = true;
 154         break;
 155       }
 156       // rewrite again with default rewriter
 157       Node mainEqSRew3 = psb.applyPredElim(mainEqSRew2, {});
 158       useBuffer = (mainEqSRew3 == conc);
 159     }
 160     break;
 161     // ========================== substitution+rewriting, CONCAT_EQ, ...
 162     case Inference::F_CONST:
 163     case Inference::F_UNIFY:
 164     case Inference::F_ENDPOINT_EMP:
 165     case Inference::F_ENDPOINT_EQ:
 166     case Inference::F_NCTN:
 167     case Inference::N_EQ_CONF:
 168     case Inference::N_CONST:
 169     case Inference::N_UNIFY:
 170     case Inference::N_ENDPOINT_EMP:
 171     case Inference::N_ENDPOINT_EQ:
 172     case Inference::N_NCTN:
 173     case Inference::SSPLIT_CST_PROP:
 174     case Inference::SSPLIT_VAR_PROP:
 175     case Inference::SSPLIT_CST:
 176     case Inference::SSPLIT_VAR:
 177     {
 178       Trace("strings-ipc-core") << "Generate core rule for " << infer
 179                                 << " (rev=" << isRev << ")" << std::endl;
 180       // All of the above inferences have the form:
 181       //   (explanation for why t and s have the same prefix/suffix) ^
 182       //   t = s ^
 183       //   (length constraint)?
 184       // We call t=s the "main equality" below. The length constraint is
 185       // optional, which we split on below.
 186       size_t nchild = ps.d_children.size();
 187       size_t mainEqIndex = 0;
 188       bool mainEqIndexSet = false;
 189       // the length constraint
 190       std::vector<Node> lenConstraint;
 191       // these inferences have a length constraint as the last explain
 192       if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY
 193           || infer == Inference::SSPLIT_CST || infer == Inference::SSPLIT_VAR
 194           || infer == Inference::SSPLIT_VAR_PROP
 195           || infer == Inference::SSPLIT_CST_PROP)
 196       {
 197         if (exp.size() >= 2)
 198         {
 199           Assert(exp.size() <= startExpIndex.size());
 200           // The index of the "main" equality is the last equality before
 201           // the length explanation.
 202           mainEqIndex = startExpIndex[exp.size() - 1] - 1;
 203           mainEqIndexSet = true;
 204           // the remainder is the length constraint
 205           lenConstraint.insert(lenConstraint.end(),
 206                                ps.d_children.begin() + mainEqIndex + 1,
 207                                ps.d_children.end());
 208         }
 209       }
 210       else if (nchild >= 1)
 211       {
 212         // The index of the main equality is the last child.
 213         mainEqIndex = nchild - 1;
 214         mainEqIndexSet = true;
 215       }
 216       Node mainEq;
 217       if (mainEqIndexSet)
 218       {
 219         mainEq = ps.d_children[mainEqIndex];
 220         Trace("strings-ipc-core") << "Main equality " << mainEq << " at index "
 221                                   << mainEqIndex << std::endl;
 222       }
 223       if (mainEq.isNull() || mainEq.getKind() != EQUAL)
 224       {
 225         Trace("strings-ipc-core")
 226             << "...failed to find main equality" << std::endl;
 227         break;
 228       }
 229       // apply MACRO_SR_PRED_ELIM using equalities up to the main eq
 230       std::vector<Node> childrenSRew;
 231       childrenSRew.push_back(mainEq);
 232       childrenSRew.insert(childrenSRew.end(),
 233                           ps.d_children.begin(),
 234                           ps.d_children.begin() + mainEqIndex);
 235       Node mainEqSRew =
 236           psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {});
 237       if (CDProof::isSame(mainEqSRew, mainEq))
 238       {
 239         Trace("strings-ipc-core") << "...undo step" << std::endl;
 240         // the rule added above was not necessary
 241         psb.popStep();
 242       }
 243       else if (mainEqSRew == conc)
 244       {
 245         Trace("strings-ipc-core") << "...success after rewrite!" << std::endl;
 246         useBuffer = true;
 247         break;
 248       }
 249       Trace("strings-ipc-core")
 250           << "Main equality after subs+rewrite " << mainEqSRew << std::endl;
 251       // now, apply CONCAT_EQ to get the remainder
 252       std::vector<Node> childrenCeq;
 253       childrenCeq.push_back(mainEqSRew);
 254       std::vector<Node> argsCeq;
 255       argsCeq.push_back(nodeIsRev);
 256       Node mainEqCeq = psb.tryStep(PfRule::CONCAT_EQ, childrenCeq, argsCeq);
 257       Trace("strings-ipc-core")
 258           << "Main equality after CONCAT_EQ " << mainEqCeq << std::endl;
 259       if (mainEqCeq.isNull() || mainEqCeq.getKind() != EQUAL)
 260       {
 261         // fail
 262         break;
 263       }
 264       else if (mainEqCeq == mainEqSRew)
 265       {
 266         Trace("strings-ipc-core") << "...undo step" << std::endl;
 267         // not necessary, probably first component of equality
 268         psb.popStep();
 269       }
 270       // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
 271       // inference involved t and s.
 272       if (infer == Inference::N_ENDPOINT_EQ
 273           || infer == Inference::N_ENDPOINT_EMP
 274           || infer == Inference::F_ENDPOINT_EQ
 275           || infer == Inference::F_ENDPOINT_EMP)
 276       {
 277         // Should be equal to conclusion already, or rewrite to it.
 278         // Notice that this step is necessary to handle the "rproc"
 279         // optimization in processSimpleNEq. Alternatively, this could
 280         // possibly be done by CONCAT_EQ with !isRev.
 281         std::vector<Node> cexp;
 282         if (psb.applyPredTransform(mainEqCeq,
 283                                    conc,
 284                                    cexp,
 285                                    MethodId::SB_DEFAULT,
 286                                    MethodId::RW_REWRITE_EQ_EXT))
 287         {
 288           Trace("strings-ipc-core") << "Transformed to " << conc
 289                                     << " via pred transform" << std::endl;
 290           // success
 291           useBuffer = true;
 292           Trace("strings-ipc-core") << "...success!" << std::endl;
 293         }
 294         // Otherwise, note that EMP rules conclude ti = "" where
 295         // t1 ++ ... ++ tn == "". However, these are very rarely applied, let
 296         // alone for 2+ children. This case is intentionally unhandled here.
 297       }
 298       else if (infer == Inference::N_CONST || infer == Inference::F_CONST
 299                || infer == Inference::N_EQ_CONF)
 300       {
 301         // should be a constant conflict
 302         std::vector<Node> childrenC;
 303         childrenC.push_back(mainEqCeq);
 304         std::vector<Node> argsC;
 305         argsC.push_back(nodeIsRev);
 306         Node mainEqC = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC);
 307         if (mainEqC == conc)
 308         {
 309           useBuffer = true;
 310           Trace("strings-ipc-core") << "...success!" << std::endl;
 311         }
 312       }
 313       else
 314       {
 315         std::vector<Node> tvec;
 316         std::vector<Node> svec;
 317         utils::getConcat(mainEqCeq[0], tvec);
 318         utils::getConcat(mainEqCeq[1], svec);
 319         Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
 320         Node s0 = svec[isRev ? svec.size() - 1 : 0];
 321         bool applySym = false;
 322         // may need to apply symmetry
 323         if ((infer == Inference::SSPLIT_CST
 324              || infer == Inference::SSPLIT_CST_PROP)
 325             && t0.isConst())
 326         {
 327           Assert(!s0.isConst());
 328           applySym = true;
 329           std::swap(t0, s0);
 330         }
 331         if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY)
 332         {
 333           if (conc.getKind() != EQUAL)
 334           {
 335             break;
 336           }
 337           // one side should match, the other side could be a split constant
 338           if (conc[0] != t0 && conc[1] != s0)
 339           {
 340             applySym = true;
 341             std::swap(t0, s0);
 342           }
 343           Assert(conc[0].isConst() == t0.isConst());
 344           Assert(conc[1].isConst() == s0.isConst());
 345         }
 346         PfRule rule = PfRule::UNKNOWN;
 347         // the form of the required length constraint expected by the proof
 348         Node lenReq;
 349         bool lenSuccess = false;
 350         if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY)
 351         {
 352           // the required premise for unify is always len(x) = len(y),
 353           // however the explanation may not be literally this. Thus, we
 354           // need to reconstruct a proof from the given explanation.
 355           // it should be the case that lenConstraint => lenReq.
 356           // We use terms in the conclusion equality, not t0, s0 here.
 357           lenReq = nm->mkNode(STRING_LENGTH, conc[0])
 358                        .eqNode(nm->mkNode(STRING_LENGTH, conc[1]));
 359           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
 360           rule = PfRule::CONCAT_UNIFY;
 361         }
 362         else if (infer == Inference::SSPLIT_VAR)
 363         {
 364           // it should be the case that lenConstraint => lenReq
 365           lenReq = nm->mkNode(STRING_LENGTH, t0)
 366                        .eqNode(nm->mkNode(STRING_LENGTH, s0))
 367                        .notNode();
 368           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
 369           rule = PfRule::CONCAT_SPLIT;
 370         }
 371         else if (infer == Inference::SSPLIT_CST)
 372         {
 373           // it should be the case that lenConstraint => lenReq
 374           lenReq = nm->mkNode(STRING_LENGTH, t0)
 375                        .eqNode(nm->mkConst(Rational(0)))
 376                        .notNode();
 377           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
 378           rule = PfRule::CONCAT_CSPLIT;
 379         }
 380         else if (infer == Inference::SSPLIT_VAR_PROP)
 381         {
 382           // it should be the case that lenConstraint => lenReq
 383           for (unsigned r = 0; r < 2; r++)
 384           {
 385             lenReq = nm->mkNode(GT,
 386                                 nm->mkNode(STRING_LENGTH, t0),
 387                                 nm->mkNode(STRING_LENGTH, s0));
 388             if (convertLengthPf(lenReq, lenConstraint, psb))
 389             {
 390               lenSuccess = true;
 391               break;
 392             }
 393             if (r == 0)
 394             {
 395               // may be the other direction
 396               applySym = true;
 397               std::swap(t0, s0);
 398             }
 399           }
 400           rule = PfRule::CONCAT_LPROP;
 401         }
 402         else if (infer == Inference::SSPLIT_CST_PROP)
 403         {
 404           // it should be the case that lenConstraint => lenReq
 405           lenReq = nm->mkNode(STRING_LENGTH, t0)
 406                        .eqNode(nm->mkConst(Rational(0)))
 407                        .notNode();
 408           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
 409           rule = PfRule::CONCAT_CPROP;
 410         }
 411         if (!lenSuccess)
 412         {
 413           Trace("strings-ipc-core")
 414               << "...failed due to length constraint" << std::endl;
 415           break;
 416         }
 417         // apply symmetry if necessary
 418         if (applySym)
 419         {
 420           std::vector<Node> childrenSymm;
 421           childrenSymm.push_back(mainEqCeq);
 422           // note this explicit step may not be necessary
 423           mainEqCeq = psb.tryStep(PfRule::SYMM, childrenSymm, {});
 424           Trace("strings-ipc-core")
 425               << "Main equality after SYMM " << mainEqCeq << std::endl;
 426         }
 427         if (rule != PfRule::UNKNOWN)
 428         {
 429           Trace("strings-ipc-core")
 430               << "Core rule length requirement is " << lenReq << std::endl;
 431           // apply the given rule
 432           std::vector<Node> childrenMain;
 433           childrenMain.push_back(mainEqCeq);
 434           childrenMain.push_back(lenReq);
 435           std::vector<Node> argsMain;
 436           argsMain.push_back(nodeIsRev);
 437           Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain);
 438           Trace("strings-ipc-core") << "Main equality after " << rule << " "
 439                                     << mainEqMain << std::endl;
 440           if (mainEqMain == mainEqCeq)
 441           {
 442             Trace("strings-ipc-core") << "...undo step" << std::endl;
 443             // not necessary, probably first component of equality
 444             psb.popStep();
 445           }
 446           // either equal or rewrites to it
 447           std::vector<Node> cexp;
 448           if (psb.applyPredTransform(mainEqMain, conc, cexp))
 449           {
 450             // requires that length success is also true
 451             useBuffer = true;
 452             Trace("strings-ipc-core") << "...success" << std::endl;
 453           }
 454           else
 455           {
 456             Trace("strings-ipc-core") << "...fail" << std::endl;
 457           }
 458         }
 459         else
 460         {
 461           // should always have given a rule to try above
 462           Assert(false) << "No reconstruction rule given for " << infer;
 463         }
 464       }
 465     }
 466     break;
 467     // ========================== Disequalities
 468     case Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
 469     case Inference::DEQ_DISL_STRINGS_SPLIT:
 470     {
 471       if (conc.getKind() != AND || conc.getNumChildren() != 2
 472           || conc[0].getKind() != EQUAL || !conc[0][0].getType().isStringLike()
 473           || conc[1].getKind() != EQUAL
 474           || conc[1][0].getKind() != STRING_LENGTH)
 475       {
 476         Trace("strings-ipc-deq") << "malformed application" << std::endl;
 477         Assert(false) << "unexpected conclusion " << conc << " for " << infer;
 478       }
 479       else
 480       {
 481         Node lenReq =
 482             nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, conc[0][0]), conc[1][1]);
 483         Trace("strings-ipc-deq")
 484             << "length requirement is " << lenReq << std::endl;
 485         if (convertLengthPf(lenReq, ps.d_children, psb))
 486         {
 487           Trace("strings-ipc-deq") << "...success length" << std::endl;
 488           // make the proof
 489           std::vector<Node> childrenMain;
 490           childrenMain.push_back(lenReq);
 491           std::vector<Node> argsMain;
 492           argsMain.push_back(nodeIsRev);
 493           Node mainConc =
 494               psb.tryStep(PfRule::STRING_DECOMPOSE, childrenMain, argsMain);
 495           Trace("strings-ipc-deq")
 496               << "...main conclusion is " << mainConc << std::endl;
 497           useBuffer = (mainConc == conc);
 498           Trace("strings-ipc-deq")
 499               << "...success is " << useBuffer << std::endl;
 500         }
 501         else
 502         {
 503           Trace("strings-ipc-deq") << "...fail length" << std::endl;
 504         }
 505       }
 506     }
 507     break;
 508     // ========================== Boolean split
 509     case Inference::CARD_SP:
 510     case Inference::LEN_SPLIT:
 511     case Inference::LEN_SPLIT_EMP:
 512     case Inference::DEQ_DISL_EMP_SPLIT:
 513     case Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
 514     case Inference::DEQ_STRINGS_EQ:
 515     case Inference::DEQ_LENS_EQ:
 516     case Inference::DEQ_LENGTH_SP:
 517     {
 518       if (conc.getKind() != OR)
 519       {
 520         // This should never happen. If it does, we resort to using
 521         // STRING_TRUST below (in production mode).
 522         Assert(false) << "Expected OR conclusion for " << infer;
 523       }
 524       else
 525       {
 526         ps.d_rule = PfRule::SPLIT;
 527         Assert(ps.d_children.empty());
 528         ps.d_args.push_back(conc[0]);
 529       }
 530     }
 531     break;
 532     // ========================== Regular expression unfolding
 533     case Inference::RE_UNFOLD_POS:
 534     case Inference::RE_UNFOLD_NEG:
 535     {
 536       if (infer == Inference::RE_UNFOLD_POS)
 537       {
 538         ps.d_rule = PfRule::RE_UNFOLD_POS;
 539       }
 540       else
 541       {
 542         ps.d_rule = PfRule::RE_UNFOLD_NEG;
 543         // it may be an optimized form of concat simplification
 544         Assert(ps.d_children.size() == 1);
 545         Node mem = ps.d_children[0];
 546         Assert(mem.getKind() == NOT && mem[0].getKind() == STRING_IN_REGEXP);
 547         if (mem[0][1].getKind() == REGEXP_CONCAT)
 548         {
 549           size_t index;
 550           Node reLen = RegExpOpr::getRegExpConcatFixed(mem[0][1], index);
 551           // if we can find a fixed length for a component, use the optimized
 552           // version
 553           if (!reLen.isNull())
 554           {
 555             ps.d_rule = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED;
 556           }
 557         }
 558       }
 559     }
 560     break;
 561     // ========================== Reduction
 562     case Inference::CTN_POS:
 563     case Inference::CTN_NEG_EQUAL:
 564     {
 565       if (ps.d_children.size() != 1)
 566       {
 567         break;
 568       }
 569       bool polarity = ps.d_children[0].getKind() != NOT;
 570       Node atom = polarity ? ps.d_children[0] : ps.d_children[0][0];
 571       std::vector<Node> args;
 572       args.push_back(atom);
 573       Node res = psb.tryStep(PfRule::STRING_EAGER_REDUCTION, {}, args);
 574       if (res.isNull())
 575       {
 576         break;
 577       }
 578       // ite( contains(x,t), x = k1 ++ t ++ k2, x != t )
 579       std::vector<Node> tiChildren;
 580       tiChildren.push_back(ps.d_children[0]);
 581       Node ctnt = psb.tryStep(
 582           polarity ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO, tiChildren, {});
 583       if (ctnt.isNull() || ctnt.getKind() != EQUAL)
 584       {
 585         break;
 586       }
 587       std::vector<Node> tchildren;
 588       tchildren.push_back(ctnt);
 589       // apply substitution { contains(x,t) -> true|false } and rewrite to get
 590       // conclusion x = k1 ++ t ++ k2 or x != t.
 591       if (psb.applyPredTransform(res, conc, tchildren))
 592       {
 593         useBuffer = true;
 594       }
 595     }
 596     break;
 597
 598     case Inference::REDUCTION:
 599     {
 600       size_t nchild = conc.getNumChildren();
 601       Node mainEq;
 602       if (conc.getKind() == EQUAL)
 603       {
 604         mainEq = conc;
 605       }
 606       else if (conc.getKind() == AND && conc[nchild - 1].getKind() == EQUAL)
 607       {
 608         mainEq = conc[nchild - 1];
 609       }
 610       if (mainEq.isNull())
 611       {
 612         Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl;
 613         Assert(false) << "Unexpected reduction " << conc;
 614         break;
 615       }
 616       std::vector<Node> argsRed;
 617       // the left hand side of the last conjunct is the term we are reducing
 618       argsRed.push_back(mainEq[0]);
 619       Node red = psb.tryStep(PfRule::STRING_REDUCTION, {}, argsRed);
 620       Trace("strings-ipc-red") << "Reduction : " << red << std::endl;
 621       if (!red.isNull())
 622       {
 623         // either equal or rewrites to it
 624         std::vector<Node> cexp;
 625         if (psb.applyPredTransform(red, conc, cexp))
 626         {
 627           Trace("strings-ipc-red") << "...success!" << std::endl;
 628           useBuffer = true;
 629         }
 630         else
 631         {
 632           Trace("strings-ipc-red") << "...failed to reduce" << std::endl;
 633         }
 634       }
 635     }
 636     break;
 637     // ========================== code injectivity
 638     case Inference::CODE_INJ:
 639     {
 640       ps.d_rule = PfRule::STRING_CODE_INJ;
 641       Assert(conc.getKind() == OR && conc.getNumChildren() == 3
 642              && conc[2].getKind() == EQUAL);
 643       ps.d_args.push_back(conc[2][0]);
 644       ps.d_args.push_back(conc[2][1]);
 645     }
 646     break;
 647     // ========================== unit injectivity
 648     case Inference::UNIT_INJ: { ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
 649     }
 650     break;
 651     // ========================== prefix conflict
 652     case Inference::PREFIX_CONFLICT:
 653     {
 654       Trace("strings-ipc-prefix") << "Prefix conflict..." << std::endl;
 655       std::vector<Node> eqs;
 656       for (const Node& e : ps.d_children)
 657       {
 658         Kind ek = e.getKind();
 659         if (ek == EQUAL)
 660         {
 661           Trace("strings-ipc-prefix") << "- equality : " << e << std::endl;
 662           eqs.push_back(e);
 663         }
 664         else if (ek == STRING_IN_REGEXP)
 665         {
 666           // unfold it and extract the equality
 667           std::vector<Node> children;
 668           children.push_back(e);
 669           std::vector<Node> args;
 670           Node eunf = psb.tryStep(PfRule::RE_UNFOLD_POS, children, args);
 671           Trace("strings-ipc-prefix")
 672               << "--- " << e << " unfolds to " << eunf << std::endl;
 673           if (eunf.isNull())
 674           {
 675             continue;
 676           }
 677           else if (eunf.getKind() == AND)
 678           {
 679             // equality is the last conjunct
 680             std::vector<Node> childrenAE;
 681             childrenAE.push_back(eunf);
 682             std::vector<Node> argsAE;
 683             argsAE.push_back(nm->mkConst(Rational(eunf.getNumChildren() - 1)));
 684             Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE);
 685             Trace("strings-ipc-prefix")
 686                 << "--- and elim to " << eunfAE << std::endl;
 687             if (eunfAE.isNull() || eunfAE.getKind() != EQUAL)
 688             {
 689               Assert(false)
 690                   << "Unexpected unfolded premise " << eunf << " for " << infer;
 691               continue;
 692             }
 693             Trace("strings-ipc-prefix")
 694                 << "- equality : " << eunfAE << std::endl;
 695             eqs.push_back(eunfAE);
 696           }
 697           else if (eunf.getKind() == EQUAL)
 698           {
 699             Trace("strings-ipc-prefix") << "- equality : " << eunf << std::endl;
 700             eqs.push_back(eunf);
 701           }
 702         }
 703         else
 704         {
 705           // not sure how to use this assumption
 706           Assert(false) << "Unexpected premise " << e << " for " << infer;
 707         }
 708       }
 709       if (eqs.empty())
 710       {
 711         break;
 712       }
 713       // connect via transitivity
 714       Node curr = eqs[0];
 715       for (size_t i = 1, esize = eqs.size(); i < esize; i++)
 716       {
 717         Node prev = curr;
 718         curr = convertTrans(curr, eqs[1], psb);
 719         if (curr.isNull())
 720         {
 721           break;
 722         }
 723         Trace("strings-ipc-prefix") << "- Via trans: " << curr << std::endl;
 724       }
 725       if (curr.isNull())
 726       {
 727         break;
 728       }
 729       Trace("strings-ipc-prefix")
 730           << "- Possible conflicting equality : " << curr << std::endl;
 731       std::vector<Node> emp;
 732       Node concE = psb.applyPredElim(curr, emp);
 733       Trace("strings-ipc-prefix")
 734           << "- After pred elim: " << concE << std::endl;
 735       if (concE == conc)
 736       {
 737         Trace("strings-ipc-prefix") << "...success!" << std::endl;
 738         useBuffer = true;
 739       }
 740     }
 741     break;
 742     // ========================== regular expressions
 743     case Inference::RE_INTER_INCLUDE:
 744     case Inference::RE_INTER_CONF:
 745     case Inference::RE_INTER_INFER:
 746     {
 747       std::vector<Node> reiExp;
 748       std::vector<Node> reis;
 749       std::vector<Node> reiChildren;
 750       std::vector<Node> reiChildrenOrig;
 751       Node x;
 752       // make the regular expression intersection that summarizes all
 753       // memberships in the explanation
 754       for (const Node& c : ps.d_children)
 755       {
 756         bool polarity = c.getKind() != NOT;
 757         Node catom = polarity ? c : c[0];
 758         if (catom.getKind() != STRING_IN_REGEXP)
 759         {
 760           Assert(c.getKind() == EQUAL);
 761           if (c.getKind() == EQUAL)
 762           {
 763             reiExp.push_back(c);
 764           }
 765           continue;
 766         }
 767         if (x.isNull())
 768         {
 769           // just take the first LHS; others should be equated to it by exp
 770           x = catom[0];
 771         }
 772         Node rcurr =
 773             polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]);
 774         reis.push_back(rcurr);
 775         Node mem = nm->mkNode(STRING_IN_REGEXP, catom[0], rcurr);
 776         reiChildren.push_back(mem);
 777         reiChildrenOrig.push_back(c);
 778       }
 779       // go back and justify each premise
 780       bool successChildren = true;
 781       for (size_t i = 0, nchild = reiChildren.size(); i < nchild; i++)
 782       {
 783         if (!psb.applyPredTransform(reiChildrenOrig[i], reiChildren[i], reiExp))
 784         {
 785           Trace("strings-ipc-re")
 786               << "... failed to justify child " << reiChildren[i] << " from "
 787               << reiChildrenOrig[i] << std::endl;
 788           successChildren = false;
 789           break;
 790         }
 791       }
 792       if (!successChildren)
 793       {
 794         break;
 795       }
 796       Node mem = psb.tryStep(PfRule::RE_INTER, reiChildren, {});
 797       Trace("strings-ipc-re")
 798           << "Regular expression summary: " << mem << std::endl;
 799       // the conclusion is rewritable to the premises via rewriting?
 800       if (psb.applyPredTransform(mem, conc, {}))
 801       {
 802         Trace("strings-ipc-re") << "... success!" << std::endl;
 803         useBuffer = true;
 804       }
 805       else
 806       {
 807         Trace("strings-ipc-re")
 808             << "...failed to rewrite to conclusion" << std::endl;
 809       }
 810     }
 811     break;
 812     // ========================== unknown and currently unsupported
 813     case Inference::CARDINALITY:
 814     case Inference::I_CYCLE_E:
 815     case Inference::I_CYCLE:
 816     case Inference::RE_DELTA:
 817     case Inference::RE_DELTA_CONF:
 818     case Inference::RE_DERIVE:
 819     case Inference::FLOOP:
 820     case Inference::FLOOP_CONFLICT:
 821     case Inference::DEQ_NORM_EMP:
 822     case Inference::CTN_TRANS:
 823     case Inference::CTN_DECOMPOSE:
 824     default:
 825       // do nothing, these will be converted to STRING_TRUST below since the
 826       // rule is unknown.
 827       break;
 828   }
 829
 830   // now see if we would succeed with the checker-to-try
 831   bool success = false;
 832   if (ps.d_rule != PfRule::UNKNOWN)
 833   {
 834     Trace("strings-ipc") << "For " << infer << ", try proof rule " << ps.d_rule
 835                          << "...";
 836     Assert(ps.d_rule != PfRule::UNKNOWN);
 837     Node pconc = psb.tryStep(ps.d_rule, ps.d_children, ps.d_args);
 838     if (pconc.isNull() || pconc != conc)
 839     {
 840       Trace("strings-ipc") << "failed, pconc is " << pconc << " (expected "
 841                            << conc << ")" << std::endl;
 842       ps.d_rule = PfRule::UNKNOWN;
 843     }
 844     else
 845     {
 846       // successfully set up a single step proof in ps
 847       success = true;
 848       Trace("strings-ipc") << "success!" << std::endl;
 849     }
 850   }
 851   else if (useBuffer)
 852   {
 853     // successfully set up a multi step proof in psb
 854     success = true;
 855   }
 856   else
 857   {
 858     Trace("strings-ipc") << "For " << infer << " " << conc
 859                          << ", no proof rule, failed" << std::endl;
 860   }
 861   if (!success)
 862   {
 863     // debug print
 864     if (Trace.isOn("strings-ipc-fail"))
 865     {
 866       Trace("strings-ipc-fail")
 867           << "InferProofCons::convert: Failed " << infer
 868           << (isRev ? " :rev " : " ") << conc << std::endl;
 869       for (const Node& ec : exp)
 870       {
 871         Trace("strings-ipc-fail") << "    e: " << ec << std::endl;
 872       }
 873     }
 874     // untrustworthy conversion, the argument of STRING_TRUST is its conclusion
 875     ps.d_args.clear();
 876     ps.d_args.push_back(conc);
 877     // use the trust rule
 878     ps.d_rule = PfRule::STRING_TRUST;
 879     // add to stats
 880     d_statistics.d_inferencesNoPf << infer;
 881   }
 882   if (Trace.isOn("strings-ipc-debug"))
 883   {
 884     if (useBuffer)
 885     {
 886       Trace("strings-ipc-debug")
 887           << "InferProofCons::convert returned buffer with "
 888           << psb.getNumSteps() << " steps:" << std::endl;
 889       const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
 890       for (const std::pair<Node, ProofStep>& step : steps)
 891       {
 892         Trace("strings-ipc-debug")
 893             << "- " << step.first << " via " << step.second << std::endl;
 894       }
 895     }
 896     else
 897     {
 898       Trace("strings-ipc-debug")
 899           << "InferProofCons::convert returned " << ps << std::endl;
 900     }
 901   }
 902 }
 903
 904 bool InferProofCons::convertLengthPf(Node lenReq,
 905                                      const std::vector<Node>& lenExp,
 906                                      TheoryProofStepBuffer& psb)
 907 {
 908   for (const Node& le : lenExp)
 909   {
 910     if (lenReq == le)
 911     {
 912       return true;
 913     }
 914   }
 915   Trace("strings-ipc-len") << "Must explain " << lenReq << " by " << lenExp
 916                            << std::endl;
 917   for (const Node& le : lenExp)
 918   {
 919     // probably rewrites to it?
 920     std::vector<Node> exp;
 921     if (psb.applyPredTransform(le, lenReq, exp))
 922     {
 923       Trace("strings-ipc-len") << "...success by rewrite" << std::endl;
 924       return true;
 925     }
 926     // maybe x != "" => len(x) != 0
 927     std::vector<Node> children;
 928     children.push_back(le);
 929     std::vector<Node> args;
 930     Node res = psb.tryStep(PfRule::STRING_LENGTH_NON_EMPTY, children, args);
 931     if (res == lenReq)
 932     {
 933       Trace("strings-ipc-len") << "...success by LENGTH_NON_EMPTY" << std::endl;
 934       return true;
 935     }
 936   }
 937   Trace("strings-ipc-len") << "...failed" << std::endl;
 938   return false;
 939 }
 940
 941 Node InferProofCons::convertTrans(Node eqa,
 942                                   Node eqb,
 943                                   TheoryProofStepBuffer& psb)
 944 {
 945   if (eqa.getKind() != EQUAL || eqb.getKind() != EQUAL)
 946   {
 947     return Node::null();
 948   }
 949   for (uint32_t i = 0; i < 2; i++)
 950   {
 951     Node eqaSym = i == 0 ? eqa[1].eqNode(eqa[0]) : eqa;
 952     for (uint32_t j = 0; j < 2; j++)
 953     {
 954       Node eqbSym = j == 0 ? eqb : eqb[1].eqNode(eqb[1]);
 955       if (eqa[i] == eqb[j])
 956       {
 957         std::vector<Node> children;
 958         children.push_back(eqaSym);
 959         children.push_back(eqbSym);
 960         return psb.tryStep(PfRule::TRANS, children, {});
 961       }
 962     }
 963   }
 964   return Node::null();
 965 }
 966
 967 std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
 968 {
 969   // temporary proof
 970   CDProof pf(d_pnm);
 971   // get the inference
 972   NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
 973   if (it == d_lazyFactMap.end())
 974   {
 975     Node factSym = CDProof::getSymmFact(fact);
 976     if (!factSym.isNull())
 977     {
 978       // Use the symmetric fact. There is no need to explictly make a
 979       // SYMM proof, as this is handled by CDProof::getProofFor below.
 980       it = d_lazyFactMap.find(factSym);
 981     }
 982   }
 983   AlwaysAssert(it != d_lazyFactMap.end());
 984   // now go back and convert it to proof steps and add to proof
 985   bool useBuffer = false;
 986   ProofStep ps;
 987   TheoryProofStepBuffer psb(d_pnm->getChecker());
 988   std::shared_ptr<InferInfo> ii = (*it).second;
 989   // run the conversion
 990   convert(ii->d_id, ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer);
 991   // make the proof based on the step or the buffer
 992   if (useBuffer)
 993   {
 994     if (!pf.addSteps(psb))
 995     {
 996       return nullptr;
 997     }
 998   }
 999   else
1000   {
1001     if (!pf.addStep(fact, ps))
1002     {
1003       return nullptr;
1004     }
1005   }
1006   return pf.getProofFor(fact);
1007 }
1008
1009 std::string InferProofCons::identify() const
1010 {
1011   return "strings::InferProofCons";
1012 }
1013
1014 }  // namespace strings
1015 }  // namespace theory
1016 }  // namespace CVC4