Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_node_algorithm.cpp	Lines:	54	75	72.0 %
Date:	2021-08-01	Branches:	59	162	36.4 %


/******************************************************************************
 * 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-eager-checking)"
                        << 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 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;
}

}  // 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	75347	void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
24		{
25	150694	std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
26		std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
27	150694	pn->getRule(), pn->getChildren(), pn->getArguments());
28	75347	getFreeAssumptionsMap(spn, amap);
29	145103	for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
30	75347	amap)
31		{
32	145103	assump.push_back(p.first);
33		}
34	75347	}
35
36	409156	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	818312	std::unordered_map<ProofNode*, bool> visited;
43	409156	std::unordered_map<ProofNode*, bool>::iterator it;
44	818312	std::vector<std::shared_ptr<ProofNode>> visit;
45	818312	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	818312	std::unordered_map<Node, uint32_t> scopeDepth;
65	818312	std::shared_ptr<ProofNode> cur;
66	409156	visit.push_back(pn);
67	20280549	do
68		{
69	20689705	cur = visit.back();
70	20689705	visit.pop_back();
71	20689705	it = visited.find(cur.get());
72	20689705	const std::vector<Node>& cargs = cur->getArguments();
73	20689705	if (it == visited.end())
74		{
75	10735124	PfRule id = cur->getRule();
76	10735124	if (id == PfRule::ASSUME)
77		{
78	5337858	visited[cur.get()] = true;
79	5337858	Assert(cargs.size() == 1);
80	10675716	Node f = cargs[0];
81	5337858	if (!scopeDepth.count(f))
82		{
83	4602132	amap[f].push_back(cur);
84		}
85		}
86		else
87		{
88	5397266	if (id == PfRule::SCOPE)
89		{
90		// mark that its arguments are bound in the current scope
91	924441	for (const Node& a : cargs)
92		{
93	762248	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	5397266	visited[cur.get()] = false;
100	5397266	visit.push_back(cur);
101	5397266	traversing.push_back(cur);
102	5397266	const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
103	20280549	for (const std::shared_ptr<ProofNode>& cp : cs)
104		{
105	44649849	if (std::find(traversing.begin(), traversing.end(), cp)
106	44649849	!= traversing.end())
107		{
108		Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
109		"--proof-eager-checking)"
110		<< std::endl;
111		}
112	14883283	visit.push_back(cp);
113		}
114		}
115		}
116	9954581	else if (!it->second)
117		{
118	5397266	Assert(!traversing.empty());
119	5397266	traversing.pop_back();
120	5397266	visited[cur.get()] = true;
121	5397266	if (cur->getRule() == PfRule::SCOPE)
122		{
123		// unbind its assumptions
124	924441	for (const Node& a : cargs)
125		{
126	762248	auto scopeCt = scopeDepth.find(a);
127	762248	Assert(scopeCt != scopeDepth.end());
128	762248	scopeCt->second -= 1;
129	762248	if (scopeCt->second == 0)
130		{
131	696108	scopeDepth.erase(scopeCt);
132		}
133		}
134		}
135		}
136	20689705	} while (!visit.empty());
137	409156	}
138
139		bool containsSubproof(ProofNode* pn, ProofNode* pnc)
140		{
141		std::unordered_set<const ProofNode*> visited;
142		return containsSubproof(pn, pnc, visited);
143		}
144
145		bool containsSubproof(ProofNode* pn,
146		ProofNode* pnc,
147		std::unordered_set<const ProofNode*>& visited)
148		{
149		std::unordered_map<const ProofNode*, bool>::iterator it;
150		std::vector<const ProofNode*> visit;
151		visit.push_back(pn);
152		const ProofNode* cur;
153		while (!visit.empty())
154		{
155		cur = visit.back();
156		visit.pop_back();
157		if (visited.find(cur) == visited.end())
158		{
159		visited.insert(cur);
160		if (cur == pnc)
161		{
162		return true;
163		}
164		const std::vector<std::shared_ptr<ProofNode>>& children =
165		cur->getChildren();
166		for (const std::shared_ptr<ProofNode>& cp : children)
167		{
168		visit.push_back(cp.get());
169		}
170		}
171		}
172		return false;
173		}
174
175		} // namespace expr
176	29280	} // namespace cvc5