src/theory/strings/normal_form.cpp

   1 /*********************                                                        */
   2 /*! \file normal_form.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   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 normal form data structure for the theory of
  13  **  strings.
  14  **/
  15
  16 #include "theory/strings/normal_form.h"
  17
  18 #include "options/strings_options.h"
  19 #include "theory/rewriter.h"
  20 #include "theory/strings/theory_strings_utils.h"
  21 #include "theory/strings/word.h"
  22
  23 using namespace std;
  24 using namespace CVC4::kind;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace strings {
  29
  30 void NormalForm::init(Node base)
  31 {
  32   Assert(base.getType().isStringLike());
  33   Assert(base.getKind() != STRING_CONCAT);
  34   d_base = base;
  35   d_nf.clear();
  36   d_isRev = false;
  37   d_exp.clear();
  38   d_expDep.clear();
  39
  40   // add to normal form
  41   if (!base.isConst() || Word::getLength(base) > 0)
  42   {
  43     d_nf.push_back(base);
  44   }
  45 }
  46
  47 void NormalForm::reverse()
  48 {
  49   std::reverse(d_nf.begin(), d_nf.end());
  50   d_isRev = !d_isRev;
  51 }
  52
  53 void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
  54 {
  55   Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
  56              STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2))
  57          == d_nf[index]);
  58   d_nf.insert(d_nf.begin() + index + 1, c2);
  59   d_nf[index] = c1;
  60   // update the dependency indices
  61   // notice this is not critical for soundness: not doing the below incrementing
  62   // will only lead to overapproximating when antecedants are required in
  63   // explanations
  64   for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
  65   {
  66     for (const auto& pep : pe.second)
  67     {
  68       // See if this can be incremented: it can if this literal is not relevant
  69       // to the current index, and hence it is not relevant for both c1 and c2.
  70       Assert(pep.second >= 0 && pep.second <= d_nf.size());
  71       bool increment = (pep.first == d_isRev)
  72                            ? pep.second > index
  73                            : (d_nf.size() - 1 - pep.second) < index;
  74       if (increment)
  75       {
  76         d_expDep[pe.first][pep.first] = pep.second + 1;
  77       }
  78     }
  79   }
  80 }
  81
  82 void NormalForm::addToExplanation(Node exp,
  83                                   unsigned new_val,
  84                                   unsigned new_rev_val)
  85 {
  86   Assert(!exp.isConst());
  87   if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
  88   {
  89     d_exp.push_back(exp);
  90   }
  91   for (unsigned k = 0; k < 2; k++)
  92   {
  93     unsigned val = k == 0 ? new_val : new_rev_val;
  94     std::map<bool, unsigned>::iterator itned = d_expDep[exp].find(k == 1);
  95     if (itned == d_expDep[exp].end())
  96     {
  97       Trace("strings-process-debug")
  98           << "Deps : set dependency on " << exp << " to " << val
  99           << " isRev=" << (k == 0) << std::endl;
 100       d_expDep[exp][k == 1] = val;
 101     }
 102     else
 103     {
 104       Trace("strings-process-debug")
 105           << "Deps : Multiple dependencies on " << exp << " : " << itned->second
 106           << " " << val << " isRev=" << (k == 0) << std::endl;
 107       // if we already have a dependency (in the case of non-linear string
 108       // equalities), it is min/max
 109       bool cmp = val > itned->second;
 110       if (cmp == (k == 1))
 111       {
 112         d_expDep[exp][k == 1] = val;
 113       }
 114     }
 115   }
 116 }
 117
 118 void NormalForm::getExplanation(int index, std::vector<Node>& curr_exp)
 119 {
 120   if (index == -1 || !options::stringMinPrefixExplain())
 121   {
 122     curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end());
 123     return;
 124   }
 125   for (const Node& exp : d_exp)
 126   {
 127     int dep = static_cast<int>(d_expDep[exp][d_isRev]);
 128     if (dep <= index)
 129     {
 130       curr_exp.push_back(exp);
 131       Trace("strings-explain-prefix-debug") << "  include : ";
 132     }
 133     else
 134     {
 135       Trace("strings-explain-prefix-debug") << "  exclude : ";
 136     }
 137     Trace("strings-explain-prefix-debug") << exp << std::endl;
 138   }
 139 }
 140
 141 Node NormalForm::collectConstantStringAt(size_t& index)
 142 {
 143   std::vector<Node> c;
 144   while (d_nf.size() > index && d_nf[index].isConst())
 145   {
 146     c.push_back(d_nf[index]);
 147     index++;
 148   }
 149   if (!c.empty())
 150   {
 151     if (d_isRev)
 152     {
 153       std::reverse(c.begin(), c.end());
 154     }
 155     Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType()));
 156     Assert(cc.isConst());
 157     return cc;
 158   }
 159   else
 160   {
 161     return Node::null();
 162   }
 163 }
 164
 165 void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
 166                                            NormalForm& nfj,
 167                                            int index_i,
 168                                            int index_j,
 169                                            std::vector<Node>& curr_exp)
 170 {
 171   Assert(nfi.d_isRev == nfj.d_isRev);
 172   Trace("strings-explain-prefix")
 173       << "Get explanation for prefix " << index_i << ", " << index_j
 174       << ", reverse = " << nfi.d_isRev << std::endl;
 175   // get explanations
 176   nfi.getExplanation(index_i, curr_exp);
 177   nfj.getExplanation(index_j, curr_exp);
 178   Trace("strings-explain-prefix")
 179       << "Included " << curr_exp.size() << " / "
 180       << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
 181   // add explanation for why they are equal
 182   Node eq = nfi.d_base.eqNode(nfj.d_base);
 183   curr_exp.push_back(eq);
 184 }
 185
 186 }  // namespace strings
 187 }  // namespace theory
 188 }  // namespace CVC4