Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Subsolver for handling code points
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/strings/code_point_solver.h"
      14                 :            : 
      15                 :            : #include "theory/strings/base_solver.h"
      16                 :            : #include "theory/strings/core_solver.h"
      17                 :            : #include "theory/strings/inference_manager.h"
      18                 :            : #include "theory/strings/solver_state.h"
      19                 :            : #include "theory/strings/term_registry.h"
      20                 :            : #include "theory/strings/word.h"
      21                 :            : #include "util/rational.h"
      22                 :            : 
      23                 :            : using namespace cvc5::internal::kind;
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace theory {
      27                 :            : namespace strings {
      28                 :            : 
      29                 :      49981 : CodePointSolver::CodePointSolver(Env& env,
      30                 :            :                                  SolverState& s,
      31                 :            :                                  InferenceManager& im,
      32                 :            :                                  TermRegistry& tr,
      33                 :            :                                  BaseSolver& bs,
      34                 :      49981 :                                  CoreSolver& cs)
      35                 :            :     : EnvObj(env),
      36                 :      49981 :       d_state(s),
      37                 :      49981 :       d_im(im),
      38                 :      49981 :       d_termReg(tr),
      39                 :      49981 :       d_bsolver(bs),
      40                 :      49981 :       d_csolver(cs)
      41                 :            : {
      42                 :      49981 :   d_negOne = nodeManager()->mkConstInt(Rational(-1));
      43                 :      49981 : }
      44                 :            : 
      45                 :      40098 : void CodePointSolver::checkCodes()
      46                 :            : {
      47                 :            :   // ensure that lemmas regarding str.code been added for each constant string
      48                 :            :   // of length one
      49         [ +  + ]:      40098 :   if (!d_termReg.hasStringCode())
      50                 :            :   {
      51                 :      37890 :     return;
      52                 :            :   }
      53                 :       2503 :   NodeManager* nm = nodeManager();
      54                 :            :   // We construct a mapping from string equivalent classes to code point
      55                 :            :   // applications. This mapping contains entries:
      56                 :            :   // (1) r -> (str.to_code t) where r is the representative of t and the
      57                 :            :   // term (str.to_code t) occurs in the equality engine.
      58                 :            :   // (2) c -> (str.to_code k) where c is a string constant of length one and
      59                 :            :   // c occurs in the equality engine (as a representative).
      60                 :            :   // This mapping omits str.to_code terms that are already equal to -1.
      61                 :       2503 :   std::map<Node, Node> codes;
      62                 :       2503 :   const std::vector<Node>& seqc = d_bsolver.getStringLikeEqc();
      63         [ +  + ]:      35411 :   for (const Node& eqc : seqc)
      64                 :            :   {
      65         [ +  + ]:      32908 :     if (!eqc.getType().isString())
      66                 :            :     {
      67                 :      21112 :       continue;
      68                 :            :     }
      69                 :      32862 :     Node codeArg;
      70         [ +  + ]:      32862 :     if (eqc.isConst())
      71                 :            :     {
      72                 :            :       // only relevant for injectivity if length is 1 (e.g. it has a valid
      73                 :            :       // code point)
      74         [ +  + ]:      11625 :       if (Word::getLength(eqc) != 1)
      75                 :            :       {
      76                 :       5719 :         continue;
      77                 :            :       }
      78                 :       5906 :       codeArg = d_termReg.ensureProxyVariableFor(eqc);
      79                 :            :     }
      80                 :            :     else
      81                 :            :     {
      82                 :      21237 :       EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
      83 [ +  - ][ +  + ]:      21237 :       if (ei == nullptr || ei->d_codeTerm.get().isNull())
                 [ +  + ]
      84                 :            :       {
      85                 :      14624 :         continue;
      86                 :            :       }
      87                 :       6613 :       codeArg = ei->d_codeTerm.get();
      88                 :            :     }
      89                 :      12519 :     Node vc = nm->mkNode(Kind::STRING_TO_CODE, codeArg);
      90                 :            :     // only relevant for injectivity if not already equal to negative one
      91         [ +  + ]:      12519 :     if (d_state.areEqual(vc, d_negOne))
      92                 :            :     {
      93                 :        723 :       continue;
      94                 :            :     }
      95                 :      11796 :     codes[eqc] = vc;
      96 [ +  + ][ +  + ]:      33585 :   }
      97 [ +  - ][ +  + ]:       2503 :   if (d_im.hasProcessed() || codes.size() <= 1)
                 [ +  + ]
      98                 :            :   {
      99                 :        295 :     return;
     100                 :            :   }
     101                 :            :   // Now, ensure that str.code is injective. We only apply injectivity for
     102                 :            :   // pairs of terms that are disequal. We check pairs of disequal terms by
     103                 :            :   // iterating over the disequalities in getRelevantDeq.
     104                 :       2208 :   eq::EqualityEngine* ee = d_state.getEqualityEngine();
     105                 :       2208 :   std::map<Node, Node>::iterator itc;
     106                 :       2208 :   const std::vector<Node>& rlvDeq = d_csolver.getRelevantDeq();
     107         [ +  + ]:       5797 :   for (const Node& eq : rlvDeq)
     108                 :            :   {
     109                 :       3589 :     bool foundCodePair = true;
     110         [ +  + ]:      21534 :     Node r[2];
     111         [ +  + ]:      21534 :     Node c[2];
     112         [ +  + ]:       9236 :     for (size_t i = 0; i < 2; i++)
     113                 :            :     {
     114                 :       6614 :       r[i] = ee->getRepresentative(eq[i]);
     115                 :       6614 :       itc = codes.find(r[i]);
     116         [ +  + ]:       6614 :       if (itc == codes.end())
     117                 :            :       {
     118                 :        967 :         foundCodePair = false;
     119                 :        967 :         break;
     120                 :            :       }
     121                 :       5647 :       c[i] = itc->second;
     122                 :            :     }
     123         [ +  + ]:       3589 :     if (!foundCodePair)
     124                 :            :     {
     125                 :        967 :       continue;
     126                 :            :     }
     127         [ +  - ]:       5244 :     Trace("strings-code-debug")
     128                 :       2622 :         << "Compare codes : " << c[0] << " " << c[1] << std::endl;
     129         [ +  + ]:       2622 :     if (d_state.areDisequal(c[0], c[1]))
     130                 :            :     {
     131                 :            :       // code already disequal
     132                 :       2334 :       continue;
     133                 :            :     }
     134                 :        288 :     Node eq_no = c[0].eqNode(d_negOne);
     135                 :        288 :     Node deq = c[0].eqNode(c[1]).negate();
     136                 :        576 :     Node eqn = c[0][0].eqNode(c[1][0]);
     137                 :            :     // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
     138                 :        576 :     Node inj_lem = nm->mkNode(Kind::OR, eq_no, deq, eqn);
     139                 :        288 :     deq = rewrite(deq);
     140                 :        288 :     d_im.addPendingPhaseRequirement(deq, false);
     141                 :        288 :     std::vector<Node> emptyVec;
     142                 :        288 :     d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ);
     143 [ +  + ][ +  + ]:      21822 :   }
         [ -  - ][ -  - ]
     144         [ +  + ]:       2503 : }
     145                 :            : 
     146                 :            : }  // namespace strings
     147                 :            : }  // namespace theory
     148                 :            : }  // namespace cvc5::internal