Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Subsolver for handling code points
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/strings/code_point_solver.h"
      17                 :            : 
      18                 :            : #include "theory/strings/base_solver.h"
      19                 :            : #include "theory/strings/core_solver.h"
      20                 :            : #include "theory/strings/inference_manager.h"
      21                 :            : #include "theory/strings/solver_state.h"
      22                 :            : #include "theory/strings/term_registry.h"
      23                 :            : #include "theory/strings/word.h"
      24                 :            : #include "util/rational.h"
      25                 :            : 
      26                 :            : using namespace cvc5::internal::kind;
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace theory {
      30                 :            : namespace strings {
      31                 :            : 
      32                 :      49272 : CodePointSolver::CodePointSolver(Env& env,
      33                 :            :                                  SolverState& s,
      34                 :            :                                  InferenceManager& im,
      35                 :            :                                  TermRegistry& tr,
      36                 :            :                                  BaseSolver& bs,
      37                 :      49272 :                                  CoreSolver& cs)
      38                 :            :     : EnvObj(env),
      39                 :            :       d_state(s),
      40                 :            :       d_im(im),
      41                 :            :       d_termReg(tr),
      42                 :            :       d_bsolver(bs),
      43                 :      49272 :       d_csolver(cs)
      44                 :            : {
      45                 :      49272 :   d_negOne = nodeManager()->mkConstInt(Rational(-1));
      46                 :      49272 : }
      47                 :            : 
      48                 :      34579 : void CodePointSolver::checkCodes()
      49                 :            : {
      50                 :            :   // ensure that lemmas regarding str.code been added for each constant string
      51                 :            :   // of length one
      52         [ +  + ]:      34579 :   if (!d_termReg.hasStringCode())
      53                 :            :   {
      54                 :      32505 :     return;
      55                 :            :   }
      56                 :       2366 :   NodeManager* nm = nodeManager();
      57                 :            :   // We construct a mapping from string equivalent classes to code point
      58                 :            :   // applications. This mapping contains entries:
      59                 :            :   // (1) r -> (str.to_code t) where r is the representative of t and the
      60                 :            :   // term (str.to_code t) occurs in the equality engine.
      61                 :            :   // (2) c -> (str.to_code k) where c is a string constant of length one and
      62                 :            :   // c occurs in the equality engine (as a representative).
      63                 :            :   // This mapping omits str.to_code terms that are already equal to -1.
      64                 :       2366 :   std::map<Node, Node> codes;
      65                 :       2366 :   const std::vector<Node>& seqc = d_bsolver.getStringLikeEqc();
      66         [ +  + ]:      34479 :   for (const Node& eqc : seqc)
      67                 :            :   {
      68         [ +  + ]:      32113 :     if (!eqc.getType().isString())
      69                 :            :     {
      70                 :      21229 :       continue;
      71                 :            :     }
      72                 :      32067 :     Node codeArg;
      73         [ +  + ]:      32067 :     if (eqc.isConst())
      74                 :            :     {
      75                 :            :       // only relevant for injectivity if length is 1 (e.g. it has a valid
      76                 :            :       // code point)
      77         [ +  + ]:      10915 :       if (Word::getLength(eqc) != 1)
      78                 :            :       {
      79                 :       5590 :         continue;
      80                 :            :       }
      81                 :       5325 :       codeArg = d_termReg.ensureProxyVariableFor(eqc);
      82                 :            :     }
      83                 :            :     else
      84                 :            :     {
      85                 :      21152 :       EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
      86 [ +  - ][ +  + ]:      21152 :       if (ei == nullptr || ei->d_codeTerm.get().isNull())
                 [ +  + ]
      87                 :            :       {
      88                 :      14809 :         continue;
      89                 :            :       }
      90                 :       6343 :       codeArg = ei->d_codeTerm.get();
      91                 :            :     }
      92                 :      11668 :     Node vc = nm->mkNode(Kind::STRING_TO_CODE, codeArg);
      93                 :            :     // only relevant for injectivity if not already equal to negative one
      94         [ +  + ]:      11668 :     if (d_state.areEqual(vc, d_negOne))
      95                 :            :     {
      96                 :        784 :       continue;
      97                 :            :     }
      98                 :      10884 :     codes[eqc] = vc;
      99                 :            :   }
     100 [ +  - ][ +  + ]:       2366 :   if (d_im.hasProcessed() || codes.size() <= 1)
                 [ +  + ]
     101                 :            :   {
     102                 :        292 :     return;
     103                 :            :   }
     104                 :            :   // Now, ensure that str.code is injective. We only apply injectivity for
     105                 :            :   // pairs of terms that are disequal. We check pairs of disequal terms by
     106                 :            :   // iterating over the disequalities in getRelevantDeq.
     107                 :       2074 :   eq::EqualityEngine* ee = d_state.getEqualityEngine();
     108                 :       2074 :   std::map<Node, Node>::iterator itc;
     109                 :       2074 :   const std::vector<Node>& rlvDeq = d_csolver.getRelevantDeq();
     110         [ +  + ]:       4529 :   for (const Node& eq : rlvDeq)
     111                 :            :   {
     112                 :       2455 :     bool foundCodePair = true;
     113 [ +  + ][ -  - ]:      12275 :     Node r[2];
     114 [ +  + ][ -  - ]:      12275 :     Node c[2];
     115         [ +  + ]:       5955 :     for (size_t i = 0; i < 2; i++)
     116                 :            :     {
     117                 :       4332 :       r[i] = ee->getRepresentative(eq[i]);
     118                 :       4332 :       itc = codes.find(r[i]);
     119         [ +  + ]:       4332 :       if (itc == codes.end())
     120                 :            :       {
     121                 :        832 :         foundCodePair = false;
     122                 :        832 :         break;
     123                 :            :       }
     124                 :       3500 :       c[i] = itc->second;
     125                 :            :     }
     126         [ +  + ]:       2455 :     if (!foundCodePair)
     127                 :            :     {
     128                 :        832 :       continue;
     129                 :            :     }
     130         [ +  - ]:       3246 :     Trace("strings-code-debug")
     131                 :       1623 :         << "Compare codes : " << c[0] << " " << c[1] << std::endl;
     132         [ +  + ]:       1623 :     if (d_state.areDisequal(c[0], c[1]))
     133                 :            :     {
     134                 :            :       // code already disequal
     135                 :       1324 :       continue;
     136                 :            :     }
     137                 :        598 :     Node eq_no = c[0].eqNode(d_negOne);
     138                 :        598 :     Node deq = c[0].eqNode(c[1]).negate();
     139                 :        897 :     Node eqn = c[0][0].eqNode(c[1][0]);
     140                 :            :     // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
     141                 :        897 :     Node inj_lem = nm->mkNode(Kind::OR, eq_no, deq, eqn);
     142                 :        299 :     deq = rewrite(deq);
     143                 :        299 :     d_im.addPendingPhaseRequirement(deq, false);
     144                 :        299 :     std::vector<Node> emptyVec;
     145                 :        299 :     d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ);
     146                 :            :   }
     147                 :            : }
     148                 :            : 
     149                 :            : }  // namespace strings
     150                 :            : }  // namespace theory
     151                 :            : }  // namespace cvc5::internal