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                 :            :  * The default model constructor for strings
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/strings/model_cons_default.h"
      14                 :            : 
      15                 :            : #include "theory/strings/core_solver.h"
      16                 :            : #include "theory/strings/solver_state.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : namespace theory {
      20                 :            : namespace strings {
      21                 :            : 
      22                 :      28777 : ModelConsDefault::ModelConsDefault(Env& env,
      23                 :            :                                    SolverState& state,
      24                 :      28777 :                                    CoreSolver& csolver)
      25                 :      28777 :     : ModelCons(env), d_state(state), d_csolver(csolver)
      26                 :            : {
      27                 :      28777 : }
      28                 :            : 
      29                 :      12188 : void ModelConsDefault::getStringRepresentativesFrom(
      30                 :            :     const std::set<Node>& termSet,
      31                 :            :     std::unordered_set<TypeNode>& repTypes,
      32                 :            :     std::map<TypeNode, std::unordered_set<Node>>& repSet,
      33                 :            :     CVC5_UNUSED std::vector<Node>& auxEq)
      34                 :            : {
      35         [ +  + ]:     135890 :   for (const Node& s : termSet)
      36                 :            :   {
      37                 :     123702 :     TypeNode tn = s.getType();
      38         [ +  + ]:     123702 :     if (tn.isStringLike())
      39                 :            :     {
      40                 :     123124 :       Node r = d_state.getRepresentative(s);
      41                 :      61562 :       repSet[tn].insert(r);
      42                 :      61562 :       repTypes.insert(tn);
      43                 :      61562 :     }
      44                 :     123702 :   }
      45                 :      12188 : }
      46                 :            : 
      47                 :       1933 : void ModelConsDefault::separateByLength(TheoryModel* m,
      48                 :            :                                         const std::vector<Node>& ns,
      49                 :            :                                         std::vector<std::vector<Node>>& cols,
      50                 :            :                                         std::vector<Node>& lts)
      51                 :            : {
      52                 :       1933 :   d_state.separateByLength(ns, cols, lts);
      53                 :            :   // look up the values of each length term
      54         [ +  + ]:      11578 :   for (Node& ll : lts)
      55                 :            :   {
      56 [ +  - ][ +  + ]:       9645 :     if (ll.isNull() || ll.isConst())
                 [ +  + ]
      57                 :            :     {
      58                 :       9635 :       continue;
      59                 :            :     }
      60                 :            :     // Previously we called Valuation::getCandidateModelValue for this purpose,
      61                 :            :     // which relied on the arithmetic theory solver to confirm the value of ll.
      62                 :            :     // However, it is better to simply ask the model object (which the
      63                 :            :     // arithmetic solver has already populated for us). Moreover this
      64                 :            :     // avoids assertion failures when using ee-mode=central.
      65         [ +  + ]:       3229 :     if (m->hasTerm(ll))
      66                 :            :     {
      67                 :       3219 :       ll = m->getRepresentative(ll);
      68                 :       3219 :       continue;
      69                 :            :     }
      70                 :            :     // Note that ll is the representative of the length in the equality engine
      71                 :            :     // of this theory, which the model may not know. This is possible when
      72                 :            :     // using ee-mode=central, where the representative may e.g. be a polynomial
      73                 :            :     // (+ (str.len x) (str.len y)) that the arithmetic solver treats as an
      74                 :            :     // auxiliary term and thus does not assign a value to. In this case, we
      75                 :            :     // look for a term in the equivalence class of ll whose value is known to
      76                 :            :     // the model, e.g. the length term (str.len z) itself.
      77                 :         10 :     eq::EqualityEngine* ee = d_state.getEqualityEngine();
      78                 :         10 :     eq::EqClassIterator eqc_i = eq::EqClassIterator(ll, ee);
      79         [ +  - ]:         28 :     while (!eqc_i.isFinished())
      80                 :            :     {
      81                 :         28 :       Node n = *eqc_i;
      82         [ +  + ]:         28 :       if (m->hasTerm(n))
      83                 :            :       {
      84                 :         10 :         Node nv = m->getRepresentative(n);
      85         [ +  - ]:         10 :         if (nv.isConst())
      86                 :            :         {
      87                 :         10 :           ll = nv;
      88                 :         10 :           break;
      89                 :            :         }
      90         [ -  + ]:         10 :       }
      91                 :         18 :       ++eqc_i;
      92         [ +  + ]:         28 :     }
      93                 :            :   }
      94                 :       1933 : }
      95                 :            : 
      96                 :      10454 : std::vector<Node> ModelConsDefault::getNormalForm(Node n)
      97                 :            : {
      98                 :      10454 :   return d_csolver.getNormalForm(n).d_nf;
      99                 :            : }
     100                 :            : 
     101                 :            : }  // namespace strings
     102                 :            : }  // namespace theory
     103                 :            : }  // namespace cvc5::internal