Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/trust_substitutions.cpp	Lines:	120	121	99.2 %
Date:	2021-05-21	Branches:	253	540	46.9 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Trust substitutions.
 */

#include "theory/trust_substitutions.h"

#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {

TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
                                           ProofNodeManager* pnm,
                                           std::string name,
                                           PfRule trustId,
                                           MethodId ids)
    : d_ctx(c),
      d_subs(c),
      d_tsubs(c),
      d_tspb(nullptr),
      d_subsPg(nullptr),
      d_applyPg(nullptr),
      d_helperPf(nullptr),
      d_name(name),
      d_trustId(trustId),
      d_ids(ids),
      d_eqtIndex(c)
{
  setProofNodeManager(pnm);
}

void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm)
{
  if (pnm != nullptr)
  {
    // should not set the proof node manager more than once
    Assert(d_tspb == nullptr);
    d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())),
        d_subsPg.reset(new LazyCDProof(
            pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
    d_applyPg.reset(
        new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
    d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx));
  }
}

void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
{
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
                      << " -> " << t << std::endl;
  d_subs.addSubstitution(x, t);
  if (isProofEnabled())
  {
    TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
    d_tsubs.push_back(tnl);
    // add to lazy proof
    d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
  }
}

void TrustSubstitutionMap::addSubstitution(TNode x,
                                           TNode t,
                                           PfRule id,
                                           const std::vector<Node>& children,
                                           const std::vector<Node>& args)
{
  if (!isProofEnabled())
  {
    addSubstitution(x, t, nullptr);
    return;
  }
  LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx);
  Node eq = x.eqNode(t);
  stepPg->addStep(eq, id, children, args);
  addSubstitution(x, t, stepPg);
}

ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
                                                            TNode t,
                                                            TrustNode tn)
{
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
                      << x << " -> " << t << " from " << tn.getProven()
                      << std::endl;
  if (!isProofEnabled() || tn.getGenerator() == nullptr)
  {
    // no generator or not proof enabled, nothing to do
    addSubstitution(x, t, nullptr);
    Trace("trust-subs") << "...no proof" << std::endl;
    return nullptr;
  }
  Node eq = x.eqNode(t);
  Node proven = tn.getProven();
  // notice that this checks syntactic equality, not CDProof::isSame since
  // tn.getGenerator() is not necessarily robust to symmetry.
  if (eq == proven)
  {
    // no rewrite required, just use the generator
    addSubstitution(x, t, tn.getGenerator());
    Trace("trust-subs") << "...use generator directly" << std::endl;
    return tn.getGenerator();
  }
  LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx);
  // Try to transform tn.getProven() to (= x t) here, if necessary
  if (!d_tspb->applyPredTransform(proven, eq, {}))
  {
    // failed to rewrite, it is critical for unsat cores that proven is a
    // premise here, since the conclusion depends on it
    addSubstitution(x, t, PfRule::TRUST_SUBS_MAP, {proven}, {eq});
    Trace("trust-subs") << "...failed to rewrite" << std::endl;
    return nullptr;
  }
  Trace("trust-subs") << "...successful rewrite" << std::endl;
  solvePg->addSteps(*d_tspb.get());
  d_tspb->clear();
  // link the given generator
  solvePg->addLazyStep(proven, tn.getGenerator());
  addSubstitution(x, t, solvePg);
  return solvePg;
}

void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
{
  if (!isProofEnabled())
  {
    // just use the basic utility
    d_subs.addSubstitutions(t.get());
    return;
  }
  // call addSubstitution above in sequence
  for (const TrustNode& tns : t.d_tsubs)
  {
    Node proven = tns.getProven();
    addSubstitution(proven[0], proven[1], tns.getGenerator());
  }
}

TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
{
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
                      << std::endl;
  Node ns = d_subs.apply(n, doRewrite);
  Trace("trust-subs") << "...subs " << ns << std::endl;
  if (n == ns)
  {
    // no change
    return TrustNode::null();
  }
  if (!isProofEnabled())
  {
    // no proofs, use null generator
    return TrustNode::mkTrustRewrite(n, ns, nullptr);
  }
  Node eq = n.eqNode(ns);
  // remember the index
  d_eqtIndex[eq] = d_tsubs.size();
  // this class will provide a proof if asked
  return TrustNode::mkTrustRewrite(n, ns, this);
}

Node TrustSubstitutionMap::apply(Node n, bool doRewrite)
{
  return d_subs.apply(n, doRewrite);
}

std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
{
  Assert(eq.getKind() == kind::EQUAL);
  Node n = eq[0];
  Node ns = eq[1];
  // Easy case: if n is in the domain of the substitution, maybe it is already
  // a proof in the substitution proof generator. This is moreover required
  // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
  // and we are asked to transform x, resulting in 5, we hence must provide
  // a proof of (= x 5) based on the substitution. However, it must be the
  // case that (= x 5) is a proven fact of the substitution generator. Hence
  // we avoid a proof that looks like:
  // ---------- from d_subsPg
  // (= x 5)
  // ---------- MACRO_SR_EQ_INTRO{x}
  // (= x 5)
  // by taking the premise proof directly.
  if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq))
  {
    return d_subsPg->getProofFor(eq);
  }
  NodeUIntMap::iterator it = d_eqtIndex.find(eq);
  Assert(it != d_eqtIndex.end());
  Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
                         << it->second << std::endl;
  Node cs = getSubstitution(it->second);
  Assert(eq != cs);
  std::vector<Node> pfChildren;
  if (!cs.isConst())
  {
    // note we will get more proof reuse if we do not special case AND here.
    if (cs.getKind() == kind::AND)
    {
      for (const Node& csc : cs)
      {
        pfChildren.push_back(csc);
        // connect substitution generator into apply generator
        d_applyPg->addLazyStep(csc, d_subsPg.get());
      }
    }
    else
    {
      pfChildren.push_back(cs);
      // connect substitution generator into apply generator
      d_applyPg->addLazyStep(cs, d_subsPg.get());
    }
  }
  Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
  // We use fixpoint as the substitution-apply identifier. Notice that it
  // suffices to use SBA_SEQUENTIAL here, but SBA_FIXPOINT is typically
  // more efficient. This is because for substitution of size n, sequential
  // substitution can either be implemented as n traversals of the term to
  // apply the substitution to, or a single traversal of the term, but n^2/2
  // traversals of the range of the substitution to prepare a simultaneous
  // substitution. Both of these options are inefficient.
  if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids, MethodId::SBA_FIXPOINT))
  {
    // if we fail for any reason, we must use a trusted step instead
    d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
  }
  Trace("trust-subs-pf") << "...made steps" << std::endl;
  // -------        ------- from external proof generators
  // x1 = t1 ...    xn = tn
  // ----------------------- AND_INTRO
  //   ...
  // --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above)
  // n == ns
  // add it to the apply proof generator.
  //
  // Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an
  // optimization motivated by the fact that n may be large and reused many
  // time. For instance, if this class is being used to track substitutions
  // derived during non-clausal simplification during preprocessing, it is
  // a fixed (possibly) large substitution applied to many terms. Having
  // a single child saves us from creating many proofs with n children, where
  // notice this proof is reused.
  d_applyPg->addSteps(*d_tspb.get());
  d_tspb->clear();
  Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
  return d_applyPg->getProofFor(eq);
}

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

SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }

bool TrustSubstitutionMap::isProofEnabled() const
{
  return d_subsPg != nullptr;
}

Node TrustSubstitutionMap::getSubstitution(size_t index)
{
  Assert(index <= d_tsubs.size());
  std::vector<Node> csubsChildren;
  for (size_t i = 0; i < index; i++)
  {
    csubsChildren.push_back(d_tsubs[i].getProven());
  }
  std::reverse(csubsChildren.begin(), csubsChildren.end());
  Node cs = NodeManager::currentNM()->mkAnd(csubsChildren);
  if (cs.getKind() == kind::AND)
  {
    d_subsPg->addStep(cs, PfRule::AND_INTRO, csubsChildren, {});
  }
  return cs;
}

}  // namespace theory
}  // 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		* Trust substitutions.
14		*/
15
16		#include "theory/trust_substitutions.h"
17
18		#include "theory/rewriter.h"
19
20		namespace cvc5 {
21		namespace theory {
22
23	28335	TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
24		ProofNodeManager* pnm,
25		std::string name,
26		PfRule trustId,
27	28335	MethodId ids)
28		: d_ctx(c),
29		d_subs(c),
30		d_tsubs(c),
31		d_tspb(nullptr),
32		d_subsPg(nullptr),
33		d_applyPg(nullptr),
34		d_helperPf(nullptr),
35		d_name(name),
36		d_trustId(trustId),
37		d_ids(ids),
38	28335	d_eqtIndex(c)
39		{
40	28335	setProofNodeManager(pnm);
41	28335	}
42
43	31452	void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm)
44		{
45	31452	if (pnm != nullptr)
46		{
47		// should not set the proof node manager more than once
48	6655	Assert(d_tspb == nullptr);
49	6655	d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())),
50	13310	d_subsPg.reset(new LazyCDProof(
51	6655	pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
52	13310	d_applyPg.reset(
53	6655	new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
54	6655	d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx));
55		}
56	31452	}
57
58	61263	void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
59		{
60	122526	Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
61	61263	<< " -> " << t << std::endl;
62	61263	d_subs.addSubstitution(x, t);
63	61263	if (isProofEnabled())
64		{
65	24900	TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
66	12450	d_tsubs.push_back(tnl);
67		// add to lazy proof
68	12450	d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
69		}
70	61263	}
71
72	2326	void TrustSubstitutionMap::addSubstitution(TNode x,
73		TNode t,
74		PfRule id,
75		const std::vector<Node>& children,
76		const std::vector<Node>& args)
77		{
78	2326	if (!isProofEnabled())
79		{
80	1417	addSubstitution(x, t, nullptr);
81	1417	return;
82		}
83	909	LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx);
84	1818	Node eq = x.eqNode(t);
85	909	stepPg->addStep(eq, id, children, args);
86	909	addSubstitution(x, t, stepPg);
87		}
88
89	53742	ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
90		TNode t,
91		TrustNode tn)
92		{
93	107484	Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
94	107484	<< x << " -> " << t << " from " << tn.getProven()
95	53742	<< std::endl;
96	53742	if (!isProofEnabled() \|\| tn.getGenerator() == nullptr)
97		{
98		// no generator or not proof enabled, nothing to do
99	47112	addSubstitution(x, t, nullptr);
100	47112	Trace("trust-subs") << "...no proof" << std::endl;
101	47112	return nullptr;
102		}
103	13260	Node eq = x.eqNode(t);
104	13260	Node proven = tn.getProven();
105		// notice that this checks syntactic equality, not CDProof::isSame since
106		// tn.getGenerator() is not necessarily robust to symmetry.
107	6630	if (eq == proven)
108		{
109		// no rewrite required, just use the generator
110	5401	addSubstitution(x, t, tn.getGenerator());
111	5401	Trace("trust-subs") << "...use generator directly" << std::endl;
112	5401	return tn.getGenerator();
113		}
114	1229	LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx);
115		// Try to transform tn.getProven() to (= x t) here, if necessary
116	1229	if (!d_tspb->applyPredTransform(proven, eq, {}))
117		{
118		// failed to rewrite, it is critical for unsat cores that proven is a
119		// premise here, since the conclusion depends on it
120	12	addSubstitution(x, t, PfRule::TRUST_SUBS_MAP, {proven}, {eq});
121	12	Trace("trust-subs") << "...failed to rewrite" << std::endl;
122	12	return nullptr;
123		}
124	1217	Trace("trust-subs") << "...successful rewrite" << std::endl;
125	1217	solvePg->addSteps(*d_tspb.get());
126	1217	d_tspb->clear();
127		// link the given generator
128	1217	solvePg->addLazyStep(proven, tn.getGenerator());
129	1217	addSubstitution(x, t, solvePg);
130	1217	return solvePg;
131		}
132
133	9221	void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
134		{
135	9221	if (!isProofEnabled())
136		{
137		// just use the basic utility
138	7515	d_subs.addSubstitutions(t.get());
139	7515	return;
140		}
141		// call addSubstitution above in sequence
142	6528	for (const TrustNode& tns : t.d_tsubs)
143		{
144	9644	Node proven = tns.getProven();
145	4822	addSubstitution(proven[0], proven[1], tns.getGenerator());
146		}
147		}
148
149	708773	TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
150		{
151	1417546	Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
152	708773	<< std::endl;
153	1417546	Node ns = d_subs.apply(n, doRewrite);
154	708771	Trace("trust-subs") << "...subs " << ns << std::endl;
155	708771	if (n == ns)
156		{
157		// no change
158	595221	return TrustNode::null();
159		}
160	113550	if (!isProofEnabled())
161		{
162		// no proofs, use null generator
163	71899	return TrustNode::mkTrustRewrite(n, ns, nullptr);
164		}
165	83302	Node eq = n.eqNode(ns);
166		// remember the index
167	41651	d_eqtIndex[eq] = d_tsubs.size();
168		// this class will provide a proof if asked
169	41651	return TrustNode::mkTrustRewrite(n, ns, this);
170		}
171
172	245654	Node TrustSubstitutionMap::apply(Node n, bool doRewrite)
173		{
174	245654	return d_subs.apply(n, doRewrite);
175		}
176
177	9893	std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
178		{
179	9893	Assert(eq.getKind() == kind::EQUAL);
180	19786	Node n = eq[0];
181	19786	Node ns = eq[1];
182		// Easy case: if n is in the domain of the substitution, maybe it is already
183		// a proof in the substitution proof generator. This is moreover required
184		// to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
185		// and we are asked to transform x, resulting in 5, we hence must provide
186		// a proof of (= x 5) based on the substitution. However, it must be the
187		// case that (= x 5) is a proven fact of the substitution generator. Hence
188		// we avoid a proof that looks like:
189		// ---------- from d_subsPg
190		// (= x 5)
191		// ---------- MACRO_SR_EQ_INTRO{x}
192		// (= x 5)
193		// by taking the premise proof directly.
194	9893	if (d_subsPg->hasStep(eq) \|\| d_subsPg->hasGenerator(eq))
195		{
196	78	return d_subsPg->getProofFor(eq);
197		}
198	9815	NodeUIntMap::iterator it = d_eqtIndex.find(eq);
199	9815	Assert(it != d_eqtIndex.end());
200	19630	Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
201	9815	<< it->second << std::endl;
202	19630	Node cs = getSubstitution(it->second);
203	9815	Assert(eq != cs);
204	19630	std::vector<Node> pfChildren;
205	9815	if (!cs.isConst())
206		{
207		// note we will get more proof reuse if we do not special case AND here.
208	3531	if (cs.getKind() == kind::AND)
209		{
210	409090	for (const Node& csc : cs)
211		{
212	405920	pfChildren.push_back(csc);
213		// connect substitution generator into apply generator
214	405920	d_applyPg->addLazyStep(csc, d_subsPg.get());
215		}
216		}
217		else
218		{
219	361	pfChildren.push_back(cs);
220		// connect substitution generator into apply generator
221	361	d_applyPg->addLazyStep(cs, d_subsPg.get());
222		}
223		}
224	9815	Trace("trust-subs-pf") << "...apply eq intro" << std::endl;
225		// We use fixpoint as the substitution-apply identifier. Notice that it
226		// suffices to use SBA_SEQUENTIAL here, but SBA_FIXPOINT is typically
227		// more efficient. This is because for substitution of size n, sequential
228		// substitution can either be implemented as n traversals of the term to
229		// apply the substitution to, or a single traversal of the term, but n^2/2
230		// traversals of the range of the substitution to prepare a simultaneous
231		// substitution. Both of these options are inefficient.
232	9815	if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids, MethodId::SBA_FIXPOINT))
233		{
234		// if we fail for any reason, we must use a trusted step instead
235		d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
236		}
237	9815	Trace("trust-subs-pf") << "...made steps" << std::endl;
238		// ------- ------- from external proof generators
239		// x1 = t1 ... xn = tn
240		// ----------------------- AND_INTRO
241		// ...
242		// --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above)
243		// n == ns
244		// add it to the apply proof generator.
245		//
246		// Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an
247		// optimization motivated by the fact that n may be large and reused many
248		// time. For instance, if this class is being used to track substitutions
249		// derived during non-clausal simplification during preprocessing, it is
250		// a fixed (possibly) large substitution applied to many terms. Having
251		// a single child saves us from creating many proofs with n children, where
252		// notice this proof is reused.
253	9815	d_applyPg->addSteps(*d_tspb.get());
254	9815	d_tspb->clear();
255	9815	Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
256	9815	return d_applyPg->getProofFor(eq);
257		}
258
259	467	std::string TrustSubstitutionMap::identify() const { return d_name; }
260
261	37718	SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
262
263	240102	bool TrustSubstitutionMap::isProofEnabled() const
264		{
265	240102	return d_subsPg != nullptr;
266		}
267
268	9815	Node TrustSubstitutionMap::getSubstitution(size_t index)
269		{
270	9815	Assert(index <= d_tsubs.size());
271	19630	std::vector<Node> csubsChildren;
272	416096	for (size_t i = 0; i < index; i++)
273		{
274	406281	csubsChildren.push_back(d_tsubs[i].getProven());
275		}
276	9815	std::reverse(csubsChildren.begin(), csubsChildren.end());
277	9815	Node cs = NodeManager::currentNM()->mkAnd(csubsChildren);
278	9815	if (cs.getKind() == kind::AND)
279		{
280	3170	d_subsPg->addStep(cs, PfRule::AND_INTRO, csubsChildren, {});
281		}
282	19630	return cs;
283		}
284
285		} // namespace theory
286	27735	} // namespace cvc5