src/theory/trust_node.cpp

   1 /*********************                                                        */
   2 /*! \file trust_node.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Implementation of the trust node utility
  13  **/
  14
  15 #include "theory/trust_node.h"
  16
  17 #include "expr/proof_ensure_closed.h"
  18 #include "expr/proof_generator.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22
  23 const char* toString(TrustNodeKind tnk)
  24 {
  25   switch (tnk)
  26   {
  27     case TrustNodeKind::CONFLICT: return "CONFLICT";
  28     case TrustNodeKind::LEMMA: return "LEMMA";
  29     case TrustNodeKind::PROP_EXP: return "PROP_EXP";
  30     case TrustNodeKind::REWRITE: return "REWRITE";
  31     default: return "?";
  32   }
  33 }
  34
  35 std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
  36 {
  37   out << toString(tnk);
  38   return out;
  39 }
  40
  41 TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
  42 {
  43   Node ckey = getConflictProven(conf);
  44   // if a generator is provided, should confirm that it can prove it
  45   Assert(g == nullptr || g->hasProofFor(ckey));
  46   return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
  47 }
  48
  49 TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
  50 {
  51   Node lkey = getLemmaProven(lem);
  52   // if a generator is provided, should confirm that it can prove it
  53   Assert(g == nullptr || g->hasProofFor(lkey));
  54   return TrustNode(TrustNodeKind::LEMMA, lkey, g);
  55 }
  56
  57 TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
  58 {
  59   Node pekey = getPropExpProven(lit, exp);
  60   Assert(g == nullptr || g->hasProofFor(pekey));
  61   return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
  62 }
  63
  64 TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g)
  65 {
  66   Node rkey = getRewriteProven(n, nr);
  67   Assert(g == nullptr || g->hasProofFor(rkey));
  68   return TrustNode(TrustNodeKind::REWRITE, rkey, g);
  69 }
  70
  71 TrustNode TrustNode::null()
  72 {
  73   return TrustNode(TrustNodeKind::INVALID, Node::null());
  74 }
  75
  76 TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
  77     : d_tnk(tnk), d_proven(p), d_gen(g)
  78 {
  79   // does not make sense to provide null node with generator
  80   Assert(!d_proven.isNull() || d_gen == nullptr);
  81 }
  82
  83 TrustNodeKind TrustNode::getKind() const { return d_tnk; }
  84
  85 Node TrustNode::getNode() const
  86 {
  87   switch (d_tnk)
  88   {
  89     // the node of lemma is the node itself
  90     case TrustNodeKind::LEMMA: return d_proven;
  91     // the node of the rewrite is the right hand side of EQUAL
  92     case TrustNodeKind::REWRITE: return d_proven[1];
  93     // the node of an explained propagation is the antecendant of an IMPLIES
  94     // the node of a conflict is underneath a NOT
  95     default: return d_proven[0];
  96   }
  97 }
  98
  99 Node TrustNode::getProven() const { return d_proven; }
 100
 101 ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
 102
 103 bool TrustNode::isNull() const { return d_proven.isNull(); }
 104
 105 std::shared_ptr<ProofNode> TrustNode::toProofNode() const
 106 {
 107   if (d_gen == nullptr)
 108   {
 109     return nullptr;
 110   }
 111   return d_gen->getProofFor(d_proven);
 112 }
 113
 114 Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
 115
 116 Node TrustNode::getLemmaProven(Node lem) { return lem; }
 117
 118 Node TrustNode::getPropExpProven(TNode lit, Node exp)
 119 {
 120   return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
 121 }
 122
 123 Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
 124
 125 void TrustNode::debugCheckClosed(const char* c,
 126                                  const char* ctx,
 127                                  bool reqNullGen)
 128 {
 129   pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen);
 130 }
 131
 132 std::string TrustNode::identifyGenerator() const
 133 {
 134   if (d_gen == nullptr)
 135   {
 136     return "null";
 137   }
 138   return d_gen->identify();
 139 }
 140
 141 std::ostream& operator<<(std::ostream& out, TrustNode n)
 142 {
 143   out << "(" << n.getKind() << " " << n.getProven() << " "
 144       << n.identifyGenerator() << ")";
 145   return out;
 146 }
 147
 148 }  // namespace theory
 149 }  // namespace CVC4