Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/prop/skolem_def_manager.cpp	Lines:	90	91	98.9 %
Date:	2021-11-07	Branches:	131	282	46.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Skolem definition manager.
 */

#include "prop/skolem_def_manager.h"

#include "expr/attribute.h"

namespace cvc5 {
namespace prop {

SkolemDefManager::SkolemDefManager(context::Context* context,
                                   context::UserContext* userContext)
    : d_skDefs(userContext), d_skActive(context)
{
}

SkolemDefManager::~SkolemDefManager() {}

void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
{
  // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
  Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
                   << std::endl;
  // in very rare cases, a skolem may be generated twice for terms that are
  // equivalent up to purification
  if (d_skDefs.find(skolem) == d_skDefs.end())
  {
    d_skDefs.insert(skolem, def);
  }
}

TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const
{
  NodeNodeMap::const_iterator it = d_skDefs.find(skolem);
  Assert(it != d_skDefs.end()) << "No skolem def for " << skolem;
  return it->second;
}

void SkolemDefManager::notifyAsserted(TNode literal,
                                      std::vector<TNode>& activatedSkolems,
                                      bool useDefs)
{
  std::unordered_set<Node> skolems;
  getSkolems(literal, skolems);
  for (const Node& k : skolems)
  {
    if (d_skActive.find(k) != d_skActive.end())
    {
      // already active
      continue;
    }
    d_skActive.insert(k);
    if (useDefs)
    {
      // add its definition to the activated list
      NodeNodeMap::const_iterator it = d_skDefs.find(k);
      Assert(it != d_skDefs.end());
      activatedSkolems.push_back(it->second);
    }
    else
    {
      // add to the activated list
      activatedSkolems.push_back(k);
    }
  }
}

struct HasSkolemTag
{
};
struct HasSkolemComputedTag
{
};
/** Attribute true for nodes with skolems in them */
typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
/** Attribute true for nodes where we have computed the above attribute */
typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;

bool SkolemDefManager::hasSkolems(TNode n) const
{
  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    if (cur.getAttribute(HasSkolemComputedAttr()))
    {
      visit.pop_back();
      // already computed
      continue;
    }
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited.insert(cur);
      if (cur.getNumChildren() == 0)
      {
        visit.pop_back();
        bool hasSkolem = false;
        if (cur.isVar())
        {
          hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
        }
        cur.setAttribute(HasSkolemAttr(), hasSkolem);
        cur.setAttribute(HasSkolemComputedAttr(), true);
      }
      else
      {
        if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
        {
          visit.push_back(cur.getOperator());
        }
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else
    {
      visit.pop_back();
      bool hasSkolem;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED
          && cur.getOperator().getAttribute(HasSkolemAttr()))
      {
        hasSkolem = true;
      }
      else
      {
        hasSkolem = false;
        for (TNode i : cur)
        {
          Assert(i.getAttribute(HasSkolemComputedAttr()));
          if (i.getAttribute(HasSkolemAttr()))
          {
            hasSkolem = true;
            break;
          }
        }
      }
      cur.setAttribute(HasSkolemAttr(), hasSkolem);
      cur.setAttribute(HasSkolemComputedAttr(), true);
    }
  } while (!visit.empty());
  Assert(n.getAttribute(HasSkolemComputedAttr()));
  return n.getAttribute(HasSkolemAttr());
}

void SkolemDefManager::getSkolems(TNode n,
                                  std::unordered_set<Node>& skolems) const
{
  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (!hasSkolems(cur))
    {
      // does not have skolems, continue
      continue;
    }
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited.insert(cur);
      if (cur.isVar())
      {
        if (d_skDefs.find(cur) != d_skDefs.end())
        {
          skolems.insert(cur);
        }
        continue;
      }
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        visit.push_back(cur.getOperator());
      }
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
}

}  // namespace prop
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Skolem definition manager.
14		*/
15
16		#include "prop/skolem_def_manager.h"
17
18		#include "expr/attribute.h"
19
20		namespace cvc5 {
21		namespace prop {
22
23	15340	SkolemDefManager::SkolemDefManager(context::Context* context,
24	15340	context::UserContext* userContext)
25	15340	: d_skDefs(userContext), d_skActive(context)
26		{
27	15340	}
28
29	15335	SkolemDefManager::~SkolemDefManager() {}
30
31	29756	void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
32		{
33		// Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
34	59512	Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
35	29756	<< std::endl;
36		// in very rare cases, a skolem may be generated twice for terms that are
37		// equivalent up to purification
38	29756	if (d_skDefs.find(skolem) == d_skDefs.end())
39		{
40	29691	d_skDefs.insert(skolem, def);
41		}
42	29756	}
43
44	2523	TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const
45		{
46	2523	NodeNodeMap::const_iterator it = d_skDefs.find(skolem);
47	2523	Assert(it != d_skDefs.end()) << "No skolem def for " << skolem;
48	2523	return it->second;
49		}
50
51	7431374	void SkolemDefManager::notifyAsserted(TNode literal,
52		std::vector<TNode>& activatedSkolems,
53		bool useDefs)
54		{
55	14862748	std::unordered_set<Node> skolems;
56	7431374	getSkolems(literal, skolems);
57	11316760	for (const Node& k : skolems)
58		{
59	3885386	if (d_skActive.find(k) != d_skActive.end())
60		{
61		// already active
62	3512563	continue;
63		}
64	372823	d_skActive.insert(k);
65	372823	if (useDefs)
66		{
67		// add its definition to the activated list
68	372823	NodeNodeMap::const_iterator it = d_skDefs.find(k);
69	372823	Assert(it != d_skDefs.end());
70	372823	activatedSkolems.push_back(it->second);
71		}
72		else
73		{
74		// add to the activated list
75		activatedSkolems.push_back(k);
76		}
77		}
78	7431374	}
79
80		struct HasSkolemTag
81		{
82		};
83		struct HasSkolemComputedTag
84		{
85		};
86		/** Attribute true for nodes with skolems in them */
87		typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
88		/** Attribute true for nodes where we have computed the above attribute */
89		typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
90
91	23266003	bool SkolemDefManager::hasSkolems(TNode n) const
92		{
93	46532006	std::unordered_set<TNode> visited;
94	23266003	std::unordered_set<TNode>::iterator it;
95	46532006	std::vector<TNode> visit;
96	46532006	TNode cur;
97	23266003	visit.push_back(n);
98	3204980	do
99		{
100	26470983	cur = visit.back();
101	50619814	if (cur.getAttribute(HasSkolemComputedAttr()))
102		{
103	24148831	visit.pop_back();
104		// already computed
105	24148831	continue;
106		}
107	2322152	it = visited.find(cur);
108	2322152	if (it == visited.end())
109		{
110	1261555	visited.insert(cur);
111	1261555	if (cur.getNumChildren() == 0)
112		{
113	200958	visit.pop_back();
114	200958	bool hasSkolem = false;
115	200958	if (cur.isVar())
116		{
117	145104	hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
118		}
119	200958	cur.setAttribute(HasSkolemAttr(), hasSkolem);
120	200958	cur.setAttribute(HasSkolemComputedAttr(), true);
121		}
122		else
123		{
124	1060597	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
125		{
126	194380	visit.push_back(cur.getOperator());
127		}
128	1060597	visit.insert(visit.end(), cur.begin(), cur.end());
129		}
130		}
131		else
132		{
133	1060597	visit.pop_back();
134		bool hasSkolem;
135	2121194	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED
136	2121194	&& cur.getOperator().getAttribute(HasSkolemAttr()))
137		{
138	42	hasSkolem = true;
139		}
140		else
141		{
142	1060555	hasSkolem = false;
143	2781386	for (TNode i : cur)
144		{
145	1866505	Assert(i.getAttribute(HasSkolemComputedAttr()));
146	1866505	if (i.getAttribute(HasSkolemAttr()))
147		{
148	145674	hasSkolem = true;
149	145674	break;
150		}
151		}
152		}
153	1060597	cur.setAttribute(HasSkolemAttr(), hasSkolem);
154	1060597	cur.setAttribute(HasSkolemComputedAttr(), true);
155		}
156	26470983	} while (!visit.empty());
157	23266003	Assert(n.getAttribute(HasSkolemComputedAttr()));
158	46532006	return n.getAttribute(HasSkolemAttr());
159		}
160
161	7435051	void SkolemDefManager::getSkolems(TNode n,
162		std::unordered_set<Node>& skolems) const
163		{
164	14870102	std::unordered_set<TNode> visited;
165	7435051	std::unordered_set<TNode>::iterator it;
166	14870102	std::vector<TNode> visit;
167	14870102	TNode cur;
168	7435051	visit.push_back(n);
169	15830952	do
170		{
171	23266003	cur = visit.back();
172	23266003	visit.pop_back();
173	23266003	if (!hasSkolems(cur))
174		{
175		// does not have skolems, continue
176	10336359	continue;
177		}
178	12929644	it = visited.find(cur);
179	12929644	if (it == visited.end())
180		{
181	12325843	visited.insert(cur);
182	16213752	if (cur.isVar())
183		{
184	3887909	if (d_skDefs.find(cur) != d_skDefs.end())
185		{
186	3887909	skolems.insert(cur);
187		}
188	3887909	continue;
189		}
190	8437934	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
191		{
192	1748710	visit.push_back(cur.getOperator());
193		}
194	8437934	visit.insert(visit.end(), cur.begin(), cur.end());
195		}
196	23266003	} while (!visit.empty());
197	7435051	}
198
199		} // namespace prop
200	31137	} // namespace cvc5