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                 :      49957 : ModelConsDefault::ModelConsDefault(Env& env,
      23                 :            :                                    SolverState& state,
      24                 :      49957 :                                    CoreSolver& csolver)
      25                 :      49957 :     : ModelCons(env), d_state(state), d_csolver(csolver)
      26                 :            : {
      27                 :      49957 : }
      28                 :            : 
      29                 :      14114 : 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         [ +  + ]:     134312 :   for (const Node& s : termSet)
      36                 :            :   {
      37                 :     120198 :     TypeNode tn = s.getType();
      38         [ +  + ]:     120198 :     if (tn.isStringLike())
      39                 :            :     {
      40                 :     119584 :       Node r = d_state.getRepresentative(s);
      41                 :      59792 :       repSet[tn].insert(r);
      42                 :      59792 :       repTypes.insert(tn);
      43                 :      59792 :     }
      44                 :     120198 :   }
      45                 :      14114 : }
      46                 :            : 
      47                 :       2163 : 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                 :       2163 :   d_state.separateByLength(ns, cols, lts);
      53                 :            :   // look up the values of each length term
      54         [ +  + ]:      12428 :   for (Node& ll : lts)
      55                 :            :   {
      56                 :            :     // Previously we called Valuation::getCandidateModelValue for this purpose,
      57                 :            :     // which relied on the arithmetic theory solver to confirm the value of ll.
      58                 :            :     // However, it is better to simply ask the model object (which the
      59                 :            :     // arithmetic solver has already populated for us). Moreover this
      60                 :            :     // avoids assertion failures when using ee-mode=central.
      61 [ +  + ][ +  - ]:      10265 :     if (!ll.isConst() && m->hasTerm(ll))
         [ +  + ][ +  + ]
                 [ -  - ]
      62                 :            :     {
      63                 :       2805 :       ll = m->getRepresentative(ll);
      64                 :            :     }
      65                 :            :   }
      66                 :       2163 : }
      67                 :            : 
      68                 :       9148 : std::vector<Node> ModelConsDefault::getNormalForm(Node n)
      69                 :            : {
      70                 :       9148 :   return d_csolver.getNormalForm(n).d_nf;
      71                 :            : }
      72                 :            : 
      73                 :            : }  // namespace strings
      74                 :            : }  // namespace theory
      75                 :            : }  // namespace cvc5::internal