Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/infer_proof_cons.cpp	Lines:	115	143	80.4 %
Date:	2021-05-22	Branches:	311	893	34.8 %


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