Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/proof_checker.cpp	Lines:	102	115	88.7 %
Date:	2021-05-22	Branches:	175	564	31.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, 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 equality proof checker.
 */

#include "theory/uf/proof_checker.h"

#include "theory/uf/theory_uf_rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace uf {

void UfProofRuleChecker::registerTo(ProofChecker* pc)
{
  // add checkers
  pc->registerChecker(PfRule::REFL, this);
  pc->registerChecker(PfRule::SYMM, this);
  pc->registerChecker(PfRule::TRANS, this);
  pc->registerChecker(PfRule::CONG, this);
  pc->registerChecker(PfRule::TRUE_INTRO, this);
  pc->registerChecker(PfRule::TRUE_ELIM, this);
  pc->registerChecker(PfRule::FALSE_INTRO, this);
  pc->registerChecker(PfRule::FALSE_ELIM, this);
  pc->registerChecker(PfRule::HO_CONG, this);
  pc->registerChecker(PfRule::HO_APP_ENCODE, this);
}

Node UfProofRuleChecker::checkInternal(PfRule id,
                                       const std::vector<Node>& children,
                                       const std::vector<Node>& args)
{
  // compute what was proven
  if (id == PfRule::REFL)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    return args[0].eqNode(args[0]);
  }
  else if (id == PfRule::SYMM)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    bool polarity = children[0].getKind() != NOT;
    Node eqp = polarity ? children[0] : children[0][0];
    if (eqp.getKind() != EQUAL)
    {
      // not a (dis)equality
      return Node::null();
    }
    Node conc = eqp[1].eqNode(eqp[0]);
    return polarity ? conc : conc.notNode();
  }
  else if (id == PfRule::TRANS)
  {
    Assert(children.size() > 0);
    Assert(args.empty());
    Node first;
    Node curr;
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
    {
      Node eqp = children[i];
      if (eqp.getKind() != EQUAL)
      {
        return Node::null();
      }
      if (first.isNull())
      {
        first = eqp[0];
      }
      else if (eqp[0] != curr)
      {
        return Node::null();
      }
      curr = eqp[1];
    }
    return first.eqNode(curr);
  }
  else if (id == PfRule::CONG)
  {
    Assert(children.size() > 0);
    Assert(args.size() >= 1 && args.size() <= 2);
    // We do congruence over builtin kinds using operatorToKind
    std::vector<Node> lchildren;
    std::vector<Node> rchildren;
    // get the kind encoded as args[0]
    Kind k;
    if (!getKind(args[0], k))
    {
      return Node::null();
    }
    if (k == kind::UNDEFINED_KIND)
    {
      return Node::null();
    }
    Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k
                        << ", metakind=" << kind::metaKindOf(k) << std::endl;
    if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
    {
      if (args.size() <= 1)
      {
        return Node::null();
      }
      // parameterized kinds require the operator
      lchildren.push_back(args[1]);
      rchildren.push_back(args[1]);
    }
    else if (args.size() > 1)
    {
      return Node::null();
    }
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
    {
      Node eqp = children[i];
      if (eqp.getKind() != EQUAL)
      {
        return Node::null();
      }
      lchildren.push_back(eqp[0]);
      rchildren.push_back(eqp[1]);
    }
    NodeManager* nm = NodeManager::currentNM();
    Node l = nm->mkNode(k, lchildren);
    Node r = nm->mkNode(k, rchildren);
    return l.eqNode(r);
  }
  else if (id == PfRule::TRUE_INTRO)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    Node trueNode = NodeManager::currentNM()->mkConst(true);
    return children[0].eqNode(trueNode);
  }
  else if (id == PfRule::TRUE_ELIM)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
        || !children[0][1].getConst<bool>())
    {
      return Node::null();
    }
    return children[0][0];
  }
  else if (id == PfRule::FALSE_INTRO)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    if (children[0].getKind() != kind::NOT)
    {
      return Node::null();
    }
    Node falseNode = NodeManager::currentNM()->mkConst(false);
    return children[0][0].eqNode(falseNode);
  }
  else if (id == PfRule::FALSE_ELIM)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
        || children[0][1].getConst<bool>())
    {
      return Node::null();
    }
    return children[0][0].notNode();
  }
  if (id == PfRule::HO_CONG)
  {
    Assert(children.size() > 0);
    std::vector<Node> lchildren;
    std::vector<Node> rchildren;
    for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
    {
      Node eqp = children[i];
      if (eqp.getKind() != EQUAL)
      {
        return Node::null();
      }
      lchildren.push_back(eqp[0]);
      rchildren.push_back(eqp[1]);
    }
    NodeManager* nm = NodeManager::currentNM();
    Node l = nm->mkNode(kind::APPLY_UF, lchildren);
    Node r = nm->mkNode(kind::APPLY_UF, rchildren);
    return l.eqNode(r);
  }
  else if (id == PfRule::HO_APP_ENCODE)
  {
    Assert(args.size() == 1);
    Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
    return args[0].eqNode(ret);
  }
  // no rule
  return Node::null();
}

}  // namespace uf
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, Andrew Reynolds, 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 equality proof checker.
14		*/
15
16		#include "theory/uf/proof_checker.h"
17
18		#include "theory/uf/theory_uf_rewriter.h"
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23		namespace theory {
24		namespace uf {
25
26	3600	void UfProofRuleChecker::registerTo(ProofChecker* pc)
27		{
28		// add checkers
29	3600	pc->registerChecker(PfRule::REFL, this);
30	3600	pc->registerChecker(PfRule::SYMM, this);
31	3600	pc->registerChecker(PfRule::TRANS, this);
32	3600	pc->registerChecker(PfRule::CONG, this);
33	3600	pc->registerChecker(PfRule::TRUE_INTRO, this);
34	3600	pc->registerChecker(PfRule::TRUE_ELIM, this);
35	3600	pc->registerChecker(PfRule::FALSE_INTRO, this);
36	3600	pc->registerChecker(PfRule::FALSE_ELIM, this);
37	3600	pc->registerChecker(PfRule::HO_CONG, this);
38	3600	pc->registerChecker(PfRule::HO_APP_ENCODE, this);
39	3600	}
40
41	2078013	Node UfProofRuleChecker::checkInternal(PfRule id,
42		const std::vector<Node>& children,
43		const std::vector<Node>& args)
44		{
45		// compute what was proven
46	2078013	if (id == PfRule::REFL)
47		{
48	545645	Assert(children.empty());
49	545645	Assert(args.size() == 1);
50	545645	return args[0].eqNode(args[0]);
51		}
52	1532368	else if (id == PfRule::SYMM)
53		{
54	663853	Assert(children.size() == 1);
55	663853	Assert(args.empty());
56	663853	bool polarity = children[0].getKind() != NOT;
57	1327706	Node eqp = polarity ? children[0] : children[0][0];
58	663853	if (eqp.getKind() != EQUAL)
59		{
60		// not a (dis)equality
61		return Node::null();
62		}
63	1327706	Node conc = eqp[1].eqNode(eqp[0]);
64	663853	return polarity ? conc : conc.notNode();
65		}
66	868515	else if (id == PfRule::TRANS)
67		{
68	277025	Assert(children.size() > 0);
69	277025	Assert(args.empty());
70	554050	Node first;
71	554050	Node curr;
72	1048729	for (size_t i = 0, nchild = children.size(); i < nchild; i++)
73		{
74	1543408	Node eqp = children[i];
75	771704	if (eqp.getKind() != EQUAL)
76		{
77		return Node::null();
78		}
79	771704	if (first.isNull())
80		{
81	277025	first = eqp[0];
82		}
83	494679	else if (eqp[0] != curr)
84		{
85		return Node::null();
86		}
87	771704	curr = eqp[1];
88		}
89	277025	return first.eqNode(curr);
90		}
91	591490	else if (id == PfRule::CONG)
92		{
93	543675	Assert(children.size() > 0);
94	543675	Assert(args.size() >= 1 && args.size() <= 2);
95		// We do congruence over builtin kinds using operatorToKind
96	1087350	std::vector<Node> lchildren;
97	1087350	std::vector<Node> rchildren;
98		// get the kind encoded as args[0]
99		Kind k;
100	543675	if (!getKind(args[0], k))
101		{
102		return Node::null();
103		}
104	543675	if (k == kind::UNDEFINED_KIND)
105		{
106		return Node::null();
107		}
108	1087350	Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k
109	543675	<< ", metakind=" << kind::metaKindOf(k) << std::endl;
110	543675	if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
111		{
112	190543	if (args.size() <= 1)
113		{
114		return Node::null();
115		}
116		// parameterized kinds require the operator
117	190543	lchildren.push_back(args[1]);
118	190543	rchildren.push_back(args[1]);
119		}
120	353132	else if (args.size() > 1)
121		{
122		return Node::null();
123		}
124	1979104	for (size_t i = 0, nchild = children.size(); i < nchild; i++)
125		{
126	2870858	Node eqp = children[i];
127	1435429	if (eqp.getKind() != EQUAL)
128		{
129		return Node::null();
130		}
131	1435429	lchildren.push_back(eqp[0]);
132	1435429	rchildren.push_back(eqp[1]);
133		}
134	543675	NodeManager* nm = NodeManager::currentNM();
135	1087350	Node l = nm->mkNode(k, lchildren);
136	1087350	Node r = nm->mkNode(k, rchildren);
137	543675	return l.eqNode(r);
138		}
139	47815	else if (id == PfRule::TRUE_INTRO)
140		{
141	7866	Assert(children.size() == 1);
142	7866	Assert(args.empty());
143	15732	Node trueNode = NodeManager::currentNM()->mkConst(true);
144	7866	return children[0].eqNode(trueNode);
145		}
146	39949	else if (id == PfRule::TRUE_ELIM)
147		{
148	21269	Assert(children.size() == 1);
149	21269	Assert(args.empty());
150	63807	if (children[0].getKind() != EQUAL \|\| !children[0][1].isConst()
151	63807	\|\| !children[0][1].getConst<bool>())
152		{
153		return Node::null();
154		}
155	21269	return children[0][0];
156		}
157	18680	else if (id == PfRule::FALSE_INTRO)
158		{
159	13766	Assert(children.size() == 1);
160	13766	Assert(args.empty());
161	13766	if (children[0].getKind() != kind::NOT)
162		{
163		return Node::null();
164		}
165	27532	Node falseNode = NodeManager::currentNM()->mkConst(false);
166	13766	return children[0][0].eqNode(falseNode);
167		}
168	4914	else if (id == PfRule::FALSE_ELIM)
169		{
170	4619	Assert(children.size() == 1);
171	4619	Assert(args.empty());
172	13857	if (children[0].getKind() != EQUAL \|\| !children[0][1].isConst()
173	13857	\|\| children[0][1].getConst<bool>())
174		{
175		return Node::null();
176		}
177	4619	return children[0][0].notNode();
178		}
179	295	if (id == PfRule::HO_CONG)
180		{
181	259	Assert(children.size() > 0);
182	518	std::vector<Node> lchildren;
183	518	std::vector<Node> rchildren;
184	969	for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
185		{
186	1420	Node eqp = children[i];
187	710	if (eqp.getKind() != EQUAL)
188		{
189		return Node::null();
190		}
191	710	lchildren.push_back(eqp[0]);
192	710	rchildren.push_back(eqp[1]);
193		}
194	259	NodeManager* nm = NodeManager::currentNM();
195	518	Node l = nm->mkNode(kind::APPLY_UF, lchildren);
196	518	Node r = nm->mkNode(kind::APPLY_UF, rchildren);
197	259	return l.eqNode(r);
198		}
199	36	else if (id == PfRule::HO_APP_ENCODE)
200		{
201	36	Assert(args.size() == 1);
202	72	Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
203	36	return args[0].eqNode(ret);
204		}
205		// no rule
206		return Node::null();
207		}
208
209		} // namespace uf
210		} // namespace theory
211	28194	} // namespace cvc5