Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/relevance_manager.cpp	Lines:	103	148	69.6 %
Date:	2021-09-07	Branches:	146	506	28.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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 relevance manager.
 */

#include "theory/relevance_manager.h"

#include <sstream>

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

RelevanceManager::RelevanceManager(context::UserContext* userContext,
                                   Valuation val)
    : d_val(val), d_input(userContext), d_computed(false), d_success(false)
{
}

void RelevanceManager::notifyPreprocessedAssertions(
    const std::vector<Node>& assertions)
{
  // add to input list, which is user-context dependent
  std::vector<Node> toProcess;
  for (const Node& a : assertions)
  {
    if (a.getKind() == AND)
    {
      // split top-level AND
      for (const Node& ac : a)
      {
        toProcess.push_back(ac);
      }
    }
    else
    {
      d_input.push_back(a);
    }
  }
  addAssertionsInternal(toProcess);
}

void RelevanceManager::notifyPreprocessedAssertion(Node n)
{
  std::vector<Node> toProcess;
  toProcess.push_back(n);
  addAssertionsInternal(toProcess);
}

void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
{
  size_t i = 0;
  while (i < toProcess.size())
  {
    Node a = toProcess[i];
    if (a.getKind() == AND)
    {
      // split AND
      for (const Node& ac : a)
      {
        toProcess.push_back(ac);
      }
    }
    else
    {
      // note that a could be a literal, in which case we could add it to
      // an "always relevant" set here.
      d_input.push_back(a);
    }
    i++;
  }
}

void RelevanceManager::resetRound()
{
  d_computed = false;
}

void RelevanceManager::computeRelevance()
{
  d_computed = true;
  d_rset.clear();
  Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
  std::unordered_map<TNode, int> cache;
  for (const Node& node: d_input)
  {
    TNode n = node;
    int val = justify(n, cache);
    if (val != 1)
    {
      std::stringstream serr;
      serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
           << n;
      Trace("rel-manager") << serr.str() << std::endl;
      Assert(false) << serr.str();
      d_success = false;
      d_rset.clear();
      return;
    }
  }
  Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
  d_success = true;
}

bool RelevanceManager::isBooleanConnective(TNode cur)
{
  Kind k = cur.getKind();
  return k == NOT || k == IMPLIES || k == AND || k == OR || k == ITE || k == XOR
         || (k == EQUAL && cur[0].getType().isBoolean());
}

bool RelevanceManager::updateJustifyLastChild(
    TNode cur,
    std::vector<int>& childrenJustify,
    std::unordered_map<TNode, int>& cache)
{
  // This method is run when we are informed that child index of cur
  // has justify status lastChildJustify. We return true if we would like to
  // compute the next child, in this case we push the status of the current
  // child to childrenJustify.
  size_t nchildren = cur.getNumChildren();
  Assert(isBooleanConnective(cur));
  size_t index = childrenJustify.size();
  Assert(index < nchildren);
  Assert(cache.find(cur[index]) != cache.end());
  Kind k = cur.getKind();
  // Lookup the last child's value in the overall cache, we may choose to
  // add this to childrenJustify if we return true.
  int lastChildJustify = cache[cur[index]];
  if (k == NOT)
  {
    cache[cur] = -lastChildJustify;
  }
  else if (k == IMPLIES || k == AND || k == OR)
  {
    if (lastChildJustify != 0)
    {
      // See if we short circuited? The value for short circuiting is false if
      // we are AND or the first child of IMPLIES.
      if (lastChildJustify
          == ((k == AND || (k == IMPLIES && index == 0)) ? -1 : 1))
      {
        cache[cur] = k == AND ? -1 : 1;
        return false;
      }
    }
    if (index + 1 == nchildren)
    {
      // finished all children, compute the overall value
      int ret = k == AND ? 1 : -1;
      for (int cv : childrenJustify)
      {
        if (cv == 0)
        {
          ret = 0;
          break;
        }
      }
      cache[cur] = ret;
    }
    else
    {
      // continue
      childrenJustify.push_back(lastChildJustify);
      return true;
    }
  }
  else if (lastChildJustify == 0)
  {
    // all other cases, an unknown child implies we are unknown
    cache[cur] = 0;
  }
  else if (k == ITE)
  {
    if (index == 0)
    {
      Assert(lastChildJustify != 0);
      // continue with branch
      childrenJustify.push_back(lastChildJustify);
      if (lastChildJustify == -1)
      {
        // also mark first branch as don't care
        childrenJustify.push_back(0);
      }
      return true;
    }
    else
    {
      // should be in proper branch
      Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
      // we are the value of the branch
      cache[cur] = lastChildJustify;
    }
  }
  else
  {
    Assert(k == XOR || k == EQUAL);
    Assert(nchildren == 2);
    Assert(lastChildJustify != 0);
    if (index == 0)
    {
      // must compute the other child
      childrenJustify.push_back(lastChildJustify);
      return true;
    }
    else
    {
      // both children known, compute value
      Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
      cache[cur] =
          ((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1
                                                                         : -1;
    }
  }
  return false;
}

int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache)
{
  // the vector of values of children
  std::unordered_map<TNode, std::vector<int>> childJustify;
  std::unordered_map<TNode, int>::iterator it;
  std::unordered_map<TNode, std::vector<int>>::iterator itc;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    // should always have Boolean type
    Assert(cur.getType().isBoolean());
    it = cache.find(cur);
    if (it != cache.end())
    {
      visit.pop_back();
      // already computed value
      continue;
    }
    itc = childJustify.find(cur);
    // have we traversed to children yet?
    if (itc == childJustify.end())
    {
      // are we not a Boolean connective (including NOT)?
      if (isBooleanConnective(cur))
      {
        // initialize its children justify vector as empty
        childJustify[cur].clear();
        // start with the first child
        visit.push_back(cur[0]);
      }
      else
      {
        visit.pop_back();
        // The atom case, lookup the value in the valuation class to
        // see its current value in the SAT solver, if it has one.
        int ret = 0;
        // otherwise we look up the value
        bool value;
        if (d_val.hasSatValue(cur, value))
        {
          ret = value ? 1 : -1;
          d_rset.insert(cur);
        }
        cache[cur] = ret;
      }
    }
    else
    {
      // this processes the impact of the current child on the value of cur,
      // and possibly requests that a new child is computed.
      if (updateJustifyLastChild(cur, itc->second, cache))
      {
        Assert(itc->second.size() < cur.getNumChildren());
        TNode nextChild = cur[itc->second.size()];
        visit.push_back(nextChild);
      }
      else
      {
        visit.pop_back();
      }
    }
  } while (!visit.empty());
  Assert(cache.find(n) != cache.end());
  return cache[n];
}

bool RelevanceManager::isRelevant(Node lit)
{
  if (!d_computed)
  {
    computeRelevance();
  }
  if (!d_success)
  {
    // always relevant if we failed to compute
    return true;
  }
  // agnostic to negation
  while (lit.getKind() == NOT)
  {
    lit = lit[0];
  }
  return d_rset.find(lit) != d_rset.end();
}

const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
    bool& success)
{
  if (!d_computed)
  {
    computeRelevance();
  }
  // update success flag
  success = d_success;
  return d_rset;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
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 relevance manager.
14		*/
15
16		#include "theory/relevance_manager.h"
17
18		#include <sstream>
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23		namespace theory {
24
25	18	RelevanceManager::RelevanceManager(context::UserContext* userContext,
26	18	Valuation val)
27	18	: d_val(val), d_input(userContext), d_computed(false), d_success(false)
28		{
29	18	}
30
31	18	void RelevanceManager::notifyPreprocessedAssertions(
32		const std::vector<Node>& assertions)
33		{
34		// add to input list, which is user-context dependent
35	36	std::vector<Node> toProcess;
36	121	for (const Node& a : assertions)
37		{
38	103	if (a.getKind() == AND)
39		{
40		// split top-level AND
41	3	for (const Node& ac : a)
42		{
43	2	toProcess.push_back(ac);
44		}
45		}
46		else
47		{
48	102	d_input.push_back(a);
49		}
50		}
51	18	addAssertionsInternal(toProcess);
52	18	}
53
54		void RelevanceManager::notifyPreprocessedAssertion(Node n)
55		{
56		std::vector<Node> toProcess;
57		toProcess.push_back(n);
58		addAssertionsInternal(toProcess);
59		}
60
61	18	void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
62		{
63	18	size_t i = 0;
64	22	while (i < toProcess.size())
65		{
66	4	Node a = toProcess[i];
67	2	if (a.getKind() == AND)
68		{
69		// split AND
70		for (const Node& ac : a)
71		{
72		toProcess.push_back(ac);
73		}
74		}
75		else
76		{
77		// note that a could be a literal, in which case we could add it to
78		// an "always relevant" set here.
79	2	d_input.push_back(a);
80		}
81	2	i++;
82		}
83	18	}
84
85	132	void RelevanceManager::resetRound()
86		{
87	132	d_computed = false;
88	132	}
89
90	83	void RelevanceManager::computeRelevance()
91		{
92	83	d_computed = true;
93	83	d_rset.clear();
94	83	Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
95	166	std::unordered_map<TNode, int> cache;
96	455	for (const Node& node: d_input)
97		{
98	744	TNode n = node;
99	372	int val = justify(n, cache);
100	372	if (val != 1)
101		{
102		std::stringstream serr;
103		serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
104		<< n;
105		Trace("rel-manager") << serr.str() << std::endl;
106		Assert(false) << serr.str();
107		d_success = false;
108		d_rset.clear();
109		return;
110		}
111		}
112	83	Trace("rel-manager") << "...success, size = " << d_rset.size() << std::endl;
113	83	d_success = true;
114		}
115
116	864	bool RelevanceManager::isBooleanConnective(TNode cur)
117		{
118	864	Kind k = cur.getKind();
119	430	return k == NOT \|\| k == IMPLIES \|\| k == AND \|\| k == OR \|\| k == ITE \|\| k == XOR
120	1246	\|\| (k == EQUAL && cur[0].getType().isBoolean());
121		}
122
123	246	bool RelevanceManager::updateJustifyLastChild(
124		TNode cur,
125		std::vector<int>& childrenJustify,
126		std::unordered_map<TNode, int>& cache)
127		{
128		// This method is run when we are informed that child index of cur
129		// has justify status lastChildJustify. We return true if we would like to
130		// compute the next child, in this case we push the status of the current
131		// child to childrenJustify.
132	246	size_t nchildren = cur.getNumChildren();
133	246	Assert(isBooleanConnective(cur));
134	246	size_t index = childrenJustify.size();
135	246	Assert(index < nchildren);
136	246	Assert(cache.find(cur[index]) != cache.end());
137	246	Kind k = cur.getKind();
138		// Lookup the last child's value in the overall cache, we may choose to
139		// add this to childrenJustify if we return true.
140	246	int lastChildJustify = cache[cur[index]];
141	246	if (k == NOT)
142		{
143	217	cache[cur] = -lastChildJustify;
144		}
145	29	else if (k == IMPLIES \|\| k == AND \|\| k == OR)
146		{
147	29	if (lastChildJustify != 0)
148		{
149		// See if we short circuited? The value for short circuiting is false if
150		// we are AND or the first child of IMPLIES.
151	29	if (lastChildJustify
152	29	== ((k == AND \|\| (k == IMPLIES && index == 0)) ? -1 : 1))
153		{
154	18	cache[cur] = k == AND ? -1 : 1;
155	18	return false;
156		}
157		}
158	11	if (index + 1 == nchildren)
159		{
160		// finished all children, compute the overall value
161	1	int ret = k == AND ? 1 : -1;
162	2	for (int cv : childrenJustify)
163		{
164	1	if (cv == 0)
165		{
166		ret = 0;
167		break;
168		}
169		}
170	1	cache[cur] = ret;
171		}
172		else
173		{
174		// continue
175	10	childrenJustify.push_back(lastChildJustify);
176	10	return true;
177	1	}
178		}
179		else if (lastChildJustify == 0)
180		{
181		// all other cases, an unknown child implies we are unknown
182		cache[cur] = 0;
183		}
184		else if (k == ITE)
185		{
186		if (index == 0)
187		{
188		Assert(lastChildJustify != 0);
189		// continue with branch
190		childrenJustify.push_back(lastChildJustify);
191		if (lastChildJustify == -1)
192		{
193		// also mark first branch as don't care
194		childrenJustify.push_back(0);
195		}
196		return true;
197		}
198		else
199		{
200		// should be in proper branch
201		Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
202		// we are the value of the branch
203		cache[cur] = lastChildJustify;
204		}
205		}
206		else
207		{
208		Assert(k == XOR \|\| k == EQUAL);
209		Assert(nchildren == 2);
210		Assert(lastChildJustify != 0);
211		if (index == 0)
212		{
213		// must compute the other child
214		childrenJustify.push_back(lastChildJustify);
215		return true;
216		}
217		else
218		{
219		// both children known, compute value
220		Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
221		cache[cur] =
222		((k == XOR ? -1 : 1) * lastChildJustify == childrenJustify[0]) ? 1
223		: -1;
224		}
225		}
226	218	return false;
227		}
228
229	372	int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache)
230		{
231		// the vector of values of children
232	744	std::unordered_map<TNode, std::vector<int>> childJustify;
233	372	std::unordered_map<TNode, int>::iterator it;
234	372	std::unordered_map<TNode, std::vector<int>>::iterator itc;
235	744	std::vector<TNode> visit;
236	744	TNode cur;
237	372	visit.push_back(n);
238	492	do
239		{
240	864	cur = visit.back();
241		// should always have Boolean type
242	864	Assert(cur.getType().isBoolean());
243	864	it = cache.find(cur);
244	864	if (it != cache.end())
245		{
246		visit.pop_back();
247		// already computed value
248		continue;
249		}
250	864	itc = childJustify.find(cur);
251		// have we traversed to children yet?
252	864	if (itc == childJustify.end())
253		{
254		// are we not a Boolean connective (including NOT)?
255	618	if (isBooleanConnective(cur))
256		{
257		// initialize its children justify vector as empty
258	236	childJustify[cur].clear();
259		// start with the first child
260	236	visit.push_back(cur[0]);
261		}
262		else
263		{
264	382	visit.pop_back();
265		// The atom case, lookup the value in the valuation class to
266		// see its current value in the SAT solver, if it has one.
267	382	int ret = 0;
268		// otherwise we look up the value
269		bool value;
270	382	if (d_val.hasSatValue(cur, value))
271		{
272	382	ret = value ? 1 : -1;
273	382	d_rset.insert(cur);
274		}
275	382	cache[cur] = ret;
276		}
277		}
278		else
279		{
280		// this processes the impact of the current child on the value of cur,
281		// and possibly requests that a new child is computed.
282	246	if (updateJustifyLastChild(cur, itc->second, cache))
283		{
284	10	Assert(itc->second.size() < cur.getNumChildren());
285	20	TNode nextChild = cur[itc->second.size()];
286	10	visit.push_back(nextChild);
287		}
288		else
289		{
290	236	visit.pop_back();
291		}
292		}
293	864	} while (!visit.empty());
294	372	Assert(cache.find(n) != cache.end());
295	744	return cache[n];
296		}
297
298	2445	bool RelevanceManager::isRelevant(Node lit)
299		{
300	2445	if (!d_computed)
301		{
302	83	computeRelevance();
303		}
304	2445	if (!d_success)
305		{
306		// always relevant if we failed to compute
307		return true;
308		}
309		// agnostic to negation
310	4851	while (lit.getKind() == NOT)
311		{
312	1203	lit = lit[0];
313		}
314	2445	return d_rset.find(lit) != d_rset.end();
315		}
316
317		const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
318		bool& success)
319		{
320		if (!d_computed)
321		{
322		computeRelevance();
323		}
324		// update success flag
325		success = d_success;
326		return d_rset;
327		}
328
329		} // namespace theory
330	29502	} // namespace cvc5