Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/expand_definitions.cpp	Lines:	69	70	98.6 %
Date:	2021-09-09	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/smt_engine.h"
#include "smt/smt_engine_stats.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, SmtEngineStatistics& stats)
    : d_env(env), d_smtStats(stats), 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/smt_engine.h"
26		#include "smt/smt_engine_stats.h"
27		#include "theory/rewriter.h"
28		#include "theory/theory.h"
29		#include "util/resource_manager.h"
30
31		using namespace cvc5::preprocessing;
32		using namespace cvc5::theory;
33		using namespace cvc5::kind;
34
35		namespace cvc5 {
36		namespace smt {
37
38	13185	ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats)
39	13185	: d_env(env), d_smtStats(stats), d_tpg(nullptr)
40		{
41	13185	}
42
43	10544	ExpandDefs::~ExpandDefs() {}
44
45	4970	Node ExpandDefs::expandDefinitions(TNode n,
46		std::unordered_map<Node, Node>& cache)
47		{
48	9940	TrustNode trn = expandDefinitions(n, cache, nullptr);
49	9940	return trn.isNull() ? Node(n) : trn.getNode();
50		}
51
52	4970	TrustNode ExpandDefs::expandDefinitions(TNode n,
53		std::unordered_map<Node, Node>& cache,
54		TConvProofGenerator* tpg)
55		{
56	9940	const TNode orig = n;
57	9940	std::stack<std::tuple<Node, Node, bool>> worklist;
58	9940	std::stack<Node> result;
59	4970	worklist.push(std::make_tuple(Node(n), Node(n), false));
60		// The worklist is made of triples, each is input / original node then the
61		// output / rewritten node and finally a flag tracking whether the children
62		// have been explored (i.e. if this is a downward or upward pass).
63
64	4970	ResourceManager* rm = d_env.getResourceManager();
65	4970	Rewriter* rr = d_env.getRewriter();
66	41349	do
67		{
68	46319	rm->spendResource(Resource::PreprocessStep);
69
70		// n is the input / original
71		// node is the output / result
72	74763	Node node;
73		bool childrenPushed;
74	46319	std::tie(n, node, childrenPushed) = worklist.top();
75	46319	worklist.pop();
76
77		// Working downwards
78	46319	if (!childrenPushed)
79		{
80		// we can short circuit (variable) leaves
81	46183	if (n.isVar())
82		{
83		// don't bother putting in the cache
84	14086	result.push(n);
85	31961	continue;
86		}
87
88		// maybe it's in the cache
89	18011	std::unordered_map<Node, Node>::iterator cacheHit = cache.find(n);
90	18011	if (cacheHit != cache.end())
91		{
92	7578	TNode ret = (*cacheHit).second;
93	3789	result.push(ret.isNull() ? n : ret);
94	3789	continue;
95		}
96	14222	theory::TheoryId tid = theory::Theory::theoryOf(node);
97	14222	theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
98
99	14222	Assert(tr != NULL);
100	28444	TrustNode trn = tr->expandDefinition(n);
101	14222	if (!trn.isNull())
102		{
103	169	node = trn.getNode();
104	169	if (tpg != nullptr)
105		{
106		tpg->addRewriteStep(
107		n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF);
108		}
109		}
110		else
111		{
112	14053	node = n;
113		}
114		// the partial functions can fall through, in which case we still
115		// consider their children
116	42666	worklist.push(std::make_tuple(
117	28444	Node(n), node, true)); // Original and rewritten result
118
119	41349	for (size_t i = 0; i < node.getNumChildren(); ++i)
120		{
121	27127	worklist.push(
122	54254	std::make_tuple(node[i],
123		node[i],
124		false)); // Rewrite the children of the result only
125		}
126		}
127		else
128		{
129		// Working upwards
130		// Reconstruct the node from it's (now rewritten) children on the stack
131
132	14222	Debug("expand") << "cons : " << node << std::endl;
133	14222	if (node.getNumChildren() > 0)
134		{
135		// cout << "cons : " << node << std::endl;
136	25042	NodeBuilder nb(node.getKind());
137	12521	if (node.getMetaKind() == metakind::PARAMETERIZED)
138		{
139	1679	Debug("expand") << "op : " << node.getOperator() << std::endl;
140		// cout << "op : " << node.getOperator() << std::endl;
141	1679	nb << node.getOperator();
142		}
143	39648	for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
144		{
145	27127	Assert(!result.empty());
146	54254	Node expanded = result.top();
147	27127	result.pop();
148		// cout << "exchld : " << expanded << std::endl;
149	27127	Debug("expand") << "exchld : " << expanded << std::endl;
150	27127	nb << expanded;
151		}
152	12521	node = nb;
153		}
154		// Only cache once all subterms are expanded
155	14222	cache[n] = n == node ? Node::null() : node;
156	14222	result.push(node);
157		}
158	46319	} while (!worklist.empty());
159
160	4970	AlwaysAssert(result.size() == 1);
161
162	9940	Node res = result.top();
163
164	4970	if (res == orig)
165		{
166	4863	return TrustNode::null();
167		}
168	107	return TrustNode::mkTrustRewrite(orig, res, tpg);
169		}
170
171	3781	void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
172		{
173	3781	if (d_tpg == nullptr)
174		{
175	11343	d_tpg.reset(new TConvProofGenerator(pnm,
176	3781	d_env.getUserContext(),
177		TConvPolicy::FIXPOINT,
178		TConvCachePolicy::NEVER,
179		"ExpandDefs::TConvProofGenerator",
180		nullptr,
181	3781	true));
182		}
183	3781	}
184
185		} // namespace smt
186	29505	} // namespace cvc5