Head

GCC Code Coverage Report

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