Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/normal_form.cpp	Lines:	84	84	100.0 %
Date:	2021-09-29	Branches:	149	336	44.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of normal form data structure for the theory of strings.
 */

#include "theory/strings/normal_form.h"

#include "options/strings_options.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

void NormalForm::init(Node base)
{
  Assert(base.getType().isStringLike());
  Assert(base.getKind() != STRING_CONCAT);
  d_base = base;
  d_nf.clear();
  d_isRev = false;
  d_exp.clear();
  d_expDep.clear();

  // add to normal form
  if (!base.isConst() || Word::getLength(base) > 0)
  {
    d_nf.push_back(base);
  }
}

void NormalForm::reverse()
{
  std::reverse(d_nf.begin(), d_nf.end());
  d_isRev = !d_isRev;
}

void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
{
  Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
             STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2))
         == d_nf[index]);
  d_nf.insert(d_nf.begin() + index + 1, c2);
  d_nf[index] = c1;
  // update the dependency indices
  // notice this is not critical for soundness: not doing the below incrementing
  // will only lead to overapproximating when antecedants are required in
  // explanations
  for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
  {
    for (const auto& pep : pe.second)
    {
      // See if this can be incremented: it can if this literal is not relevant
      // to the current index, and hence it is not relevant for both c1 and c2.
      Assert(pep.second >= 0 && pep.second <= d_nf.size());
      bool increment = (pep.first == d_isRev)
                           ? pep.second > index
                           : (d_nf.size() - 1 - pep.second) < index;
      if (increment)
      {
        d_expDep[pe.first][pep.first] = pep.second + 1;
      }
    }
  }
}

void NormalForm::addToExplanation(Node exp,
                                  unsigned new_val,
                                  unsigned new_rev_val)
{
  Assert(!exp.isConst());
  if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
  {
    d_exp.push_back(exp);
  }
  for (unsigned k = 0; k < 2; k++)
  {
    unsigned val = k == 0 ? new_val : new_rev_val;
    std::map<bool, unsigned>::iterator itned = d_expDep[exp].find(k == 1);
    if (itned == d_expDep[exp].end())
    {
      Trace("strings-process-debug")
          << "Deps : set dependency on " << exp << " to " << val
          << " isRev=" << (k == 0) << std::endl;
      d_expDep[exp][k == 1] = val;
    }
    else
    {
      Trace("strings-process-debug")
          << "Deps : Multiple dependencies on " << exp << " : " << itned->second
          << " " << val << " isRev=" << (k == 0) << std::endl;
      // if we already have a dependency (in the case of non-linear string
      // equalities), it is min/max
      bool cmp = val > itned->second;
      if (cmp == (k == 1))
      {
        d_expDep[exp][k == 1] = val;
      }
    }
  }
}

void NormalForm::getExplanation(int index, std::vector<Node>& curr_exp)
{
  if (index == -1 || !options::stringMinPrefixExplain())
  {
    curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end());
    return;
  }
  for (const Node& exp : d_exp)
  {
    int dep = static_cast<int>(d_expDep[exp][d_isRev]);
    if (dep <= index)
    {
      curr_exp.push_back(exp);
      Trace("strings-explain-prefix-debug") << "  include : ";
    }
    else
    {
      Trace("strings-explain-prefix-debug") << "  exclude : ";
    }
    Trace("strings-explain-prefix-debug") << exp << std::endl;
  }
}

Node NormalForm::collectConstantStringAt(size_t& index)
{
  std::vector<Node> c;
  while (d_nf.size() > index && d_nf[index].isConst())
  {
    c.push_back(d_nf[index]);
    index++;
  }
  if (!c.empty())
  {
    if (d_isRev)
    {
      std::reverse(c.begin(), c.end());
    }
    Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType()));
    Assert(cc.isConst());
    return cc;
  }
  else
  {
    return Node::null();
  }
}

void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
                                           NormalForm& nfj,
                                           int index_i,
                                           int index_j,
                                           std::vector<Node>& curr_exp)
{
  Assert(nfi.d_isRev == nfj.d_isRev);
  Trace("strings-explain-prefix")
      << "Get explanation for prefix " << index_i << ", " << index_j
      << ", reverse = " << nfi.d_isRev << std::endl;
  // get explanations
  nfi.getExplanation(index_i, curr_exp);
  nfj.getExplanation(index_j, curr_exp);
  Trace("strings-explain-prefix")
      << "Included " << curr_exp.size() << " / "
      << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
  // add explanation for why they are equal
  Node eq = nfi.d_base.eqNode(nfj.d_base);
  curr_exp.push_back(eq);
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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		* Implementation of normal form data structure for the theory of 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 cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace strings {
29
30	103931	void NormalForm::init(Node base)
31		{
32	103931	Assert(base.getType().isStringLike());
33	103931	Assert(base.getKind() != STRING_CONCAT);
34	103931	d_base = base;
35	103931	d_nf.clear();
36	103931	d_isRev = false;
37	103931	d_exp.clear();
38	103931	d_expDep.clear();
39
40		// add to normal form
41	103931	if (!base.isConst() \|\| Word::getLength(base) > 0)
42		{
43	93754	d_nf.push_back(base);
44		}
45	103931	}
46
47	42676	void NormalForm::reverse()
48		{
49	42676	std::reverse(d_nf.begin(), d_nf.end());
50	42676	d_isRev = !d_isRev;
51	42676	}
52
53	4531	void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
54		{
55	4531	Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
56		STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2))
57		== d_nf[index]);
58	4531	d_nf.insert(d_nf.begin() + index + 1, c2);
59	4531	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	14819	for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
65		{
66	30864	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	20576	Assert(pep.second >= 0 && pep.second <= d_nf.size());
71	20576	bool increment = (pep.first == d_isRev)
72	30864	? pep.second > index
73	30864	: (d_nf.size() - 1 - pep.second) < index;
74	20576	if (increment)
75		{
76	8697	d_expDep[pe.first][pep.first] = pep.second + 1;
77		}
78		}
79		}
80	4531	}
81
82	428863	void NormalForm::addToExplanation(Node exp,
83		unsigned new_val,
84		unsigned new_rev_val)
85		{
86	428863	Assert(!exp.isConst());
87	428863	if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
88		{
89	426825	d_exp.push_back(exp);
90		}
91	1286589	for (unsigned k = 0; k < 2; k++)
92		{
93	857726	unsigned val = k == 0 ? new_val : new_rev_val;
94	857726	std::map<bool, unsigned>::iterator itned = d_expDep[exp].find(k == 1);
95	857726	if (itned == d_expDep[exp].end())
96		{
97	1707300	Trace("strings-process-debug")
98	853650	<< "Deps : set dependency on " << exp << " to " << val
99	853650	<< " isRev=" << (k == 0) << std::endl;
100	853650	d_expDep[exp][k == 1] = val;
101		}
102		else
103		{
104	8152	Trace("strings-process-debug")
105	4076	<< "Deps : Multiple dependencies on " << exp << " : " << itned->second
106	4076	<< " " << 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	4076	bool cmp = val > itned->second;
110	4076	if (cmp == (k == 1))
111		{
112	2038	d_expDep[exp][k == 1] = val;
113		}
114		}
115		}
116	428863	}
117
118	25120	void NormalForm::getExplanation(int index, std::vector<Node>& curr_exp)
119		{
120	25120	if (index == -1 \|\| !options::stringMinPrefixExplain())
121		{
122	2710	curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end());
123	2710	return;
124		}
125	98091	for (const Node& exp : d_exp)
126		{
127	75681	int dep = static_cast<int>(d_expDep[exp][d_isRev]);
128	75681	if (dep <= index)
129		{
130	42872	curr_exp.push_back(exp);
131	42872	Trace("strings-explain-prefix-debug") << " include : ";
132		}
133		else
134		{
135	32809	Trace("strings-explain-prefix-debug") << " exclude : ";
136		}
137	75681	Trace("strings-explain-prefix-debug") << exp << std::endl;
138		}
139		}
140
141	7427	Node NormalForm::collectConstantStringAt(size_t& index)
142		{
143	14854	std::vector<Node> c;
144	19659	while (d_nf.size() > index && d_nf[index].isConst())
145		{
146	6116	c.push_back(d_nf[index]);
147	6116	index++;
148		}
149	7427	if (!c.empty())
150		{
151	4918	if (d_isRev)
152		{
153	2664	std::reverse(c.begin(), c.end());
154		}
155	9836	Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType()));
156	4918	Assert(cc.isConst());
157	4918	return cc;
158		}
159		else
160		{
161	2509	return Node::null();
162		}
163		}
164
165	12560	void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
166		NormalForm& nfj,
167		int index_i,
168		int index_j,
169		std::vector<Node>& curr_exp)
170		{
171	12560	Assert(nfi.d_isRev == nfj.d_isRev);
172	25120	Trace("strings-explain-prefix")
173	12560	<< "Get explanation for prefix " << index_i << ", " << index_j
174	12560	<< ", reverse = " << nfi.d_isRev << std::endl;
175		// get explanations
176	12560	nfi.getExplanation(index_i, curr_exp);
177	12560	nfj.getExplanation(index_j, curr_exp);
178	25120	Trace("strings-explain-prefix")
179	25120	<< "Included " << curr_exp.size() << " / "
180	12560	<< (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
181		// add explanation for why they are equal
182	25120	Node eq = nfi.d_base.eqNode(nfj.d_base);
183	12560	curr_exp.push_back(eq);
184	12560	}
185
186		} // namespace strings
187		} // namespace theory
188	22746	} // namespace cvc5