Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/preprocess_proof_generator.cpp	Lines:	99	107	92.5 %
Date:	2021-05-22	Branches:	209	492	42.5 %


/******************************************************************************
 * 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 "expr/proof.h"
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
#include "options/proof_options.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, nullptr),
      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)
{
  Trace("smt-proof-pp-debug")
      << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
  if (d_src.find(n) == d_src.end())
  {
    // if no proof generator provided for (non-true) assertion
    if (pg == nullptr && (!n.isConst() || !n.getConst<bool>()))
    {
      checkEagerPedantic(d_ra);
    }
    d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
  }
  else
  {
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
  }
}

void PreprocessProofGenerator::notifyNewTrustedAssert(theory::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(theory::TrustNode::mkTrustRewrite(n, np, pg));
}

void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
{
  if (tnp.isNull())
  {
    // no rewrite, nothing to do
    return;
  }
  Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE);
  Node np = tnp.getNode();
  Trace("smt-proof-pp-debug")
      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
      << 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)
{
  NodeTrustNodeMap::iterator it = d_src.find(f);
  if (it == d_src.end())
  {
    // could be an assumption, return nullptr
    return nullptr;
  }
  // make CDProof to construct the proof below
  CDProof cdp(d_pnm);

  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
                    << ") input " << f << std::endl;
  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") << "...get provided proof" << std::endl;
      std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
      if (pfr != nullptr)
      {
        Trace("smt-pppg") << "...add provided" << std::endl;
        Assert(pfr->getResult() == proven);
        cdp.addProof(pfr);
        proofStepProcessed = true;
      }

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

      if (!proofStepProcessed)
      {
        Trace("smt-pppg") << "...add missing step" << std::endl;
        // add trusted step, the rule depends on the kind of trust node
        cdp.addStep(proven,
                    tnk == theory::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::proofEagerChecking())
  {
    // 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 "expr/proof.h"
22		#include "expr/proof_checker.h"
23		#include "expr/proof_node.h"
24		#include "options/proof_options.h"
25		#include "theory/rewriter.h"
26
27		namespace cvc5 {
28		namespace smt {
29
30	7200	PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
31		context::Context* c,
32		std::string name,
33		PfRule ra,
34	7200	PfRule rpp)
35		: d_pnm(pnm),
36	7200	d_ctx(c ? c : &d_context),
37		d_src(d_ctx),
38		d_helperProofs(pnm, d_ctx),
39		d_inputPf(pnm, nullptr),
40		d_name(name),
41		d_ra(ra),
42	14400	d_rpp(rpp)
43		{
44	7200	}
45
46	38072	void PreprocessProofGenerator::notifyInput(Node n)
47		{
48	38072	notifyNewAssert(n, &d_inputPf);
49	38072	}
50
51	86846	void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
52		{
53	173692	Trace("smt-proof-pp-debug")
54	86846	<< "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
55	86846	if (d_src.find(n) == d_src.end())
56		{
57		// if no proof generator provided for (non-true) assertion
58	82814	if (pg == nullptr && (!n.isConst() \|\| !n.getConst<bool>()))
59		{
60	1508	checkEagerPedantic(d_ra);
61		}
62	82814	d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
63		}
64		else
65		{
66	4032	Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
67		}
68	86846	}
69
70	28683	void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn)
71		{
72	28683	notifyNewAssert(tn.getProven(), tn.getGenerator());
73	28683	}
74
75	32920	void PreprocessProofGenerator::notifyPreprocessed(Node n,
76		Node np,
77		ProofGenerator* pg)
78		{
79		// only do anything if indeed it rewrote
80	32920	if (n == np)
81		{
82		return;
83		}
84		// call the trusted version
85	32920	notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg));
86		}
87
88	48306	void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
89		{
90	48306	if (tnp.isNull())
91		{
92		// no rewrite, nothing to do
93		return;
94		}
95	48306	Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE);
96	96612	Node np = tnp.getNode();
97	96612	Trace("smt-proof-pp-debug")
98	96612	<< "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
99	48306	<< std::endl;
100	48306	if (d_src.find(np) == d_src.end())
101		{
102	40290	if (tnp.getGenerator() == nullptr)
103		{
104	2851	checkEagerPedantic(d_rpp);
105		}
106	40290	d_src[np] = tnp;
107		}
108		else
109		{
110	8016	Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
111		}
112		}
113
114	54594	std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
115		{
116	54594	NodeTrustNodeMap::iterator it = d_src.find(f);
117	54594	if (it == d_src.end())
118		{
119		// could be an assumption, return nullptr
120	17456	return nullptr;
121		}
122		// make CDProof to construct the proof below
123	74276	CDProof cdp(d_pnm);
124
125	74276	Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
126	37138	<< ") input " << f << std::endl;
127	74276	Node curr = f;
128	74276	std::vector<Node> transChildren;
129	74276	std::unordered_set<Node> processed;
130		bool success;
131		// we connect the proof of f to its source via the map d_src until we
132		// discover that its source is a preprocessing lemma (a lemma stored in d_src)
133		// or otherwise it is assumed to be an input assumption.
134	49358	do
135		{
136	49358	success = false;
137	49358	if (it != d_src.end())
138		{
139	49358	Assert((*it).second.getNode() == curr);
140		// get the proven node
141	98716	Node proven = (*it).second.getProven();
142	49358	Assert(!proven.isNull());
143	49358	Trace("smt-pppg") << "...process proven " << proven << std::endl;
144	49358	if (processed.find(proven) != processed.end())
145		{
146		Unhandled() << "Cyclic steps in preprocess proof generator";
147		continue;
148		}
149	49358	processed.insert(proven);
150	49358	bool proofStepProcessed = false;
151
152		// if a generator for the step was provided, it is stored in the proof
153	49358	Trace("smt-pppg") << "...get provided proof" << std::endl;
154	98716	std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
155	49358	if (pfr != nullptr)
156		{
157	48365	Trace("smt-pppg") << "...add provided" << std::endl;
158	48365	Assert(pfr->getResult() == proven);
159	48365	cdp.addProof(pfr);
160	48365	proofStepProcessed = true;
161		}
162
163	49358	Trace("smt-pppg") << "...update" << std::endl;
164	49358	theory::TrustNodeKind tnk = (*it).second.getKind();
165	49358	if (tnk == theory::TrustNodeKind::REWRITE)
166		{
167	12220	Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
168	12220	Assert(proven.getKind() == kind::EQUAL);
169	12220	if (!proofStepProcessed)
170		{
171		// maybe its just a simple rewrite?
172	873	if (proven[1] == theory::Rewriter::rewrite(proven[0]))
173		{
174	10	cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
175	10	proofStepProcessed = true;
176		}
177		}
178	12220	transChildren.push_back(proven);
179		// continue with source
180	12220	curr = proven[0];
181	12220	success = true;
182		// find the next node
183	12220	it = d_src.find(curr);
184		}
185		else
186		{
187	37138	Trace("smt-pppg") << "...lemma" << std::endl;
188	37138	Assert(tnk == theory::TrustNodeKind::LEMMA);
189		}
190
191	49358	if (!proofStepProcessed)
192		{
193	983	Trace("smt-pppg") << "...add missing step" << std::endl;
194		// add trusted step, the rule depends on the kind of trust node
195	1966	cdp.addStep(proven,
196		tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp,
197		{},
198	983	{proven});
199		}
200		}
201		} while (success);
202
203		// prove ( curr == f ), which is not necessary if they are the same
204		// modulo symmetry.
205	37138	if (!CDProof::isSame(f, curr))
206		{
207	20654	Node fullRewrite = curr.eqNode(f);
208	10327	if (transChildren.size() >= 2)
209		{
210	1170	Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
211	1170	std::reverse(transChildren.begin(), transChildren.end());
212	1170	cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
213		}
214	10327	Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
215		// prove f
216	10327	cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
217	10327	Trace("smt-pppg") << "...finished" << std::endl;
218		}
219
220		// overall, proof is:
221		// --------- from proof generator ---------- from proof generator
222		// F_1 = F_2 ... F_{n-1} = F_n
223		// ---? -------------------------------------------------- TRANS
224		// F_1 F_1 = F_n
225		// ---------------- EQ_RESOLVE
226		// F_n
227		// Note F_1 may have been given a proof if it was not an input assumption.
228
229	37138	return cdp.getProofFor(f);
230		}
231
232	3600	ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
233
234	407	LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
235		{
236	407	return d_helperProofs.allocateProof(nullptr, d_ctx);
237		}
238
239	44184	std::string PreprocessProofGenerator::identify() const { return d_name; }
240
241	4359	void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
242		{
243	4359	if (options::proofEagerChecking())
244		{
245		// catch a pedantic failure now, which otherwise would not be
246		// triggered since we are doing lazy proof generation
247		ProofChecker* pc = d_pnm->getChecker();
248		std::stringstream serr;
249		if (pc->isPedanticFailure(r, serr))
250		{
251		Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
252		<< serr.str();
253		}
254		}
255	4359	}
256
257		} // namespace smt
258	28191	} // namespace cvc5