Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/proof_checker.cpp	Lines:	58	72	80.6 %
Date:	2021-05-22	Branches:	126	470	26.8 %


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

#include "theory/datatypes/proof_checker.h"

#include "expr/dtype_cons.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace datatypes {

void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
{
  pc->registerChecker(PfRule::DT_UNIF, this);
  pc->registerChecker(PfRule::DT_INST, this);
  pc->registerChecker(PfRule::DT_COLLAPSE, this);
  pc->registerChecker(PfRule::DT_SPLIT, this);
  pc->registerChecker(PfRule::DT_CLASH, this);
  // trusted rules
  pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
}

Node DatatypesProofRuleChecker::checkInternal(PfRule id,
                                              const std::vector<Node>& children,
                                              const std::vector<Node>& args)
{
  NodeManager* nm = NodeManager::currentNM();
  if (id == PfRule::DT_UNIF)
  {
    Assert(children.size() == 1);
    Assert(args.size() == 1);
    uint32_t i;
    if (children[0].getKind() != kind::EQUAL
        || children[0][0].getKind() != kind::APPLY_CONSTRUCTOR
        || children[0][1].getKind() != kind::APPLY_CONSTRUCTOR
        || children[0][0].getOperator() != children[0][1].getOperator()
        || !getUInt32(args[0], i))
    {
      return Node::null();
    }
    if (i >= children[0][0].getNumChildren())
    {
      return Node::null();
    }
    Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren());
    return children[0][0][i].eqNode(children[0][1][i]);
  }
  else if (id == PfRule::DT_INST)
  {
    Assert(children.empty());
    Assert(args.size() == 2);
    Node t = args[0];
    TypeNode tn = t.getType();
    uint32_t i;
    if (!tn.isDatatype() || !getUInt32(args[1], i))
    {
      return Node::null();
    }
    const DType& dt = tn.getDType();
    if (i >= dt.getNumConstructors())
    {
      return Node::null();
    }
    Node tester = utils::mkTester(t, i, dt);
    Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
    return tester.eqNode(t.eqNode(ticons));
  }
  else if (id == PfRule::DT_COLLAPSE)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    Node t = args[0];
    if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
        || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
    {
      return Node::null();
    }
    Node selector = t.getOperator();
    size_t constructorIndex = utils::indexOf(t[0].getOperator());
    const DType& dt = utils::datatypeOf(selector);
    const DTypeConstructor& dtc = dt[constructorIndex];
    int selectorIndex = dtc.getSelectorIndexInternal(selector);
    Node r =
        selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
    return t.eqNode(r);
  }
  else if (id == PfRule::DT_SPLIT)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    TypeNode tn = args[0].getType();
    if (!tn.isDatatype())
    {
      return Node::null();
    }
    const DType& dt = tn.getDType();
    return utils::mkSplit(args[0], dt);
  }
  else if (id == PfRule::DT_CLASH)
  {
    Assert(children.size() == 2);
    Assert(args.empty());
    if (children[0].getKind() != kind::APPLY_TESTER
        || children[1].getKind() != kind::APPLY_TESTER
        || children[0][0] != children[1][0] || children[0] == children[1])
    {
      return Node::null();
    }
    return nm->mkConst(false);
  }
  else if (id == PfRule::DT_TRUST)
  {
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }
  // no rule
  return Node::null();
}

}  // 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
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 datatypes proof checker.
14		*/
15
16		#include "theory/datatypes/proof_checker.h"
17
18		#include "expr/dtype_cons.h"
19		#include "theory/datatypes/theory_datatypes_utils.h"
20		#include "theory/rewriter.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace datatypes {
25
26	3600	void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
27		{
28	3600	pc->registerChecker(PfRule::DT_UNIF, this);
29	3600	pc->registerChecker(PfRule::DT_INST, this);
30	3600	pc->registerChecker(PfRule::DT_COLLAPSE, this);
31	3600	pc->registerChecker(PfRule::DT_SPLIT, this);
32	3600	pc->registerChecker(PfRule::DT_CLASH, this);
33		// trusted rules
34	3600	pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
35	3600	}
36
37	9300	Node DatatypesProofRuleChecker::checkInternal(PfRule id,
38		const std::vector<Node>& children,
39		const std::vector<Node>& args)
40		{
41	9300	NodeManager* nm = NodeManager::currentNM();
42	9300	if (id == PfRule::DT_UNIF)
43		{
44	702	Assert(children.size() == 1);
45	702	Assert(args.size() == 1);
46		uint32_t i;
47	1404	if (children[0].getKind() != kind::EQUAL
48	1404	\|\| children[0][0].getKind() != kind::APPLY_CONSTRUCTOR
49	1404	\|\| children[0][1].getKind() != kind::APPLY_CONSTRUCTOR
50	1404	\|\| children[0][0].getOperator() != children[0][1].getOperator()
51	2106	\|\| !getUInt32(args[0], i))
52		{
53		return Node::null();
54		}
55	702	if (i >= children[0][0].getNumChildren())
56		{
57		return Node::null();
58		}
59	702	Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren());
60	702	return children[0][0][i].eqNode(children[0][1][i]);
61		}
62	8598	else if (id == PfRule::DT_INST)
63		{
64	3167	Assert(children.empty());
65	3167	Assert(args.size() == 2);
66	6334	Node t = args[0];
67	6334	TypeNode tn = t.getType();
68		uint32_t i;
69	3167	if (!tn.isDatatype() \|\| !getUInt32(args[1], i))
70		{
71		return Node::null();
72		}
73	3167	const DType& dt = tn.getDType();
74	3167	if (i >= dt.getNumConstructors())
75		{
76		return Node::null();
77		}
78	6334	Node tester = utils::mkTester(t, i, dt);
79	6334	Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
80	3167	return tester.eqNode(t.eqNode(ticons));
81		}
82	5431	else if (id == PfRule::DT_COLLAPSE)
83		{
84	3652	Assert(children.empty());
85	3652	Assert(args.size() == 1);
86	7304	Node t = args[0];
87	7304	if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
88	7304	\|\| t[0].getKind() != kind::APPLY_CONSTRUCTOR)
89		{
90		return Node::null();
91		}
92	7304	Node selector = t.getOperator();
93	3652	size_t constructorIndex = utils::indexOf(t[0].getOperator());
94	3652	const DType& dt = utils::datatypeOf(selector);
95	3652	const DTypeConstructor& dtc = dt[constructorIndex];
96	3652	int selectorIndex = dtc.getSelectorIndexInternal(selector);
97		Node r =
98	7304	selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
99	3652	return t.eqNode(r);
100		}
101	1779	else if (id == PfRule::DT_SPLIT)
102		{
103	1324	Assert(children.empty());
104	1324	Assert(args.size() == 1);
105	2648	TypeNode tn = args[0].getType();
106	1324	if (!tn.isDatatype())
107		{
108		return Node::null();
109		}
110	1324	const DType& dt = tn.getDType();
111	1324	return utils::mkSplit(args[0], dt);
112		}
113	455	else if (id == PfRule::DT_CLASH)
114		{
115		Assert(children.size() == 2);
116		Assert(args.empty());
117		if (children[0].getKind() != kind::APPLY_TESTER
118		\|\| children[1].getKind() != kind::APPLY_TESTER
119		\|\| children[0][0] != children[1][0] \|\| children[0] == children[1])
120		{
121		return Node::null();
122		}
123		return nm->mkConst(false);
124		}
125	455	else if (id == PfRule::DT_TRUST)
126		{
127	455	Assert(!args.empty());
128	455	Assert(args[0].getType().isBoolean());
129	455	return args[0];
130		}
131		// no rule
132		return Node::null();
133		}
134
135		} // namespace datatypes
136		} // namespace theory
137	28191	} // namespace cvc5