Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_node_algorithm.cpp	Lines:	126	137	92.0 %
Date:	2021-11-07	Branches:	166	328	50.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa
 *
 * 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 proof node algorithm utilities.
 */

#include "proof/proof_node_algorithm.h"

#include "proof/proof_node.h"

namespace cvc5 {
namespace expr {

void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
{
  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
  std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
      pn->getRule(), pn->getChildren(), pn->getArguments());
  getFreeAssumptionsMap(spn, amap);
  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
       amap)
  {
    assump.push_back(p.first);
  }
}

void getFreeAssumptionsMap(
    std::shared_ptr<ProofNode> pn,
    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
{
  // proof should not be cyclic
  // visited set false after preorder traversal, true after postorder traversal
  std::unordered_map<ProofNode*, bool> visited;
  std::unordered_map<ProofNode*, bool>::iterator it;
  std::vector<std::shared_ptr<ProofNode>> visit;
  std::vector<std::shared_ptr<ProofNode>> traversing;
  // Maps a bound assumption to the number of bindings it is under
  // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
  // (ASSUME x), and x would be mapped to 1.
  //
  // This map is used to track which nodes are in scope while traversing the
  // DAG. The in-scope assumptions are keys in the map. They're removed when
  // their binding count drops to zero. Let's annotate the above example to
  // serve as an illustration:
  //
  //   (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
  //
  // This is how the map changes during the traversal:
  //   after  previsiting SCOPE0: { y: 1 }
  //   after  previsiting SCOPE1: { y: 2, x: 1 }
  //   at                 ASSUME: { y: 2, x: 1 } (so x is in scope!)
  //   after postvisiting SCOPE1: { y: 1 }
  //   after postvisiting SCOPE2: {}
  //
  std::unordered_map<Node, uint32_t> scopeDepth;
  std::shared_ptr<ProofNode> cur;
  visit.push_back(pn);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur.get());
    const std::vector<Node>& cargs = cur->getArguments();
    if (it == visited.end())
    {
      PfRule id = cur->getRule();
      if (id == PfRule::ASSUME)
      {
        visited[cur.get()] = true;
        Assert(cargs.size() == 1);
        Node f = cargs[0];
        if (!scopeDepth.count(f))
        {
          amap[f].push_back(cur);
        }
      }
      else
      {
        if (id == PfRule::SCOPE)
        {
          // mark that its arguments are bound in the current scope
          for (const Node& a : cargs)
          {
            scopeDepth[a] += 1;
          }
          // will need to unbind the variables below
        }
        // The following loop cannot be merged with the loop above because the
        // same subproof
        visited[cur.get()] = false;
        visit.push_back(cur);
        traversing.push_back(cur);
        const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
        for (const std::shared_ptr<ProofNode>& cp : cs)
        {
          if (std::find(traversing.begin(), traversing.end(), cp)
              != traversing.end())
          {
            Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
                           "--proof-check=eager)"
                        << std::endl;
          }
          visit.push_back(cp);
        }
      }
    }
    else if (!it->second)
    {
      Assert(!traversing.empty());
      traversing.pop_back();
      visited[cur.get()] = true;
      if (cur->getRule() == PfRule::SCOPE)
      {
        // unbind its assumptions
        for (const Node& a : cargs)
        {
          auto scopeCt = scopeDepth.find(a);
          Assert(scopeCt != scopeDepth.end());
          scopeCt->second -= 1;
          if (scopeCt->second == 0)
          {
            scopeDepth.erase(scopeCt);
          }
        }
      }
    }
  } while (!visit.empty());
}

bool containsAssumption(const ProofNode* pn,
                        std::unordered_map<const ProofNode*, bool>& caMap)
{
  std::unordered_map<const ProofNode*, bool> visited;
  std::unordered_map<const ProofNode*, bool>::iterator it;
  std::vector<const ProofNode*> visit;
  visit.push_back(pn);
  bool foundAssumption = false;
  const ProofNode* cur;
  while (!visit.empty())
  {
    cur = visit.back();
    visit.pop_back();
    // have we already computed?
    it = caMap.find(cur);
    if (it != caMap.end())
    {
      // if cached, we set found assumption to true if applicable and continue
      if (it->second)
      {
        foundAssumption = true;
      }
      continue;
    }
    it = visited.find(cur);
    if (it == visited.end())
    {
      PfRule r = cur->getRule();
      if (r == PfRule::ASSUME)
      {
        visited[cur] = true;
        caMap[cur] = true;
        foundAssumption = true;
      }
      else if (!foundAssumption)
      {
        // if we haven't found an assumption yet, recurse. Otherwise, we will
        // not bother computing whether this subproof contains an assumption
        // since we know its parent already contains one by another child.
        visited[cur] = false;
        visit.push_back(cur);
        const std::vector<std::shared_ptr<ProofNode>>& children =
            cur->getChildren();
        for (const std::shared_ptr<ProofNode>& cp : children)
        {
          visit.push_back(cp.get());
        }
      }
    }
    else if (!it->second)
    {
      visited[cur] = true;
      // we contain an assumption if we've found an assumption in a child
      caMap[cur] = foundAssumption;
    }
  }
  return caMap[cur];
}

bool containsAssumption(const ProofNode* pn)
{
  std::unordered_map<const ProofNode*, bool> caMap;
  return containsAssumption(pn, caMap);
}

bool containsSubproof(ProofNode* pn, ProofNode* pnc)
{
  std::unordered_set<const ProofNode*> visited;
  return containsSubproof(pn, pnc, visited);
}

bool containsSubproof(ProofNode* pn,
                      ProofNode* pnc,
                      std::unordered_set<const ProofNode*>& visited)
{
  std::unordered_map<const ProofNode*, bool>::iterator it;
  std::vector<const ProofNode*> visit;
  visit.push_back(pn);
  const ProofNode* cur;
  while (!visit.empty())
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      visited.insert(cur);
      if (cur == pnc)
      {
        return true;
      }
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& cp : children)
      {
        visit.push_back(cp.get());
      }
    }
  }
  return false;
}

bool isSingletonClause(TNode res,
                       const std::vector<Node>& children,
                       const std::vector<Node>& args)
{
  if (res.getKind() != kind::OR)
  {
    return true;
  }
  size_t i;
  Node trueNode = NodeManager::currentNM()->mkConst(true);
  // Find out the last child to introduced res, if any. We only need to
  // look at the last one because any previous introduction would have
  // been eliminated.
  //
  // After the loop finishes i is the index of the child C_i that
  // introduced res. If i=0 none of the children introduced res as a
  // subterm and therefore it cannot be a singleton clause.
  for (i = children.size(); i > 0; --i)
  {
    // only non-singleton clauses may be introducing
    // res, so we only care about non-singleton or nodes. We check then
    // against the kind and whether the whole or node occurs as a pivot of
    // the respective resolution
    if (children[i - 1].getKind() != kind::OR)
    {
      continue;
    }
    size_t pivotIndex = (i != 1) ? 2 * (i - 1) - 1 : 1;
    if (args[pivotIndex] == children[i - 1]
        || args[pivotIndex].notNode() == children[i - 1])
    {
      continue;
    }
    // if res occurs as a subterm of a non-singleton premise
    if (std::find(children[i - 1].begin(), children[i - 1].end(), res)
        != children[i - 1].end())
    {
      break;
    }
  }

  // If res is a subterm of one of the children we still need to check if
  // that subterm is eliminated
  if (i > 0)
  {
    bool posFirst = (i == 1) ? (args[0] == trueNode)
                             : (args[(2 * (i - 1)) - 2] == trueNode);
    Node pivot = (i == 1) ? args[1] : args[(2 * (i - 1)) - 1];

    // Check if it is eliminated by the previous resolution step
    if ((res == pivot && !posFirst) || (res.notNode() == pivot && posFirst)
        || (pivot.notNode() == res && posFirst))
    {
      // We decrease i by one, since it could have been the case that i
      // was equal to children.size(), so that we return false in the end
      --i;
    }
    else
    {
      // Otherwise check if any subsequent premise eliminates it
      for (; i < children.size(); ++i)
      {
        posFirst = args[(2 * i) - 2] == trueNode;
        pivot = args[(2 * i) - 1];
        // To eliminate res, the clause must contain it with opposite
        // polarity. There are three successful cases, according to the
        // pivot and its sign
        //
        // - res is the same as the pivot and posFirst is true, which
        // means that the clause contains its negation and eliminates it
        //
        // - res is the negation of the pivot and posFirst is false, so
        // the clause contains the node whose negation is res. Note that
        // this case may either be res.notNode() == pivot or res ==
        // pivot.notNode().
        if ((res == pivot && posFirst) || (res.notNode() == pivot && !posFirst)
            || (pivot.notNode() == res && !posFirst))
        {
          break;
        }
      }
    }
  }
  // if not eliminated (loop went to the end), then it's a singleton
  // clause
  return i == children.size();
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa
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 proof node algorithm utilities.
14		*/
15
16		#include "proof/proof_node_algorithm.h"
17
18		#include "proof/proof_node.h"
19
20		namespace cvc5 {
21		namespace expr {
22
23	83013	void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
24		{
25	166026	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
26		std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
27	166026	pn->getRule(), pn->getChildren(), pn->getArguments());
28	83013	getFreeAssumptionsMap(spn, amap);
29	108687	for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
30	83013	amap)
31		{
32	108687	assump.push_back(p.first);
33		}
34	83013	}
35
36	382596	void getFreeAssumptionsMap(
37		std::shared_ptr<ProofNode> pn,
38		std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
39		{
40		// proof should not be cyclic
41		// visited set false after preorder traversal, true after postorder traversal
42	765192	std::unordered_map<ProofNode*, bool> visited;
43	382596	std::unordered_map<ProofNode*, bool>::iterator it;
44	765192	std::vector<std::shared_ptr<ProofNode>> visit;
45	765192	std::vector<std::shared_ptr<ProofNode>> traversing;
46		// Maps a bound assumption to the number of bindings it is under
47		// e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
48		// (ASSUME x), and x would be mapped to 1.
49		//
50		// This map is used to track which nodes are in scope while traversing the
51		// DAG. The in-scope assumptions are keys in the map. They're removed when
52		// their binding count drops to zero. Let's annotate the above example to
53		// serve as an illustration:
54		//
55		// (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
56		//
57		// This is how the map changes during the traversal:
58		// after previsiting SCOPE0: { y: 1 }
59		// after previsiting SCOPE1: { y: 2, x: 1 }
60		// at ASSUME: { y: 2, x: 1 } (so x is in scope!)
61		// after postvisiting SCOPE1: { y: 1 }
62		// after postvisiting SCOPE2: {}
63		//
64	765192	std::unordered_map<Node, uint32_t> scopeDepth;
65	765192	std::shared_ptr<ProofNode> cur;
66	382596	visit.push_back(pn);
67	18829870	do
68		{
69	19212466	cur = visit.back();
70	19212466	visit.pop_back();
71	19212466	it = visited.find(cur.get());
72	19212466	const std::vector<Node>& cargs = cur->getArguments();
73	19212466	if (it == visited.end())
74		{
75	9634367	PfRule id = cur->getRule();
76	9634367	if (id == PfRule::ASSUME)
77		{
78	3494279	visited[cur.get()] = true;
79	3494279	Assert(cargs.size() == 1);
80	6988558	Node f = cargs[0];
81	3494279	if (!scopeDepth.count(f))
82		{
83	2777478	amap[f].push_back(cur);
84		}
85		}
86		else
87		{
88	6140088	if (id == PfRule::SCOPE)
89		{
90		// mark that its arguments are bound in the current scope
91	931097	for (const Node& a : cargs)
92		{
93	753197	scopeDepth[a] += 1;
94		}
95		// will need to unbind the variables below
96		}
97		// The following loop cannot be merged with the loop above because the
98		// same subproof
99	6140088	visited[cur.get()] = false;
100	6140088	visit.push_back(cur);
101	6140088	traversing.push_back(cur);
102	6140088	const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
103	18829870	for (const std::shared_ptr<ProofNode>& cp : cs)
104		{
105	38069346	if (std::find(traversing.begin(), traversing.end(), cp)
106	38069346	!= traversing.end())
107		{
108		Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
109		"--proof-check=eager)"
110		<< std::endl;
111		}
112	12689782	visit.push_back(cp);
113		}
114		}
115		}
116	9578099	else if (!it->second)
117		{
118	6140088	Assert(!traversing.empty());
119	6140088	traversing.pop_back();
120	6140088	visited[cur.get()] = true;
121	6140088	if (cur->getRule() == PfRule::SCOPE)
122		{
123		// unbind its assumptions
124	931097	for (const Node& a : cargs)
125		{
126	753197	auto scopeCt = scopeDepth.find(a);
127	753197	Assert(scopeCt != scopeDepth.end());
128	753197	scopeCt->second -= 1;
129	753197	if (scopeCt->second == 0)
130		{
131	678929	scopeDepth.erase(scopeCt);
132		}
133		}
134		}
135		}
136	19212466	} while (!visit.empty());
137	382596	}
138
139	2300416	bool containsAssumption(const ProofNode* pn,
140		std::unordered_map<const ProofNode*, bool>& caMap)
141		{
142	4600832	std::unordered_map<const ProofNode*, bool> visited;
143	2300416	std::unordered_map<const ProofNode*, bool>::iterator it;
144	4600832	std::vector<const ProofNode*> visit;
145	2300416	visit.push_back(pn);
146	2300416	bool foundAssumption = false;
147		const ProofNode* cur;
148	18672908	while (!visit.empty())
149		{
150	8186246	cur = visit.back();
151	8186246	visit.pop_back();
152		// have we already computed?
153	8186246	it = caMap.find(cur);
154	12022172	if (it != caMap.end())
155		{
156		// if cached, we set found assumption to true if applicable and continue
157	3835926	if (it->second)
158		{
159	2303899	foundAssumption = true;
160		}
161	3835926	continue;
162		}
163	4350320	it = visited.find(cur);
164	4350320	if (it == visited.end())
165		{
166	2300416	PfRule r = cur->getRule();
167	2300416	if (r == PfRule::ASSUME)
168		{
169	250512	visited[cur] = true;
170	250512	caMap[cur] = true;
171	250512	foundAssumption = true;
172		}
173	2049904	else if (!foundAssumption)
174		{
175		// if we haven't found an assumption yet, recurse. Otherwise, we will
176		// not bother computing whether this subproof contains an assumption
177		// since we know its parent already contains one by another child.
178	2049904	visited[cur] = false;
179	2049904	visit.push_back(cur);
180		const std::vector<std::shared_ptr<ProofNode>>& children =
181	2049904	cur->getChildren();
182	5885830	for (const std::shared_ptr<ProofNode>& cp : children)
183		{
184	3835926	visit.push_back(cp.get());
185		}
186		}
187		}
188	2049904	else if (!it->second)
189		{
190	2049904	visited[cur] = true;
191		// we contain an assumption if we've found an assumption in a child
192	2049904	caMap[cur] = foundAssumption;
193		}
194		}
195	4600832	return caMap[cur];
196		}
197
198		bool containsAssumption(const ProofNode* pn)
199		{
200		std::unordered_map<const ProofNode*, bool> caMap;
201		return containsAssumption(pn, caMap);
202		}
203
204		bool containsSubproof(ProofNode* pn, ProofNode* pnc)
205		{
206		std::unordered_set<const ProofNode*> visited;
207		return containsSubproof(pn, pnc, visited);
208		}
209
210	208	bool containsSubproof(ProofNode* pn,
211		ProofNode* pnc,
212		std::unordered_set<const ProofNode*>& visited)
213		{
214	208	std::unordered_map<const ProofNode*, bool>::iterator it;
215	416	std::vector<const ProofNode*> visit;
216	208	visit.push_back(pn);
217		const ProofNode* cur;
218	3250	while (!visit.empty())
219		{
220	1521	cur = visit.back();
221	1521	visit.pop_back();
222	1521	if (visited.find(cur) == visited.end())
223		{
224	1390	visited.insert(cur);
225	1390	if (cur == pnc)
226		{
227		return true;
228		}
229		const std::vector<std::shared_ptr<ProofNode>>& children =
230	1390	cur->getChildren();
231	2703	for (const std::shared_ptr<ProofNode>& cp : children)
232		{
233	1313	visit.push_back(cp.get());
234		}
235		}
236		}
237	208	return false;
238		}
239
240	49738	bool isSingletonClause(TNode res,
241		const std::vector<Node>& children,
242		const std::vector<Node>& args)
243		{
244	49738	if (res.getKind() != kind::OR)
245		{
246	8714	return true;
247		}
248		size_t i;
249	82048	Node trueNode = NodeManager::currentNM()->mkConst(true);
250		// Find out the last child to introduced res, if any. We only need to
251		// look at the last one because any previous introduction would have
252		// been eliminated.
253		//
254		// After the loop finishes i is the index of the child C_i that
255		// introduced res. If i=0 none of the children introduced res as a
256		// subterm and therefore it cannot be a singleton clause.
257	916165	for (i = children.size(); i > 0; --i)
258		{
259		// only non-singleton clauses may be introducing
260		// res, so we only care about non-singleton or nodes. We check then
261		// against the kind and whether the whole or node occurs as a pivot of
262		// the respective resolution
263	875235	if (children[i - 1].getKind() != kind::OR)
264		{
265	213862	continue;
266		}
267	661373	size_t pivotIndex = (i != 1) ? 2 * (i - 1) - 1 : 1;
268	1322746	if (args[pivotIndex] == children[i - 1]
269	1322746	\|\| args[pivotIndex].notNode() == children[i - 1])
270		{
271	1003	continue;
272		}
273		// if res occurs as a subterm of a non-singleton premise
274	1981110	if (std::find(children[i - 1].begin(), children[i - 1].end(), res)
275	1981110	!= children[i - 1].end())
276		{
277	94	break;
278		}
279		}
280
281		// If res is a subterm of one of the children we still need to check if
282		// that subterm is eliminated
283	41024	if (i > 0)
284		{
285	186	bool posFirst = (i == 1) ? (args[0] == trueNode)
286	186	: (args[(2 * (i - 1)) - 2] == trueNode);
287	188	Node pivot = (i == 1) ? args[1] : args[(2 * (i - 1)) - 1];
288
289		// Check if it is eliminated by the previous resolution step
290	188	if ((res == pivot && !posFirst) \|\| (res.notNode() == pivot && posFirst)
291	282	\|\| (pivot.notNode() == res && posFirst))
292		{
293		// We decrease i by one, since it could have been the case that i
294		// was equal to children.size(), so that we return false in the end
295		--i;
296		}
297		else
298		{
299		// Otherwise check if any subsequent premise eliminates it
300	182	for (; i < children.size(); ++i)
301		{
302	53	posFirst = args[(2 * i) - 2] == trueNode;
303	53	pivot = args[(2 * i) - 1];
304		// To eliminate res, the clause must contain it with opposite
305		// polarity. There are three successful cases, according to the
306		// pivot and its sign
307		//
308		// - res is the same as the pivot and posFirst is true, which
309		// means that the clause contains its negation and eliminates it
310		//
311		// - res is the negation of the pivot and posFirst is false, so
312		// the clause contains the node whose negation is res. Note that
313		// this case may either be res.notNode() == pivot or res ==
314		// pivot.notNode().
315	115	if ((res == pivot && posFirst) \|\| (res.notNode() == pivot && !posFirst)
316	150	\|\| (pivot.notNode() == res && !posFirst))
317		{
318	9	break;
319		}
320		}
321		}
322		}
323		// if not eliminated (loop went to the end), then it's a singleton
324		// clause
325	41024	return i == children.size();
326		}
327
328		} // namespace expr
329	31137	} // namespace cvc5