Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/builtin/proof_checker.cpp	Lines:	171	220	77.7 %
Date:	2021-09-07	Branches:	303	958	31.6 %


/******************************************************************************
 * 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 equality proof checker.
 */

#include "theory/builtin/proof_checker.h"

#include "expr/skolem_manager.h"
#include "smt/env.h"
#include "smt/term_formula_removal.h"
#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
#include "theory/theory.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace builtin {

BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env) {}

void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
{
  pc->registerChecker(PfRule::ASSUME, this);
  pc->registerChecker(PfRule::SCOPE, this);
  pc->registerChecker(PfRule::SUBS, this);
  pc->registerChecker(PfRule::REWRITE, this);
  pc->registerChecker(PfRule::EVALUATE, this);
  pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
  pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
  pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
  pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
  pc->registerChecker(PfRule::THEORY_REWRITE, this);
  pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
  // trusted rules
  pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
  pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
  pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
  pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
  pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
  pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
  pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3);
}

Node BuiltinProofRuleChecker::applySubstitutionRewrite(
    Node n,
    const std::vector<Node>& exp,
    MethodId ids,
    MethodId ida,
    MethodId idr)
{
  Node nks = applySubstitution(n, exp, ids, ida);
  return applyRewrite(nks, idr);
}

Node BuiltinProofRuleChecker::applyRewrite(TNode n, MethodId idr)
{
  return d_env.getRewriter()->rewriteViaMethod(n, idr);
}

bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
                                                    TNode& var,
                                                    TNode& subs,
                                                    MethodId ids)
{
  if (ids == MethodId::SB_DEFAULT)
  {
    if (exp.getKind() != EQUAL)
    {
      return false;
    }
    var = exp[0];
    subs = exp[1];
  }
  else if (ids == MethodId::SB_LITERAL)
  {
    bool polarity = exp.getKind() != NOT;
    var = polarity ? exp : exp[0];
    subs = NodeManager::currentNM()->mkConst(polarity);
  }
  else if (ids == MethodId::SB_FORMULA)
  {
    var = exp;
    subs = NodeManager::currentNM()->mkConst(true);
  }
  else
  {
    Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
                     "substitution for "
                  << ids << std::endl;
    return false;
  }
  return true;
}

bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
                                                 std::vector<TNode>& vars,
                                                 std::vector<TNode>& subs,
                                                 std::vector<TNode>& from,
                                                 MethodId ids)
{
  TNode v;
  TNode s;
  if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
  {
    for (const Node& ec : exp)
    {
      // non-recursive, do not use nested AND
      if (!getSubstitutionForLit(ec, v, s, ids))
      {
        return false;
      }
      vars.push_back(v);
      subs.push_back(s);
      from.push_back(ec);
    }
    return true;
  }
  bool ret = getSubstitutionForLit(exp, v, s, ids);
  vars.push_back(v);
  subs.push_back(s);
  from.push_back(exp);
  return ret;
}

Node BuiltinProofRuleChecker::applySubstitution(Node n,
                                                Node exp,
                                                MethodId ids,
                                                MethodId ida)
{
  std::vector<Node> expv{exp};
  return applySubstitution(n, expv, ids, ida);
}

Node BuiltinProofRuleChecker::applySubstitution(Node n,
                                                const std::vector<Node>& exp,
                                                MethodId ids,
                                                MethodId ida)
{
  std::vector<TNode> vars;
  std::vector<TNode> subs;
  std::vector<TNode> from;
  for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
  {
    if (exp[i].isNull())
    {
      return Node::null();
    }
    if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
    {
      return Node::null();
    }
  }
  if (ida == MethodId::SBA_SIMUL)
  {
    // simply apply the simultaneous substitution now
    return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
  }
  else if (ida == MethodId::SBA_FIXPOINT)
  {
    SubstitutionMap sm;
    for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
    {
      sm.addSubstitution(vars[i], subs[i]);
    }
    Node ns = sm.apply(n);
    return ns;
  }
  Assert(ida == MethodId::SBA_SEQUENTIAL);
  // we prefer n traversals of the term to n^2/2 traversals of range terms
  Node ns = n;
  for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
  {
    TNode v = vars[(nvars - 1) - i];
    TNode s = subs[(nvars - 1) - i];
    ns = ns.substitute(v, s);
  }
  return ns;
}

Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                                            const std::vector<Node>& children,
                                            const std::vector<Node>& args)
{
  NodeManager * nm = NodeManager::currentNM();
  // compute what was proven
  if (id == PfRule::ASSUME)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    Assert(args[0].getType().isBoolean());
    return args[0];
  }
  else if (id == PfRule::SCOPE)
  {
    Assert(children.size() == 1);
    if (args.empty())
    {
      // no antecedant
      return children[0];
    }
    Node ant = nm->mkAnd(args);
    // if the conclusion is false, its the negated antencedant only
    if (children[0].isConst() && !children[0].getConst<bool>())
    {
      return ant.notNode();
    }
    return nm->mkNode(IMPLIES, ant, children[0]);
  }
  else if (id == PfRule::SUBS)
  {
    Assert(children.size() > 0);
    Assert(1 <= args.size() && args.size() <= 2);
    MethodId ids = MethodId::SB_DEFAULT;
    if (args.size() == 2 && !getMethodId(args[1], ids))
    {
      return Node::null();
    }
    std::vector<Node> exp;
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
    {
      exp.push_back(children[i]);
    }
    Node res = applySubstitution(args[0], exp, ids);
    if (res.isNull())
    {
      return Node::null();
    }
    return args[0].eqNode(res);
  }
  else if (id == PfRule::REWRITE)
  {
    Assert(children.empty());
    Assert(1 <= args.size() && args.size() <= 2);
    MethodId idr = MethodId::RW_REWRITE;
    if (args.size() == 2 && !getMethodId(args[1], idr))
    {
      return Node::null();
    }
    Node res = applyRewrite(args[0], idr);
    if (res.isNull())
    {
      return Node::null();
    }
    return args[0].eqNode(res);
  }
  else if (id == PfRule::EVALUATE)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
    if (res.isNull())
    {
      return Node::null();
    }
    return args[0].eqNode(res);
  }
  else if (id == PfRule::MACRO_SR_EQ_INTRO)
  {
    Assert(1 <= args.size() && args.size() <= 4);
    MethodId ids, ida, idr;
    if (!getMethodIds(args, ids, ida, idr, 1))
    {
      return Node::null();
    }
    Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
    if (res.isNull())
    {
      return Node::null();
    }
    return args[0].eqNode(res);
  }
  else if (id == PfRule::MACRO_SR_PRED_INTRO)
  {
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
                             << args[0] << std::endl;
    Assert(1 <= args.size() && args.size() <= 4);
    MethodId ids, ida, idr;
    if (!getMethodIds(args, ids, ida, idr, 1))
    {
      return Node::null();
    }
    Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
    if (res.isNull())
    {
      return Node::null();
    }
    Trace("builtin-pfcheck") << "Result is " << res << std::endl;
    Trace("builtin-pfcheck") << "Witness form is "
                             << SkolemManager::getOriginalForm(res) << std::endl;
    // **** NOTE: can rewrite the witness form here. This enables certain lemmas
    // to be provable, e.g. (= k t) where k is a purification Skolem for t.
    res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
    if (!res.isConst() || !res.getConst<bool>())
    {
      Trace("builtin-pfcheck")
          << "Failed to rewrite to true, res=" << res << std::endl;
      return Node::null();
    }
    Trace("builtin-pfcheck") << "...success" << std::endl;
    return args[0];
  }
  else if (id == PfRule::MACRO_SR_PRED_ELIM)
  {
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
                             << args.size() << std::endl;
    Assert(children.size() >= 1);
    Assert(args.size() <= 3);
    std::vector<Node> exp;
    exp.insert(exp.end(), children.begin() + 1, children.end());
    MethodId ids, ida, idr;
    if (!getMethodIds(args, ids, ida, idr, 0))
    {
      return Node::null();
    }
    Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
    Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
    return res1;
  }
  else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
  {
    Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
                             << args.size() << std::endl;
    Assert(children.size() >= 1);
    Assert(1 <= args.size() && args.size() <= 4);
    Assert(args[0].getType().isBoolean());
    MethodId ids, ida, idr;
    if (!getMethodIds(args, ids, ida, idr, 1))
    {
      return Node::null();
    }
    std::vector<Node> exp;
    exp.insert(exp.end(), children.begin() + 1, children.end());
    Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
    Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
    // if not already equal, do rewriting
    if (res1 != res2)
    {
      // can rewrite the witness forms
      res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
      res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
      if (res1.isNull() || res1 != res2)
      {
        Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
        Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
        return Node::null();
      }
    }
    return args[0];
  }
  else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    return RemoveTermFormulas::getAxiomFor(args[0]);
  }
  else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
           || id == PfRule::THEORY_PREPROCESS
           || id == PfRule::THEORY_PREPROCESS_LEMMA
           || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
           || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
           || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
           || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ
           || id == PfRule::THEORY_INFERENCE)
  {
    // "trusted" rules
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }

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

bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
{
  uint32_t i;
  if (!getUInt32(n, i))
  {
    return false;
  }
  tid = static_cast<TheoryId>(i);
  return true;
}

Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
{
  return NodeManager::currentNM()->mkConst(
      Rational(static_cast<uint32_t>(tid)));
}

}  // namespace builtin
}  // 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 equality proof checker.
14		*/
15
16		#include "theory/builtin/proof_checker.h"
17
18		#include "expr/skolem_manager.h"
19		#include "smt/env.h"
20		#include "smt/term_formula_removal.h"
21		#include "theory/evaluator.h"
22		#include "theory/rewriter.h"
23		#include "theory/substitutions.h"
24		#include "theory/theory.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace builtin {
31
32	9926	BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env) {}
33
34	3786	void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
35		{
36	3786	pc->registerChecker(PfRule::ASSUME, this);
37	3786	pc->registerChecker(PfRule::SCOPE, this);
38	3786	pc->registerChecker(PfRule::SUBS, this);
39	3786	pc->registerChecker(PfRule::REWRITE, this);
40	3786	pc->registerChecker(PfRule::EVALUATE, this);
41	3786	pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
42	3786	pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
43	3786	pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
44	3786	pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
45	3786	pc->registerChecker(PfRule::THEORY_REWRITE, this);
46	3786	pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
47		// trusted rules
48	3786	pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
49	3786	pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
50	3786	pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
51	3786	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
52	3786	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
53	3786	pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
54	3786	pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
55	3786	pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
56	3786	pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
57	3786	pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
58	3786	pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
59	3786	pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3);
60	3786	}
61
62	1488905	Node BuiltinProofRuleChecker::applySubstitutionRewrite(
63		Node n,
64		const std::vector<Node>& exp,
65		MethodId ids,
66		MethodId ida,
67		MethodId idr)
68		{
69	2977810	Node nks = applySubstitution(n, exp, ids, ida);
70	2977810	return applyRewrite(nks, idr);
71		}
72
73	1673614	Node BuiltinProofRuleChecker::applyRewrite(TNode n, MethodId idr)
74		{
75	1673614	return d_env.getRewriter()->rewriteViaMethod(n, idr);
76		}
77
78	2994183	bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
79		TNode& var,
80		TNode& subs,
81		MethodId ids)
82		{
83	2994183	if (ids == MethodId::SB_DEFAULT)
84		{
85	2978543	if (exp.getKind() != EQUAL)
86		{
87		return false;
88		}
89	2978543	var = exp[0];
90	2978543	subs = exp[1];
91		}
92	15640	else if (ids == MethodId::SB_LITERAL)
93		{
94	15640	bool polarity = exp.getKind() != NOT;
95	15640	var = polarity ? exp : exp[0];
96	15640	subs = NodeManager::currentNM()->mkConst(polarity);
97		}
98		else if (ids == MethodId::SB_FORMULA)
99		{
100		var = exp;
101		subs = NodeManager::currentNM()->mkConst(true);
102		}
103		else
104		{
105		Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
106		"substitution for "
107		<< ids << std::endl;
108		return false;
109		}
110	2994183	return true;
111		}
112
113	2994183	bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
114		std::vector<TNode>& vars,
115		std::vector<TNode>& subs,
116		std::vector<TNode>& from,
117		MethodId ids)
118		{
119	5988366	TNode v;
120	5988366	TNode s;
121	2994183	if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
122		{
123		for (const Node& ec : exp)
124		{
125		// non-recursive, do not use nested AND
126		if (!getSubstitutionForLit(ec, v, s, ids))
127		{
128		return false;
129		}
130		vars.push_back(v);
131		subs.push_back(s);
132		from.push_back(ec);
133		}
134		return true;
135		}
136	2994183	bool ret = getSubstitutionForLit(exp, v, s, ids);
137	2994183	vars.push_back(v);
138	2994183	subs.push_back(s);
139	2994183	from.push_back(exp);
140	2994183	return ret;
141		}
142
143		Node BuiltinProofRuleChecker::applySubstitution(Node n,
144		Node exp,
145		MethodId ids,
146		MethodId ida)
147		{
148		std::vector<Node> expv{exp};
149		return applySubstitution(n, expv, ids, ida);
150		}
151
152	1511129	Node BuiltinProofRuleChecker::applySubstitution(Node n,
153		const std::vector<Node>& exp,
154		MethodId ids,
155		MethodId ida)
156		{
157	3022258	std::vector<TNode> vars;
158	3022258	std::vector<TNode> subs;
159	3022258	std::vector<TNode> from;
160	3954417	for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
161		{
162	2443288	if (exp[i].isNull())
163		{
164		return Node::null();
165		}
166	2443288	if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
167		{
168		return Node::null();
169		}
170		}
171	1511129	if (ida == MethodId::SBA_SIMUL)
172		{
173		// simply apply the simultaneous substitution now
174		return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
175		}
176	1511129	else if (ida == MethodId::SBA_FIXPOINT)
177		{
178	60822	SubstitutionMap sm;
179	2439396	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
180		{
181	2408985	sm.addSubstitution(vars[i], subs[i]);
182		}
183	60822	Node ns = sm.apply(n);
184	30411	return ns;
185		}
186	1480718	Assert(ida == MethodId::SBA_SEQUENTIAL);
187		// we prefer n traversals of the term to n^2/2 traversals of range terms
188	2961436	Node ns = n;
189	1515021	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
190		{
191	68606	TNode v = vars[(nvars - 1) - i];
192	68606	TNode s = subs[(nvars - 1) - i];
193	34303	ns = ns.substitute(v, s);
194		}
195	1480718	return ns;
196		}
197
198	1139525	Node BuiltinProofRuleChecker::checkInternal(PfRule id,
199		const std::vector<Node>& children,
200		const std::vector<Node>& args)
201		{
202	1139525	NodeManager * nm = NodeManager::currentNM();
203		// compute what was proven
204	1139525	if (id == PfRule::ASSUME)
205		{
206		Assert(children.empty());
207		Assert(args.size() == 1);
208		Assert(args[0].getType().isBoolean());
209		return args[0];
210		}
211	1139525	else if (id == PfRule::SCOPE)
212		{
213	115123	Assert(children.size() == 1);
214	115123	if (args.empty())
215		{
216		// no antecedant
217		return children[0];
218		}
219	230246	Node ant = nm->mkAnd(args);
220		// if the conclusion is false, its the negated antencedant only
221	115123	if (children[0].isConst() && !children[0].getConst<bool>())
222		{
223	68519	return ant.notNode();
224		}
225	46604	return nm->mkNode(IMPLIES, ant, children[0]);
226		}
227	1024402	else if (id == PfRule::SUBS)
228		{
229		Assert(children.size() > 0);
230		Assert(1 <= args.size() && args.size() <= 2);
231		MethodId ids = MethodId::SB_DEFAULT;
232		if (args.size() == 2 && !getMethodId(args[1], ids))
233		{
234		return Node::null();
235		}
236		std::vector<Node> exp;
237		for (size_t i = 0, nchild = children.size(); i < nchild; i++)
238		{
239		exp.push_back(children[i]);
240		}
241		Node res = applySubstitution(args[0], exp, ids);
242		if (res.isNull())
243		{
244		return Node::null();
245		}
246		return args[0].eqNode(res);
247		}
248	1024402	else if (id == PfRule::REWRITE)
249		{
250	2737	Assert(children.empty());
251	2737	Assert(1 <= args.size() && args.size() <= 2);
252	2737	MethodId idr = MethodId::RW_REWRITE;
253	2737	if (args.size() == 2 && !getMethodId(args[1], idr))
254		{
255		return Node::null();
256		}
257	5474	Node res = applyRewrite(args[0], idr);
258	2737	if (res.isNull())
259		{
260		return Node::null();
261		}
262	2737	return args[0].eqNode(res);
263		}
264	1021665	else if (id == PfRule::EVALUATE)
265		{
266	28346	Assert(children.empty());
267	28346	Assert(args.size() == 1);
268	56692	Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
269	28346	if (res.isNull())
270		{
271		return Node::null();
272		}
273	28346	return args[0].eqNode(res);
274		}
275	993319	else if (id == PfRule::MACRO_SR_EQ_INTRO)
276		{
277	25313	Assert(1 <= args.size() && args.size() <= 4);
278		MethodId ids, ida, idr;
279	25313	if (!getMethodIds(args, ids, ida, idr, 1))
280		{
281		return Node::null();
282		}
283	50626	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
284	25313	if (res.isNull())
285		{
286		return Node::null();
287		}
288	25313	return args[0].eqNode(res);
289		}
290	968006	else if (id == PfRule::MACRO_SR_PRED_INTRO)
291		{
292	19276	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
293	9638	<< args[0] << std::endl;
294	9638	Assert(1 <= args.size() && args.size() <= 4);
295		MethodId ids, ida, idr;
296	9638	if (!getMethodIds(args, ids, ida, idr, 1))
297		{
298		return Node::null();
299		}
300	19276	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
301	9638	if (res.isNull())
302		{
303		return Node::null();
304		}
305	9638	Trace("builtin-pfcheck") << "Result is " << res << std::endl;
306	19276	Trace("builtin-pfcheck") << "Witness form is "
307	9638	<< SkolemManager::getOriginalForm(res) << std::endl;
308		// **** NOTE: can rewrite the witness form here. This enables certain lemmas
309		// to be provable, e.g. (= k t) where k is a purification Skolem for t.
310	9638	res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
311	9638	if (!res.isConst() \|\| !res.getConst<bool>())
312		{
313	4	Trace("builtin-pfcheck")
314	2	<< "Failed to rewrite to true, res=" << res << std::endl;
315	2	return Node::null();
316		}
317	9636	Trace("builtin-pfcheck") << "...success" << std::endl;
318	9636	return args[0];
319		}
320	958368	else if (id == PfRule::MACRO_SR_PRED_ELIM)
321		{
322	1272	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
323	636	<< args.size() << std::endl;
324	636	Assert(children.size() >= 1);
325	636	Assert(args.size() <= 3);
326	1272	std::vector<Node> exp;
327	636	exp.insert(exp.end(), children.begin() + 1, children.end());
328		MethodId ids, ida, idr;
329	636	if (!getMethodIds(args, ids, ida, idr, 0))
330		{
331		return Node::null();
332		}
333	1272	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
334	636	Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
335	636	return res1;
336		}
337	957732	else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
338		{
339	1453318	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
340	726659	<< args.size() << std::endl;
341	726659	Assert(children.size() >= 1);
342	726659	Assert(1 <= args.size() && args.size() <= 4);
343	726659	Assert(args[0].getType().isBoolean());
344		MethodId ids, ida, idr;
345	726659	if (!getMethodIds(args, ids, ida, idr, 1))
346		{
347		return Node::null();
348		}
349	1453318	std::vector<Node> exp;
350	726659	exp.insert(exp.end(), children.begin() + 1, children.end());
351	1453318	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
352	1453318	Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
353		// if not already equal, do rewriting
354	726659	if (res1 != res2)
355		{
356		// can rewrite the witness forms
357	798	res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
358	798	res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
359	798	if (res1.isNull() \|\| res1 != res2)
360		{
361	218	Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
362	218	Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
363	218	return Node::null();
364		}
365		}
366	726441	return args[0];
367		}
368	231073	else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
369		{
370	3235	Assert(children.empty());
371	3235	Assert(args.size() == 1);
372	3235	return RemoveTermFormulas::getAxiomFor(args[0]);
373		}
374	227838	else if (id == PfRule::PREPROCESS \|\| id == PfRule::PREPROCESS_LEMMA
375	226960	\|\| id == PfRule::THEORY_PREPROCESS
376	225953	\|\| id == PfRule::THEORY_PREPROCESS_LEMMA
377	225734	\|\| id == PfRule::THEORY_EXPAND_DEF \|\| id == PfRule::WITNESS_AXIOM
378	225720	\|\| id == PfRule::THEORY_LEMMA \|\| id == PfRule::THEORY_REWRITE
379	2896	\|\| id == PfRule::TRUST_REWRITE \|\| id == PfRule::TRUST_SUBS
380	2896	\|\| id == PfRule::TRUST_SUBS_MAP \|\| id == PfRule::TRUST_SUBS_EQ
381	2843	\|\| id == PfRule::THEORY_INFERENCE)
382		{
383		// "trusted" rules
384	227838	Assert(!args.empty());
385	227838	Assert(args[0].getType().isBoolean());
386	227838	return args[0];
387		}
388
389		// no rule
390		return Node::null();
391		}
392
393	109	bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
394		{
395		uint32_t i;
396	109	if (!getUInt32(n, i))
397		{
398		return false;
399		}
400	109	tid = static_cast<TheoryId>(i);
401	109	return true;
402		}
403
404	206808	Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
405		{
406		return NodeManager::currentNM()->mkConst(
407	206808	Rational(static_cast<uint32_t>(tid)));
408		}
409
410		} // namespace builtin
411		} // namespace theory
412	29502	} // namespace cvc5