src/theory/trust_substitutions.cpp

   1 /*********************                                                        */
   2 /*! \file trust_substitutions.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 Trust substitutions
  13  **/
  14
  15 #include "theory/trust_substitutions.h"
  16
  17 #include "theory/rewriter.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21
  22 TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
  23                                            ProofNodeManager* pnm)
  24     : d_subs(c)
  25 {
  26 }
  27
  28 void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
  29 {
  30   d_subs.addSubstitution(x, t);
  31 }
  32
  33 TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
  34 {
  35   Node ns = d_subs.apply(n);
  36   if (doRewrite)
  37   {
  38     ns = Rewriter::rewrite(ns);
  39   }
  40   return TrustNode::mkTrustRewrite(n, ns, nullptr);
  41 }
  42
  43 void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn)
  44 {
  45   if (!isProofEnabled() || tn.getGenerator() == nullptr)
  46   {
  47     // no generator or not proof enabled, nothing to do
  48     addSubstitution(x, t, nullptr);
  49     return;
  50   }
  51   // NOTE: can try to transform tn.getProven() to (= x t) here
  52   addSubstitution(x, t, nullptr);
  53 }
  54
  55 SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
  56
  57 bool TrustSubstitutionMap::isProofEnabled() const { return false; }
  58
  59 }  // namespace theory
  60 }  // namespace CVC4