src/theory/strings/eqc_info.cpp

   1 /*********************                                                        */
   2 /*! \file eqc_info.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tianyi Liang
   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 equivalence class info for the theory of strings
  13  **/
  14
  15 #include "theory/strings/eqc_info.h"
  16
  17 #include "theory/strings/theory_strings_utils.h"
  18 #include "theory/strings/word.h"
  19
  20 using namespace std;
  21 using namespace CVC4::context;
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace strings {
  27
  28 EqcInfo::EqcInfo(context::Context* c)
  29     : d_lengthTerm(c),
  30       d_codeTerm(c),
  31       d_cardinalityLemK(c),
  32       d_normalizedLength(c),
  33       d_prefixC(c),
  34       d_suffixC(c)
  35 {
  36 }
  37
  38 Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
  39 {
  40   // check conflict
  41   Node prev = isSuf ? d_suffixC : d_prefixC;
  42   if (!prev.isNull())
  43   {
  44     Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
  45                                        << " post=" << isSuf << std::endl;
  46     Node prevC = utils::getConstantEndpoint(prev, isSuf);
  47     Assert(!prevC.isNull());
  48     Assert(prevC.isConst());
  49     if (c.isNull())
  50     {
  51       c = utils::getConstantEndpoint(t, isSuf);
  52       Assert(!c.isNull());
  53     }
  54     Assert(c.isConst());
  55     bool conflict = false;
  56     // if the constant prefixes are different
  57     if (c != prevC)
  58     {
  59       // conflicts between constants should be handled by equality engine
  60       Assert(!t.isConst() || !prev.isConst());
  61       Trace("strings-eager-pconf-debug")
  62           << "Check conflict constants " << prevC << ", " << c << std::endl;
  63       size_t pvs = Word::getLength(prevC);
  64       size_t cvs = Word::getLength(c);
  65       if (pvs == cvs || (pvs > cvs && t.isConst())
  66           || (cvs > pvs && prev.isConst()))
  67       {
  68         // If equal length, cannot be equal due to node check above.
  69         // If one is fully constant and has less length than the other, then the
  70         // other will not fit and we are in conflict.
  71         conflict = true;
  72       }
  73       else
  74       {
  75         Node larges = pvs > cvs ? prevC : c;
  76         Node smalls = pvs > cvs ? c : prevC;
  77         if (isSuf)
  78         {
  79           conflict = !Word::hasSuffix(larges, smalls);
  80         }
  81         else
  82         {
  83           conflict = !Word::hasPrefix(larges, smalls);
  84         }
  85       }
  86       if (!conflict && (pvs > cvs || prev.isConst()))
  87       {
  88         // current is subsumed, either shorter prefix or the other is a full
  89         // constant
  90         return Node::null();
  91       }
  92     }
  93     else if (!t.isConst())
  94     {
  95       // current is subsumed since the other may be a full constant
  96       return Node::null();
  97     }
  98     if (conflict)
  99     {
 100       Trace("strings-eager-pconf")
 101           << "Conflict for " << prevC << ", " << c << std::endl;
 102       std::vector<Node> ccs;
 103       Node r[2];
 104       for (unsigned i = 0; i < 2; i++)
 105       {
 106         Node tp = i == 0 ? t : prev;
 107         if (tp.getKind() == STRING_IN_REGEXP)
 108         {
 109           ccs.push_back(tp);
 110           r[i] = tp[0];
 111         }
 112         else
 113         {
 114           r[i] = tp;
 115         }
 116       }
 117       if (r[0] != r[1])
 118       {
 119         ccs.push_back(r[0].eqNode(r[1]));
 120       }
 121       Assert(!ccs.empty());
 122       Node ret =
 123           ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
 124       Trace("strings-eager-pconf")
 125           << "String: eager prefix conflict: " << ret << std::endl;
 126       return ret;
 127     }
 128   }
 129   if (isSuf)
 130   {
 131     d_suffixC = t;
 132   }
 133   else
 134   {
 135     d_prefixC = t;
 136   }
 137   return Node::null();
 138 }
 139
 140 }  // namespace strings
 141 }  // namespace theory
 142 }  // namespace CVC4