Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/solver_state.cpp	Lines:	100	104	96.2 %
Date:	2021-11-05	Branches:	154	332	46.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tianyi Liang, Mathias Preiner
 *
 * 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 the solver state of the theory of strings.
 */

#include "theory/strings/solver_state.h"

#include "theory/rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"

using namespace std;
using namespace cvc5::context;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

SolverState::SolverState(Env& env, Valuation& v)
    : TheoryState(env, v),
      d_eeDisequalities(env.getContext()),
      d_pendingConflictSet(env.getContext(), false),
      d_pendingConflict(InferenceId::UNKNOWN)
{
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
  d_false = NodeManager::currentNM()->mkConst(false);
}

SolverState::~SolverState()
{
  for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
  {
    delete it.second;
  }
}

const context::CDList<Node>& SolverState::getDisequalityList() const
{
  return d_eeDisequalities;
}

void SolverState::addDisequality(TNode t1, TNode t2)
{
  d_eeDisequalities.push_back(t1.eqNode(t2));
}

EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
{
  std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
  if (eqc_i != d_eqcInfo.end())
  {
    return eqc_i->second;
  }
  if (doMake)
  {
    EqcInfo* ei = new EqcInfo(d_env.getContext());
    d_eqcInfo[eqc] = ei;
    return ei;
  }
  return nullptr;
}

TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }

Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
{
  Assert(areEqual(t, te));
  Node lt = utils::mkNLength(te);
  if (hasTerm(lt))
  {
    // use own length if it exists, leads to shorter explanation
    return lt;
  }
  EqcInfo* ei = getOrMakeEqcInfo(t, false);
  Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
  if (lengthTerm.isNull())
  {
    // typically shouldnt be necessary
    lengthTerm = t;
  }
  else
  {
    lengthTerm = lengthTerm[0];
  }
  Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
                   << std::endl;
  if (te != lengthTerm)
  {
    exp.push_back(te.eqNode(lengthTerm));
  }
  return Rewriter::rewrite(
      NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
}

Node SolverState::getLength(Node t, std::vector<Node>& exp)
{
  return getLengthExp(t, exp, t);
}

Node SolverState::explainNonEmpty(Node s)
{
  Assert(s.getType().isStringLike());
  Node emp = Word::mkEmptyWord(s.getType());
  if (areDisequal(s, emp))
  {
    return s.eqNode(emp).negate();
  }
  Node sLen = utils::mkNLength(s);
  if (areDisequal(sLen, d_zero))
  {
    return sLen.eqNode(d_zero).negate();
  }
  return Node::null();
}

bool SolverState::isEqualEmptyWord(Node s, Node& emps)
{
  Node sr = getRepresentative(s);
  if (sr.isConst())
  {
    if (Word::getLength(sr) == 0)
    {
      emps = sr;
      return true;
    }
  }
  return false;
}

void SolverState::setPendingMergeConflict(Node conf, InferenceId id)
{
  if (d_pendingConflictSet.get())
  {
    // already set conflict
    return;
  }
  InferInfo iiPrefixConf(id);
  iiPrefixConf.d_conc = d_false;
  utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
  setPendingConflict(iiPrefixConf);
}

void SolverState::setPendingConflict(InferInfo& ii)
{
  if (!d_pendingConflictSet.get())
  {
    d_pendingConflict = ii;
    d_pendingConflictSet.set(true);
  }
}

bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }

bool SolverState::getPendingConflict(InferInfo& ii) const
{
  if (d_pendingConflictSet)
  {
    ii = d_pendingConflict;
    return true;
  }
  return false;
}

std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
                                                   TNode lit)
{
  return d_valuation.entailmentCheck(mode, lit);
}

void SolverState::separateByLength(
    const std::vector<Node>& n,
    std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
    std::map<TypeNode, std::vector<Node>>& lts)
{
  unsigned leqc_counter = 0;
  // map (length, type) to an equivalence class identifier
  std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
  // backwards map
  std::map<unsigned, std::pair<Node, TypeNode>> leqc_to_eqc;
  // Collection of eqc for each identifier. Notice that some identifiers may
  // not have an associated length in the mappings above, if the length of
  // an equivalence class is unknown.
  std::map<unsigned, std::vector<Node> > eqc_to_strings;
  for (const Node& eqc : n)
  {
    Assert(d_ee->getRepresentative(eqc) == eqc);
    TypeNode tnEqc = eqc.getType();
    EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
    Node lt = ei ? ei->d_lengthTerm : Node::null();
    if (!lt.isNull())
    {
      Node r = d_ee->getRepresentative(lt);
      std::pair<Node, TypeNode> lkey(r, tnEqc);
      if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
      {
        eqc_to_leqc[lkey] = leqc_counter;
        leqc_to_eqc[leqc_counter] = lkey;
        leqc_counter++;
      }
      eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc);
    }
    else
    {
      eqc_to_strings[leqc_counter].push_back(eqc);
      leqc_counter++;
    }
  }
  for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
  {
    Assert(!p.second.empty());
    // get the type of the collection
    TypeNode stn = p.second[0].getType();
    cols[stn].emplace_back(p.second.begin(), p.second.end());
    lts[stn].push_back(leqc_to_eqc[p.first].first);
  }
}

}  // 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, Tianyi Liang, Mathias Preiner
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 the solver state of the theory of strings.
14		*/
15
16		#include "theory/strings/solver_state.h"
17
18		#include "theory/rewriter.h"
19		#include "theory/strings/theory_strings_utils.h"
20		#include "theory/strings/word.h"
21		#include "util/rational.h"
22
23		using namespace std;
24		using namespace cvc5::context;
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace strings {
30
31	15271	SolverState::SolverState(Env& env, Valuation& v)
32		: TheoryState(env, v),
33		d_eeDisequalities(env.getContext()),
34		d_pendingConflictSet(env.getContext(), false),
35	15271	d_pendingConflict(InferenceId::UNKNOWN)
36		{
37	15271	d_zero = NodeManager::currentNM()->mkConst(Rational(0));
38	15271	d_false = NodeManager::currentNM()->mkConst(false);
39	15271	}
40
41	30532	SolverState::~SolverState()
42		{
43	71507	for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
44		{
45	56241	delete it.second;
46		}
47	15266	}
48
49	13992	const context::CDList<Node>& SolverState::getDisequalityList() const
50		{
51	13992	return d_eeDisequalities;
52		}
53
54	104170	void SolverState::addDisequality(TNode t1, TNode t2)
55		{
56	104170	d_eeDisequalities.push_back(t1.eqNode(t2));
57	104170	}
58
59	2520300	EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
60		{
61	2520300	std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
62	2520300	if (eqc_i != d_eqcInfo.end())
63		{
64	1782421	return eqc_i->second;
65		}
66	737879	if (doMake)
67		{
68	56241	EqcInfo* ei = new EqcInfo(d_env.getContext());
69	56241	d_eqcInfo[eqc] = ei;
70	56241	return ei;
71		}
72	681638	return nullptr;
73		}
74
75		TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
76
77	1147628	Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
78		{
79	1147628	Assert(areEqual(t, te));
80	2295256	Node lt = utils::mkNLength(te);
81	1147628	if (hasTerm(lt))
82		{
83		// use own length if it exists, leads to shorter explanation
84	1145180	return lt;
85		}
86	2448	EqcInfo* ei = getOrMakeEqcInfo(t, false);
87	4896	Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
88	2448	if (lengthTerm.isNull())
89		{
90		// typically shouldnt be necessary
91	2406	lengthTerm = t;
92		}
93		else
94		{
95	42	lengthTerm = lengthTerm[0];
96		}
97	4896	Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
98	2448	<< std::endl;
99	2448	if (te != lengthTerm)
100		{
101	42	exp.push_back(te.eqNode(lengthTerm));
102		}
103		return Rewriter::rewrite(
104	2448	NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
105		}
106
107	1147624	Node SolverState::getLength(Node t, std::vector<Node>& exp)
108		{
109	1147624	return getLengthExp(t, exp, t);
110		}
111
112	17354	Node SolverState::explainNonEmpty(Node s)
113		{
114	17354	Assert(s.getType().isStringLike());
115	34708	Node emp = Word::mkEmptyWord(s.getType());
116	17354	if (areDisequal(s, emp))
117		{
118	7480	return s.eqNode(emp).negate();
119		}
120	19748	Node sLen = utils::mkNLength(s);
121	9874	if (areDisequal(sLen, d_zero))
122		{
123	9863	return sLen.eqNode(d_zero).negate();
124		}
125	11	return Node::null();
126		}
127
128	948512	bool SolverState::isEqualEmptyWord(Node s, Node& emps)
129		{
130	1897024	Node sr = getRepresentative(s);
131	948512	if (sr.isConst())
132		{
133	247358	if (Word::getLength(sr) == 0)
134		{
135	34302	emps = sr;
136	34302	return true;
137		}
138		}
139	914210	return false;
140		}
141
142	796	void SolverState::setPendingMergeConflict(Node conf, InferenceId id)
143		{
144	796	if (d_pendingConflictSet.get())
145		{
146		// already set conflict
147	62	return;
148		}
149	1468	InferInfo iiPrefixConf(id);
150	734	iiPrefixConf.d_conc = d_false;
151	734	utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
152	734	setPendingConflict(iiPrefixConf);
153		}
154
155	734	void SolverState::setPendingConflict(InferInfo& ii)
156		{
157	734	if (!d_pendingConflictSet.get())
158		{
159	734	d_pendingConflict = ii;
160	734	d_pendingConflictSet.set(true);
161		}
162	734	}
163
164	1071941	bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
165
166	617	bool SolverState::getPendingConflict(InferInfo& ii) const
167		{
168	617	if (d_pendingConflictSet)
169		{
170	617	ii = d_pendingConflict;
171	617	return true;
172		}
173		return false;
174		}
175
176	8430	std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
177		TNode lit)
178		{
179	8430	return d_valuation.entailmentCheck(mode, lit);
180		}
181
182	25069	void SolverState::separateByLength(
183		const std::vector<Node>& n,
184		std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
185		std::map<TypeNode, std::vector<Node>>& lts)
186		{
187	25069	unsigned leqc_counter = 0;
188		// map (length, type) to an equivalence class identifier
189	50138	std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
190		// backwards map
191	50138	std::map<unsigned, std::pair<Node, TypeNode>> leqc_to_eqc;
192		// Collection of eqc for each identifier. Notice that some identifiers may
193		// not have an associated length in the mappings above, if the length of
194		// an equivalence class is unknown.
195	50138	std::map<unsigned, std::vector<Node> > eqc_to_strings;
196	105172	for (const Node& eqc : n)
197		{
198	80103	Assert(d_ee->getRepresentative(eqc) == eqc);
199	160206	TypeNode tnEqc = eqc.getType();
200	80103	EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
201	160206	Node lt = ei ? ei->d_lengthTerm : Node::null();
202	80103	if (!lt.isNull())
203		{
204	160206	Node r = d_ee->getRepresentative(lt);
205	160206	std::pair<Node, TypeNode> lkey(r, tnEqc);
206	80103	if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
207		{
208	50729	eqc_to_leqc[lkey] = leqc_counter;
209	50729	leqc_to_eqc[leqc_counter] = lkey;
210	50729	leqc_counter++;
211		}
212	80103	eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc);
213		}
214		else
215		{
216		eqc_to_strings[leqc_counter].push_back(eqc);
217		leqc_counter++;
218		}
219		}
220	75798	for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
221		{
222	50729	Assert(!p.second.empty());
223		// get the type of the collection
224	101458	TypeNode stn = p.second[0].getType();
225	50729	cols[stn].emplace_back(p.second.begin(), p.second.end());
226	50729	lts[stn].push_back(leqc_to_eqc[p.first].first);
227		}
228	25069	}
229
230		} // namespace strings
231		} // namespace theory
232	31125	} // namespace cvc5