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_generator.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21
  22 const char* toString(TrustNodeKind tnk)
  23 {
  24   switch (tnk)
  25   {
  26     case TrustNodeKind::CONFLICT: return "CONFLICT";
  27     case TrustNodeKind::LEMMA: return "LEMMA";
  28     case TrustNodeKind::PROP_EXP: return "PROP_EXP";
  29     case TrustNodeKind::REWRITE: return "REWRITE";
  30     default: return "?";
  31   }
  32 }
  33
  34 std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
  35 {
  36   out << toString(tnk);
  37   return out;
  38 }
  39
  40 TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
  41 {
  42   Node ckey = getConflictProven(conf);
  43   // if a generator is provided, should confirm that it can prove it
  44   Assert(g == nullptr || g->hasProofFor(ckey));
  45   return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
  46 }
  47
  48 TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
  49 {
  50   Node lkey = getLemmaProven(lem);
  51   // if a generator is provided, should confirm that it can prove it
  52   Assert(g == nullptr || g->hasProofFor(lkey));
  53   return TrustNode(TrustNodeKind::LEMMA, lkey, g);
  54 }
  55
  56 TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
  57 {
  58   Node pekey = getPropExpProven(lit, exp);
  59   Assert(g == nullptr || g->hasProofFor(pekey));
  60   return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
  61 }
  62
  63 TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g)
  64 {
  65   Node rkey = getRewriteProven(n, nr);
  66   Assert(g == nullptr || g->hasProofFor(rkey));
  67   return TrustNode(TrustNodeKind::REWRITE, rkey, g);
  68 }
  69
  70 TrustNode TrustNode::null()
  71 {
  72   return TrustNode(TrustNodeKind::INVALID, Node::null());
  73 }
  74
  75 TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
  76     : d_tnk(tnk), d_proven(p), d_gen(g)
  77 {
  78   // does not make sense to provide null node with generator
  79   Assert(!d_proven.isNull() || d_gen == nullptr);
  80 }
  81
  82 TrustNodeKind TrustNode::getKind() const { return d_tnk; }
  83
  84 Node TrustNode::getNode() const
  85 {
  86   switch (d_tnk)
  87   {
  88     // the node of lemma is the node itself
  89     case TrustNodeKind::LEMMA: return d_proven;
  90     // the node of the rewrite is the right hand side of EQUAL
  91     case TrustNodeKind::REWRITE: return d_proven[1];
  92     // the node of an explained propagation is the antecendant of an IMPLIES
  93     // the node of a conflict is underneath a NOT
  94     default: return d_proven[0];
  95   }
  96 }
  97
  98 Node TrustNode::getProven() const { return d_proven; }
  99 ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
 100
 101 bool TrustNode::isNull() const { return d_proven.isNull(); }
 102
 103 Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
 104
 105 Node TrustNode::getLemmaProven(Node lem) { return lem; }
 106
 107 Node TrustNode::getPropExpProven(TNode lit, Node exp)
 108 {
 109   return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
 110 }
 111
 112 Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
 113
 114 std::ostream& operator<<(std::ostream& out, TrustNode n)
 115 {
 116   out << "(trust " << n.getNode() << ")";
 117   return out;
 118 }
 119
 120 }  // namespace theory
 121 }  // namespace CVC4