src/theory/theory_preprocessor.cpp

   1 /*********************                                                        */
   2 /*! \file theory_preprocessor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
   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                                        context::UserContext* userContext,
  30                                        ProofNodeManager* pnm)
  31     : d_engine(engine),
  32       d_logicInfo(engine.getLogicInfo()),
  33       d_ppCache(userContext),
  34       d_tfr(userContext, pnm),
  35       d_tpg(pnm ? new TConvProofGenerator(
  36                       pnm,
  37                       userContext,
  38                       TConvPolicy::FIXPOINT,
  39                       TConvCachePolicy::NEVER,
  40                       "TheoryPreprocessor::preprocess_rewrite",
  41                       &d_iqtc)
  42                 : nullptr),
  43       d_tspg(nullptr),
  44       d_tpgRew(pnm ? new TConvProofGenerator(pnm,
  45                                              userContext,
  46                                              TConvPolicy::FIXPOINT,
  47                                              TConvCachePolicy::NEVER,
  48                                              "TheoryPreprocessor::rewrite")
  49                    : nullptr),
  50       d_tspgNoPp(nullptr),
  51       d_lp(pnm ? new LazyCDProof(pnm,
  52                                  nullptr,
  53                                  userContext,
  54                                  "TheoryPreprocessor::LazyCDProof")
  55                : nullptr)
  56 {
  57   if (isProofEnabled())
  58   {
  59     // Make the main term conversion sequence generator, which tracks up to
  60     // three conversions made in succession:
  61     // (1) theory preprocessing+rewriting
  62     // (2) term formula removal
  63     // (3) rewriting
  64     // Steps (1) and (3) use a common term conversion generator.
  65     std::vector<ProofGenerator*> ts;
  66     ts.push_back(d_tpg.get());
  67     ts.push_back(d_tfr.getTConvProofGenerator());
  68     ts.push_back(d_tpg.get());
  69     d_tspg.reset(new TConvSeqProofGenerator(
  70         pnm, ts, userContext, "TheoryPreprocessor::sequence"));
  71     // Make the "no preprocess" term conversion sequence generator, which
  72     // applies only steps (2) and (3), where notice (3) must use the
  73     // "pure rewrite" term conversion (d_tpgRew).
  74     std::vector<ProofGenerator*> tsNoPp;
  75     tsNoPp.push_back(d_tfr.getTConvProofGenerator());
  76     tsNoPp.push_back(d_tpgRew.get());
  77     d_tspgNoPp.reset(new TConvSeqProofGenerator(
  78         pnm, tsNoPp, userContext, "TheoryPreprocessor::sequence_no_pp"));
  79   }
  80 }
  81
  82 TheoryPreprocessor::~TheoryPreprocessor() {}
  83
  84 TrustNode TheoryPreprocessor::preprocess(TNode node,
  85                                          std::vector<TrustNode>& newLemmas,
  86                                          std::vector<Node>& newSkolems,
  87                                          bool doTheoryPreprocess,
  88                                          bool fixedPoint)
  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, fixed point
 105   TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, fixedPoint);
 106   Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
 107
 108   if (Debug.isOn("lemma-ites"))
 109   {
 110     Debug("lemma-ites") << "removed ITEs from lemma: " << rtfNode << endl;
 111     Debug("lemma-ites") << " + now have the following " << newLemmas.size()
 112                         << " lemma(s):" << endl;
 113     for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)
 114     {
 115       Debug("lemma-ites") << " + " << newLemmas[i].getNode() << endl;
 116     }
 117     Debug("lemma-ites") << endl;
 118   }
 119   // Rewrite the main node, we rewrite and store the proof step, if necessary,
 120   // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
 121   Node retNode = rewriteWithProof(rtfNode);
 122
 123   if (Trace.isOn("tpp-debug"))
 124   {
 125     if (node != ppNode)
 126     {
 127       Trace("tpp-debug") << "after preprocessing : " << ppNode << std::endl;
 128     }
 129     if (rtfNode != ppNode)
 130     {
 131       Trace("tpp-debug") << "after rtf : " << rtfNode << std::endl;
 132     }
 133     if (retNode != rtfNode)
 134     {
 135       Trace("tpp-debug") << "after rewriting : " << retNode << std::endl;
 136     }
 137     Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
 138   }
 139   if (node == retNode)
 140   {
 141     Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
 142                        << std::endl;
 143     // no change
 144     Assert(newLemmas.empty());
 145     return TrustNode::null();
 146   }
 147
 148   // Now, sequence the conversion steps if proofs are enabled.
 149   TrustNode tret;
 150   if (isProofEnabled())
 151   {
 152     std::vector<Node> cterms;
 153     cterms.push_back(node);
 154     if (doTheoryPreprocess)
 155     {
 156       cterms.push_back(ppNode);
 157     }
 158     cterms.push_back(rtfNode);
 159     cterms.push_back(retNode);
 160     // We have that:
 161     // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
 162     // ppNode -> rtfNode via term formula removal
 163     // rtfNode -> retNode via rewriting
 164     if (!doTheoryPreprocess)
 165     {
 166       // If preprocessing is not performed, we cannot use the main sequence
 167       // generator, instead we use d_tspgNoPp.
 168       // We register the top-level rewrite in the pure rewrite term converter.
 169       d_tpgRew->addRewriteStep(
 170           rtfNode, retNode, PfRule::REWRITE, {}, {rtfNode});
 171       // Now get the trust node from the sequence generator
 172       tret = d_tspgNoPp->mkTrustRewriteSequence(cterms);
 173     }
 174     else
 175     {
 176       // we wil use the sequence generator
 177       tret = d_tspg->mkTrustRewriteSequence(cterms);
 178     }
 179     tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
 180   }
 181   else
 182   {
 183     tret = TrustNode::mkTrustRewrite(node, retNode, nullptr);
 184   }
 185
 186   // now, rewrite the lemmas
 187   Trace("tpp-debug") << "TheoryPreprocessor::preprocess: process lemmas"
 188                      << std::endl;
 189   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
 190   {
 191     // get the trust node to process
 192     TrustNode trn = newLemmas[i];
 193     trn.debugCheckClosed(
 194         "tpp-debug", "TheoryPreprocessor::lemma_new_initial", false);
 195     Assert(trn.getKind() == TrustNodeKind::LEMMA);
 196     Node assertion = trn.getNode();
 197     // rewrite, which is independent of d_tpg, since additional lemmas
 198     // are justified separately.
 199     Node rewritten = Rewriter::rewrite(assertion);
 200     if (assertion != rewritten)
 201     {
 202       if (isProofEnabled())
 203       {
 204         Assert(d_lp != nullptr);
 205         // store in the lazy proof
 206         d_lp->addLazyStep(assertion,
 207                           trn.getGenerator(),
 208                           PfRule::THEORY_PREPROCESS_LEMMA,
 209                           true,
 210                           "TheoryPreprocessor::rewrite_lemma_new");
 211         d_lp->addStep(rewritten,
 212                       PfRule::MACRO_SR_PRED_TRANSFORM,
 213                       {assertion},
 214                       {rewritten});
 215       }
 216       newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
 217     }
 218     Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
 219     newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
 220   }
 221   Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
 222                      << tret.getNode() << std::endl;
 223   return tret;
 224 }
 225
 226 TrustNode TheoryPreprocessor::preprocess(TNode node, bool doTheoryPreprocess)
 227 {
 228   // ignore lemmas, no fixed point
 229   std::vector<TrustNode> newLemmas;
 230   std::vector<Node> newSkolems;
 231   return preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, false);
 232 }
 233
 234 TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
 235                                               std::vector<TrustNode>& newLemmas,
 236                                               std::vector<Node>& newSkolems,
 237                                               bool doTheoryPreprocess,
 238                                               bool fixedPoint)
 239 {
 240   // what was originally proven
 241   Node lemma = node.getProven();
 242   TrustNode tplemma =
 243       preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess, fixedPoint);
 244   if (tplemma.isNull())
 245   {
 246     // no change needed
 247     return node;
 248   }
 249   Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
 250   // what it was preprocessed to
 251   Node lemmap = tplemma.getNode();
 252   Assert(lemmap != node.getProven());
 253   // process the preprocessing
 254   if (isProofEnabled())
 255   {
 256     Assert(d_lp != nullptr);
 257     // add the original proof to the lazy proof
 258     d_lp->addLazyStep(node.getProven(), node.getGenerator());
 259     // only need to do anything if lemmap changed in a non-trivial way
 260     if (!CDProof::isSame(lemmap, lemma))
 261     {
 262       d_lp->addLazyStep(tplemma.getProven(),
 263                         tplemma.getGenerator(),
 264                         PfRule::PREPROCESS_LEMMA,
 265                         true,
 266                         "TheoryEngine::lemma_pp");
 267       // ---------- from node -------------- from theory preprocess
 268       // lemma                lemma = lemmap
 269       // ------------------------------------------ EQ_RESOLVE
 270       // lemmap
 271       std::vector<Node> pfChildren;
 272       pfChildren.push_back(lemma);
 273       pfChildren.push_back(tplemma.getProven());
 274       d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
 275     }
 276   }
 277   return TrustNode::mkTrustLemma(lemmap, d_lp.get());
 278 }
 279
 280 TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
 281                                               bool doTheoryPreprocess)
 282 {
 283   // ignore lemmas, no fixed point
 284   std::vector<TrustNode> newLemmas;
 285   std::vector<Node> newSkolems;
 286   return preprocessLemma(
 287       node, newLemmas, newSkolems, doTheoryPreprocess, false);
 288 }
 289
 290 RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
 291 {
 292   return d_tfr;
 293 }
 294
 295 struct preprocess_stack_element
 296 {
 297   TNode node;
 298   bool children_added;
 299   preprocess_stack_element(TNode n) : node(n), children_added(false) {}
 300 };
 301
 302 TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
 303 {
 304   Trace("theory::preprocess")
 305       << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
 306   // spendResource();
 307
 308   // Do a topological sort of the subexpressions and substitute them
 309   vector<preprocess_stack_element> toVisit;
 310   toVisit.push_back(assertion);
 311
 312   while (!toVisit.empty())
 313   {
 314     // The current node we are processing
 315     preprocess_stack_element& stackHead = toVisit.back();
 316     TNode current = stackHead.node;
 317
 318     Trace("theory::preprocess-debug")
 319         << "TheoryPreprocessor::theoryPreprocess(" << assertion
 320         << "): processing " << current << endl;
 321
 322     // If node already in the cache we're done, pop from the stack
 323     NodeMap::iterator find = d_ppCache.find(current);
 324     if (find != d_ppCache.end())
 325     {
 326       toVisit.pop_back();
 327       continue;
 328     }
 329
 330     if (!d_logicInfo.isTheoryEnabled(Theory::theoryOf(current))
 331         && Theory::theoryOf(current) != THEORY_SAT_SOLVER)
 332     {
 333       stringstream ss;
 334       ss << "The logic was specified as " << d_logicInfo.getLogicString()
 335          << ", which doesn't include " << Theory::theoryOf(current)
 336          << ", but got a preprocessing-time fact for that theory." << endl
 337          << "The fact:" << endl
 338          << current;
 339       throw LogicException(ss.str());
 340     }
 341
 342     // If this is an atom, we preprocess its terms with the theory ppRewriter
 343     if (Theory::theoryOf(current) != THEORY_BOOL)
 344     {
 345       Node ppRewritten = ppTheoryRewrite(current);
 346       d_ppCache[current] = ppRewritten;
 347       Assert(Rewriter::rewrite(d_ppCache[current].get())
 348              == d_ppCache[current].get());
 349       continue;
 350     }
 351
 352     // Not yet substituted, so process
 353     if (stackHead.children_added)
 354     {
 355       // Children have been processed, so substitute
 356       NodeBuilder<> builder(current.getKind());
 357       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
 358       {
 359         builder << current.getOperator();
 360       }
 361       for (unsigned i = 0; i < current.getNumChildren(); ++i)
 362       {
 363         Assert(d_ppCache.find(current[i]) != d_ppCache.end());
 364         builder << d_ppCache[current[i]].get();
 365       }
 366       // Mark the substitution and continue
 367       Node result = builder;
 368       if (result != current)
 369       {
 370         result = rewriteWithProof(result);
 371       }
 372       Trace("theory::preprocess-debug")
 373           << "TheoryPreprocessor::theoryPreprocess(" << assertion
 374           << "): setting " << current << " -> " << result << endl;
 375       d_ppCache[current] = result;
 376       toVisit.pop_back();
 377     }
 378     else
 379     {
 380       // Mark that we have added the children if any
 381       if (current.getNumChildren() > 0)
 382       {
 383         stackHead.children_added = true;
 384         // We need to add the children
 385         for (TNode::iterator child_it = current.begin();
 386              child_it != current.end();
 387              ++child_it)
 388         {
 389           TNode childNode = *child_it;
 390           NodeMap::iterator childFind = d_ppCache.find(childNode);
 391           if (childFind == d_ppCache.end())
 392           {
 393             toVisit.push_back(childNode);
 394           }
 395         }
 396       }
 397       else
 398       {
 399         // No children, so we're done
 400         Trace("theory::preprocess-debug")
 401             << "SubstitutionMap::internalSubstitute(" << assertion
 402             << "): setting " << current << " -> " << current << endl;
 403         d_ppCache[current] = current;
 404         toVisit.pop_back();
 405       }
 406     }
 407   }
 408   // Return the substituted version
 409   Node res = d_ppCache[assertion];
 410   return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
 411 }
 412
 413 // Recursively traverse a term and call the theory rewriter on its sub-terms
 414 Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
 415 {
 416   NodeMap::iterator find = d_ppCache.find(term);
 417   if (find != d_ppCache.end())
 418   {
 419     return (*find).second;
 420   }
 421   if (term.getNumChildren() == 0)
 422   {
 423     return preprocessWithProof(term);
 424   }
 425   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 426   // We must rewrite before preprocessing, because some terms when rewritten
 427   // may introduce new terms that are not top-level and require preprocessing.
 428   // An example of this is (forall ((x Int)) (and (tail L) (P x))) which
 429   // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
 430   // must be preprocessed as a child here.
 431   Node newTerm = rewriteWithProof(term);
 432   // do not rewrite inside quantifiers
 433   if (newTerm.getNumChildren() > 0 && !newTerm.isClosure())
 434   {
 435     NodeBuilder<> newNode(newTerm.getKind());
 436     if (newTerm.getMetaKind() == kind::metakind::PARAMETERIZED)
 437     {
 438       newNode << newTerm.getOperator();
 439     }
 440     for (const Node& nt : newTerm)
 441     {
 442       newNode << ppTheoryRewrite(nt);
 443     }
 444     newTerm = Node(newNode);
 445     newTerm = rewriteWithProof(newTerm);
 446   }
 447   newTerm = preprocessWithProof(newTerm);
 448   d_ppCache[term] = newTerm;
 449   Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
 450   return newTerm;
 451 }
 452
 453 Node TheoryPreprocessor::rewriteWithProof(Node term)
 454 {
 455   Node termr = Rewriter::rewrite(term);
 456   // store rewrite step if tracking proofs and it rewrites
 457   if (isProofEnabled())
 458   {
 459     // may rewrite the same term more than once, thus check hasRewriteStep
 460     if (termr != term)
 461     {
 462       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
 463                          << term << " -> " << termr << std::endl;
 464       // always use term context hash 0 (default)
 465       d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
 466     }
 467   }
 468   return termr;
 469 }
 470
 471 Node TheoryPreprocessor::preprocessWithProof(Node term)
 472 {
 473   // Important that it is in rewritten form, to ensure that the rewrite steps
 474   // recorded in d_tpg are functional. In other words, there should not
 475   // be steps from the same term to multiple rewritten forms, which would be
 476   // the case if we registered a preprocessing step for a non-rewritten term.
 477   Assert(term == Rewriter::rewrite(term));
 478   // We never call ppRewrite on equalities here, since equalities have a
 479   // special status. In particular, notice that theory preprocessing can be
 480   // called on all formulas asserted to theory engine, including those generated
 481   // as new literals appearing in lemmas. Calling ppRewrite on equalities is
 482   // incompatible with theory combination where a split on equality requested
 483   // by a theory could be preprocessed to something else, thus making theory
 484   // combination either non-terminating or result in solution soundness.
 485   // Notice that an alternative solution is to ensure that certain lemmas
 486   // (e.g. splits from theory combination) can never have theory preprocessing
 487   // applied to them. However, it is more uniform to say that theory
 488   // preprocessing is applied to all formulas. This makes it so that e.g.
 489   // theory solvers do not need to specify whether they want their lemmas to
 490   // be theory-preprocessed or not.
 491   if (term.getKind() == kind::EQUAL)
 492   {
 493     return term;
 494   }
 495   // call ppRewrite for the given theory
 496   TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
 497   if (trn.isNull())
 498   {
 499     // no change, return original term
 500     return term;
 501   }
 502   Node termr = trn.getNode();
 503   Assert(term != termr);
 504   if (isProofEnabled())
 505   {
 506     if (trn.getGenerator() != nullptr)
 507     {
 508       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
 509                          << term << " -> " << termr << std::endl;
 510       trn.debugCheckClosed("tpp-debug",
 511                            "TheoryPreprocessor::preprocessWithProof");
 512       // always use term context hash 0 (default)
 513       d_tpg->addRewriteStep(
 514           term, termr, trn.getGenerator(), PfRule::ASSUME, true);
 515     }
 516     else
 517     {
 518       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
 519                          << term << " -> " << termr << std::endl;
 520       // small step trust
 521       d_tpg->addRewriteStep(
 522           term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});
 523     }
 524   }
 525   termr = rewriteWithProof(termr);
 526   return ppTheoryRewrite(termr);
 527 }
 528
 529 bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
 530
 531 }  // namespace theory
 532 }  // namespace CVC4