Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/assertion_pipeline.cpp	Lines:	84	86	97.7 %
Date:	2021-09-29	Branches:	123	348	35.3 %


/******************************************************************************
 * 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	9520	AssertionPipeline::AssertionPipeline()
30		: d_realAssertionsEnd(0),
31		d_storeSubstsInAsserts(false),
32		d_substsIndex(0),
33		d_assumptionsStart(0),
34		d_numAssumptions(0),
35	9520	d_pppg(nullptr)
36		{
37	9520	}
38
39	11532	void AssertionPipeline::clear()
40		{
41	11532	d_nodes.clear();
42	11532	d_realAssertionsEnd = 0;
43	11532	d_assumptionsStart = 0;
44	11532	d_numAssumptions = 0;
45	11532	}
46
47	74585	void AssertionPipeline::push_back(Node n,
48		bool isAssumption,
49		bool isInput,
50		ProofGenerator* pgen)
51		{
52	74585	d_nodes.push_back(n);
53	74585	if (isAssumption)
54		{
55	1617	Assert(pgen == nullptr);
56	1617	if (d_numAssumptions == 0)
57		{
58	1594	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	1617	Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
65	1617	d_numAssumptions++;
66		}
67	149170	Trace("assert-pipeline") << "Assertions: ...new assertion " << n
68	74585	<< ", isInput=" << isInput << std::endl;
69	74585	if (isProofEnabled())
70		{
71	2005	if (!isInput)
72		{
73		// notice this is always called, regardless of whether pgen is nullptr
74	997	d_pppg->notifyNewAssert(n, pgen);
75		}
76		else
77		{
78	1008	Assert(pgen == nullptr);
79		// n is an input assertion, whose proof should be ASSUME.
80	1008	d_pppg->notifyInput(n);
81		}
82		}
83	74585	}
84
85	9632	void AssertionPipeline::pushBackTrusted(TrustNode trn)
86		{
87	9632	Assert(trn.getKind() == TrustNodeKind::LEMMA);
88		// push back what was proven
89	9632	push_back(trn.getProven(), false, false, trn.getGenerator());
90	9632	}
91
92	183095	void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
93		{
94	183095	if (n == d_nodes[i])
95		{
96		// no change, skip
97	131363	return;
98		}
99	103464	Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
100	51732	<< n << std::endl;
101	51732	if (isProofEnabled())
102		{
103	565	d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
104		}
105	51732	d_nodes[i] = n;
106		}
107
108	154857	void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
109		{
110	154857	if (trn.isNull())
111		{
112		// null trust node denotes no change, nothing to do
113	105955	return;
114		}
115	48902	Assert(trn.getKind() == TrustNodeKind::REWRITE);
116	48902	Assert(trn.getProven()[0] == d_nodes[i]);
117	48902	replace(i, trn.getNode(), trn.getGenerator());
118		}
119
120	143	void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
121		{
122	143	d_pppg = pppg;
123	143	}
124
125	129298	bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
126
127	2444	void AssertionPipeline::enableStoreSubstsInAsserts()
128		{
129	2444	d_storeSubstsInAsserts = true;
130	2444	d_substsIndex = d_nodes.size();
131	2444	d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
132	2444	}
133
134	6098	void AssertionPipeline::disableStoreSubstsInAsserts()
135		{
136	6098	d_storeSubstsInAsserts = false;
137	6098	}
138
139	943	void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
140		{
141	943	Assert(d_storeSubstsInAsserts);
142	943	Assert(n.getKind() == kind::EQUAL);
143	943	conjoin(d_substsIndex, n, pg);
144	943	}
145
146	3068	void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
147		{
148	3068	NodeManager* nm = NodeManager::currentNM();
149	6049	Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
150	6049	Node newConjr = theory::Rewriter::rewrite(newConj);
151	6136	Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
152	3068	<< d_nodes[i] << std::endl;
153	6136	Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
154	3068	<< ", got " << newConjr << std::endl;
155	3068	if (newConjr == d_nodes[i])
156		{
157		// trivial, skip
158	87	return;
159		}
160	2981	if (isProofEnabled())
161		{
162	17	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	15	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	2	LazyCDProof* lcp = d_pppg->allocateHelperProof();
178	2	lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
179	2	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	2	newConj = n;
183		}
184		else
185		{
186		lcp->addLazyStep(d_nodes[i], d_pppg);
187		lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
188		}
189	2	if (newConjr != newConj)
190		{
191	6	lcp->addStep(
192	4	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	2	d_pppg->notifyNewAssert(newConjr, lcp);
200		}
201		}
202	2981	d_nodes[i] = newConjr;
203	2981	Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
204		}
205
206		} // namespace preprocessing
207	22746	} // namespace cvc5