Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/relevance_manager.cpp	Lines:	119	168	70.8 %
Date:	2021-11-07	Branches:	161	552	29.2 %


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

#include "options/smt_options.h"
#include "smt/env.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val)
    : d_val(val),
      d_input(lemContext),
      d_computed(false),
      d_success(false),
      d_trackRSetExp(false),
      d_miniscopeTopLevel(true)
{
  if (options::produceDifficulty())
  {
    d_dman.reset(new DifficultyManager(lemContext, val));
    d_trackRSetExp = true;
    // we cannot miniscope AND at the top level, since we need to
    // preserve the exact form of preprocessed assertions so the dependencies
    // are tracked.
    d_miniscopeTopLevel = 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 (d_miniscopeTopLevel && 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 (d_miniscopeTopLevel && a.getKind() == AND)
    {
      // difficulty tracking disables miniscoping of AND
      Assert(d_dman == nullptr);
      // 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();
  d_rsetExp.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);
          if (d_trackRSetExp)
          {
            d_rsetExp[cur] = n;
          }
        }
        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;
}

void RelevanceManager::notifyLemma(Node n)
{
  if (d_dman != nullptr)
  {
    // ensure we know which literals are relevant, and why
    computeRelevance();
    d_dman->notifyLemma(d_rsetExp, n);
  }
}

void RelevanceManager::notifyCandidateModel(TheoryModel* m)
{
  if (d_dman != nullptr)
  {
    d_dman->notifyCandidateModel(d_input, m);
  }
}

void RelevanceManager::getDifficultyMap(std::map<Node, Node>& dmap)
{
  if (d_dman != nullptr)
  {
    d_dman->getDifficultyMap(dmap);
  }
}

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