Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/assertion_pipeline.cpp	Lines:	86	86	100.0 %
Date:	2021-08-16	Branches:	135	348	38.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, 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.
 * ****************************************************************************
 *
 * AssertionPipeline stores a list of assertions modified by
 * preprocessing passes.
 */

#include "preprocessing/assertion_pipeline.h"

#include "expr/node_manager.h"
#include "options/smt_options.h"
#include "proof/lazy_proof.h"
#include "smt/preprocess_proof_generator.h"
#include "theory/builtin/proof_checker.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace preprocessing {

AssertionPipeline::AssertionPipeline()
    : d_realAssertionsEnd(0),
      d_storeSubstsInAsserts(false),
      d_substsIndex(0),
      d_assumptionsStart(0),
      d_numAssumptions(0),
      d_pppg(nullptr)
{
}

void AssertionPipeline::clear()
{
  d_nodes.clear();
  d_realAssertionsEnd = 0;
  d_assumptionsStart = 0;
  d_numAssumptions = 0;
}

void AssertionPipeline::push_back(Node n,
                                  bool isAssumption,
                                  bool isInput,
                                  ProofGenerator* pgen)
{
  d_nodes.push_back(n);
  if (isAssumption)
  {
    Assert(pgen == nullptr);
    if (d_numAssumptions == 0)
    {
      d_assumptionsStart = d_nodes.size() - 1;
    }
    // Currently, we assume that assumptions are all added one after another
    // and that we store them in the same vector as the assertions. Once we
    // split the assertions up into multiple vectors (see issue #2473), we will
    // not have this limitation anymore.
    Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
    d_numAssumptions++;
  }
  Trace("assert-pipeline") << "Assertions: ...new assertion " << n
                           << ", isInput=" << isInput << std::endl;
  if (isProofEnabled())
  {
    if (!isInput)
    {
      // notice this is always called, regardless of whether pgen is nullptr
      d_pppg->notifyNewAssert(n, pgen);
    }
    else
    {
      Assert(pgen == nullptr);
      // n is an input assertion, whose proof should be ASSUME.
      d_pppg->notifyInput(n);
    }
  }
}

void AssertionPipeline::pushBackTrusted(TrustNode trn)
{
  Assert(trn.getKind() == TrustNodeKind::LEMMA);
  // push back what was proven
  push_back(trn.getProven(), false, false, trn.getGenerator());
}

void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
{
  if (n == d_nodes[i])
  {
    // no change, skip
    return;
  }
  Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
                           << n << std::endl;
  if (isProofEnabled())
  {
    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
  }
  d_nodes[i] = n;
}

void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
{
  if (trn.isNull())
  {
    // null trust node denotes no change, nothing to do
    return;
  }
  Assert(trn.getKind() == TrustNodeKind::REWRITE);
  Assert(trn.getProven()[0] == d_nodes[i]);
  replace(i, trn.getNode(), trn.getGenerator());
}

void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
{
  d_pppg = pppg;
}

bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }

void AssertionPipeline::enableStoreSubstsInAsserts()
{
  d_storeSubstsInAsserts = true;
  d_substsIndex = d_nodes.size();
  d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
}

void AssertionPipeline::disableStoreSubstsInAsserts()
{
  d_storeSubstsInAsserts = false;
}

void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
{
  Assert(d_storeSubstsInAsserts);
  Assert(n.getKind() == kind::EQUAL);
  conjoin(d_substsIndex, n, pg);
}

void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
{
  NodeManager* nm = NodeManager::currentNM();
  Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
  Node newConjr = theory::Rewriter::rewrite(newConj);
  Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
                           << d_nodes[i] << std::endl;
  Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
                                 << ", got " << newConjr << std::endl;
  if (newConjr == d_nodes[i])
  {
    // trivial, skip
    return;
  }
  if (isProofEnabled())
  {
    if (newConjr == n)
    {
      // don't care about the previous proof and can simply plug in the
      // proof from pg if the resulting assertion is the same as n.
      d_pppg->notifyNewAssert(newConjr, pg);
    }
    else
    {
      // ---------- from pppg   --------- from pg
      // d_nodes[i]                n
      // -------------------------------- AND_INTRO
      //      d_nodes[i] ^ n
      // -------------------------------- MACRO_SR_PRED_TRANSFORM
      //   rewrite( d_nodes[i] ^ n )
      // allocate a fresh proof which will act as the proof generator
      LazyCDProof* lcp = d_pppg->allocateHelperProof();
      lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
      if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
      {
        // skip the AND_INTRO if the previous d_nodes[i] was true
        newConj = n;
      }
      else
      {
        lcp->addLazyStep(d_nodes[i], d_pppg);
        lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
      }
      if (newConjr != newConj)
      {
        lcp->addStep(
            newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
      }
      // Notice we have constructed a proof of a new assertion, where d_pppg
      // is referenced in the lazy proof above. If alternatively we had
      // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
      // have used notifyPreprocessed. However, it is simpler to make the
      // above proof.
      d_pppg->notifyNewAssert(newConjr, lcp);
    }
  }
  d_nodes[i] = newConjr;
  Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
}

}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, 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		* AssertionPipeline stores a list of assertions modified by
14		* preprocessing passes.
15		*/
16
17		#include "preprocessing/assertion_pipeline.h"
18
19		#include "expr/node_manager.h"
20		#include "options/smt_options.h"
21		#include "proof/lazy_proof.h"
22		#include "smt/preprocess_proof_generator.h"
23		#include "theory/builtin/proof_checker.h"
24		#include "theory/rewriter.h"
25
26		namespace cvc5 {
27		namespace preprocessing {
28
29	10503	AssertionPipeline::AssertionPipeline()
30		: d_realAssertionsEnd(0),
31		d_storeSubstsInAsserts(false),
32		d_substsIndex(0),
33		d_assumptionsStart(0),
34		d_numAssumptions(0),
35	10503	d_pppg(nullptr)
36		{
37	10503	}
38
39	18383	void AssertionPipeline::clear()
40		{
41	18383	d_nodes.clear();
42	18383	d_realAssertionsEnd = 0;
43	18383	d_assumptionsStart = 0;
44	18383	d_numAssumptions = 0;
45	18383	}
46
47	128709	void AssertionPipeline::push_back(Node n,
48		bool isAssumption,
49		bool isInput,
50		ProofGenerator* pgen)
51		{
52	128709	d_nodes.push_back(n);
53	128709	if (isAssumption)
54		{
55	2408	Assert(pgen == nullptr);
56	2408	if (d_numAssumptions == 0)
57		{
58	2374	d_assumptionsStart = d_nodes.size() - 1;
59		}
60		// Currently, we assume that assumptions are all added one after another
61		// and that we store them in the same vector as the assertions. Once we
62		// split the assertions up into multiple vectors (see issue #2473), we will
63		// not have this limitation anymore.
64	2408	Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
65	2408	d_numAssumptions++;
66		}
67	257418	Trace("assert-pipeline") << "Assertions: ...new assertion " << n
68	128709	<< ", isInput=" << isInput << std::endl;
69	128709	if (isProofEnabled())
70		{
71	55226	if (!isInput)
72		{
73		// notice this is always called, regardless of whether pgen is nullptr
74	17817	d_pppg->notifyNewAssert(n, pgen);
75		}
76		else
77		{
78	37409	Assert(pgen == nullptr);
79		// n is an input assertion, whose proof should be ASSUME.
80	37409	d_pppg->notifyInput(n);
81		}
82		}
83	128709	}
84
85	20547	void AssertionPipeline::pushBackTrusted(TrustNode trn)
86		{
87	20547	Assert(trn.getKind() == TrustNodeKind::LEMMA);
88		// push back what was proven
89	20547	push_back(trn.getProven(), false, false, trn.getGenerator());
90	20547	}
91
92	301370	void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
93		{
94	301370	if (n == d_nodes[i])
95		{
96		// no change, skip
97	217238	return;
98		}
99	168264	Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
100	84132	<< n << std::endl;
101	84132	if (isProofEnabled())
102		{
103	32996	d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
104		}
105	84132	d_nodes[i] = n;
106		}
107
108	245438	void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
109		{
110	245438	if (trn.isNull())
111		{
112		// null trust node denotes no change, nothing to do
113	165841	return;
114		}
115	79597	Assert(trn.getKind() == TrustNodeKind::REWRITE);
116	79597	Assert(trn.getProven()[0] == d_nodes[i]);
117	79597	replace(i, trn.getNode(), trn.getGenerator());
118		}
119
120	3768	void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
121		{
122	3768	d_pppg = pppg;
123	3768	}
124
125	216599	bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
126
127	3754	void AssertionPipeline::enableStoreSubstsInAsserts()
128		{
129	3754	d_storeSubstsInAsserts = true;
130	3754	d_substsIndex = d_nodes.size();
131	3754	d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
132	3754	}
133
134	9996	void AssertionPipeline::disableStoreSubstsInAsserts()
135		{
136	9996	d_storeSubstsInAsserts = false;
137	9996	}
138
139	1367	void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
140		{
141	1367	Assert(d_storeSubstsInAsserts);
142	1367	Assert(n.getKind() == kind::EQUAL);
143	1367	conjoin(d_substsIndex, n, pg);
144	1367	}
145
146	3857	void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
147		{
148	3857	NodeManager* nm = NodeManager::currentNM();
149	7615	Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
150	7615	Node newConjr = theory::Rewriter::rewrite(newConj);
151	7714	Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
152	3857	<< d_nodes[i] << std::endl;
153	7714	Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
154	3857	<< ", got " << newConjr << std::endl;
155	3857	if (newConjr == d_nodes[i])
156		{
157		// trivial, skip
158	99	return;
159		}
160	3758	if (isProofEnabled())
161		{
162	860	if (newConjr == n)
163		{
164		// don't care about the previous proof and can simply plug in the
165		// proof from pg if the resulting assertion is the same as n.
166	449	d_pppg->notifyNewAssert(newConjr, pg);
167		}
168		else
169		{
170		// ---------- from pppg --------- from pg
171		// d_nodes[i] n
172		// -------------------------------- AND_INTRO
173		// d_nodes[i] ^ n
174		// -------------------------------- MACRO_SR_PRED_TRANSFORM
175		// rewrite( d_nodes[i] ^ n )
176		// allocate a fresh proof which will act as the proof generator
177	411	LazyCDProof* lcp = d_pppg->allocateHelperProof();
178	411	lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
179	411	if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
180		{
181		// skip the AND_INTRO if the previous d_nodes[i] was true
182	198	newConj = n;
183		}
184		else
185		{
186	213	lcp->addLazyStep(d_nodes[i], d_pppg);
187	213	lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
188		}
189	411	if (newConjr != newConj)
190		{
191	1227	lcp->addStep(
192	818	newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
193		}
194		// Notice we have constructed a proof of a new assertion, where d_pppg
195		// is referenced in the lazy proof above. If alternatively we had
196		// constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
197		// have used notifyPreprocessed. However, it is simpler to make the
198		// above proof.
199	411	d_pppg->notifyNewAssert(newConjr, lcp);
200		}
201		}
202	3758	d_nodes[i] = newConjr;
203	3758	Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
204		}
205
206		} // namespace preprocessing
207	29340	} // namespace cvc5