Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/builtin/proof_checker.cpp	Lines:	199	281	70.8 %
Date:	2021-05-24	Branches:	346	1086	31.9 %


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

const char* toString(MethodId id)
{
  switch (id)
  {
    case MethodId::RW_REWRITE: return "RW_REWRITE";
    case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
    case MethodId::RW_EVALUATE: return "RW_EVALUATE";
    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
    case MethodId::SB_LITERAL: return "SB_LITERAL";
    case MethodId::SB_FORMULA: return "SB_FORMULA";
    case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
    case MethodId::SBA_SIMUL: return "SBA_SIMUL";
    case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
    default: return "MethodId::Unknown";
  };
}

std::ostream& operator<<(std::ostream& out, MethodId id)
{
  out << toString(id);
  return out;
}

Node mkMethodId(MethodId id)
{
  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
}

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);
}

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;
}

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

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)
  {
    // "trusted" rules
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }

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

bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
                                           MethodId& ids,
                                           MethodId& ida,
                                           MethodId& idr,
                                           size_t index)
{
  ids = MethodId::SB_DEFAULT;
  ida = MethodId::SBA_SEQUENTIAL;
  idr = MethodId::RW_REWRITE;
  for (size_t offset = 0; offset <= 2; offset++)
  {
    if (args.size() > index + offset)
    {
      MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
      if (!getMethodId(args[index + offset], id))
      {
        Trace("builtin-pfcheck")
            << "Failed to get id from " << args[index + offset] << std::endl;
        return false;
      }
    }
    else
    {
      break;
    }
  }
  Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
                           << ida << " / " << idr << "\n";
  return true;
}

void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
                                           MethodId ids,
                                           MethodId ida,
                                           MethodId idr)
{
  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
  bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
  if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
  {
    args.push_back(mkMethodId(ids));
  }
  if (ndefApply || ndefRewriter)
  {
    args.push_back(mkMethodId(ida));
  }
  if (ndefRewriter)
  {
    args.push_back(mkMethodId(idr));
  }
}

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
30		const char* toString(MethodId id)
31		{
32		switch (id)
33		{
34		case MethodId::RW_REWRITE: return "RW_REWRITE";
35		case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
36		case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
37		case MethodId::RW_EVALUATE: return "RW_EVALUATE";
38		case MethodId::RW_IDENTITY: return "RW_IDENTITY";
39		case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
40		case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
41		case MethodId::SB_DEFAULT: return "SB_DEFAULT";
42		case MethodId::SB_LITERAL: return "SB_LITERAL";
43		case MethodId::SB_FORMULA: return "SB_FORMULA";
44		case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
45		case MethodId::SBA_SIMUL: return "SBA_SIMUL";
46		case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
47		default: return "MethodId::Unknown";
48		};
49		}
50
51		std::ostream& operator<<(std::ostream& out, MethodId id)
52		{
53		out << toString(id);
54		return out;
55		}
56
57	218578	Node mkMethodId(MethodId id)
58		{
59	218578	return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
60		}
61
62		namespace builtin {
63
64	3600	void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
65		{
66	3600	pc->registerChecker(PfRule::ASSUME, this);
67	3600	pc->registerChecker(PfRule::SCOPE, this);
68	3600	pc->registerChecker(PfRule::SUBS, this);
69	3600	pc->registerChecker(PfRule::REWRITE, this);
70	3600	pc->registerChecker(PfRule::EVALUATE, this);
71	3600	pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
72	3600	pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
73	3600	pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
74	3600	pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
75	3600	pc->registerChecker(PfRule::THEORY_REWRITE, this);
76	3600	pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
77		// trusted rules
78	3600	pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1);
79	3600	pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3);
80	3600	pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
81	3600	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
82	3600	pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
83	3600	pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
84	3600	pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
85	3600	pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
86	3600	pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
87	3600	pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
88	3600	}
89
90	1235676	Node BuiltinProofRuleChecker::applySubstitutionRewrite(
91		Node n,
92		const std::vector<Node>& exp,
93		MethodId ids,
94		MethodId ida,
95		MethodId idr)
96		{
97	2471352	Node nks = applySubstitution(n, exp, ids, ida);
98	2471352	return applyRewrite(nks, idr);
99		}
100
101	1463921	Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
102		{
103	2927842	Trace("builtin-pfcheck-debug")
104	1463921	<< "applyRewrite (" << idr << "): " << n << std::endl;
105	1463921	if (idr == MethodId::RW_REWRITE)
106		{
107	1427709	return Rewriter::rewrite(n);
108		}
109	36212	if (idr == MethodId::RW_EXT_REWRITE)
110		{
111		return d_ext_rewriter.extendedRewrite(n);
112		}
113	36212	if (idr == MethodId::RW_REWRITE_EQ_EXT)
114		{
115	104	return Rewriter::rewriteEqualityExt(n);
116		}
117	36108	if (idr == MethodId::RW_EVALUATE)
118		{
119		Evaluator eval;
120	36108	return eval.eval(n, {}, {}, false);
121		}
122		if (idr == MethodId::RW_IDENTITY)
123		{
124		// does nothing
125		return n;
126		}
127		// unknown rewriter
128		Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for "
129		<< idr << std::endl;
130		return n;
131		}
132
133	2126389	bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
134		TNode& var,
135		TNode& subs,
136		MethodId ids)
137		{
138	2126389	if (ids == MethodId::SB_DEFAULT)
139		{
140	2086637	if (exp.getKind() != EQUAL)
141		{
142		return false;
143		}
144	2086637	var = exp[0];
145	2086637	subs = exp[1];
146		}
147	39752	else if (ids == MethodId::SB_LITERAL)
148		{
149	39752	bool polarity = exp.getKind() != NOT;
150	39752	var = polarity ? exp : exp[0];
151	39752	subs = NodeManager::currentNM()->mkConst(polarity);
152		}
153		else if (ids == MethodId::SB_FORMULA)
154		{
155		var = exp;
156		subs = NodeManager::currentNM()->mkConst(true);
157		}
158		else
159		{
160		Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
161		"substitution for "
162		<< ids << std::endl;
163		return false;
164		}
165	2126389	return true;
166		}
167
168	2126389	bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
169		std::vector<TNode>& vars,
170		std::vector<TNode>& subs,
171		std::vector<TNode>& from,
172		MethodId ids)
173		{
174	4252778	TNode v;
175	4252778	TNode s;
176	2126389	if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT)
177		{
178		for (const Node& ec : exp)
179		{
180		// non-recursive, do not use nested AND
181		if (!getSubstitutionForLit(ec, v, s, ids))
182		{
183		return false;
184		}
185		vars.push_back(v);
186		subs.push_back(s);
187		from.push_back(ec);
188		}
189		return true;
190		}
191	2126389	bool ret = getSubstitutionForLit(exp, v, s, ids);
192	2126389	vars.push_back(v);
193	2126389	subs.push_back(s);
194	2126389	from.push_back(exp);
195	2126389	return ret;
196		}
197
198		Node BuiltinProofRuleChecker::applySubstitution(Node n,
199		Node exp,
200		MethodId ids,
201		MethodId ida)
202		{
203		std::vector<Node> expv{exp};
204		return applySubstitution(n, expv, ids, ida);
205		}
206
207	1257285	Node BuiltinProofRuleChecker::applySubstitution(Node n,
208		const std::vector<Node>& exp,
209		MethodId ids,
210		MethodId ida)
211		{
212	2514570	std::vector<TNode> vars;
213	2514570	std::vector<TNode> subs;
214	2514570	std::vector<TNode> from;
215	3103598	for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
216		{
217	1846313	if (exp[i].isNull())
218		{
219		return Node::null();
220		}
221	1846313	if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
222		{
223		return Node::null();
224		}
225		}
226	1257285	if (ida == MethodId::SBA_SIMUL)
227		{
228		// simply apply the simultaneous substitution now
229		return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
230		}
231	1257285	else if (ida == MethodId::SBA_FIXPOINT)
232		{
233	64492	SubstitutionMap sm;
234	1796770	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
235		{
236	1764524	sm.addSubstitution(vars[i], subs[i]);
237		}
238	64492	Node ns = sm.apply(n);
239	32246	return ns;
240		}
241	1225039	Assert(ida == MethodId::SBA_SEQUENTIAL);
242		// we prefer n traversals of the term to n^2/2 traversals of range terms
243	2450078	Node ns = n;
244	1306828	for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
245		{
246	163578	TNode v = vars[(nvars - 1) - i];
247	163578	TNode s = subs[(nvars - 1) - i];
248	81789	ns = ns.substitute(v, s);
249		}
250	1225039	return ns;
251		}
252
253	88889	bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
254		{
255		uint32_t index;
256	88889	if (!getUInt32(n, index))
257		{
258		return false;
259		}
260	88889	i = static_cast<MethodId>(index);
261	88889	return true;
262		}
263
264	1219915	Node BuiltinProofRuleChecker::checkInternal(PfRule id,
265		const std::vector<Node>& children,
266		const std::vector<Node>& args)
267		{
268	1219915	NodeManager * nm = NodeManager::currentNM();
269		// compute what was proven
270	1219915	if (id == PfRule::ASSUME)
271		{
272		Assert(children.empty());
273		Assert(args.size() == 1);
274		Assert(args[0].getType().isBoolean());
275		return args[0];
276		}
277	1219915	else if (id == PfRule::SCOPE)
278		{
279	200667	Assert(children.size() == 1);
280	200667	if (args.empty())
281		{
282		// no antecedant
283		return children[0];
284		}
285	401334	Node ant = nm->mkAnd(args);
286		// if the conclusion is false, its the negated antencedant only
287	200667	if (children[0].isConst() && !children[0].getConst<bool>())
288		{
289	91043	return ant.notNode();
290		}
291	109624	return nm->mkNode(IMPLIES, ant, children[0]);
292		}
293	1019248	else if (id == PfRule::SUBS)
294		{
295		Assert(children.size() > 0);
296		Assert(1 <= args.size() && args.size() <= 2);
297		MethodId ids = MethodId::SB_DEFAULT;
298		if (args.size() == 2 && !getMethodId(args[1], ids))
299		{
300		return Node::null();
301		}
302		std::vector<Node> exp;
303		for (size_t i = 0, nchild = children.size(); i < nchild; i++)
304		{
305		exp.push_back(children[i]);
306		}
307		Node res = applySubstitution(args[0], exp, ids);
308		if (res.isNull())
309		{
310		return Node::null();
311		}
312		return args[0].eqNode(res);
313		}
314	1019248	else if (id == PfRule::REWRITE)
315		{
316	48937	Assert(children.empty());
317	48937	Assert(1 <= args.size() && args.size() <= 2);
318	48937	MethodId idr = MethodId::RW_REWRITE;
319	48937	if (args.size() == 2 && !getMethodId(args[1], idr))
320		{
321		return Node::null();
322		}
323	97874	Node res = applyRewrite(args[0], idr);
324	48937	if (res.isNull())
325		{
326		return Node::null();
327		}
328	48937	return args[0].eqNode(res);
329		}
330	970311	else if (id == PfRule::EVALUATE)
331		{
332	36108	Assert(children.empty());
333	36108	Assert(args.size() == 1);
334	72216	Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
335	36108	if (res.isNull())
336		{
337		return Node::null();
338		}
339	36108	return args[0].eqNode(res);
340		}
341	934203	else if (id == PfRule::MACRO_SR_EQ_INTRO)
342		{
343	28895	Assert(1 <= args.size() && args.size() <= 4);
344		MethodId ids, ida, idr;
345	28895	if (!getMethodIds(args, ids, ida, idr, 1))
346		{
347		return Node::null();
348		}
349	57790	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
350	28895	if (res.isNull())
351		{
352		return Node::null();
353		}
354	28895	return args[0].eqNode(res);
355		}
356	905308	else if (id == PfRule::MACRO_SR_PRED_INTRO)
357		{
358	107552	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
359	53776	<< args[0] << std::endl;
360	53776	Assert(1 <= args.size() && args.size() <= 4);
361		MethodId ids, ida, idr;
362	53776	if (!getMethodIds(args, ids, ida, idr, 1))
363		{
364		return Node::null();
365		}
366	107552	Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
367	53776	if (res.isNull())
368		{
369		return Node::null();
370		}
371	53776	Trace("builtin-pfcheck") << "Result is " << res << std::endl;
372	107552	Trace("builtin-pfcheck") << "Witness form is "
373	53776	<< SkolemManager::getOriginalForm(res) << std::endl;
374		// **** NOTE: can rewrite the witness form here. This enables certain lemmas
375		// to be provable, e.g. (= k t) where k is a purification Skolem for t.
376	53776	res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
377	53776	if (!res.isConst() \|\| !res.getConst<bool>())
378		{
379	24	Trace("builtin-pfcheck")
380	12	<< "Failed to rewrite to true, res=" << res << std::endl;
381	12	return Node::null();
382		}
383	53764	Trace("builtin-pfcheck") << "...success" << std::endl;
384	53764	return args[0];
385		}
386	851532	else if (id == PfRule::MACRO_SR_PRED_ELIM)
387		{
388	16730	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
389	8365	<< args.size() << std::endl;
390	8365	Assert(children.size() >= 1);
391	8365	Assert(args.size() <= 3);
392	16730	std::vector<Node> exp;
393	8365	exp.insert(exp.end(), children.begin() + 1, children.end());
394		MethodId ids, ida, idr;
395	8365	if (!getMethodIds(args, ids, ida, idr, 0))
396		{
397		return Node::null();
398		}
399	16730	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
400	8365	Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
401	8365	return res1;
402		}
403	843167	else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
404		{
405	1144640	Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
406	572320	<< args.size() << std::endl;
407	572320	Assert(children.size() >= 1);
408	572320	Assert(1 <= args.size() && args.size() <= 4);
409	572320	Assert(args[0].getType().isBoolean());
410		MethodId ids, ida, idr;
411	572320	if (!getMethodIds(args, ids, ida, idr, 1))
412		{
413		return Node::null();
414		}
415	1144640	std::vector<Node> exp;
416	572320	exp.insert(exp.end(), children.begin() + 1, children.end());
417	1144640	Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
418	1144640	Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
419		// if not already equal, do rewriting
420	572320	if (res1 != res2)
421		{
422		// can rewrite the witness forms
423	650	res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
424	650	res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
425	650	if (res1.isNull() \|\| res1 != res2)
426		{
427	108	Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
428	108	Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
429	108	return Node::null();
430		}
431		}
432	572212	return args[0];
433		}
434	270847	else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
435		{
436	15060	Assert(children.empty());
437	15060	Assert(args.size() == 1);
438	15060	return RemoveTermFormulas::getAxiomFor(args[0]);
439		}
440	255787	else if (id == PfRule::PREPROCESS \|\| id == PfRule::PREPROCESS_LEMMA
441	254583	\|\| id == PfRule::THEORY_PREPROCESS
442	251390	\|\| id == PfRule::THEORY_PREPROCESS_LEMMA
443	228142	\|\| id == PfRule::THEORY_EXPAND_DEF \|\| id == PfRule::WITNESS_AXIOM
444	228067	\|\| id == PfRule::THEORY_LEMMA \|\| id == PfRule::THEORY_REWRITE
445	76	\|\| id == PfRule::TRUST_REWRITE \|\| id == PfRule::TRUST_SUBS
446	37	\|\| id == PfRule::TRUST_SUBS_MAP)
447		{
448		// "trusted" rules
449	255787	Assert(!args.empty());
450	255787	Assert(args[0].getType().isBoolean());
451	255787	return args[0];
452		}
453
454		// no rule
455		return Node::null();
456		}
457
458	663356	bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
459		MethodId& ids,
460		MethodId& ida,
461		MethodId& idr,
462		size_t index)
463		{
464	663356	ids = MethodId::SB_DEFAULT;
465	663356	ida = MethodId::SBA_SEQUENTIAL;
466	663356	idr = MethodId::RW_REWRITE;
467	732569	for (size_t offset = 0; offset <= 2; offset++)
468		{
469	732508	if (args.size() > index + offset)
470		{
471	69213	MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
472	69213	if (!getMethodId(args[index + offset], id))
473		{
474		Trace("builtin-pfcheck")
475		<< "Failed to get id from " << args[index + offset] << std::endl;
476		return false;
477		}
478		}
479		else
480		{
481	663295	break;
482		}
483		}
484	1326712	Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
485	663356	<< ida << " / " << idr << "\n";
486	663356	return true;
487		}
488
489	12303	void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
490		MethodId ids,
491		MethodId ida,
492		MethodId idr)
493		{
494	12303	bool ndefRewriter = (idr != MethodId::RW_REWRITE);
495	12303	bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
496	12303	if (ids != MethodId::SB_DEFAULT \|\| ndefRewriter \|\| ndefApply)
497		{
498	10796	args.push_back(mkMethodId(ids));
499		}
500	12303	if (ndefApply \|\| ndefRewriter)
501		{
502	10796	args.push_back(mkMethodId(ida));
503		}
504	12303	if (ndefRewriter)
505		{
506	35	args.push_back(mkMethodId(idr));
507		}
508	12303	}
509
510		bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
511		{
512		uint32_t i;
513		if (!getUInt32(n, i))
514		{
515		return false;
516		}
517		tid = static_cast<TheoryId>(i);
518		return true;
519		}
520
521	197743	Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
522		{
523		return NodeManager::currentNM()->mkConst(
524	197743	Rational(static_cast<uint32_t>(tid)));
525		}
526
527		} // namespace builtin
528		} // namespace theory
529	28191	} // namespace cvc5