From 77551190ce7c58031dd57c3c80cad987ff5135c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Aug 2021 17:28:55 -0500 Subject: [PATCH] Proper printing of proofs in the internal calculus (#6975) --- src/proof/proof_node_to_sexpr.cpp | 183 +++++++++++++++++++++++++++--- src/proof/proof_node_to_sexpr.h | 50 +++++++- 2 files changed, 217 insertions(+), 16 deletions(-) diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp index 85fc2395e..67a43fedc 100644 --- a/src/proof/proof_node_to_sexpr.cpp +++ b/src/proof/proof_node_to_sexpr.cpp @@ -19,7 +19,9 @@ #include #include "options/proof_options.h" +#include "proof/proof_checker.h" #include "proof/proof_node.h" +#include "theory/builtin/proof_checker.h" using namespace cvc5::kind; @@ -71,7 +73,8 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) traversing.pop_back(); std::vector children; // add proof rule - children.push_back(getOrMkPfRuleVariable(cur->getRule())); + PfRule r = cur->getRule(); + children.push_back(getOrMkPfRuleVariable(r)); if (options::proofPrintConclusion()) { children.push_back(d_conclusionMarker); @@ -93,18 +96,14 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) // needed to ensure builtin operators are not treated as operators // this can be the case for CONG where d_args may contain a builtin // operator - std::vector argsSafe; - for (const Node& a : args) + std::vector argsPrint; + for (size_t i = 0, nargs = args.size(); i < nargs; i++) { - Node av = a; - if (a.getNumChildren() == 0 - && NodeManager::operatorToKind(a) != UNDEFINED_KIND) - { - av = getOrMkNodeVariable(a); - } - argsSafe.push_back(av); + ArgFormat f = getArgumentFormat(cur, i); + Node av = getArgument(args[i], f); + argsPrint.push_back(av); } - Node argsC = nm->mkNode(SEXPR, argsSafe); + Node argsC = nm->mkNode(SEXPR, argsPrint); children.push_back(argsC); } d_pnMap[cur] = nm->mkNode(SEXPR, children); @@ -129,10 +128,96 @@ Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r) d_pfrMap[r] = var; return var; } +Node ProofNodeToSExpr::getOrMkKindVariable(TNode n) +{ + Kind k; + if (!ProofRuleChecker::getKind(n, k)) + { + // just use self if we failed to get the node, throw a debug failure + Assert(false) << "Expected kind node, got " << n; + return n; + } + std::map::iterator it = d_kindMap.find(k); + if (it != d_kindMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << k; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_kindMap[k] = var; + return var; +} + +Node ProofNodeToSExpr::getOrMkTheoryIdVariable(TNode n) +{ + theory::TheoryId tid; + if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(n, tid)) + { + // just use self if we failed to get the node, throw a debug failure + Assert(false) << "Expected theory id node, got " << n; + return n; + } + std::map::iterator it = d_tidMap.find(tid); + if (it != d_tidMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << tid; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_tidMap[tid] = var; + return var; +} + +Node ProofNodeToSExpr::getOrMkMethodIdVariable(TNode n) +{ + MethodId mid; + if (!getMethodId(n, mid)) + { + // just use self if we failed to get the node, throw a debug failure + Assert(false) << "Expected method id node, got " << n; + return n; + } + std::map::iterator it = d_midMap.find(mid); + if (it != d_midMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << mid; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_midMap[mid] = var; + return var; +} +Node ProofNodeToSExpr::getOrMkInferenceIdVariable(TNode n) +{ + theory::InferenceId iid; + if (!theory::getInferenceId(n, iid)) + { + // just use self if we failed to get the node, throw a debug failure + Assert(false) << "Expected inference id node, got " << n; + return n; + } + std::map::iterator it = d_iidMap.find(iid); + if (it != d_iidMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << iid; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_iidMap[iid] = var; + return var; +} -Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) +Node ProofNodeToSExpr::getOrMkNodeVariable(TNode n) { - std::map::iterator it = d_nodeMap.find(n); + std::map::iterator it = d_nodeMap.find(n); if (it != d_nodeMap.end()) { return it->second; @@ -145,4 +230,76 @@ Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) return var; } +Node ProofNodeToSExpr::getArgument(Node arg, ArgFormat f) +{ + switch (f) + { + case ArgFormat::KIND: return getOrMkKindVariable(arg); + case ArgFormat::THEORY_ID: return getOrMkTheoryIdVariable(arg); + case ArgFormat::METHOD_ID: return getOrMkMethodIdVariable(arg); + case ArgFormat::INFERENCE_ID: return getOrMkInferenceIdVariable(arg); + case ArgFormat::NODE_VAR: return getOrMkNodeVariable(arg); + default: return arg; + } +} + +ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat( + const ProofNode* pn, size_t i) +{ + PfRule r = pn->getRule(); + switch (r) + { + case PfRule::CONG: + { + if (i == 0) + { + return ArgFormat::KIND; + } + const std::vector& args = pn->getArguments(); + Assert(i < args.size()); + if (args[i].getNumChildren() == 0 + && NodeManager::operatorToKind(args[i]) != UNDEFINED_KIND) + { + return ArgFormat::NODE_VAR; + } + } + break; + case PfRule::SUBS: + case PfRule::REWRITE: + case PfRule::MACRO_SR_EQ_INTRO: + case PfRule::MACRO_SR_PRED_INTRO: + case PfRule::MACRO_SR_PRED_TRANSFORM: + if (i > 0) + { + return ArgFormat::METHOD_ID; + } + break; + case PfRule::MACRO_SR_PRED_ELIM: return ArgFormat::METHOD_ID; break; + case PfRule::THEORY_LEMMA: + case PfRule::THEORY_REWRITE: + if (i == 1) + { + return ArgFormat::THEORY_ID; + } + else if (r == PfRule::THEORY_REWRITE && i == 2) + { + return ArgFormat::METHOD_ID; + } + break; + case PfRule::INSTANTIATE: + { + Assert(!pn->getChildren().empty()); + Node q = pn->getChildren()[0]->getResult(); + Assert(q.getKind() == kind::FORALL); + if (i == q[0].getNumChildren()) + { + return ArgFormat::INFERENCE_ID; + } + } + break; + default: break; + } + return ArgFormat::DEFAULT; +} + } // namespace cvc5 diff --git a/src/proof/proof_node_to_sexpr.h b/src/proof/proof_node_to_sexpr.h index c358f3445..83d719aaf 100644 --- a/src/proof/proof_node_to_sexpr.h +++ b/src/proof/proof_node_to_sexpr.h @@ -20,8 +20,12 @@ #include +#include "expr/kind.h" #include "expr/node.h" +#include "proof/method_id.h" #include "proof/proof_rule.h" +#include "theory/inference_id.h" +#include "theory/theory_id.h" namespace cvc5 { @@ -46,8 +50,32 @@ class ProofNodeToSExpr Node convertToSExpr(const ProofNode* pn); private: + /** argument format, determines how to print an argument */ + enum class ArgFormat + { + // just use the argument itself + DEFAULT, + // print the argument as a kind + KIND, + // print the argument as a theory id + THEORY_ID, + // print the argument as a method id + METHOD_ID, + // print the argument as an inference id + INFERENCE_ID, + // print a variable whose name is the term (see getOrMkNodeVariable) + NODE_VAR + }; /** map proof rules to a variable */ std::map d_pfrMap; + /** map kind to a variable displaying the kind they represent */ + std::map d_kindMap; + /** map theory ids to a variable displaying the theory id they represent */ + std::map d_tidMap; + /** map method ids to a variable displaying the method id they represent */ + std::map d_midMap; + /** map infer ids to a variable displaying the method id they represent */ + std::map d_iidMap; /** Dummy ":args" marker */ Node d_argsMarker; /** Dummy ":conclusion" marker */ @@ -58,11 +86,27 @@ class ProofNodeToSExpr * map nodes to a bound variable, used for nodes that have special AST status * like builtin operators */ - std::map d_nodeMap; + std::map d_nodeMap; /** get or make pf rule variable */ Node getOrMkPfRuleVariable(PfRule r); - /** get or make node variable */ - Node getOrMkNodeVariable(Node n); + /** get or make kind variable from the kind embedded in n */ + Node getOrMkKindVariable(TNode n); + /** get or make theory id variable */ + Node getOrMkTheoryIdVariable(TNode n); + /** get or make method id variable */ + Node getOrMkMethodIdVariable(TNode n); + /** get or make inference id variable */ + Node getOrMkInferenceIdVariable(TNode n); + /** + * Get or make node variable that prints the same as n but has SEXPR type. + * This is used to ensure the type checker does not complain when trying to + * print e.g. builtin operators as first-class terms in the SEXPR. + */ + Node getOrMkNodeVariable(TNode n); + /** get argument based on the provided format */ + Node getArgument(Node arg, ArgFormat f); + /** get argument format for proof node */ + ArgFormat getArgumentFormat(const ProofNode* pn, size_t i); }; } // namespace cvc5 -- 2.30.2