Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/proof_checker.cpp	Lines:	62	85	72.9 %
Date:	2021-11-07	Branches:	99	378	26.2 %


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

#include "theory/quantifiers/proof_checker.h"

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "theory/builtin/proof_checker.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
{
  // add checkers
  pc->registerChecker(PfRule::SKOLEM_INTRO, this);
  pc->registerChecker(PfRule::EXISTS_INTRO, this);
  pc->registerChecker(PfRule::SKOLEMIZE, this);
  pc->registerChecker(PfRule::INSTANTIATE, this);
  pc->registerChecker(PfRule::ALPHA_EQUIV, this);
  // trusted rules
  pc->registerTrustedChecker(PfRule::QUANTIFIERS_PREPROCESS, this, 3);
}

Node QuantifiersProofRuleChecker::checkInternal(
    PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  // compute what was proven
  if (id == PfRule::EXISTS_INTRO)
  {
    Assert(children.size() == 1);
    Assert(args.size() == 1);
    Node p = children[0];
    Node exists = args[0];
    if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1)
    {
      return Node::null();
    }
    std::unordered_map<Node, Node> subs;
    if (!expr::match(exists[1], p, subs))
    {
      return Node::null();
    }
    // substitution must contain only the variable of the existential
    for (const std::pair<const Node, Node>& s : subs)
    {
      if (s.first != exists[0][0])
      {
        return Node::null();
      }
    }
    return exists;
  }
  else if (id == PfRule::SKOLEM_INTRO)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    Node t = SkolemManager::getOriginalForm(args[0]);
    return args[0].eqNode(t);
  }
  else if (id == PfRule::SKOLEMIZE)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    // can use either negated FORALL or EXISTS
    if (children[0].getKind() != EXISTS
        && (children[0].getKind() != NOT || children[0][0].getKind() != FORALL))
    {
      return Node::null();
    }
    Node exists;
    if (children[0].getKind() == EXISTS)
    {
      exists = children[0];
    }
    else
    {
      std::vector<Node> echildren(children[0][0].begin(), children[0][0].end());
      echildren[1] = echildren[1].notNode();
      exists = nm->mkNode(EXISTS, echildren);
    }
    std::vector<Node> skolems;
    Node res = sm->mkSkolemize(exists, skolems, "k");
    return res;
  }
  else if (id == PfRule::INSTANTIATE)
  {
    Assert(children.size() == 1);
    // note we may have more arguments than just the term vector
    if (children[0].getKind() != FORALL
        || args.size() < children[0][0].getNumChildren())
    {
      return Node::null();
    }
    Node body = children[0][1];
    std::vector<Node> vars;
    std::vector<Node> subs;
    for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++)
    {
      vars.push_back(children[0][0][i]);
      subs.push_back(args[i]);
    }
    Node inst =
        body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
    return inst;
  }
  else if (id == PfRule::ALPHA_EQUIV)
  {
    Assert(children.empty());
    if (args[0].getKind() != kind::FORALL)
    {
      return Node::null();
    }
    // arguments must be equalities that are bound variables that are
    // pairwise unique
    std::unordered_set<Node> allVars[2];
    std::vector<Node> vars;
    std::vector<Node> newVars;
    for (size_t i = 1, nargs = args.size(); i < nargs; i++)
    {
      if (args[i].getKind() != kind::EQUAL)
      {
        return Node::null();
      }
      for (size_t j = 0; j < 2; j++)
      {
        Node v = args[i][j];
        if (v.getKind() != kind::BOUND_VARIABLE
            || allVars[j].find(v) != allVars[j].end())
        {
          return Node::null();
        }
        allVars[j].insert(v);
      }
      vars.push_back(args[i][0]);
      newVars.push_back(args[i][1]);
    }
    Node renamedBody = args[0].substitute(
        vars.begin(), vars.end(), newVars.begin(), newVars.end());
    return args[0].eqNode(renamedBody);
  }
  else if (id == PfRule::QUANTIFIERS_PREPROCESS)
  {
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }

  // no rule
  return Node::null();
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* 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 quantifiers proof checker.
14		*/
15
16		#include "theory/quantifiers/proof_checker.h"
17
18		#include "expr/node_algorithm.h"
19		#include "expr/skolem_manager.h"
20		#include "theory/builtin/proof_checker.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28	7989	void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
29		{
30		// add checkers
31	7989	pc->registerChecker(PfRule::SKOLEM_INTRO, this);
32	7989	pc->registerChecker(PfRule::EXISTS_INTRO, this);
33	7989	pc->registerChecker(PfRule::SKOLEMIZE, this);
34	7989	pc->registerChecker(PfRule::INSTANTIATE, this);
35	7989	pc->registerChecker(PfRule::ALPHA_EQUIV, this);
36		// trusted rules
37	7989	pc->registerTrustedChecker(PfRule::QUANTIFIERS_PREPROCESS, this, 3);
38	7989	}
39
40	6512	Node QuantifiersProofRuleChecker::checkInternal(
41		PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
42		{
43	6512	NodeManager* nm = NodeManager::currentNM();
44	6512	SkolemManager* sm = nm->getSkolemManager();
45		// compute what was proven
46	6512	if (id == PfRule::EXISTS_INTRO)
47		{
48		Assert(children.size() == 1);
49		Assert(args.size() == 1);
50		Node p = children[0];
51		Node exists = args[0];
52		if (exists.getKind() != kind::EXISTS \|\| exists[0].getNumChildren() != 1)
53		{
54		return Node::null();
55		}
56		std::unordered_map<Node, Node> subs;
57		if (!expr::match(exists[1], p, subs))
58		{
59		return Node::null();
60		}
61		// substitution must contain only the variable of the existential
62		for (const std::pair<const Node, Node>& s : subs)
63		{
64		if (s.first != exists[0][0])
65		{
66		return Node::null();
67		}
68		}
69		return exists;
70		}
71	6512	else if (id == PfRule::SKOLEM_INTRO)
72		{
73	4981	Assert(children.empty());
74	4981	Assert(args.size() == 1);
75	9962	Node t = SkolemManager::getOriginalForm(args[0]);
76	4981	return args[0].eqNode(t);
77		}
78	1531	else if (id == PfRule::SKOLEMIZE)
79		{
80	198	Assert(children.size() == 1);
81	198	Assert(args.empty());
82		// can use either negated FORALL or EXISTS
83	396	if (children[0].getKind() != EXISTS
84	396	&& (children[0].getKind() != NOT \|\| children[0][0].getKind() != FORALL))
85		{
86		return Node::null();
87		}
88	396	Node exists;
89	198	if (children[0].getKind() == EXISTS)
90		{
91	38	exists = children[0];
92		}
93		else
94		{
95	320	std::vector<Node> echildren(children[0][0].begin(), children[0][0].end());
96	160	echildren[1] = echildren[1].notNode();
97	160	exists = nm->mkNode(EXISTS, echildren);
98		}
99	396	std::vector<Node> skolems;
100	396	Node res = sm->mkSkolemize(exists, skolems, "k");
101	198	return res;
102		}
103	1333	else if (id == PfRule::INSTANTIATE)
104		{
105	1311	Assert(children.size() == 1);
106		// note we may have more arguments than just the term vector
107	2622	if (children[0].getKind() != FORALL
108	2622	\|\| args.size() < children[0][0].getNumChildren())
109		{
110		return Node::null();
111		}
112	2622	Node body = children[0][1];
113	2622	std::vector<Node> vars;
114	2622	std::vector<Node> subs;
115	4575	for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++)
116		{
117	3264	vars.push_back(children[0][0][i]);
118	3264	subs.push_back(args[i]);
119		}
120		Node inst =
121	2622	body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
122	1311	return inst;
123		}
124	22	else if (id == PfRule::ALPHA_EQUIV)
125		{
126	22	Assert(children.empty());
127	22	if (args[0].getKind() != kind::FORALL)
128		{
129		return Node::null();
130		}
131		// arguments must be equalities that are bound variables that are
132		// pairwise unique
133	44	std::unordered_set<Node> allVars[2];
134	44	std::vector<Node> vars;
135	44	std::vector<Node> newVars;
136	55	for (size_t i = 1, nargs = args.size(); i < nargs; i++)
137		{
138	33	if (args[i].getKind() != kind::EQUAL)
139		{
140		return Node::null();
141		}
142	99	for (size_t j = 0; j < 2; j++)
143		{
144	132	Node v = args[i][j];
145	132	if (v.getKind() != kind::BOUND_VARIABLE
146	66	\|\| allVars[j].find(v) != allVars[j].end())
147		{
148		return Node::null();
149		}
150	66	allVars[j].insert(v);
151		}
152	33	vars.push_back(args[i][0]);
153	33	newVars.push_back(args[i][1]);
154		}
155	22	Node renamedBody = args[0].substitute(
156	44	vars.begin(), vars.end(), newVars.begin(), newVars.end());
157	22	return args[0].eqNode(renamedBody);
158		}
159		else if (id == PfRule::QUANTIFIERS_PREPROCESS)
160		{
161		Assert(!args.empty());
162		Assert(args[0].getType().isBoolean());
163		return args[0];
164		}
165
166		// no rule
167		return Node::null();
168		}
169
170		} // namespace quantifiers
171		} // namespace theory
172	31137	} // namespace cvc5