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     default: return "?";
  30   }
  31 }
  32
  33 std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
  34 {
  35   out << toString(tnk);
  36   return out;
  37 }
  38
  39 TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
  40 {
  41   Node ckey = getConflictProven(conf);
  42   // if a generator is provided, should confirm that it can prove it
  43   Assert(g == nullptr || g->hasProofFor(ckey));
  44   return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
  45 }
  46
  47 TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
  48 {
  49   Node lkey = getLemmaProven(lem);
  50   // if a generator is provided, should confirm that it can prove it
  51   Assert(g == nullptr || g->hasProofFor(lkey));
  52   return TrustNode(TrustNodeKind::LEMMA, lkey, g);
  53 }
  54
  55 TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
  56 {
  57   Node pekey = getPropExpProven(lit, exp);
  58   Assert(g == nullptr || g->hasProofFor(pekey));
  59   return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
  60 }
  61
  62 TrustNode TrustNode::null()
  63 {
  64   return TrustNode(TrustNodeKind::INVALID, Node::null());
  65 }
  66
  67 TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
  68     : d_tnk(tnk), d_proven(p), d_gen(g)
  69 {
  70   // does not make sense to provide null node with generator
  71   Assert(!d_proven.isNull() || d_gen == nullptr);
  72 }
  73
  74 TrustNodeKind TrustNode::getKind() const { return d_tnk; }
  75
  76 Node TrustNode::getNode() const
  77 {
  78   return d_tnk == TrustNodeKind::LEMMA ? d_proven : d_proven[0];
  79 }
  80
  81 Node TrustNode::getProven() const { return d_proven; }
  82 ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
  83
  84 bool TrustNode::isNull() const { return d_proven.isNull(); }
  85
  86 Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
  87
  88 Node TrustNode::getLemmaProven(Node lem) { return lem; }
  89
  90 Node TrustNode::getPropExpProven(TNode lit, Node exp)
  91 {
  92   return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
  93 }
  94
  95 std::ostream& operator<<(std::ostream& out, TrustNode n)
  96 {
  97   out << "(trust " << n.getNode() << ")";
  98   return out;
  99 }
 100
 101 }  // namespace theory
 102 }  // namespace CVC4