src/theory/theory_preprocessor.cpp

   1 /*********************                                                        */
   2 /*! \file theory_preprocessor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
   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 The theory preprocessor
  13  **/
  14
  15 #include "theory/theory_preprocessor.h"
  16
  17 #include "expr/lazy_proof.h"
  18 #include "expr/skolem_manager.h"
  19 #include "theory/logic_info.h"
  20 #include "theory/rewriter.h"
  21 #include "theory/theory_engine.h"
  22
  23 using namespace std;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
  29                                        RemoveTermFormulas& tfr,
  30                                        context::UserContext* userContext,
  31                                        ProofNodeManager* pnm)
  32     : d_engine(engine),
  33       d_logicInfo(engine.getLogicInfo()),
  34       d_ppCache(userContext),
  35       d_tfr(tfr),
  36       d_tpg(pnm ? new TConvProofGenerator(
  37                       pnm,
  38                       userContext,
  39                       TConvPolicy::FIXPOINT,
  40                       TConvCachePolicy::NEVER,
  41                       "TheoryPreprocessor::preprocess_rewrite",
  42                       &d_iqtc)
  43                 : nullptr),
  44       d_tspg(nullptr),
  45       d_tpgRew(pnm ? new TConvProofGenerator(pnm,
  46                                              userContext,
  47                                              TConvPolicy::FIXPOINT,
  48                                              TConvCachePolicy::NEVER,
  49                                              "TheoryPreprocessor::rewrite")
  50                    : nullptr),
  51       d_tspgNoPp(nullptr),
  52       d_lp(pnm ? new LazyCDProof(pnm,
  53                                  nullptr,
  54                                  userContext,
  55                                  "TheoryPreprocessor::LazyCDProof")
  56                : nullptr)
  57 {
  58   if (isProofEnabled())
  59   {
  60     // Make the main term conversion sequence generator, which tracks up to
  61     // three conversions made in succession:
  62     // (1) theory preprocessing+rewriting
  63     // (2) term formula removal
  64     // (3) rewriting
  65     // Steps (1) and (3) use a common term conversion generator.
  66     std::vector<ProofGenerator*> ts;
  67     ts.push_back(d_tpg.get());
  68     ts.push_back(d_tfr.getTConvProofGenerator());
  69     ts.push_back(d_tpg.get());
  70     d_tspg.reset(new TConvSeqProofGenerator(
  71         pnm, ts, userContext, "TheoryPreprocessor::sequence"));
  72     // Make the "no preprocess" term conversion sequence generator, which
  73     // applies only steps (2) and (3), where notice (3) must use the
  74     // "pure rewrite" term conversion (d_tpgRew).
  75     std::vector<ProofGenerator*> tsNoPp;
  76     tsNoPp.push_back(d_tfr.getTConvProofGenerator());
  77     tsNoPp.push_back(d_tpgRew.get());
  78     d_tspgNoPp.reset(new TConvSeqProofGenerator(
  79         pnm, tsNoPp, userContext, "TheoryPreprocessor::sequence_no_pp"));
  80   }
  81 }
  82
  83 TheoryPreprocessor::~TheoryPreprocessor() {}
  84
  85 TrustNode TheoryPreprocessor::preprocess(TNode node,
  86                                          std::vector<TrustNode>& newLemmas,
  87                                          std::vector<Node>& newSkolems,
  88                                          bool doTheoryPreprocess)
  89 {
  90   // In this method, all rewriting steps of node are stored in d_tpg.
  91
  92   Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
  93                      << ", doTheoryPreprocess=" << doTheoryPreprocess
  94                      << std::endl;
  95   // Run theory preprocessing, maybe
  96   Node ppNode = node;
  97   if (doTheoryPreprocess)
  98   {
  99     // run theory preprocessing
 100     TrustNode tpp = theoryPreprocess(node);
 101     ppNode = tpp.getNode();
 102   }
 103
 104   // Remove the ITEs
 105   TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
 106   Node rtfNode = ttfr.getNode();
 107
 108   if (Debug.isOn("lemma-ites"))
 109   {
 110     Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode()
 111                         << endl;
 112     Debug("lemma-ites") << " + now have the following " << newLemmas.size()
 113                         << " lemma(s):" << endl;
 114     for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)
 115     {
 116       Debug("lemma-ites") << " + " << newLemmas[i].getNode() << endl;
 117     }
 118     Debug("lemma-ites") << endl;
 119   }
 120   // Rewrite the main node, we rewrite and store the proof step, if necessary,
 121   // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
 122   Node retNode = rewriteWithProof(rtfNode);
 123
 124   if (Trace.isOn("tpp-debug"))
 125   {
 126     if (node != ppNode)
 127     {
 128       Trace("tpp-debug") << "after preprocessing : " << ppNode << std::endl;
 129     }
 130     if (rtfNode != ppNode)
 131     {
 132       Trace("tpp-debug") << "after rtf : " << rtfNode << std::endl;
 133     }
 134     if (retNode != rtfNode)
 135     {
 136       Trace("tpp-debug") << "after rewriting : " << retNode << std::endl;
 137     }
 138     Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
 139   }
 140   if (node == retNode)
 141   {
 142     // no change
 143     Assert(newLemmas.empty());
 144     return TrustNode::null();
 145   }
 146
 147   // Now, sequence the conversion steps if proofs are enabled.
 148   TrustNode tret;
 149   if (isProofEnabled())
 150   {
 151     std::vector<Node> cterms;
 152     cterms.push_back(node);
 153     if (doTheoryPreprocess)
 154     {
 155       cterms.push_back(ppNode);
 156     }
 157     cterms.push_back(rtfNode);
 158     cterms.push_back(retNode);
 159     // We have that:
 160     // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
 161     // ppNode -> rtfNode via term formula removal
 162     // rtfNode -> retNode via rewriting
 163     if (!doTheoryPreprocess)
 164     {
 165       // If preprocessing is not performed, we cannot use the main sequence
 166       // generator, instead we use d_tspgNoPp.
 167       // We register the top-level rewrite in the pure rewrite term converter.
 168       d_tpgRew->addRewriteStep(
 169           rtfNode, retNode, PfRule::REWRITE, {}, {rtfNode});
 170       // Now get the trust node from the sequence generator
 171       tret = d_tspgNoPp->mkTrustRewriteSequence(cterms);
 172     }
 173     else
 174     {
 175       // we wil use the sequence generator
 176       tret = d_tspg->mkTrustRewriteSequence(cterms);
 177     }
 178     tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
 179   }
 180   else
 181   {
 182     tret = TrustNode::mkTrustRewrite(node, retNode, nullptr);
 183   }
 184
 185   // now, rewrite the lemmas
 186   Trace("tpp-debug") << "TheoryPreprocessor::preprocess: process lemmas"
 187                      << std::endl;
 188   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
 189   {
 190     // get the trust node to process
 191     TrustNode trn = newLemmas[i];
 192     trn.debugCheckClosed(
 193         "tpp-debug", "TheoryPreprocessor::lemma_new_initial", false);
 194     Assert(trn.getKind() == TrustNodeKind::LEMMA);
 195     Node assertion = trn.getNode();
 196     // rewrite, which is independent of d_tpg, since additional lemmas
 197     // are justified separately.
 198     Node rewritten = Rewriter::rewrite(assertion);
 199     if (assertion != rewritten)
 200     {
 201       if (isProofEnabled())
 202       {
 203         Assert(d_lp != nullptr);
 204         // store in the lazy proof
 205         d_lp->addLazyStep(assertion,
 206                           trn.getGenerator(),
 207                           PfRule::THEORY_PREPROCESS_LEMMA,
 208                           true,
 209                           "TheoryPreprocessor::rewrite_lemma_new");
 210         d_lp->addStep(rewritten,
 211                       PfRule::MACRO_SR_PRED_TRANSFORM,
 212                       {assertion},
 213                       {rewritten});
 214       }
 215       newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
 216     }
 217     Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
 218     newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
 219   }
 220   Trace("tpp-debug") << "Preprocessed: " << node << " " << retNode << std::endl;
 221   return tret;
 222 }
 223
 224 struct preprocess_stack_element
 225 {
 226   TNode node;
 227   bool children_added;
 228   preprocess_stack_element(TNode n) : node(n), children_added(false) {}
 229 };
 230
 231 TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
 232 {
 233   Trace("theory::preprocess")
 234       << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
 235   // spendResource();
 236
 237   // Do a topological sort of the subexpressions and substitute them
 238   vector<preprocess_stack_element> toVisit;
 239   toVisit.push_back(assertion);
 240
 241   while (!toVisit.empty())
 242   {
 243     // The current node we are processing
 244     preprocess_stack_element& stackHead = toVisit.back();
 245     TNode current = stackHead.node;
 246
 247     Trace("theory::preprocess-debug")
 248         << "TheoryPreprocessor::theoryPreprocess(" << assertion
 249         << "): processing " << current << endl;
 250
 251     // If node already in the cache we're done, pop from the stack
 252     NodeMap::iterator find = d_ppCache.find(current);
 253     if (find != d_ppCache.end())
 254     {
 255       toVisit.pop_back();
 256       continue;
 257     }
 258
 259     if (!d_logicInfo.isTheoryEnabled(Theory::theoryOf(current))
 260         && Theory::theoryOf(current) != THEORY_SAT_SOLVER)
 261     {
 262       stringstream ss;
 263       ss << "The logic was specified as " << d_logicInfo.getLogicString()
 264          << ", which doesn't include " << Theory::theoryOf(current)
 265          << ", but got a preprocessing-time fact for that theory." << endl
 266          << "The fact:" << endl
 267          << current;
 268       throw LogicException(ss.str());
 269     }
 270
 271     // If this is an atom, we preprocess its terms with the theory ppRewriter
 272     if (Theory::theoryOf(current) != THEORY_BOOL)
 273     {
 274       Node ppRewritten = ppTheoryRewrite(current);
 275       d_ppCache[current] = ppRewritten;
 276       Assert(Rewriter::rewrite(d_ppCache[current].get())
 277              == d_ppCache[current].get());
 278       continue;
 279     }
 280
 281     // Not yet substituted, so process
 282     if (stackHead.children_added)
 283     {
 284       // Children have been processed, so substitute
 285       NodeBuilder<> builder(current.getKind());
 286       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
 287       {
 288         builder << current.getOperator();
 289       }
 290       for (unsigned i = 0; i < current.getNumChildren(); ++i)
 291       {
 292         Assert(d_ppCache.find(current[i]) != d_ppCache.end());
 293         builder << d_ppCache[current[i]].get();
 294       }
 295       // Mark the substitution and continue
 296       Node result = builder;
 297       if (result != current)
 298       {
 299         result = rewriteWithProof(result);
 300       }
 301       Trace("theory::preprocess-debug")
 302           << "TheoryPreprocessor::theoryPreprocess(" << assertion
 303           << "): setting " << current << " -> " << result << endl;
 304       d_ppCache[current] = result;
 305       toVisit.pop_back();
 306     }
 307     else
 308     {
 309       // Mark that we have added the children if any
 310       if (current.getNumChildren() > 0)
 311       {
 312         stackHead.children_added = true;
 313         // We need to add the children
 314         for (TNode::iterator child_it = current.begin();
 315              child_it != current.end();
 316              ++child_it)
 317         {
 318           TNode childNode = *child_it;
 319           NodeMap::iterator childFind = d_ppCache.find(childNode);
 320           if (childFind == d_ppCache.end())
 321           {
 322             toVisit.push_back(childNode);
 323           }
 324         }
 325       }
 326       else
 327       {
 328         // No children, so we're done
 329         Trace("theory::preprocess-debug")
 330             << "SubstitutionMap::internalSubstitute(" << assertion
 331             << "): setting " << current << " -> " << current << endl;
 332         d_ppCache[current] = current;
 333         toVisit.pop_back();
 334       }
 335     }
 336   }
 337   // Return the substituted version
 338   Node res = d_ppCache[assertion];
 339   return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
 340 }
 341
 342 // Recursively traverse a term and call the theory rewriter on its sub-terms
 343 Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
 344 {
 345   NodeMap::iterator find = d_ppCache.find(term);
 346   if (find != d_ppCache.end())
 347   {
 348     return (*find).second;
 349   }
 350   unsigned nc = term.getNumChildren();
 351   if (nc == 0)
 352   {
 353     return preprocessWithProof(term);
 354   }
 355   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 356
 357   Node newTerm = term;
 358   // do not rewrite inside quantifiers
 359   if (!term.isClosure())
 360   {
 361     NodeBuilder<> newNode(term.getKind());
 362     if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
 363     {
 364       newNode << term.getOperator();
 365     }
 366     unsigned i;
 367     for (i = 0; i < nc; ++i)
 368     {
 369       newNode << ppTheoryRewrite(term[i]);
 370     }
 371     newTerm = Node(newNode);
 372   }
 373   newTerm = rewriteWithProof(newTerm);
 374   newTerm = preprocessWithProof(newTerm);
 375   d_ppCache[term] = newTerm;
 376   Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
 377   return newTerm;
 378 }
 379
 380 Node TheoryPreprocessor::rewriteWithProof(Node term)
 381 {
 382   Node termr = Rewriter::rewrite(term);
 383   // store rewrite step if tracking proofs and it rewrites
 384   if (isProofEnabled())
 385   {
 386     // may rewrite the same term more than once, thus check hasRewriteStep
 387     if (termr != term)
 388     {
 389       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
 390                          << term << " -> " << termr << std::endl;
 391       // always use term context hash 0 (default)
 392       d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
 393     }
 394   }
 395   return termr;
 396 }
 397
 398 Node TheoryPreprocessor::preprocessWithProof(Node term)
 399 {
 400   // Important that it is in rewritten form, to ensure that the rewrite steps
 401   // recorded in d_tpg are functional. In other words, there should not
 402   // be steps from the same term to multiple rewritten forms, which would be
 403   // the case if we registered a preprocessing step for a non-rewritten term.
 404   Assert(term == Rewriter::rewrite(term));
 405   // call ppRewrite for the given theory
 406   TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
 407   if (trn.isNull())
 408   {
 409     // no change, return original term
 410     return term;
 411   }
 412   Node termr = trn.getNode();
 413   Assert(term != termr);
 414   if (isProofEnabled())
 415   {
 416     if (trn.getGenerator() != nullptr)
 417     {
 418       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
 419                          << term << " -> " << termr << std::endl;
 420       trn.debugCheckClosed("tpp-debug",
 421                            "TheoryPreprocessor::preprocessWithProof");
 422       // always use term context hash 0 (default)
 423       d_tpg->addRewriteStep(
 424           term, termr, trn.getGenerator(), PfRule::ASSUME, true);
 425     }
 426     else
 427     {
 428       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
 429                          << term << " -> " << termr << std::endl;
 430       // small step trust
 431       d_tpg->addRewriteStep(
 432           term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});
 433     }
 434   }
 435   termr = rewriteWithProof(termr);
 436   return ppTheoryRewrite(termr);
 437 }
 438
 439 bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
 440
 441 }  // namespace theory
 442 }  // namespace CVC4