Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/preprocess_proof_generator.cpp	Lines:	111	119	93.3 %
Date:	2021-09-05	Branches:	245	552	44.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * The implementation of the module for proofs for preprocessing in an
 * SMT engine.
 */

#include "smt/preprocess_proof_generator.h"

#include <sstream>

#include "options/proof_options.h"
#include "proof/method_id.h"
#include "proof/proof.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace smt {

PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
                                                   context::Context* c,
                                                   std::string name,
                                                   PfRule ra,
                                                   PfRule rpp)
    : d_pnm(pnm),
      d_ctx(c ? c : &d_context),
      d_src(d_ctx),
      d_helperProofs(pnm, d_ctx),
      d_inputPf(pnm, c, "InputProof"),
      d_name(name),
      d_ra(ra),
      d_rpp(rpp)
{
}

void PreprocessProofGenerator::notifyInput(Node n)
{
  notifyNewAssert(n, &d_inputPf);
}

void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
{
  if (n.isConst() && n.getConst<bool>())
  {
    // ignore true assertions
    return;
  }
  Trace("smt-proof-pp-debug")
      << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
      << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl;
  if (d_src.find(n) == d_src.end())
  {
    // if no proof generator provided for (non-true) assertion
    if (pg == nullptr)
    {
      checkEagerPedantic(d_ra);
    }
    d_src[n] = TrustNode::mkTrustLemma(n, pg);
  }
  else
  {
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
  }
}

void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
{
  notifyNewAssert(tn.getProven(), tn.getGenerator());
}

void PreprocessProofGenerator::notifyPreprocessed(Node n,
                                                  Node np,
                                                  ProofGenerator* pg)
{
  // only do anything if indeed it rewrote
  if (n == np)
  {
    return;
  }
  // call the trusted version
  notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
}

void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
{
  if (tnp.isNull())
  {
    // no rewrite, nothing to do
    return;
  }
  Assert(tnp.getKind() == TrustNodeKind::REWRITE);
  Node np = tnp.getNode();
  Trace("smt-proof-pp-debug")
      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
  if (d_src.find(np) == d_src.end())
  {
    if (tnp.getGenerator() == nullptr)
    {
      checkEagerPedantic(d_rpp);
    }
    d_src[np] = tnp;
  }
  else
  {
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
  }
}

std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
{
  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
                    << ") input " << f << std::endl;
  NodeTrustNodeMap::iterator it = d_src.find(f);
  if (it == d_src.end())
  {
    Trace("smt-pppg") << "...no proof for " << identify() << " " << f
                      << std::endl;
    // could be an assumption, return nullptr
    return nullptr;
  }
  // make CDProof to construct the proof below
  CDProof cdp(d_pnm);

  Node curr = f;
  std::vector<Node> transChildren;
  std::unordered_set<Node> processed;
  bool success;
  // we connect the proof of f to its source via the map d_src until we
  // discover that its source is a preprocessing lemma (a lemma stored in d_src)
  // or otherwise it is assumed to be an input assumption.
  do
  {
    success = false;
    if (it != d_src.end())
    {
      Assert((*it).second.getNode() == curr);
      // get the proven node
      Node proven = (*it).second.getProven();
      Assert(!proven.isNull());
      Trace("smt-pppg") << "...process proven " << proven << std::endl;
      if (processed.find(proven) != processed.end())
      {
        Unhandled() << "Cyclic steps in preprocess proof generator";
        continue;
      }
      processed.insert(proven);
      bool proofStepProcessed = false;

      // if a generator for the step was provided, it is stored in the proof
      Trace("smt-pppg-debug")
          << "...get provided proof " << (*it).second << std::endl;
      std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
      if (pfr != nullptr)
      {
        Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl;
        Assert(pfr->getResult() == proven);
        cdp.addProof(pfr);
        proofStepProcessed = true;
      }

      Trace("smt-pppg-debug") << "...update" << std::endl;
      TrustNodeKind tnk = (*it).second.getKind();
      if (tnk == TrustNodeKind::REWRITE)
      {
        Trace("smt-pppg-debug")
            << "...rewritten from " << proven[0] << std::endl;
        Assert(proven.getKind() == kind::EQUAL);
        if (!proofStepProcessed)
        {
          // maybe its just an (extended) rewrite?
          theory::quantifiers::ExtendedRewriter extr(true);
          Node pr = extr.extendedRewrite(proven[0]);
          if (proven[1] == pr)
          {
            Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
            Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
            cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0], idr});
            proofStepProcessed = true;
          }
        }
        transChildren.push_back(proven);
        // continue with source
        curr = proven[0];
        success = true;
        // find the next node
        Trace("smt-pppg") << "...continue " << curr << std::endl;
        it = d_src.find(curr);
      }
      else
      {
        Trace("smt-pppg") << "...lemma" << std::endl;
        Assert(tnk == TrustNodeKind::LEMMA);
      }

      if (!proofStepProcessed)
      {
        Trace("smt-pppg-debug")
            << "...justify missing step with "
            << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
        // add trusted step, the rule depends on the kind of trust node
        cdp.addStep(
            proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
      }
    }
  } while (success);

  // prove ( curr == f ), which is not necessary if they are the same
  // modulo symmetry.
  if (!CDProof::isSame(f, curr))
  {
    Node fullRewrite = curr.eqNode(f);
    if (transChildren.size() >= 2)
    {
      Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
      std::reverse(transChildren.begin(), transChildren.end());
      cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
    }
    Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
    // prove f
    cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
    Trace("smt-pppg") << "...finished" << std::endl;
  }

  // overall, proof is:
  //        --------- from proof generator       ---------- from proof generator
  //        F_1 = F_2          ...               F_{n-1} = F_n
  // ---?   -------------------------------------------------- TRANS
  // F_1    F_1 = F_n
  // ---------------- EQ_RESOLVE
  // F_n
  // Note F_1 may have been given a proof if it was not an input assumption.

  return cdp.getProofFor(f);
}

ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }

LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
{
  return d_helperProofs.allocateProof(nullptr, d_ctx);
}

std::string PreprocessProofGenerator::identify() const { return d_name; }

void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
{
  if (options::proofCheck() == options::ProofCheckMode::EAGER)
  {
    // catch a pedantic failure now, which otherwise would not be
    // triggered since we are doing lazy proof generation
    ProofChecker* pc = d_pnm->getChecker();
    std::stringstream serr;
    if (pc->isPedanticFailure(r, serr))
    {
      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
                  << serr.str();
    }
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer
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		* The implementation of the module for proofs for preprocessing in an
14		* SMT engine.
15		*/
16
17		#include "smt/preprocess_proof_generator.h"
18
19		#include <sstream>
20
21		#include "options/proof_options.h"
22		#include "proof/method_id.h"
23		#include "proof/proof.h"
24		#include "proof/proof_checker.h"
25		#include "proof/proof_node.h"
26		#include "theory/quantifiers/extended_rewrite.h"
27		#include "theory/rewriter.h"
28
29		namespace cvc5 {
30		namespace smt {
31
32	7568	PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
33		context::Context* c,
34		std::string name,
35		PfRule ra,
36	7568	PfRule rpp)
37		: d_pnm(pnm),
38	7568	d_ctx(c ? c : &d_context),
39		d_src(d_ctx),
40		d_helperProofs(pnm, d_ctx),
41		d_inputPf(pnm, c, "InputProof"),
42		d_name(name),
43		d_ra(ra),
44	15136	d_rpp(rpp)
45		{
46	7568	}
47
48	37466	void PreprocessProofGenerator::notifyInput(Node n)
49		{
50	37466	notifyNewAssert(n, &d_inputPf);
51	37466	}
52
53	84341	void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
54		{
55	84341	if (n.isConst() && n.getConst<bool>())
56		{
57		// ignore true assertions
58	5503	return;
59		}
60	157676	Trace("smt-proof-pp-debug")
61	157676	<< "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
62	78838	<< " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl;
63	78838	if (d_src.find(n) == d_src.end())
64		{
65		// if no proof generator provided for (non-true) assertion
66	76180	if (pg == nullptr)
67		{
68	304	checkEagerPedantic(d_ra);
69		}
70	76180	d_src[n] = TrustNode::mkTrustLemma(n, pg);
71		}
72		else
73		{
74	2658	Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
75		}
76		}
77
78	28250	void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
79		{
80	28250	notifyNewAssert(tn.getProven(), tn.getGenerator());
81	28250	}
82
83	32404	void PreprocessProofGenerator::notifyPreprocessed(Node n,
84		Node np,
85		ProofGenerator* pg)
86		{
87		// only do anything if indeed it rewrote
88	32404	if (n == np)
89		{
90		return;
91		}
92		// call the trusted version
93	32404	notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
94		}
95
96	47543	void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
97		{
98	47543	if (tnp.isNull())
99		{
100		// no rewrite, nothing to do
101		return;
102		}
103	47543	Assert(tnp.getKind() == TrustNodeKind::REWRITE);
104	95086	Node np = tnp.getNode();
105	95086	Trace("smt-proof-pp-debug")
106	47543	<< "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
107	47543	if (d_src.find(np) == d_src.end())
108		{
109	40277	if (tnp.getGenerator() == nullptr)
110		{
111	2192	checkEagerPedantic(d_rpp);
112		}
113	40277	d_src[np] = tnp;
114		}
115		else
116		{
117	7266	Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
118		}
119		}
120
121	55864	std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
122		{
123	111728	Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
124	55864	<< ") input " << f << std::endl;
125	55864	NodeTrustNodeMap::iterator it = d_src.find(f);
126	55864	if (it == d_src.end())
127		{
128	33558	Trace("smt-pppg") << "...no proof for " << identify() << " " << f
129	16779	<< std::endl;
130		// could be an assumption, return nullptr
131	16779	return nullptr;
132		}
133		// make CDProof to construct the proof below
134	78170	CDProof cdp(d_pnm);
135
136	78170	Node curr = f;
137	78170	std::vector<Node> transChildren;
138	78170	std::unordered_set<Node> processed;
139		bool success;
140		// we connect the proof of f to its source via the map d_src until we
141		// discover that its source is a preprocessing lemma (a lemma stored in d_src)
142		// or otherwise it is assumed to be an input assumption.
143	52210	do
144		{
145	52210	success = false;
146	52210	if (it != d_src.end())
147		{
148	52210	Assert((*it).second.getNode() == curr);
149		// get the proven node
150	104420	Node proven = (*it).second.getProven();
151	52210	Assert(!proven.isNull());
152	52210	Trace("smt-pppg") << "...process proven " << proven << std::endl;
153	52210	if (processed.find(proven) != processed.end())
154		{
155		Unhandled() << "Cyclic steps in preprocess proof generator";
156		continue;
157		}
158	52210	processed.insert(proven);
159	52210	bool proofStepProcessed = false;
160
161		// if a generator for the step was provided, it is stored in the proof
162	104420	Trace("smt-pppg-debug")
163	52210	<< "...get provided proof " << (*it).second << std::endl;
164	104420	std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
165	52210	if (pfr != nullptr)
166		{
167	51382	Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl;
168	51382	Assert(pfr->getResult() == proven);
169	51382	cdp.addProof(pfr);
170	51382	proofStepProcessed = true;
171		}
172
173	52210	Trace("smt-pppg-debug") << "...update" << std::endl;
174	52210	TrustNodeKind tnk = (*it).second.getKind();
175	52210	if (tnk == TrustNodeKind::REWRITE)
176		{
177	26250	Trace("smt-pppg-debug")
178	13125	<< "...rewritten from " << proven[0] << std::endl;
179	13125	Assert(proven.getKind() == kind::EQUAL);
180	13125	if (!proofStepProcessed)
181		{
182		// maybe its just an (extended) rewrite?
183	1426	theory::quantifiers::ExtendedRewriter extr(true);
184	1426	Node pr = extr.extendedRewrite(proven[0]);
185	713	if (proven[1] == pr)
186		{
187	16	Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
188	8	Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
189	8	cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0], idr});
190	8	proofStepProcessed = true;
191		}
192		}
193	13125	transChildren.push_back(proven);
194		// continue with source
195	13125	curr = proven[0];
196	13125	success = true;
197		// find the next node
198	13125	Trace("smt-pppg") << "...continue " << curr << std::endl;
199	13125	it = d_src.find(curr);
200		}
201		else
202		{
203	39085	Trace("smt-pppg") << "...lemma" << std::endl;
204	39085	Assert(tnk == TrustNodeKind::LEMMA);
205		}
206
207	52210	if (!proofStepProcessed)
208		{
209	1640	Trace("smt-pppg-debug")
210	820	<< "...justify missing step with "
211	820	<< (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
212		// add trusted step, the rule depends on the kind of trust node
213	1640	cdp.addStep(
214	820	proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
215		}
216		}
217		} while (success);
218
219		// prove ( curr == f ), which is not necessary if they are the same
220		// modulo symmetry.
221	39085	if (!CDProof::isSame(f, curr))
222		{
223	22016	Node fullRewrite = curr.eqNode(f);
224	11008	if (transChildren.size() >= 2)
225		{
226	1439	Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
227	1439	std::reverse(transChildren.begin(), transChildren.end());
228	1439	cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
229		}
230	11008	Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
231		// prove f
232	11008	cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
233	11008	Trace("smt-pppg") << "...finished" << std::endl;
234		}
235
236		// overall, proof is:
237		// --------- from proof generator ---------- from proof generator
238		// F_1 = F_2 ... F_{n-1} = F_n
239		// ---? -------------------------------------------------- TRANS
240		// F_1 F_1 = F_n
241		// ---------------- EQ_RESOLVE
242		// F_n
243		// Note F_1 may have been given a proof if it was not an input assumption.
244
245	39085	return cdp.getProofFor(f);
246		}
247
248	3784	ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
249
250	411	LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
251		{
252	411	return d_helperProofs.allocateProof(nullptr, d_ctx);
253		}
254
255	143612	std::string PreprocessProofGenerator::identify() const { return d_name; }
256
257	2496	void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
258		{
259	2496	if (options::proofCheck() == options::ProofCheckMode::EAGER)
260		{
261		// catch a pedantic failure now, which otherwise would not be
262		// triggered since we are doing lazy proof generation
263		ProofChecker* pc = d_pnm->getChecker();
264		std::stringstream serr;
265		if (pc->isPedanticFailure(r, serr))
266		{
267		Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
268		<< serr.str();
269		}
270		}
271	2496	}
272
273		} // namespace smt
274	29505	} // namespace cvc5