Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/eager_solver.cpp	Lines:	136	138	98.6 %
Date:	2021-11-07	Branches:	336	724	46.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tianyi Liang, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * The eager solver.
 */

#include "theory/strings/eager_solver.h"

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

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

EagerSolver::EagerSolver(Env& env,
                         SolverState& state,
                         TermRegistry& treg,
                         ArithEntail& aent)
    : EnvObj(env), d_state(state), d_treg(treg), d_aent(aent)
{
}

EagerSolver::~EagerSolver() {}

void EagerSolver::eqNotifyNewClass(TNode t)
{
  Kind k = t.getKind();
  if (k == STRING_LENGTH || k == STRING_TO_CODE)
  {
    eq::EqualityEngine* ee = d_state.getEqualityEngine();
    Node r = ee->getRepresentative(t[0]);
    EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
    if (k == STRING_LENGTH)
    {
      ei->d_lengthTerm = t;
      // also assume it as upper/lower bound as applicable for the equivalence
      // class info of t.
      EqcInfo* eil = nullptr;
      for (size_t i = 0; i < 2; i++)
      {
        Node b = getBoundForLength(t, i == 0);
        if (b.isNull())
        {
          continue;
        }
        if (eil == nullptr)
        {
          eil = d_state.getOrMakeEqcInfo(t);
        }
        if (i == 0)
        {
          eil->d_firstBound = t;
        }
        else if (i == 1)
        {
          eil->d_secondBound = t;
        }
      }
    }
    else
    {
      ei->d_codeTerm = t[0];
    }
  }
  else if (t.isConst())
  {
    TypeNode tn = t.getType();
    if (tn.isStringLike() || tn.isInteger())
    {
      EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
      ei->d_firstBound = t;
      ei->d_secondBound = t;
    }
  }
  else if (k == STRING_CONCAT)
  {
    addEndpointsToEqcInfo(t, t, t);
  }
}

void EagerSolver::eqNotifyMerge(TNode t1, TNode t2)
{
  EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false);
  if (e2 == nullptr)
  {
    return;
  }
  // always create it if e2 was non-null
  EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
  // check for conflict
  Node conf = checkForMergeConflict(t1, t2, e1, e2);
  if (!conf.isNull())
  {
    InferenceId id = t1.getType().isStringLike()
                         ? InferenceId::STRINGS_PREFIX_CONFLICT
                         : InferenceId::STRINGS_ARITH_BOUND_CONFLICT;
    d_state.setPendingMergeConflict(conf, id);
    return;
  }
  // add information from e2 to e1
  if (!e2->d_lengthTerm.get().isNull())
  {
    e1->d_lengthTerm.set(e2->d_lengthTerm);
  }
  if (!e2->d_codeTerm.get().isNull())
  {
    e1->d_codeTerm.set(e2->d_codeTerm);
  }
  if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
  {
    e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
  }
  if (!e2->d_normalizedLength.get().isNull())
  {
    e1->d_normalizedLength.set(e2->d_normalizedLength);
  }
}

void EagerSolver::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
{
  if (t1.getType().isStringLike())
  {
    // store disequalities between strings, may need to check if their lengths
    // are equal/disequal
    d_state.addDisequality(t1, t2);
  }
}

void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
{
  Assert(concat.getKind() == STRING_CONCAT
         || concat.getKind() == REGEXP_CONCAT);
  EqcInfo* ei = nullptr;
  // check each side
  for (unsigned r = 0; r < 2; r++)
  {
    unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1;
    Node c = utils::getConstantComponent(concat[index]);
    if (!c.isNull())
    {
      if (ei == nullptr)
      {
        ei = d_state.getOrMakeEqcInfo(eqc);
      }
      Trace("strings-eager-pconf-debug")
          << "New term: " << concat << " for " << t << " with prefix " << c
          << " (" << (r == 1) << ")" << std::endl;
      Node conf = ei->addEndpointConst(t, c, r == 1);
      if (!conf.isNull())
      {
        d_state.setPendingMergeConflict(conf,
                                        InferenceId::STRINGS_PREFIX_CONFLICT);
        return;
      }
    }
  }
}

Node EagerSolver::checkForMergeConflict(Node a,
                                        Node b,
                                        EqcInfo* ea,
                                        EqcInfo* eb)
{
  Assert(eb != nullptr && ea != nullptr);
  Assert(a.getType() == b.getType());
  Assert(a.getType().isStringLike() || a.getType().isInteger());
  // check prefix, suffix
  for (size_t i = 0; i < 2; i++)
  {
    Node n = i == 0 ? eb->d_firstBound.get() : eb->d_secondBound.get();
    if (!n.isNull())
    {
      Node conf;
      if (a.getType().isStringLike())
      {
        conf = ea->addEndpointConst(n, Node::null(), i == 1);
      }
      else
      {
        Trace("strings-eager-aconf-debug")
            << "addArithmeticBound " << n << " into " << a << " from " << b
            << std::endl;
        conf = addArithmeticBound(ea, n, i == 0);
      }
      if (!conf.isNull())
      {
        return conf;
      }
    }
  }
  return Node::null();
}

void EagerSolver::notifyFact(TNode atom,
                             bool polarity,
                             TNode fact,
                             bool isInternal)
{
  if (atom.getKind() == STRING_IN_REGEXP)
  {
    if (polarity && atom[1].getKind() == REGEXP_CONCAT)
    {
      eq::EqualityEngine* ee = d_state.getEqualityEngine();
      Node eqc = ee->getRepresentative(atom[0]);
      addEndpointsToEqcInfo(atom, atom[1], eqc);
    }
  }
}

Node EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
{
  Assert(e != nullptr);
  Assert(!t.isNull());
  Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
  Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL)
      << "Unexpected bound " << tb << " from " << t;
  Rational br = tb.getConst<Rational>();
  Node prev = isLower ? e->d_firstBound : e->d_secondBound;
  // check if subsumed
  if (!prev.isNull())
  {
    // convert to bound
    Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
    Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL);
    Rational prevbr = prevb.getConst<Rational>();
    if (prevbr == br || (br < prevbr) == isLower)
    {
      // subsumed
      return Node::null();
    }
  }
  Node prevo = isLower ? e->d_secondBound : e->d_firstBound;
  Trace("strings-eager-aconf-debug")
      << "Check conflict for bounds " << t << " " << prevo << std::endl;
  if (!prevo.isNull())
  {
    // are we in conflict?
    Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
    Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL);
    Rational prevobr = prevob.getConst<Rational>();
    if (prevobr != br && (prevobr < br) == isLower)
    {
      // conflict
      Node ret = EqcInfo::mkMergeConflict(t, prevo);
      Trace("strings-eager-aconf")
          << "String: eager arithmetic bound conflict: " << ret << std::endl;
      return ret;
    }
  }
  if (isLower)
  {
    e->d_firstBound = t;
  }
  else
  {
    e->d_secondBound = t;
  }
  return Node::null();
}

Node EagerSolver::getBoundForLength(Node len, bool isLower)
{
  Assert(len.getKind() == STRING_LENGTH);
  // it is prohibitively expensive to convert to original form and rewrite,
  // since this may invoke the rewriter on lengths of complex terms. Instead,
  // we convert to original term the argument, then call the utility method
  // for computing the length of the argument, implicitly under an application
  // of length (ArithEntail::getConstantBoundLength).
  // convert to original form
  Node olent = SkolemManager::getOriginalForm(len[0]);
  // get the bound
  Node c = d_aent.getConstantBoundLength(olent, isLower);
  Trace("strings-eager-aconf-debug")
      << "Constant " << (isLower ? "lower" : "upper") << " bound for " << len
      << " is " << c << ", from original form " << olent << std::endl;
  return c;
}

}  // 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, Andres Noetzli
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		* The eager solver.
14		*/
15
16		#include "theory/strings/eager_solver.h"
17
18		#include "theory/strings/theory_strings_utils.h"
19		#include "util/rational.h"
20
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace strings {
26
27	15273	EagerSolver::EagerSolver(Env& env,
28		SolverState& state,
29		TermRegistry& treg,
30	15273	ArithEntail& aent)
31	15273	: EnvObj(env), d_state(state), d_treg(treg), d_aent(aent)
32		{
33	15273	}
34
35	15268	EagerSolver::~EagerSolver() {}
36
37	130768	void EagerSolver::eqNotifyNewClass(TNode t)
38		{
39	130768	Kind k = t.getKind();
40	130768	if (k == STRING_LENGTH \|\| k == STRING_TO_CODE)
41		{
42	38458	eq::EqualityEngine* ee = d_state.getEqualityEngine();
43	76916	Node r = ee->getRepresentative(t[0]);
44	38458	EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
45	38458	if (k == STRING_LENGTH)
46		{
47	35480	ei->d_lengthTerm = t;
48		// also assume it as upper/lower bound as applicable for the equivalence
49		// class info of t.
50	35480	EqcInfo* eil = nullptr;
51	106440	for (size_t i = 0; i < 2; i++)
52		{
53	110941	Node b = getBoundForLength(t, i == 0);
54	70960	if (b.isNull())
55		{
56	30979	continue;
57		}
58	39981	if (eil == nullptr)
59		{
60	35480	eil = d_state.getOrMakeEqcInfo(t);
61		}
62	39981	if (i == 0)
63		{
64	35480	eil->d_firstBound = t;
65		}
66	4501	else if (i == 1)
67		{
68	4501	eil->d_secondBound = t;
69		}
70		}
71		}
72		else
73		{
74	2978	ei->d_codeTerm = t[0];
75	38458	}
76		}
77	92310	else if (t.isConst())
78		{
79	56096	TypeNode tn = t.getType();
80	28048	if (tn.isStringLike() \|\| tn.isInteger())
81		{
82	23671	EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
83	23671	ei->d_firstBound = t;
84	23671	ei->d_secondBound = t;
85		}
86		}
87	64262	else if (k == STRING_CONCAT)
88		{
89	11142	addEndpointsToEqcInfo(t, t, t);
90		}
91	130768	}
92
93	1421054	void EagerSolver::eqNotifyMerge(TNode t1, TNode t2)
94		{
95	1421054	EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false);
96	1421054	if (e2 == nullptr)
97		{
98	1371464	return;
99		}
100		// always create it if e2 was non-null
101	735710	EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
102		// check for conflict
103	1470644	Node conf = checkForMergeConflict(t1, t2, e1, e2);
104	735710	if (!conf.isNull())
105		{
106	1552	InferenceId id = t1.getType().isStringLike()
107	776	? InferenceId::STRINGS_PREFIX_CONFLICT
108	776	: InferenceId::STRINGS_ARITH_BOUND_CONFLICT;
109	776	d_state.setPendingMergeConflict(conf, id);
110	776	return;
111		}
112		// add information from e2 to e1
113	734934	if (!e2->d_lengthTerm.get().isNull())
114		{
115	365235	e1->d_lengthTerm.set(e2->d_lengthTerm);
116		}
117	734934	if (!e2->d_codeTerm.get().isNull())
118		{
119	18463	e1->d_codeTerm.set(e2->d_codeTerm);
120		}
121	734934	if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
122		{
123		e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
124		}
125	734934	if (!e2->d_normalizedLength.get().isNull())
126		{
127	124	e1->d_normalizedLength.set(e2->d_normalizedLength);
128		}
129		}
130
131	225020	void EagerSolver::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
132		{
133	225020	if (t1.getType().isStringLike())
134		{
135		// store disequalities between strings, may need to check if their lengths
136		// are equal/disequal
137	104196	d_state.addDisequality(t1, t2);
138		}
139	225020	}
140
141	16611	void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
142		{
143	16611	Assert(concat.getKind() == STRING_CONCAT
144		\|\| concat.getKind() == REGEXP_CONCAT);
145	16611	EqcInfo* ei = nullptr;
146		// check each side
147	49809	for (unsigned r = 0; r < 2; r++)
148		{
149	33218	unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1;
150	66416	Node c = utils::getConstantComponent(concat[index]);
151	33218	if (!c.isNull())
152		{
153	9483	if (ei == nullptr)
154		{
155	7690	ei = d_state.getOrMakeEqcInfo(eqc);
156		}
157	18966	Trace("strings-eager-pconf-debug")
158	9483	<< "New term: " << concat << " for " << t << " with prefix " << c
159	9483	<< " (" << (r == 1) << ")" << std::endl;
160	18946	Node conf = ei->addEndpointConst(t, c, r == 1);
161	9483	if (!conf.isNull())
162		{
163	20	d_state.setPendingMergeConflict(conf,
164		InferenceId::STRINGS_PREFIX_CONFLICT);
165	20	return;
166		}
167		}
168		}
169		}
170
171	735710	Node EagerSolver::checkForMergeConflict(Node a,
172		Node b,
173		EqcInfo* ea,
174		EqcInfo* eb)
175		{
176	735710	Assert(eb != nullptr && ea != nullptr);
177	735710	Assert(a.getType() == b.getType());
178	735710	Assert(a.getType().isStringLike() \|\| a.getType().isInteger());
179		// check prefix, suffix
180	2205785	for (size_t i = 0; i < 2; i++)
181		{
182	2940926	Node n = i == 0 ? eb->d_firstBound.get() : eb->d_secondBound.get();
183	1470851	if (!n.isNull())
184		{
185	912440	Node conf;
186	456608	if (a.getType().isStringLike())
187		{
188	83572	conf = ea->addEndpointConst(n, Node::null(), i == 1);
189		}
190		else
191		{
192	746072	Trace("strings-eager-aconf-debug")
193	373036	<< "addArithmeticBound " << n << " into " << a << " from " << b
194	373036	<< std::endl;
195	373036	conf = addArithmeticBound(ea, n, i == 0);
196		}
197	456608	if (!conf.isNull())
198		{
199	776	return conf;
200		}
201		}
202		}
203	734934	return Node::null();
204		}
205
206	1074645	void EagerSolver::notifyFact(TNode atom,
207		bool polarity,
208		TNode fact,
209		bool isInternal)
210		{
211	1074645	if (atom.getKind() == STRING_IN_REGEXP)
212		{
213	25621	if (polarity && atom[1].getKind() == REGEXP_CONCAT)
214		{
215	5469	eq::EqualityEngine* ee = d_state.getEqualityEngine();
216	10938	Node eqc = ee->getRepresentative(atom[0]);
217	5469	addEndpointsToEqcInfo(atom, atom[1], eqc);
218		}
219		}
220	1074645	}
221
222	373036	Node EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
223		{
224	373036	Assert(e != nullptr);
225	373036	Assert(!t.isNull());
226	746072	Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
227	746072	Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL)
228	373036	<< "Unexpected bound " << tb << " from " << t;
229	746072	Rational br = tb.getConst<Rational>();
230	746072	Node prev = isLower ? e->d_firstBound : e->d_secondBound;
231		// check if subsumed
232	373036	if (!prev.isNull())
233		{
234		// convert to bound
235	394765	Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
236	372364	Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL);
237	394765	Rational prevbr = prevb.getConst<Rational>();
238	372364	if (prevbr == br \|\| (br < prevbr) == isLower)
239		{
240		// subsumed
241	349963	return Node::null();
242		}
243		}
244	46146	Node prevo = isLower ? e->d_secondBound : e->d_firstBound;
245	46146	Trace("strings-eager-aconf-debug")
246	23073	<< "Check conflict for bounds " << t << " " << prevo << std::endl;
247	23073	if (!prevo.isNull())
248		{
249		// are we in conflict?
250	275	Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
251	275	Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL);
252	275	Rational prevobr = prevob.getConst<Rational>();
253	275	if (prevobr != br && (prevobr < br) == isLower)
254		{
255		// conflict
256	550	Node ret = EqcInfo::mkMergeConflict(t, prevo);
257	550	Trace("strings-eager-aconf")
258	275	<< "String: eager arithmetic bound conflict: " << ret << std::endl;
259	275	return ret;
260		}
261		}
262	22798	if (isLower)
263		{
264	22798	e->d_firstBound = t;
265		}
266		else
267		{
268		e->d_secondBound = t;
269		}
270	22798	return Node::null();
271		}
272
273	526440	Node EagerSolver::getBoundForLength(Node len, bool isLower)
274		{
275	526440	Assert(len.getKind() == STRING_LENGTH);
276		// it is prohibitively expensive to convert to original form and rewrite,
277		// since this may invoke the rewriter on lengths of complex terms. Instead,
278		// we convert to original term the argument, then call the utility method
279		// for computing the length of the argument, implicitly under an application
280		// of length (ArithEntail::getConstantBoundLength).
281		// convert to original form
282	1052880	Node olent = SkolemManager::getOriginalForm(len[0]);
283		// get the bound
284	526440	Node c = d_aent.getConstantBoundLength(olent, isLower);
285	1052880	Trace("strings-eager-aconf-debug")
286	526440	<< "Constant " << (isLower ? "lower" : "upper") << " bound for " << len
287	526440	<< " is " << c << ", from original form " << olent << std::endl;
288	1052880	return c;
289		}
290
291		} // namespace strings
292		} // namespace theory
293	31137	} // namespace cvc5