Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/builtin/proof_checker.cpp	Lines:	178	233	76.4 %
Date:	2021-08-14	Branches:	316	1008	31.3 %


/******************************************************************************
 * 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/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 {

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(Node n, MethodId idr)
{
  Trace("builtin-pfcheck-debug")
      << "applyRewrite (" << idr << "): " << n << std::endl;
  if (idr == MethodId::RW_REWRITE)
  {
    return Rewriter::rewrite(n);
  }
  if (idr == MethodId::RW_EXT_REWRITE)
  {
    return d_ext_rewriter.extendedRewrite(n);
  }
  if (idr == MethodId::RW_REWRITE_EQ_EXT)
  {
    return Rewriter::rewriteEqualityExt(n);
  }
  if (idr == MethodId::RW_EVALUATE)
  {
    Evaluator eval;
    return eval.eval(n, {}, {}, false);
  }
  if (idr == MethodId::RW_IDENTITY)
  {
    // does nothing
    return n;
  }
  // unknown rewriter
  Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for "
                << idr << std::endl;
  return n;
}

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/term_formula_removal.h"
20		#include "theory/evaluator.h"
21		#include "theory/rewriter.h"
22		#include "theory/substitutions.h"
23		#include "theory/theory.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace builtin {
30
31	3768	void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
32		{
33	3768	pc->registerChecker(PfRule::ASSUME, this);
34	3768	pc->registerChecker(PfRule::SCOPE, this);
35	3768	pc->registerChecker(PfRule::SUBS, this);
36	3768	pc->registerChecker(PfRule::REWRITE, this);
37	3768	pc->registerChecker(PfRule::EVALUATE, this);
38	3768	pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
39	3768	pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
40	3768	pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
41	3768	pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
42	3768	pc->registerChecker(PfRule::THEORY_REWRITE, this);
43	3768	pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
44		// trusted rules
45	3768	pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
46	3768	pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
47	3768	pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
48	3768	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
49	3768	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
50	3768	pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
51	3768	pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
52	3768	pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
53	3768	pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
54	3768	pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
55	3768	pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
56	3768	pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3);
57	3768	}
58
59	1407243	Node BuiltinProofRuleChecker::applySubstitutionRewrite(
60		Node n,
61		const std::vector<Node>& exp,
62		MethodId ids,
63		MethodId ida,
64		MethodId idr)
65		{
66	2814486	Node nks = applySubstitution(n, exp, ids, ida);
67	2814486	return applyRewrite(nks, idr);
68		}
69
70	1654528	Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
71		{
72	3309056	Trace("builtin-pfcheck-debug")
73	1654528	<< "applyRewrite (" << idr << "): " << n << std::endl;
74	1654528	if (idr == MethodId::RW_REWRITE)
75		{
76	1614858	return Rewriter::rewrite(n);
77		}
78	39670	if (idr == MethodId::RW_EXT_REWRITE)
79		{
80		return d_ext_rewriter.extendedRewrite(n);
81		}
82	39670	if (idr == MethodId::RW_REWRITE_EQ_EXT)
83		{
84	294	return Rewriter::rewriteEqualityExt(n);
85		}
86	39376	if (idr == MethodId::RW_EVALUATE)
87		{
88		Evaluator eval;
89	39376	return eval.eval(n, {}, {}, false);
90		}
91		if (idr == MethodId::RW_IDENTITY)
92		{
93		// does nothing
94		return n;
95		}
96		// unknown rewriter
97		Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for "
98		<< idr << std::endl;
99		return n;
100		}
101
102	3690402	bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
103		TNode& var,
104		TNode& subs,
105		MethodId ids)
106		{
107	3690402	if (ids == MethodId::SB_DEFAULT)
108		{
109	3652652	if (exp.getKind() != EQUAL)
110		{
111		return false;
112		}
113	3652652	var = exp[0];
114	3652652	subs = exp[1];
115		}
116	37750	else if (ids == MethodId::SB_LITERAL)
117		{
118	37750	bool polarity = exp.getKind() != NOT;
119	37750	var = polarity ? exp : exp[0];
120	37750	subs = NodeManager::currentNM()->mkConst(polarity);
121		}
122		else if (ids == MethodId::SB_FORMULA)
123		{
124		var = exp;
125		subs = NodeManager::currentNM()->mkConst(true);
126		}
127		else
128		{
129		Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
130		"substitution for "
131		<< ids << std::endl;
132		return false;
133		}
134	3690402	return true;
135		}
136
137	3690402	bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
138		std::vector<TNode>& vars,
139		std::vector<TNode>& subs,
140		std::vector<TNode>& from,
141		MethodId ids)
142		{
143	7380804	TNode v;
144	7380804	TNode s;
145	3690402	if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
146		{
147		for (const Node& ec : exp)
148		{
149		// non-recursive, do not use nested AND
150		if (!getSubstitutionForLit(ec, v, s, ids))
151		{
152		return false;
153		}
154		vars.push_back(v);
155		subs.push_back(s);
156		from.push_back(ec);
157		}
158		return true;
159		}
160	3690402	bool ret = getSubstitutionForLit(exp, v, s, ids);
161	3690402	vars.push_back(v);
162	3690402	subs.push_back(s);
163	3690402	from.push_back(exp);
164	3690402	return ret;
165		}
166
167		Node BuiltinProofRuleChecker::applySubstitution(Node n,
168		Node exp,
169		MethodId ids,
170		MethodId ida)
171		{
172		std::vector<Node> expv{exp};
173		return applySubstitution(n, expv, ids, ida);
174		}
175
176	1429238	Node BuiltinProofRuleChecker::applySubstitution(Node n,
177		const std::vector<Node>& exp,
178		MethodId ids,
179		MethodId ida)
180		{
181	2858476	std::vector<TNode> vars;
182	2858476	std::vector<TNode> subs;
183	2858476	std::vector<TNode> from;
184	4568975	for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
185		{
186	3139737	if (exp[i].isNull())
187		{
188		return Node::null();
189		}
190	3139737	if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
191		{
192		return Node::null();
193		}
194		}
195	1429238	if (ida == MethodId::SBA_SIMUL)
196		{
197		// simply apply the simultaneous substitution now
198		return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
199		}
200	1429238	else if (ida == MethodId::SBA_FIXPOINT)
201		{
202	72994	SubstitutionMap sm;
203	3089676	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
204		{
205	3053179	sm.addSubstitution(vars[i], subs[i]);
206		}
207	72994	Node ns = sm.apply(n);
208	36497	return ns;
209		}
210	1392741	Assert(ida == MethodId::SBA_SEQUENTIAL);
211		// we prefer n traversals of the term to n^2/2 traversals of range terms
212	2785482	Node ns = n;
213	1479299	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
214		{
215	173116	TNode v = vars[(nvars - 1) - i];
216	173116	TNode s = subs[(nvars - 1) - i];
217	86558	ns = ns.substitute(v, s);
218		}
219	1392741	return ns;
220		}
221
222	1315940	Node BuiltinProofRuleChecker::checkInternal(PfRule id,
223		const std::vector<Node>& children,
224		const std::vector<Node>& args)
225		{
226	1315940	NodeManager * nm = NodeManager::currentNM();
227		// compute what was proven
228	1315940	if (id == PfRule::ASSUME)
229		{
230		Assert(children.empty());
231		Assert(args.size() == 1);
232		Assert(args[0].getType().isBoolean());
233		return args[0];
234		}
235	1315940	else if (id == PfRule::SCOPE)
236		{
237	189708	Assert(children.size() == 1);
238	189708	if (args.empty())
239		{
240		// no antecedant
241		return children[0];
242		}
243	379416	Node ant = nm->mkAnd(args);
244		// if the conclusion is false, its the negated antencedant only
245	189708	if (children[0].isConst() && !children[0].getConst<bool>())
246		{
247	97516	return ant.notNode();
248		}
249	92192	return nm->mkNode(IMPLIES, ant, children[0]);
250		}
251	1126232	else if (id == PfRule::SUBS)
252		{
253		Assert(children.size() > 0);
254		Assert(1 <= args.size() && args.size() <= 2);
255		MethodId ids = MethodId::SB_DEFAULT;
256		if (args.size() == 2 && !getMethodId(args[1], ids))
257		{
258		return Node::null();
259		}
260		std::vector<Node> exp;
261		for (size_t i = 0, nchild = children.size(); i < nchild; i++)
262		{
263		exp.push_back(children[i]);
264		}
265		Node res = applySubstitution(args[0], exp, ids);
266		if (res.isNull())
267		{
268		return Node::null();
269		}
270		return args[0].eqNode(res);
271		}
272	1126232	else if (id == PfRule::REWRITE)
273		{
274	56585	Assert(children.empty());
275	56585	Assert(1 <= args.size() && args.size() <= 2);
276	56585	MethodId idr = MethodId::RW_REWRITE;
277	56585	if (args.size() == 2 && !getMethodId(args[1], idr))
278		{
279		return Node::null();
280		}
281	113170	Node res = applyRewrite(args[0], idr);
282	56585	if (res.isNull())
283		{
284		return Node::null();
285		}
286	56585	return args[0].eqNode(res);
287		}
288	1069647	else if (id == PfRule::EVALUATE)
289		{
290	39376	Assert(children.empty());
291	39376	Assert(args.size() == 1);
292	78752	Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
293	39376	if (res.isNull())
294		{
295		return Node::null();
296		}
297	39376	return args[0].eqNode(res);
298		}
299	1030271	else if (id == PfRule::MACRO_SR_EQ_INTRO)
300		{
301	31399	Assert(1 <= args.size() && args.size() <= 4);
302		MethodId ids, ida, idr;
303	31399	if (!getMethodIds(args, ids, ida, idr, 1))
304		{
305		return Node::null();
306		}
307	62798	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
308	31399	if (res.isNull())
309		{
310		return Node::null();
311		}
312	31399	return args[0].eqNode(res);
313		}
314	998872	else if (id == PfRule::MACRO_SR_PRED_INTRO)
315		{
316	122162	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
317	61081	<< args[0] << std::endl;
318	61081	Assert(1 <= args.size() && args.size() <= 4);
319		MethodId ids, ida, idr;
320	61081	if (!getMethodIds(args, ids, ida, idr, 1))
321		{
322		return Node::null();
323		}
324	122162	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
325	61081	if (res.isNull())
326		{
327		return Node::null();
328		}
329	61081	Trace("builtin-pfcheck") << "Result is " << res << std::endl;
330	122162	Trace("builtin-pfcheck") << "Witness form is "
331	61081	<< SkolemManager::getOriginalForm(res) << std::endl;
332		// **** NOTE: can rewrite the witness form here. This enables certain lemmas
333		// to be provable, e.g. (= k t) where k is a purification Skolem for t.
334	61081	res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
335	61081	if (!res.isConst() \|\| !res.getConst<bool>())
336		{
337	38	Trace("builtin-pfcheck")
338	19	<< "Failed to rewrite to true, res=" << res << std::endl;
339	19	return Node::null();
340		}
341	61062	Trace("builtin-pfcheck") << "...success" << std::endl;
342	61062	return args[0];
343		}
344	937791	else if (id == PfRule::MACRO_SR_PRED_ELIM)
345		{
346	17242	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
347	8621	<< args.size() << std::endl;
348	8621	Assert(children.size() >= 1);
349	8621	Assert(args.size() <= 3);
350	17242	std::vector<Node> exp;
351	8621	exp.insert(exp.end(), children.begin() + 1, children.end());
352		MethodId ids, ida, idr;
353	8621	if (!getMethodIds(args, ids, ida, idr, 0))
354		{
355		return Node::null();
356		}
357	17242	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
358	8621	Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
359	8621	return res1;
360		}
361	929170	else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
362		{
363	1306142	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
364	653071	<< args.size() << std::endl;
365	653071	Assert(children.size() >= 1);
366	653071	Assert(1 <= args.size() && args.size() <= 4);
367	653071	Assert(args[0].getType().isBoolean());
368		MethodId ids, ida, idr;
369	653071	if (!getMethodIds(args, ids, ida, idr, 1))
370		{
371		return Node::null();
372		}
373	1306142	std::vector<Node> exp;
374	653071	exp.insert(exp.end(), children.begin() + 1, children.end());
375	1306142	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
376	1306142	Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
377		// if not already equal, do rewriting
378	653071	if (res1 != res2)
379		{
380		// can rewrite the witness forms
381	1936	res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
382	1936	res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
383	1936	if (res1.isNull() \|\| res1 != res2)
384		{
385	256	Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
386	256	Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
387	256	return Node::null();
388		}
389		}
390	652815	return args[0];
391		}
392	276099	else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
393		{
394	14280	Assert(children.empty());
395	14280	Assert(args.size() == 1);
396	14280	return RemoveTermFormulas::getAxiomFor(args[0]);
397		}
398	261819	else if (id == PfRule::PREPROCESS \|\| id == PfRule::PREPROCESS_LEMMA
399	260749	\|\| id == PfRule::THEORY_PREPROCESS
400	257041	\|\| id == PfRule::THEORY_PREPROCESS_LEMMA
401	228608	\|\| id == PfRule::THEORY_EXPAND_DEF \|\| id == PfRule::WITNESS_AXIOM
402	228548	\|\| id == PfRule::THEORY_LEMMA \|\| id == PfRule::THEORY_REWRITE
403	109	\|\| id == PfRule::TRUST_REWRITE \|\| id == PfRule::TRUST_SUBS
404	100	\|\| id == PfRule::TRUST_SUBS_MAP \|\| id == PfRule::TRUST_SUBS_EQ
405	60	\|\| id == PfRule::THEORY_INFERENCE)
406		{
407		// "trusted" rules
408	261819	Assert(!args.empty());
409	261819	Assert(args[0].getType().isBoolean());
410	261819	return args[0];
411		}
412
413		// no rule
414		return Node::null();
415		}
416
417	109	bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
418		{
419		uint32_t i;
420	109	if (!getUInt32(n, i))
421		{
422		return false;
423		}
424	109	tid = static_cast<TheoryId>(i);
425	109	return true;
426		}
427
428	202803	Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
429		{
430		return NodeManager::currentNM()->mkConst(
431	202803	Rational(static_cast<uint32_t>(tid)));
432		}
433
434		} // namespace builtin
435		} // namespace theory
436	29340	} // namespace cvc5