Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/solver_state.cpp	Lines:	101	106	95.3 %
Date:	2021-05-22	Branches:	156	338	46.2 %


/******************************************************************************
 * 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"

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

namespace cvc5 {
namespace theory {
namespace strings {

SolverState::SolverState(context::Context* c,
                         context::UserContext* u,
                         Valuation& v)
    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, 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_context);
    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;
  }
  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::setPendingPrefixConflictWhen(Node conf)
{
  if (conf.isNull() || d_pendingConflictSet.get())
  {
    return;
  }
  InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT);
  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;
  NodeManager* nm = NodeManager::currentNM();
  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())
    {
      lt = nm->mkNode(STRING_LENGTH, lt);
      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
22		using namespace std;
23		using namespace cvc5::context;
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace strings {
29
30	9460	SolverState::SolverState(context::Context* c,
31		context::UserContext* u,
32	9460	Valuation& v)
33	9460	: TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN)
34		{
35	9460	d_zero = NodeManager::currentNM()->mkConst(Rational(0));
36	9460	d_false = NodeManager::currentNM()->mkConst(false);
37	9460	}
38
39	18920	SolverState::~SolverState()
40		{
41	31062	for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
42		{
43	21602	delete it.second;
44		}
45	9460	}
46
47	9730	const context::CDList<Node>& SolverState::getDisequalityList() const
48		{
49	9730	return d_eeDisequalities;
50		}
51
52	45874	void SolverState::addDisequality(TNode t1, TNode t2)
53		{
54	45874	d_eeDisequalities.push_back(t1.eqNode(t2));
55	45874	}
56
57	1062533	EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
58		{
59	1062533	std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
60	1062533	if (eqc_i != d_eqcInfo.end())
61		{
62	525693	return eqc_i->second;
63		}
64	536840	if (doMake)
65		{
66	21602	EqcInfo* ei = new EqcInfo(d_context);
67	21602	d_eqcInfo[eqc] = ei;
68	21602	return ei;
69		}
70	515238	return nullptr;
71		}
72
73		TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
74
75	475862	Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
76		{
77	475862	Assert(areEqual(t, te));
78	951724	Node lt = utils::mkNLength(te);
79	475862	if (hasTerm(lt))
80		{
81		// use own length if it exists, leads to shorter explanation
82	475289	return lt;
83		}
84	573	EqcInfo* ei = getOrMakeEqcInfo(t, false);
85	1146	Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
86	573	if (lengthTerm.isNull())
87		{
88		// typically shouldnt be necessary
89	535	lengthTerm = t;
90		}
91	1146	Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
92	573	<< std::endl;
93	573	if (te != lengthTerm)
94		{
95	38	exp.push_back(te.eqNode(lengthTerm));
96		}
97		return Rewriter::rewrite(
98	573	NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
99		}
100
101	475858	Node SolverState::getLength(Node t, std::vector<Node>& exp)
102		{
103	475858	return getLengthExp(t, exp, t);
104		}
105
106	11463	Node SolverState::explainNonEmpty(Node s)
107		{
108	11463	Assert(s.getType().isStringLike());
109	22926	Node emp = Word::mkEmptyWord(s.getType());
110	11463	if (areDisequal(s, emp))
111		{
112	4202	return s.eqNode(emp).negate();
113		}
114	14522	Node sLen = utils::mkNLength(s);
115	7261	if (areDisequal(sLen, d_zero))
116		{
117	7261	return sLen.eqNode(d_zero).negate();
118		}
119		return Node::null();
120		}
121
122	486910	bool SolverState::isEqualEmptyWord(Node s, Node& emps)
123		{
124	973820	Node sr = getRepresentative(s);
125	486910	if (sr.isConst())
126		{
127	117908	if (Word::getLength(sr) == 0)
128		{
129	15423	emps = sr;
130	15423	return true;
131		}
132		}
133	471487	return false;
134		}
135
136	45415	void SolverState::setPendingPrefixConflictWhen(Node conf)
137		{
138	45415	if (conf.isNull() \|\| d_pendingConflictSet.get())
139		{
140	45127	return;
141		}
142	576	InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT);
143	288	iiPrefixConf.d_conc = d_false;
144	288	utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
145	288	setPendingConflict(iiPrefixConf);
146		}
147
148	288	void SolverState::setPendingConflict(InferInfo& ii)
149		{
150	288	if (!d_pendingConflictSet.get())
151		{
152	288	d_pendingConflict = ii;
153	288	d_pendingConflictSet.set(true);
154		}
155	288	}
156
157	528985	bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
158
159	242	bool SolverState::getPendingConflict(InferInfo& ii) const
160		{
161	242	if (d_pendingConflictSet)
162		{
163	242	ii = d_pendingConflict;
164	242	return true;
165		}
166		return false;
167		}
168
169	4989	std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
170		TNode lit)
171		{
172	4989	return d_valuation.entailmentCheck(mode, lit);
173		}
174
175	17446	void SolverState::separateByLength(
176		const std::vector<Node>& n,
177		std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
178		std::map<TypeNode, std::vector<Node>>& lts)
179		{
180	17446	unsigned leqc_counter = 0;
181		// map (length, type) to an equivalence class identifier
182	34892	std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
183		// backwards map
184	34892	std::map<unsigned, std::pair<Node, TypeNode>> leqc_to_eqc;
185		// Collection of eqc for each identifier. Notice that some identifiers may
186		// not have an associated length in the mappings above, if the length of
187		// an equivalence class is unknown.
188	34892	std::map<unsigned, std::vector<Node> > eqc_to_strings;
189	17446	NodeManager* nm = NodeManager::currentNM();
190	71734	for (const Node& eqc : n)
191		{
192	54288	Assert(d_ee->getRepresentative(eqc) == eqc);
193	108576	TypeNode tnEqc = eqc.getType();
194	54288	EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
195	108576	Node lt = ei ? ei->d_lengthTerm : Node::null();
196	54288	if (!lt.isNull())
197		{
198	54288	lt = nm->mkNode(STRING_LENGTH, lt);
199	108576	Node r = d_ee->getRepresentative(lt);
200	108576	std::pair<Node, TypeNode> lkey(r, tnEqc);
201	54288	if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
202		{
203	32677	eqc_to_leqc[lkey] = leqc_counter;
204	32677	leqc_to_eqc[leqc_counter] = lkey;
205	32677	leqc_counter++;
206		}
207	54288	eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc);
208		}
209		else
210		{
211		eqc_to_strings[leqc_counter].push_back(eqc);
212		leqc_counter++;
213		}
214		}
215	50123	for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
216		{
217	32677	Assert(!p.second.empty());
218		// get the type of the collection
219	65354	TypeNode stn = p.second[0].getType();
220	32677	cols[stn].emplace_back(p.second.begin(), p.second.end());
221	32677	lts[stn].push_back(leqc_to_eqc[p.first].first);
222		}
223	17446	}
224
225		} // namespace strings
226		} // namespace theory
227	28194	} // namespace cvc5