src/theory/trust_substitutions.cpp

   1 /*********************                                                        */
   2 /*! \file trust_substitutions.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Gereon Kremer
   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                                            std::string name,
  25                                            PfRule trustId,
  26                                            MethodId ids)
  27     : d_ctx(c),
  28       d_subs(c),
  29       d_pnm(pnm),
  30       d_tsubs(c),
  31       d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
  32       d_subsPg(
  33           pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg")
  34               : nullptr),
  35       d_applyPg(pnm ? new LazyCDProof(
  36                           pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
  37                     : nullptr),
  38       d_helperPf(pnm, c),
  39       d_currentSubs(c),
  40       d_name(name),
  41       d_trustId(trustId),
  42       d_ids(ids)
  43 {
  44 }
  45
  46 void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
  47 {
  48   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
  49                       << " -> " << t << std::endl;
  50   d_subs.addSubstitution(x, t);
  51   if (isProofEnabled())
  52   {
  53     TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
  54     d_tsubs.push_back(tnl);
  55     // current substitution node is no longer valid.
  56     d_currentSubs = Node::null();
  57     // add to lazy proof
  58     d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
  59   }
  60 }
  61
  62 void TrustSubstitutionMap::addSubstitution(TNode x,
  63                                            TNode t,
  64                                            PfRule id,
  65                                            const std::vector<Node>& args)
  66 {
  67   if (!isProofEnabled())
  68   {
  69     addSubstitution(x, t, nullptr);
  70     return;
  71   }
  72   LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx);
  73   Node eq = x.eqNode(t);
  74   stepPg->addStep(eq, id, {}, args);
  75   addSubstitution(x, t, stepPg);
  76 }
  77
  78 ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
  79                                                             TNode t,
  80                                                             TrustNode tn)
  81 {
  82   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
  83                       << x << " -> " << t << " from " << tn.getProven()
  84                       << std::endl;
  85   if (!isProofEnabled() || tn.getGenerator() == nullptr)
  86   {
  87     // no generator or not proof enabled, nothing to do
  88     addSubstitution(x, t, nullptr);
  89     Trace("trust-subs") << "...no proof" << std::endl;
  90     return nullptr;
  91   }
  92   Node eq = x.eqNode(t);
  93   Node proven = tn.getProven();
  94   // notice that this checks syntactic equality, not CDProof::isSame since
  95   // tn.getGenerator() is not necessarily robust to symmetry.
  96   if (eq == proven)
  97   {
  98     // no rewrite required, just use the generator
  99     addSubstitution(x, t, tn.getGenerator());
 100     Trace("trust-subs") << "...use generator directly" << std::endl;
 101     return tn.getGenerator();
 102   }
 103   LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx);
 104   // Try to transform tn.getProven() to (= x t) here, if necessary
 105   if (!d_tspb->applyPredTransform(proven, eq, {}))
 106   {
 107     // failed to rewrite
 108     addSubstitution(x, t, nullptr);
 109     Trace("trust-subs") << "...failed to rewrite" << std::endl;
 110     return nullptr;
 111   }
 112   Trace("trust-subs") << "...successful rewrite" << std::endl;
 113   solvePg->addSteps(*d_tspb.get());
 114   d_tspb->clear();
 115   // link the given generator
 116   solvePg->addLazyStep(proven, tn.getGenerator());
 117   addSubstitution(x, t, solvePg);
 118   return solvePg;
 119 }
 120
 121 void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
 122 {
 123   if (!isProofEnabled())
 124   {
 125     // just use the basic utility
 126     d_subs.addSubstitutions(t.get());
 127     return;
 128   }
 129   // call addSubstitution above in sequence
 130   for (const TrustNode& tns : t.d_tsubs)
 131   {
 132     Node proven = tns.getProven();
 133     addSubstitution(proven[0], proven[1], tns.getGenerator());
 134   }
 135 }
 136
 137 TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
 138 {
 139   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
 140                       << std::endl;
 141   Node ns = d_subs.apply(n);
 142   Trace("trust-subs") << "...subs " << ns << std::endl;
 143   // rewrite if indicated
 144   if (doRewrite)
 145   {
 146     ns = Rewriter::rewrite(ns);
 147     Trace("trust-subs") << "...rewrite " << ns << std::endl;
 148   }
 149   if (n == ns)
 150   {
 151     // no change
 152     return TrustNode::null();
 153   }
 154   if (!isProofEnabled())
 155   {
 156     // no proofs, use null generator
 157     return TrustNode::mkTrustRewrite(n, ns, nullptr);
 158   }
 159   Node cs = getCurrentSubstitution();
 160   Trace("trust-subs")
 161       << "TrustSubstitutionMap::addSubstitution: current substitution is " << cs
 162       << std::endl;
 163   // Easy case: if n is in the domain of the substitution, maybe it is already
 164   // a proof in the substitution proof generator. This is moreover required
 165   // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
 166   // and we are asked to transform x, resulting in 5, we hence must provide
 167   // a proof of (= x 5) based on the substitution. However, it must be the
 168   // case that (= x 5) is a proven fact of the substitution generator. Hence
 169   // we avoid a proof that looks like:
 170   // ---------- from d_subsPg
 171   // (= x 5)
 172   // ---------- MACRO_SR_EQ_INTRO{x}
 173   // (= x 5)
 174   // by taking the premise proof directly.
 175   Node eq = n.eqNode(ns);
 176   if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq))
 177   {
 178     return TrustNode::mkTrustRewrite(n, ns, d_subsPg.get());
 179   }
 180   Assert(eq != cs);
 181   std::vector<Node> pfChildren;
 182   if (!cs.isConst())
 183   {
 184     // note we will get more proof reuse if we do not special case AND here.
 185     if (cs.getKind() == kind::AND)
 186     {
 187       for (const Node& csc : cs)
 188       {
 189         pfChildren.push_back(csc);
 190         // connect substitution generator into apply generator
 191         d_applyPg->addLazyStep(csc, d_subsPg.get());
 192       }
 193     }
 194     else
 195     {
 196       pfChildren.push_back(cs);
 197       // connect substitution generator into apply generator
 198       d_applyPg->addLazyStep(cs, d_subsPg.get());
 199     }
 200   }
 201   if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
 202   {
 203     // if we fail for any reason, we must use a trusted step instead
 204     d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
 205   }
 206   // -------        ------- from external proof generators
 207   // x1 = t1 ...    xn = tn
 208   // ----------------------- AND_INTRO
 209   //   ...
 210   // --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above)
 211   // n == ns
 212   // add it to the apply proof generator.
 213   //
 214   // Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an
 215   // optimization motivated by the fact that n may be large and reused many
 216   // time. For instance, if this class is being used to track substitutions
 217   // derived during non-clausal simplification during preprocessing, it is
 218   // a fixed (possibly) large substitution applied to many terms. Having
 219   // a single child saves us from creating many proofs with n children, where
 220   // notice this proof is reused.
 221   d_applyPg->addSteps(*d_tspb.get());
 222   d_tspb->clear();
 223   return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get());
 224 }
 225
 226 SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
 227
 228 bool TrustSubstitutionMap::isProofEnabled() const
 229 {
 230   return d_subsPg != nullptr;
 231 }
 232
 233 Node TrustSubstitutionMap::getCurrentSubstitution()
 234 {
 235   Assert(isProofEnabled());
 236   if (!d_currentSubs.get().isNull())
 237   {
 238     return d_currentSubs;
 239   }
 240   std::vector<Node> csubsChildren;
 241   for (const TrustNode& tns : d_tsubs)
 242   {
 243     csubsChildren.push_back(tns.getProven());
 244   }
 245   std::reverse(csubsChildren.begin(),csubsChildren.end());
 246   d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
 247   if (d_currentSubs.get().getKind() == kind::AND)
 248   {
 249     d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {});
 250   }
 251   return d_currentSubs;
 252 }
 253
 254 }  // namespace theory
 255 }  // namespace CVC4