Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/proof_node_to_sexpr.cpp	Lines:	63	79	79.7 %
Date:	2021-05-24	Branches:	97	288	33.7 %


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

#include "expr/proof_node_to_sexpr.h"

#include <iostream>
#include <sstream>

#include "expr/proof_node.h"
#include "options/proof_options.h"

using namespace cvc5::kind;

namespace cvc5 {

ProofNodeToSExpr::ProofNodeToSExpr()
{
  NodeManager* nm = NodeManager::currentNM();
  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
  d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
}

Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
{
  NodeManager* nm = NodeManager::currentNM();
  std::map<const ProofNode*, Node>::iterator it;
  std::vector<const ProofNode*> visit;
  std::vector<const ProofNode*> traversing;
  const ProofNode* cur;
  visit.push_back(pn);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = d_pnMap.find(cur);

    if (it == d_pnMap.end())
    {
      d_pnMap[cur] = Node::null();
      traversing.push_back(cur);
      visit.push_back(cur);
      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
      for (const std::shared_ptr<ProofNode>& cp : pc)
      {
        if (std::find(traversing.begin(), traversing.end(), cp.get())
            != traversing.end())
        {
          Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
                         "--proof-eager-checking)"
                      << std::endl;
          return Node::null();
        }
        visit.push_back(cp.get());
      }
    }
    else if (it->second.isNull())
    {
      Assert(!traversing.empty());
      traversing.pop_back();
      std::vector<Node> children;
      // add proof rule
      children.push_back(getOrMkPfRuleVariable(cur->getRule()));
      if (options::proofPrintConclusion())
      {
        children.push_back(d_conclusionMarker);
        children.push_back(cur->getResult());
      }
      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
      for (const std::shared_ptr<ProofNode>& cp : pc)
      {
        it = d_pnMap.find(cp.get());
        Assert(it != d_pnMap.end());
        Assert(!it->second.isNull());
        children.push_back(it->second);
      }
      // add arguments
      const std::vector<Node>& args = cur->getArguments();
      if (!args.empty())
      {
        children.push_back(d_argsMarker);
        // needed to ensure builtin operators are not treated as operators
        // this can be the case for CONG where d_args may contain a builtin
        // operator
        std::vector<Node> argsSafe;
        for (const Node& a : args)
        {
          Node av = a;
          if (a.getNumChildren() == 0
              && NodeManager::operatorToKind(a) != UNDEFINED_KIND)
          {
            av = getOrMkNodeVariable(a);
          }
          argsSafe.push_back(av);
        }
        Node argsC = nm->mkNode(SEXPR, argsSafe);
        children.push_back(argsC);
      }
      d_pnMap[cur] = nm->mkNode(SEXPR, children);
    }
  } while (!visit.empty());
  Assert(d_pnMap.find(pn) != d_pnMap.end());
  Assert(!d_pnMap.find(pn)->second.isNull());
  return d_pnMap[pn];
}

Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
{
  std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
  if (it != d_pfrMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << r;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_pfrMap[r] = var;
  return var;
}

Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
{
  std::map<Node, Node>::iterator it = d_nodeMap.find(n);
  if (it != d_nodeMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << n;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_nodeMap[n] = var;
  return var;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, 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 proof node to s-expression.
14		*/
15
16		#include "expr/proof_node_to_sexpr.h"
17
18		#include <iostream>
19		#include <sstream>
20
21		#include "expr/proof_node.h"
22		#include "options/proof_options.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27
28	32818	ProofNodeToSExpr::ProofNodeToSExpr()
29		{
30	32818	NodeManager* nm = NodeManager::currentNM();
31	32818	d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
32	32818	d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
33	32818	}
34
35	32818	Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
36		{
37	32818	NodeManager* nm = NodeManager::currentNM();
38	32818	std::map<const ProofNode*, Node>::iterator it;
39	65636	std::vector<const ProofNode*> visit;
40	65636	std::vector<const ProofNode*> traversing;
41		const ProofNode* cur;
42	32818	visit.push_back(pn);
43	384344	do
44		{
45	417162	cur = visit.back();
46	417162	visit.pop_back();
47	417162	it = d_pnMap.find(cur);
48
49	417162	if (it == d_pnMap.end())
50		{
51	208579	d_pnMap[cur] = Node::null();
52	208579	traversing.push_back(cur);
53	208579	visit.push_back(cur);
54	208579	const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
55	384344	for (const std::shared_ptr<ProofNode>& cp : pc)
56		{
57	527295	if (std::find(traversing.begin(), traversing.end(), cp.get())
58	527295	!= traversing.end())
59		{
60		Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
61		"--proof-eager-checking)"
62		<< std::endl;
63		return Node::null();
64		}
65	175765	visit.push_back(cp.get());
66		}
67		}
68	208583	else if (it->second.isNull())
69		{
70	208579	Assert(!traversing.empty());
71	208579	traversing.pop_back();
72	417158	std::vector<Node> children;
73		// add proof rule
74	208579	children.push_back(getOrMkPfRuleVariable(cur->getRule()));
75	417158	if (options::proofPrintConclusion())
76		{
77		children.push_back(d_conclusionMarker);
78		children.push_back(cur->getResult());
79		}
80	208579	const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
81	384344	for (const std::shared_ptr<ProofNode>& cp : pc)
82		{
83	175765	it = d_pnMap.find(cp.get());
84	175765	Assert(it != d_pnMap.end());
85	175765	Assert(!it->second.isNull());
86	175765	children.push_back(it->second);
87		}
88		// add arguments
89	208579	const std::vector<Node>& args = cur->getArguments();
90	208579	if (!args.empty())
91		{
92	191700	children.push_back(d_argsMarker);
93		// needed to ensure builtin operators are not treated as operators
94		// this can be the case for CONG where d_args may contain a builtin
95		// operator
96	383400	std::vector<Node> argsSafe;
97	416260	for (const Node& a : args)
98		{
99	449120	Node av = a;
100	449120	if (a.getNumChildren() == 0
101	449120	&& NodeManager::operatorToKind(a) != UNDEFINED_KIND)
102		{
103		av = getOrMkNodeVariable(a);
104		}
105	224560	argsSafe.push_back(av);
106		}
107	383400	Node argsC = nm->mkNode(SEXPR, argsSafe);
108	191700	children.push_back(argsC);
109		}
110	208579	d_pnMap[cur] = nm->mkNode(SEXPR, children);
111		}
112	417162	} while (!visit.empty());
113	32818	Assert(d_pnMap.find(pn) != d_pnMap.end());
114	32818	Assert(!d_pnMap.find(pn)->second.isNull());
115	32818	return d_pnMap[pn];
116		}
117
118	208579	Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
119		{
120	208579	std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
121	208579	if (it != d_pfrMap.end())
122		{
123	60121	return it->second;
124		}
125	296916	std::stringstream ss;
126	148458	ss << r;
127	148458	NodeManager* nm = NodeManager::currentNM();
128	296916	Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
129	148458	d_pfrMap[r] = var;
130	148458	return var;
131		}
132
133		Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
134		{
135		std::map<Node, Node>::iterator it = d_nodeMap.find(n);
136		if (it != d_nodeMap.end())
137		{
138		return it->second;
139		}
140		std::stringstream ss;
141		ss << n;
142		NodeManager* nm = NodeManager::currentNM();
143		Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
144		d_nodeMap[n] = var;
145		return var;
146		}
147
148	236770	} // namespace cvc5