Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/expand_definitions.cpp	Lines:	67	68	98.5 %
Date:	2021-11-07	Branches:	126	268	47.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, 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 expand definitions for an SMT engine.
 */

#include "smt/expand_definitions.h"

#include <stack>
#include <utility>

#include "expr/node_manager_attributes.h"
#include "preprocessing/assertion_pipeline.h"
#include "proof/conv_proof_generator.h"
#include "smt/env.h"
#include "smt/solver_engine.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "util/resource_manager.h"

using namespace cvc5::preprocessing;
using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

ExpandDefs::ExpandDefs(Env& env) : d_env(env), d_tpg(nullptr) {}

ExpandDefs::~ExpandDefs() {}

Node ExpandDefs::expandDefinitions(TNode n,
                                   std::unordered_map<Node, Node>& cache)
{
  TrustNode trn = expandDefinitions(n, cache, nullptr);
  return trn.isNull() ? Node(n) : trn.getNode();
}

TrustNode ExpandDefs::expandDefinitions(TNode n,
                                        std::unordered_map<Node, Node>& cache,
                                        TConvProofGenerator* tpg)
{
  const TNode orig = n;
  std::stack<std::tuple<Node, Node, bool>> worklist;
  std::stack<Node> result;
  worklist.push(std::make_tuple(Node(n), Node(n), false));
  // The worklist is made of triples, each is input / original node then the
  // output / rewritten node and finally a flag tracking whether the children
  // have been explored (i.e. if this is a downward or upward pass).

  ResourceManager* rm = d_env.getResourceManager();
  Rewriter* rr = d_env.getRewriter();
  do
  {
    rm->spendResource(Resource::PreprocessStep);

    // n is the input / original
    // node is the output / result
    Node node;
    bool childrenPushed;
    std::tie(n, node, childrenPushed) = worklist.top();
    worklist.pop();

    // Working downwards
    if (!childrenPushed)
    {
      // we can short circuit (variable) leaves
      if (n.isVar())
      {
        // don't bother putting in the cache
        result.push(n);
        continue;
      }

      // maybe it's in the cache
      std::unordered_map<Node, Node>::iterator cacheHit = cache.find(n);
      if (cacheHit != cache.end())
      {
        TNode ret = (*cacheHit).second;
        result.push(ret.isNull() ? n : ret);
        continue;
      }
      theory::TheoryId tid = theory::Theory::theoryOf(node);
      theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);

      Assert(tr != NULL);
      TrustNode trn = tr->expandDefinition(n);
      if (!trn.isNull())
      {
        node = trn.getNode();
        if (tpg != nullptr)
        {
          tpg->addRewriteStep(
              n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF);
        }
      }
      else
      {
        node = n;
      }
      // the partial functions can fall through, in which case we still
      // consider their children
      worklist.push(std::make_tuple(
          Node(n), node, true));  // Original and rewritten result

      for (size_t i = 0; i < node.getNumChildren(); ++i)
      {
        worklist.push(
            std::make_tuple(node[i],
                            node[i],
                            false));  // Rewrite the children of the result only
      }
    }
    else
    {
      // Working upwards
      // Reconstruct the node from it's (now rewritten) children on the stack

      Debug("expand") << "cons : " << node << std::endl;
      if (node.getNumChildren() > 0)
      {
        // cout << "cons : " << node << std::endl;
        NodeBuilder nb(node.getKind());
        if (node.getMetaKind() == metakind::PARAMETERIZED)
        {
          Debug("expand") << "op   : " << node.getOperator() << std::endl;
          // cout << "op   : " << node.getOperator() << std::endl;
          nb << node.getOperator();
        }
        for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
        {
          Assert(!result.empty());
          Node expanded = result.top();
          result.pop();
          // cout << "exchld : " << expanded << std::endl;
          Debug("expand") << "exchld : " << expanded << std::endl;
          nb << expanded;
        }
        node = nb;
      }
      // Only cache once all subterms are expanded
      cache[n] = n == node ? Node::null() : node;
      result.push(node);
    }
  } while (!worklist.empty());

  AlwaysAssert(result.size() == 1);

  Node res = result.top();

  if (res == orig)
  {
    return TrustNode::null();
  }
  return TrustNode::mkTrustRewrite(orig, res, tpg);
}

void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
{
  if (d_tpg == nullptr)
  {
    d_tpg.reset(new TConvProofGenerator(pnm,
                                        d_env.getUserContext(),
                                        TConvPolicy::FIXPOINT,
                                        TConvCachePolicy::NEVER,
                                        "ExpandDefs::TConvProofGenerator",
                                        nullptr,
                                        true));
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, 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 expand definitions for an SMT engine.
14		*/
15
16		#include "smt/expand_definitions.h"
17
18		#include <stack>
19		#include <utility>
20
21		#include "expr/node_manager_attributes.h"
22		#include "preprocessing/assertion_pipeline.h"
23		#include "proof/conv_proof_generator.h"
24		#include "smt/env.h"
25		#include "smt/solver_engine.h"
26		#include "theory/rewriter.h"
27		#include "theory/theory.h"
28		#include "util/resource_manager.h"
29
30		using namespace cvc5::preprocessing;
31		using namespace cvc5::theory;
32		using namespace cvc5::kind;
33
34		namespace cvc5 {
35		namespace smt {
36
37	18633	ExpandDefs::ExpandDefs(Env& env) : d_env(env), d_tpg(nullptr) {}
38
39	15884	ExpandDefs::~ExpandDefs() {}
40
41	12607	Node ExpandDefs::expandDefinitions(TNode n,
42		std::unordered_map<Node, Node>& cache)
43		{
44	25214	TrustNode trn = expandDefinitions(n, cache, nullptr);
45	25214	return trn.isNull() ? Node(n) : trn.getNode();
46		}
47
48	12607	TrustNode ExpandDefs::expandDefinitions(TNode n,
49		std::unordered_map<Node, Node>& cache,
50		TConvProofGenerator* tpg)
51		{
52	25214	const TNode orig = n;
53	25214	std::stack<std::tuple<Node, Node, bool>> worklist;
54	25214	std::stack<Node> result;
55	12607	worklist.push(std::make_tuple(Node(n), Node(n), false));
56		// The worklist is made of triples, each is input / original node then the
57		// output / rewritten node and finally a flag tracking whether the children
58		// have been explored (i.e. if this is a downward or upward pass).
59
60	12607	ResourceManager* rm = d_env.getResourceManager();
61	12607	Rewriter* rr = d_env.getRewriter();
62	55731	do
63		{
64	68338	rm->spendResource(Resource::PreprocessStep);
65
66		// n is the input / original
67		// node is the output / result
68	108856	Node node;
69		bool childrenPushed;
70	68338	std::tie(n, node, childrenPushed) = worklist.top();
71	68338	worklist.pop();
72
73		// Working downwards
74	68338	if (!childrenPushed)
75		{
76		// we can short circuit (variable) leaves
77	71593	if (n.isVar())
78		{
79		// don't bother putting in the cache
80	23514	result.push(n);
81	51334	continue;
82		}
83
84		// maybe it's in the cache
85	24565	std::unordered_map<Node, Node>::iterator cacheHit = cache.find(n);
86	24565	if (cacheHit != cache.end())
87		{
88	8612	TNode ret = (*cacheHit).second;
89	4306	result.push(ret.isNull() ? n : ret);
90	4306	continue;
91		}
92	20259	theory::TheoryId tid = theory::Theory::theoryOf(node);
93	20259	theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
94
95	20259	Assert(tr != NULL);
96	40518	TrustNode trn = tr->expandDefinition(n);
97	20259	if (!trn.isNull())
98		{
99	194	node = trn.getNode();
100	194	if (tpg != nullptr)
101		{
102		tpg->addRewriteStep(
103		n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF);
104		}
105		}
106		else
107		{
108	20065	node = n;
109		}
110		// the partial functions can fall through, in which case we still
111		// consider their children
112	60777	worklist.push(std::make_tuple(
113	40518	Node(n), node, true)); // Original and rewritten result
114
115	55731	for (size_t i = 0; i < node.getNumChildren(); ++i)
116		{
117	35472	worklist.push(
118	70944	std::make_tuple(node[i],
119		node[i],
120		false)); // Rewrite the children of the result only
121		}
122		}
123		else
124		{
125		// Working upwards
126		// Reconstruct the node from it's (now rewritten) children on the stack
127
128	20259	Debug("expand") << "cons : " << node << std::endl;
129	20259	if (node.getNumChildren() > 0)
130		{
131		// cout << "cons : " << node << std::endl;
132	33432	NodeBuilder nb(node.getKind());
133	16716	if (node.getMetaKind() == metakind::PARAMETERIZED)
134		{
135	1927	Debug("expand") << "op : " << node.getOperator() << std::endl;
136		// cout << "op : " << node.getOperator() << std::endl;
137	1927	nb << node.getOperator();
138		}
139	52188	for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
140		{
141	35472	Assert(!result.empty());
142	70944	Node expanded = result.top();
143	35472	result.pop();
144		// cout << "exchld : " << expanded << std::endl;
145	35472	Debug("expand") << "exchld : " << expanded << std::endl;
146	35472	nb << expanded;
147		}
148	16716	node = nb;
149		}
150		// Only cache once all subterms are expanded
151	20259	cache[n] = n == node ? Node::null() : node;
152	20259	result.push(node);
153		}
154	68338	} while (!worklist.empty());
155
156	12607	AlwaysAssert(result.size() == 1);
157
158	25214	Node res = result.top();
159
160	12607	if (res == orig)
161		{
162	12474	return TrustNode::null();
163		}
164	133	return TrustNode::mkTrustRewrite(orig, res, tpg);
165		}
166
167	7989	void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
168		{
169	7989	if (d_tpg == nullptr)
170		{
171	23967	d_tpg.reset(new TConvProofGenerator(pnm,
172	7989	d_env.getUserContext(),
173		TConvPolicy::FIXPOINT,
174		TConvCachePolicy::NEVER,
175		"ExpandDefs::TConvProofGenerator",
176		nullptr,
177	7989	true));
178		}
179	7989	}
180
181		} // namespace smt
182	31137	} // namespace cvc5