Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_node_to_sexpr.cpp	Lines:	119	172	69.2 %
Date:	2021-08-06	Branches:	156	606	25.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 "proof/proof_node_to_sexpr.h"

#include <iostream>
#include <sstream>

#include "options/proof_options.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
#include "theory/builtin/proof_checker.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
      PfRule r = cur->getRule();
      children.push_back(getOrMkPfRuleVariable(r));
      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> argsPrint;
        for (size_t i = 0, nargs = args.size(); i < nargs; i++)
        {
          ArgFormat f = getArgumentFormat(cur, i);
          Node av = getArgument(args[i], f);
          argsPrint.push_back(av);
        }
        Node argsC = nm->mkNode(SEXPR, argsPrint);
        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::getOrMkKindVariable(TNode n)
{
  Kind k;
  if (!ProofRuleChecker::getKind(n, k))
  {
    // just use self if we failed to get the node, throw a debug failure
    Assert(false) << "Expected kind node, got " << n;
    return n;
  }
  std::map<Kind, Node>::iterator it = d_kindMap.find(k);
  if (it != d_kindMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << k;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_kindMap[k] = var;
  return var;
}

Node ProofNodeToSExpr::getOrMkTheoryIdVariable(TNode n)
{
  theory::TheoryId tid;
  if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(n, tid))
  {
    // just use self if we failed to get the node, throw a debug failure
    Assert(false) << "Expected theory id node, got " << n;
    return n;
  }
  std::map<theory::TheoryId, Node>::iterator it = d_tidMap.find(tid);
  if (it != d_tidMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << tid;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_tidMap[tid] = var;
  return var;
}

Node ProofNodeToSExpr::getOrMkMethodIdVariable(TNode n)
{
  MethodId mid;
  if (!getMethodId(n, mid))
  {
    // just use self if we failed to get the node, throw a debug failure
    Assert(false) << "Expected method id node, got " << n;
    return n;
  }
  std::map<MethodId, Node>::iterator it = d_midMap.find(mid);
  if (it != d_midMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << mid;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_midMap[mid] = var;
  return var;
}
Node ProofNodeToSExpr::getOrMkInferenceIdVariable(TNode n)
{
  theory::InferenceId iid;
  if (!theory::getInferenceId(n, iid))
  {
    // just use self if we failed to get the node, throw a debug failure
    Assert(false) << "Expected inference id node, got " << n;
    return n;
  }
  std::map<theory::InferenceId, Node>::iterator it = d_iidMap.find(iid);
  if (it != d_iidMap.end())
  {
    return it->second;
  }
  std::stringstream ss;
  ss << iid;
  NodeManager* nm = NodeManager::currentNM();
  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
  d_iidMap[iid] = var;
  return var;
}

Node ProofNodeToSExpr::getOrMkNodeVariable(TNode n)
{
  std::map<TNode, 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;
}

Node ProofNodeToSExpr::getArgument(Node arg, ArgFormat f)
{
  switch (f)
  {
    case ArgFormat::KIND: return getOrMkKindVariable(arg);
    case ArgFormat::THEORY_ID: return getOrMkTheoryIdVariable(arg);
    case ArgFormat::METHOD_ID: return getOrMkMethodIdVariable(arg);
    case ArgFormat::INFERENCE_ID: return getOrMkInferenceIdVariable(arg);
    case ArgFormat::NODE_VAR: return getOrMkNodeVariable(arg);
    default: return arg;
  }
}

ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
    const ProofNode* pn, size_t i)
{
  PfRule r = pn->getRule();
  switch (r)
  {
    case PfRule::CONG:
    {
      if (i == 0)
      {
        return ArgFormat::KIND;
      }
      const std::vector<Node>& args = pn->getArguments();
      Assert(i < args.size());
      if (args[i].getNumChildren() == 0
          && NodeManager::operatorToKind(args[i]) != UNDEFINED_KIND)
      {
        return ArgFormat::NODE_VAR;
      }
    }
    break;
    case PfRule::SUBS:
    case PfRule::REWRITE:
    case PfRule::MACRO_SR_EQ_INTRO:
    case PfRule::MACRO_SR_PRED_INTRO:
    case PfRule::MACRO_SR_PRED_TRANSFORM:
      if (i > 0)
      {
        return ArgFormat::METHOD_ID;
      }
      break;
    case PfRule::MACRO_SR_PRED_ELIM: return ArgFormat::METHOD_ID; break;
    case PfRule::THEORY_LEMMA:
    case PfRule::THEORY_REWRITE:
      if (i == 1)
      {
        return ArgFormat::THEORY_ID;
      }
      else if (r == PfRule::THEORY_REWRITE && i == 2)
      {
        return ArgFormat::METHOD_ID;
      }
      break;
    case PfRule::INSTANTIATE:
    {
      Assert(!pn->getChildren().empty());
      Node q = pn->getChildren()[0]->getResult();
      Assert(q.getKind() == kind::FORALL);
      if (i == q[0].getNumChildren())
      {
        return ArgFormat::INFERENCE_ID;
      }
    }
    break;
    default: break;
  }
  return ArgFormat::DEFAULT;
}

}  // 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 "proof/proof_node_to_sexpr.h"
17
18		#include <iostream>
19		#include <sstream>
20
21		#include "options/proof_options.h"
22		#include "proof/proof_checker.h"
23		#include "proof/proof_node.h"
24		#include "theory/builtin/proof_checker.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29
30	37859	ProofNodeToSExpr::ProofNodeToSExpr()
31		{
32	37859	NodeManager* nm = NodeManager::currentNM();
33	37859	d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
34	37859	d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
35	37859	}
36
37	37859	Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
38		{
39	37859	NodeManager* nm = NodeManager::currentNM();
40	37859	std::map<const ProofNode*, Node>::iterator it;
41	75718	std::vector<const ProofNode*> visit;
42	75718	std::vector<const ProofNode*> traversing;
43		const ProofNode* cur;
44	37859	visit.push_back(pn);
45	445887	do
46		{
47	483746	cur = visit.back();
48	483746	visit.pop_back();
49	483746	it = d_pnMap.find(cur);
50
51	483746	if (it == d_pnMap.end())
52		{
53	241849	d_pnMap[cur] = Node::null();
54	241849	traversing.push_back(cur);
55	241849	visit.push_back(cur);
56	241849	const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
57	445887	for (const std::shared_ptr<ProofNode>& cp : pc)
58		{
59	612114	if (std::find(traversing.begin(), traversing.end(), cp.get())
60	612114	!= traversing.end())
61		{
62		Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
63		"--proof-eager-checking)"
64		<< std::endl;
65		return Node::null();
66		}
67	204038	visit.push_back(cp.get());
68		}
69		}
70	241897	else if (it->second.isNull())
71		{
72	241849	Assert(!traversing.empty());
73	241849	traversing.pop_back();
74	483698	std::vector<Node> children;
75		// add proof rule
76	241849	PfRule r = cur->getRule();
77	241849	children.push_back(getOrMkPfRuleVariable(r));
78	483698	if (options::proofPrintConclusion())
79		{
80		children.push_back(d_conclusionMarker);
81		children.push_back(cur->getResult());
82		}
83	241849	const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
84	445887	for (const std::shared_ptr<ProofNode>& cp : pc)
85		{
86	204038	it = d_pnMap.find(cp.get());
87	204038	Assert(it != d_pnMap.end());
88	204038	Assert(!it->second.isNull());
89	204038	children.push_back(it->second);
90		}
91		// add arguments
92	241849	const std::vector<Node>& args = cur->getArguments();
93	241849	if (!args.empty())
94		{
95	222439	children.push_back(d_argsMarker);
96		// needed to ensure builtin operators are not treated as operators
97		// this can be the case for CONG where d_args may contain a builtin
98		// operator
99	444878	std::vector<Node> argsPrint;
100	483060	for (size_t i = 0, nargs = args.size(); i < nargs; i++)
101		{
102	260621	ArgFormat f = getArgumentFormat(cur, i);
103	521242	Node av = getArgument(args[i], f);
104	260621	argsPrint.push_back(av);
105		}
106	444878	Node argsC = nm->mkNode(SEXPR, argsPrint);
107	222439	children.push_back(argsC);
108		}
109	241849	d_pnMap[cur] = nm->mkNode(SEXPR, children);
110		}
111	483746	} while (!visit.empty());
112	37859	Assert(d_pnMap.find(pn) != d_pnMap.end());
113	37859	Assert(!d_pnMap.find(pn)->second.isNull());
114	37859	return d_pnMap[pn];
115		}
116
117	241849	Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
118		{
119	241849	std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
120	241849	if (it != d_pfrMap.end())
121		{
122	70783	return it->second;
123		}
124	342132	std::stringstream ss;
125	171066	ss << r;
126	171066	NodeManager* nm = NodeManager::currentNM();
127	342132	Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
128	171066	d_pfrMap[r] = var;
129	171066	return var;
130		}
131	61	Node ProofNodeToSExpr::getOrMkKindVariable(TNode n)
132		{
133		Kind k;
134	61	if (!ProofRuleChecker::getKind(n, k))
135		{
136		// just use self if we failed to get the node, throw a debug failure
137		Assert(false) << "Expected kind node, got " << n;
138		return n;
139		}
140	61	std::map<Kind, Node>::iterator it = d_kindMap.find(k);
141	61	if (it != d_kindMap.end())
142		{
143	20	return it->second;
144		}
145	82	std::stringstream ss;
146	41	ss << k;
147	41	NodeManager* nm = NodeManager::currentNM();
148	82	Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
149	41	d_kindMap[k] = var;
150	41	return var;
151		}
152
153	109	Node ProofNodeToSExpr::getOrMkTheoryIdVariable(TNode n)
154		{
155		theory::TheoryId tid;
156	109	if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(n, tid))
157		{
158		// just use self if we failed to get the node, throw a debug failure
159		Assert(false) << "Expected theory id node, got " << n;
160		return n;
161		}
162	109	std::map<theory::TheoryId, Node>::iterator it = d_tidMap.find(tid);
163	109	if (it != d_tidMap.end())
164		{
165	100	return it->second;
166		}
167	18	std::stringstream ss;
168	9	ss << tid;
169	9	NodeManager* nm = NodeManager::currentNM();
170	18	Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
171	9	d_tidMap[tid] = var;
172	9	return var;
173		}
174
175	109	Node ProofNodeToSExpr::getOrMkMethodIdVariable(TNode n)
176		{
177		MethodId mid;
178	109	if (!getMethodId(n, mid))
179		{
180		// just use self if we failed to get the node, throw a debug failure
181		Assert(false) << "Expected method id node, got " << n;
182		return n;
183		}
184	109	std::map<MethodId, Node>::iterator it = d_midMap.find(mid);
185	109	if (it != d_midMap.end())
186		{
187	99	return it->second;
188		}
189	20	std::stringstream ss;
190	10	ss << mid;
191	10	NodeManager* nm = NodeManager::currentNM();
192	20	Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
193	10	d_midMap[mid] = var;
194	10	return var;
195		}
196		Node ProofNodeToSExpr::getOrMkInferenceIdVariable(TNode n)
197		{
198		theory::InferenceId iid;
199		if (!theory::getInferenceId(n, iid))
200		{
201		// just use self if we failed to get the node, throw a debug failure
202		Assert(false) << "Expected inference id node, got " << n;
203		return n;
204		}
205		std::map<theory::InferenceId, Node>::iterator it = d_iidMap.find(iid);
206		if (it != d_iidMap.end())
207		{
208		return it->second;
209		}
210		std::stringstream ss;
211		ss << iid;
212		NodeManager* nm = NodeManager::currentNM();
213		Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
214		d_iidMap[iid] = var;
215		return var;
216		}
217
218		Node ProofNodeToSExpr::getOrMkNodeVariable(TNode n)
219		{
220		std::map<TNode, Node>::iterator it = d_nodeMap.find(n);
221		if (it != d_nodeMap.end())
222		{
223		return it->second;
224		}
225		std::stringstream ss;
226		ss << n;
227		NodeManager* nm = NodeManager::currentNM();
228		Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
229		d_nodeMap[n] = var;
230		return var;
231		}
232
233	260621	Node ProofNodeToSExpr::getArgument(Node arg, ArgFormat f)
234		{
235	260621	switch (f)
236		{
237	61	case ArgFormat::KIND: return getOrMkKindVariable(arg);
238	109	case ArgFormat::THEORY_ID: return getOrMkTheoryIdVariable(arg);
239	109	case ArgFormat::METHOD_ID: return getOrMkMethodIdVariable(arg);
240		case ArgFormat::INFERENCE_ID: return getOrMkInferenceIdVariable(arg);
241		case ArgFormat::NODE_VAR: return getOrMkNodeVariable(arg);
242	260342	default: return arg;
243		}
244		}
245
246	260621	ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
247		const ProofNode* pn, size_t i)
248		{
249	260621	PfRule r = pn->getRule();
250	260621	switch (r)
251		{
252	61	case PfRule::CONG:
253		{
254	61	if (i == 0)
255		{
256	61	return ArgFormat::KIND;
257		}
258		const std::vector<Node>& args = pn->getArguments();
259		Assert(i < args.size());
260		if (args[i].getNumChildren() == 0
261		&& NodeManager::operatorToKind(args[i]) != UNDEFINED_KIND)
262		{
263		return ArgFormat::NODE_VAR;
264		}
265		}
266		break;
267	65628	case PfRule::SUBS:
268		case PfRule::REWRITE:
269		case PfRule::MACRO_SR_EQ_INTRO:
270		case PfRule::MACRO_SR_PRED_INTRO:
271		case PfRule::MACRO_SR_PRED_TRANSFORM:
272	65628	if (i > 0)
273		{
274		return ArgFormat::METHOD_ID;
275		}
276	65628	break;
277		case PfRule::MACRO_SR_PRED_ELIM: return ArgFormat::METHOD_ID; break;
278	327	case PfRule::THEORY_LEMMA:
279		case PfRule::THEORY_REWRITE:
280	327	if (i == 1)
281		{
282	109	return ArgFormat::THEORY_ID;
283		}
284	218	else if (r == PfRule::THEORY_REWRITE && i == 2)
285		{
286	109	return ArgFormat::METHOD_ID;
287		}
288	109	break;
289		case PfRule::INSTANTIATE:
290		{
291		Assert(!pn->getChildren().empty());
292		Node q = pn->getChildren()[0]->getResult();
293		Assert(q.getKind() == kind::FORALL);
294		if (i == q[0].getNumChildren())
295		{
296		return ArgFormat::INFERENCE_ID;
297		}
298		}
299		break;
300	194605	default: break;
301		}
302	260342	return ArgFormat::DEFAULT;
303		}
304
305	271171	} // namespace cvc5