Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/infer_proof_cons.cpp	Lines:	111	144	77.1 %
Date:	2021-09-07	Branches:	298	895	33.3 %


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