Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/builtin/proof_checker.cpp	Lines:	170	219	77.6 %
Date:	2021-11-07	Branches:	304	960	31.7 %


/******************************************************************************
 * 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/rewriter.h"
#include "theory/substitutions.h"
#include "theory/theory.h"
#include "util/rational.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);
  pc->registerChecker(PfRule::ALETHE_RULE, this);
}

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