+bool InferProofCons::addProofTo(CDProof* pf,
+ Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp)
+{
+ // now go back and convert it to proof steps and add to proof
+ bool useBuffer = false;
+ ProofStep ps;
+ TheoryProofStepBuffer psb(pf->getManager()->getChecker());
+ // run the conversion
+ convert(infer, isRev, conc, exp, ps, psb, useBuffer);
+ // make the proof based on the step or the buffer
+ if (useBuffer)
+ {
+ if (!pf->addSteps(psb))
+ {
+ return false;
+ }
+ }
+ else
+ {
+ if (!pf->addStep(conc, ps))
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+void InferProofCons::packArgs(Node conc,
+ InferenceId infer,
+ bool isRev,
+ const std::vector<Node>& exp,
+ std::vector<Node>& args)
+{
+ args.push_back(conc);
+ args.push_back(mkInferenceIdNode(infer));
+ args.push_back(NodeManager::currentNM()->mkConst(isRev));
+ // The vector exp is stored as arguments; its flatten form are premises. We
+ // need both since the grouping of exp is important, e.g. { (and a b), c }
+ // is different from { a, b, c } in the convert routine, since positions
+ // of formulas in exp have special meaning.
+ args.insert(args.end(), exp.begin(), exp.end());
+}
+
+bool InferProofCons::unpackArgs(const std::vector<Node>& args,
+ Node& conc,
+ InferenceId& infer,
+ bool& isRev,
+ std::vector<Node>& exp)
+{
+ Assert(args.size() >= 3);
+ conc = args[0];
+ if (!getInferenceId(args[1], infer))
+ {
+ return false;
+ }
+ isRev = args[2].getConst<bool>();
+ exp.insert(exp.end(), args.begin() + 3, args.end());
+ return true;
+}
+