Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/infer_proof_cons.cpp	Lines:	115	143	80.4 %
Date:	2021-08-17	Branches:	313	891	35.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of inference to proof conversion  for datatypes.
 */

#include "theory/datatypes/infer_proof_cons.h"

#include "proof/proof.h"
#include "proof/proof_checker.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/model_manager.h"
#include "theory/rewriter.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace datatypes {

InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm)
    : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c)
{
  Assert(d_pnm != nullptr);
}

void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
{
  TNode fact = di->d_conc;
  if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
  {
    return;
  }
  Node symFact = CDProof::getSymmFact(fact);
  if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
  {
    return;
  }
  d_lazyFactMap.insert(fact, di);
}

void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp)
{
  Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp
                  << std::endl;
  // split into vector
  std::vector<Node> expv;
  if (!exp.isNull() && !exp.isConst())
  {
    if (exp.getKind() == AND)
    {
      for (const Node& ec : exp)
      {
        expv.push_back(ec);
      }
    }
    else
    {
      expv.push_back(exp);
    }
  }
  NodeManager* nm = NodeManager::currentNM();
  bool success = false;
  switch (infer)
  {
    case InferenceId::DATATYPES_UNIF:
    {
      Assert(expv.size() == 1);
      Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR
             && exp[1].getKind() == APPLY_CONSTRUCTOR
             && exp[0].getOperator() == exp[1].getOperator());
      Node narg;
      // we may be asked for a proof of (not P) coming from (= P false) or
      // (= false P), or similarly P from (= P true) or (= true P).
      bool concPol = conc.getKind() != NOT;
      Node concAtom = concPol ? conc : conc[0];
      Node unifConc = conc;
      for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++)
      {
        bool argSuccess = false;
        if (conc.getKind() == EQUAL)
        {
          argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]);
        }
        else
        {
          for (size_t j = 0; j < 2; j++)
          {
            if (exp[j][i] == concAtom && exp[1 - j][i].isConst()
                && exp[1 - j][i].getConst<bool>() == concPol)
            {
              argSuccess = true;
              unifConc = exp[0][i].eqNode(exp[1][i]);
              break;
            }
          }
        }
        if (argSuccess)
        {
          narg = nm->mkConst(Rational(i));
          break;
        }
      }
      if (!narg.isNull())
      {
        if (conc.getKind() == EQUAL)
        {
          // normal case where we conclude an equality
          cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg});
        }
        else
        {
          // must use true or false elim to prove the final
          cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg});
          // may use symmetry
          Node eq = concAtom.eqNode(nm->mkConst(concPol));
          cdp->addStep(
              conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {});
        }
        success = true;
      }
    }
    break;
    case InferenceId::DATATYPES_INST:
    {
      if (expv.size() == 1)
      {
        Assert(conc.getKind() == EQUAL);
        int n = utils::isTester(exp);
        if (n >= 0)
        {
          Node t = exp[0];
          Node nn = nm->mkConst(Rational(n));
          Node eq = exp.eqNode(conc);
          cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
          cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});
          success = true;
        }
      }
    }
    break;
    case InferenceId::DATATYPES_SPLIT:
    {
      Assert(expv.empty());
      Node t = conc.getKind() == OR ? conc[0][0] : conc[0];
      cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t});
      success = true;
    }
    break;
    case InferenceId::DATATYPES_COLLAPSE_SEL:
    {
      Assert(exp.getKind() == EQUAL);
      Node concEq = conc;
      // might be a Boolean conclusion
      if (conc.getKind() != EQUAL)
      {
        bool concPol = conc.getKind() != NOT;
        Node concAtom = concPol ? conc : conc[0];
        concEq = concAtom.eqNode(nm->mkConst(concPol));
      }
      Assert(concEq.getKind() == EQUAL
             && concEq[0].getKind() == APPLY_SELECTOR_TOTAL);
      Assert(exp[0].getType().isDatatype());
      Node sop = concEq[0].getOperator();
      Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
      Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
      // exp[0] = exp[1]
      // --------------------- CONG        ----------------- DT_COLLAPSE
      // s(exp[0]) = s(exp[1])             s(exp[1]) = r
      // --------------------------------------------------- TRANS
      // s(exp[0]) = r
      Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
      Node seq = sl.eqNode(sr);
      cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
      Node sceq = sr.eqNode(concEq[1]);
      cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
      cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
      if (conc.getKind() != EQUAL)
      {
        PfRule eid =
            conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
        cdp->addStep(conc, eid, {concEq}, {});
      }
      success = true;
    }
    break;
    case InferenceId::DATATYPES_CLASH_CONFLICT:
    {
      cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {});
      success = true;
    }
    break;
    case InferenceId::DATATYPES_TESTER_CONFLICT:
    {
      // rewrites to false under substitution
      Node fn = nm->mkConst(false);
      cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {});
      success = true;
    }
    break;
    case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
    {
      Assert(expv.size() == 3);
      Node tester1 = expv[0];
      Node tester1c =
          nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]);
      cdp->addStep(tester1c,
                   PfRule::MACRO_SR_PRED_TRANSFORM,
                   {expv[1], expv[2]},
                   {tester1c});
      Node fn = nm->mkConst(false);
      cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {});
      success = true;
    }
    break;
    case InferenceId::DATATYPES_PURIFY:
    {
      cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {});
      success = true;
    }
    break;
    // inferences currently not supported
    case InferenceId::DATATYPES_LABEL_EXH:
    case InferenceId::DATATYPES_BISIMILAR:
    case InferenceId::DATATYPES_CYCLE:
    default:
      Trace("dt-ipc") << "...no conversion for inference " << infer
                      << std::endl;
      break;
  }

  if (!success)
  {
    // failed to reconstruct, add trust
    Trace("dt-ipc") << "...failed " << infer << std::endl;
    cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
  }
  else
  {
    Trace("dt-ipc") << "...success" << std::endl;
  }
}

std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
{
  Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl;
  // temporary proof
  CDProof pf(d_pnm);
  // get the inference
  NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact);
  if (it == d_lazyFactMap.end())
  {
    Node factSym = CDProof::getSymmFact(fact);
    if (!factSym.isNull())
    {
      // Use the symmetric fact. There is no need to explictly make a
      // SYMM proof, as this is handled by CDProof::getProofFor below.
      it = d_lazyFactMap.find(factSym);
    }
  }
  AlwaysAssert(it != d_lazyFactMap.end());
  // now go back and convert it to proof steps and add to proof
  std::shared_ptr<DatatypesInference> di = (*it).second;
  // run the conversion
  convert(di->getId(), di->d_conc, di->d_exp, &pf);
  return pf.getProofFor(fact);
}

std::string InferProofCons::identify() const
{
  return "datatypes::InferProofCons";
}

}  // namespace datatypes
}  // 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, Aina Niemetz
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		* Implementation of inference to proof conversion for datatypes.
14		*/
15
16		#include "theory/datatypes/infer_proof_cons.h"
17
18		#include "proof/proof.h"
19		#include "proof/proof_checker.h"
20		#include "theory/datatypes/theory_datatypes_utils.h"
21		#include "theory/model_manager.h"
22		#include "theory/rewriter.h"
23		#include "util/rational.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace datatypes {
30
31	2449	InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm)
32	2449	: d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c)
33		{
34	2449	Assert(d_pnm != nullptr);
35	2449	}
36
37	13827	void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
38		{
39	27581	TNode fact = di->d_conc;
40	13827	if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
41		{
42	70	return;
43		}
44	27511	Node symFact = CDProof::getSymmFact(fact);
45	13757	if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
46		{
47	3	return;
48		}
49	13754	d_lazyFactMap.insert(fact, di);
50		}
51
52	6723	void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp)
53		{
54	13446	Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp
55	6723	<< std::endl;
56		// split into vector
57	13446	std::vector<Node> expv;
58	6723	if (!exp.isNull() && !exp.isConst())
59		{
60	5293	if (exp.getKind() == AND)
61		{
62	367	for (const Node& ec : exp)
63		{
64	266	expv.push_back(ec);
65		}
66		}
67		else
68		{
69	5192	expv.push_back(exp);
70		}
71		}
72	6723	NodeManager* nm = NodeManager::currentNM();
73	6723	bool success = false;
74	6723	switch (infer)
75		{
76	793	case InferenceId::DATATYPES_UNIF:
77		{
78	793	Assert(expv.size() == 1);
79	793	Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR
80		&& exp[1].getKind() == APPLY_CONSTRUCTOR
81		&& exp[0].getOperator() == exp[1].getOperator());
82	1586	Node narg;
83		// we may be asked for a proof of (not P) coming from (= P false) or
84		// (= false P), or similarly P from (= P true) or (= true P).
85	793	bool concPol = conc.getKind() != NOT;
86	1586	Node concAtom = concPol ? conc : conc[0];
87	1586	Node unifConc = conc;
88	1298	for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++)
89		{
90	1297	bool argSuccess = false;
91	1297	if (conc.getKind() == EQUAL)
92		{
93	1297	argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]);
94		}
95		else
96		{
97		for (size_t j = 0; j < 2; j++)
98		{
99		if (exp[j][i] == concAtom && exp[1 - j][i].isConst()
100		&& exp[1 - j][i].getConst<bool>() == concPol)
101		{
102		argSuccess = true;
103		unifConc = exp[0][i].eqNode(exp[1][i]);
104		break;
105		}
106		}
107		}
108	1297	if (argSuccess)
109		{
110	792	narg = nm->mkConst(Rational(i));
111	792	break;
112		}
113		}
114	793	if (!narg.isNull())
115		{
116	792	if (conc.getKind() == EQUAL)
117		{
118		// normal case where we conclude an equality
119	792	cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg});
120		}
121		else
122		{
123		// must use true or false elim to prove the final
124		cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg});
125		// may use symmetry
126		Node eq = concAtom.eqNode(nm->mkConst(concPol));
127		cdp->addStep(
128		conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {});
129		}
130	792	success = true;
131	793	}
132		}
133	793	break;
134	3141	case InferenceId::DATATYPES_INST:
135		{
136	3141	if (expv.size() == 1)
137		{
138	2819	Assert(conc.getKind() == EQUAL);
139	2819	int n = utils::isTester(exp);
140	2819	if (n >= 0)
141		{
142	5638	Node t = exp[0];
143	5638	Node nn = nm->mkConst(Rational(n));
144	5638	Node eq = exp.eqNode(conc);
145	2819	cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
146	2819	cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});
147	2819	success = true;
148		}
149		}
150		}
151	3141	break;
152	1108	case InferenceId::DATATYPES_SPLIT:
153		{
154	1108	Assert(expv.empty());
155	2216	Node t = conc.getKind() == OR ? conc[0][0] : conc[0];
156	1108	cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t});
157	2216	success = true;
158		}
159	1108	break;
160	1334	case InferenceId::DATATYPES_COLLAPSE_SEL:
161		{
162	1334	Assert(exp.getKind() == EQUAL);
163	2668	Node concEq = conc;
164		// might be a Boolean conclusion
165	1334	if (conc.getKind() != EQUAL)
166		{
167	51	bool concPol = conc.getKind() != NOT;
168	102	Node concAtom = concPol ? conc : conc[0];
169	51	concEq = concAtom.eqNode(nm->mkConst(concPol));
170		}
171	1334	Assert(concEq.getKind() == EQUAL
172		&& concEq[0].getKind() == APPLY_SELECTOR_TOTAL);
173	1334	Assert(exp[0].getType().isDatatype());
174	2668	Node sop = concEq[0].getOperator();
175	2668	Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
176	2668	Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
177		// exp[0] = exp[1]
178		// --------------------- CONG ----------------- DT_COLLAPSE
179		// s(exp[0]) = s(exp[1]) s(exp[1]) = r
180		// --------------------------------------------------- TRANS
181		// s(exp[0]) = r
182	2668	Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
183	2668	Node seq = sl.eqNode(sr);
184	1334	cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
185	2668	Node sceq = sr.eqNode(concEq[1]);
186	1334	cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
187	1334	cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
188	1334	if (conc.getKind() != EQUAL)
189		{
190		PfRule eid =
191	51	conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
192	51	cdp->addStep(conc, eid, {concEq}, {});
193		}
194	2668	success = true;
195		}
196	1334	break;
197	124	case InferenceId::DATATYPES_CLASH_CONFLICT:
198		{
199	124	cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {});
200	124	success = true;
201		}
202	124	break;
203	78	case InferenceId::DATATYPES_TESTER_CONFLICT:
204		{
205		// rewrites to false under substitution
206	156	Node fn = nm->mkConst(false);
207	78	cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {});
208	156	success = true;
209		}
210	78	break;
211		case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
212		{
213		Assert(expv.size() == 3);
214		Node tester1 = expv[0];
215		Node tester1c =
216		nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]);
217		cdp->addStep(tester1c,
218		PfRule::MACRO_SR_PRED_TRANSFORM,
219		{expv[1], expv[2]},
220		{tester1c});
221		Node fn = nm->mkConst(false);
222		cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {});
223		success = true;
224		}
225		break;
226		case InferenceId::DATATYPES_PURIFY:
227		{
228		cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {});
229		success = true;
230		}
231		break;
232		// inferences currently not supported
233	145	case InferenceId::DATATYPES_LABEL_EXH:
234		case InferenceId::DATATYPES_BISIMILAR:
235		case InferenceId::DATATYPES_CYCLE:
236		default:
237	290	Trace("dt-ipc") << "...no conversion for inference " << infer
238	145	<< std::endl;
239	145	break;
240		}
241
242	6723	if (!success)
243		{
244		// failed to reconstruct, add trust
245	468	Trace("dt-ipc") << "...failed " << infer << std::endl;
246	468	cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
247		}
248		else
249		{
250	6255	Trace("dt-ipc") << "...success" << std::endl;
251		}
252	6723	}
253
254	6723	std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
255		{
256	6723	Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl;
257		// temporary proof
258	13446	CDProof pf(d_pnm);
259		// get the inference
260	6723	NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact);
261	6723	if (it == d_lazyFactMap.end())
262		{
263		Node factSym = CDProof::getSymmFact(fact);
264		if (!factSym.isNull())
265		{
266		// Use the symmetric fact. There is no need to explictly make a
267		// SYMM proof, as this is handled by CDProof::getProofFor below.
268		it = d_lazyFactMap.find(factSym);
269		}
270		}
271	6723	AlwaysAssert(it != d_lazyFactMap.end());
272		// now go back and convert it to proof steps and add to proof
273	13446	std::shared_ptr<DatatypesInference> di = (*it).second;
274		// run the conversion
275	6723	convert(di->getId(), di->d_conc, di->d_exp, &pf);
276	13446	return pf.getProofFor(fact);
277		}
278
279	16328	std::string InferProofCons::identify() const
280		{
281	16328	return "datatypes::InferProofCons";
282		}
283
284		} // namespace datatypes
285		} // namespace theory
286	29337	} // namespace cvc5