src/smt/preprocessor.cpp

   1 /*********************                                                        */
   2 /*! \file preprocessor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
   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 preprocessor of the SMT engine.
  13  **/
  14
  15 #include "smt/preprocessor.h"
  16
  17 #include "options/smt_options.h"
  18 #include "printer/printer.h"
  19 #include "smt/abstract_values.h"
  20 #include "smt/assertions.h"
  21 #include "smt/dump.h"
  22 #include "smt/smt_engine.h"
  23
  24 using namespace CVC4::theory;
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace smt {
  29
  30 Preprocessor::Preprocessor(SmtEngine& smt,
  31                            context::UserContext* u,
  32                            AbstractValues& abs,
  33                            SmtEngineStatistics& stats)
  34     : d_context(u),
  35       d_smt(smt),
  36       d_absValues(abs),
  37       d_propagator(true, true),
  38       d_assertionsProcessed(u, false),
  39       d_exDefs(smt, *smt.getResourceManager(), stats),
  40       d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
  41       d_pnm(nullptr)
  42 {
  43 }
  44
  45 Preprocessor::~Preprocessor()
  46 {
  47   if (d_propagator.getNeedsFinish())
  48   {
  49     d_propagator.finish();
  50     d_propagator.setNeedsFinish(false);
  51   }
  52 }
  53
  54 void Preprocessor::finishInit()
  55 {
  56   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
  57       &d_smt, &d_propagator, d_pnm));
  58
  59   // initialize the preprocessing passes
  60   d_processor.finishInit(d_ppContext.get());
  61 }
  62
  63 bool Preprocessor::process(Assertions& as)
  64 {
  65   preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
  66
  67   // should not be called if empty
  68   Assert(ap.size() != 0)
  69       << "Can only preprocess a non-empty list of assertions";
  70
  71   if (d_assertionsProcessed && options::incrementalSolving())
  72   {
  73     // TODO(b/1255): Substitutions in incremental mode should be managed with a
  74     // proper data structure.
  75     ap.enableStoreSubstsInAsserts();
  76   }
  77   else
  78   {
  79     ap.disableStoreSubstsInAsserts();
  80   }
  81
  82   // process the assertions, return true if no conflict is discovered
  83   return d_processor.apply(as);
  84 }
  85
  86 void Preprocessor::postprocess(Assertions& as)
  87 {
  88   preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
  89   // if incremental, compute which variables are assigned
  90   if (options::incrementalSolving())
  91   {
  92     d_ppContext->recordSymbolsInAssertions(ap.ref());
  93   }
  94
  95   // mark that we've processed assertions
  96   d_assertionsProcessed = true;
  97 }
  98
  99 void Preprocessor::clearLearnedLiterals()
 100 {
 101   d_propagator.getLearnedLiterals().clear();
 102 }
 103
 104 void Preprocessor::cleanup() { d_processor.cleanup(); }
 105
 106 Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
 107 {
 108   std::unordered_map<Node, Node, NodeHashFunction> cache;
 109   return d_exDefs.expandDefinitions(n, cache, expandOnly);
 110 }
 111
 112 Node Preprocessor::expandDefinitions(
 113     const Node& node,
 114     std::unordered_map<Node, Node, NodeHashFunction>& cache,
 115     bool expandOnly)
 116 {
 117   Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
 118   // Substitute out any abstract values in node.
 119   Node n = d_absValues.substituteAbstractValues(node);
 120   if (options::typeChecking())
 121   {
 122     // Ensure node is type-checked at this point.
 123     n.getType(true);
 124   }
 125   // expand only = true
 126   return d_exDefs.expandDefinitions(n, cache, expandOnly);
 127 }
 128
 129 Node Preprocessor::simplify(const Node& node)
 130 {
 131   Trace("smt") << "SMT simplify(" << node << ")" << endl;
 132   if (Dump.isOn("benchmark"))
 133   {
 134     d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
 135         d_smt.getOutputManager().getDumpOut(), node);
 136   }
 137   Node nas = d_absValues.substituteAbstractValues(node);
 138   if (options::typeChecking())
 139   {
 140     // ensure node is type-checked at this point
 141     nas.getType(true);
 142   }
 143   std::unordered_map<Node, Node, NodeHashFunction> cache;
 144   Node n = d_exDefs.expandDefinitions(nas, cache);
 145   TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
 146   Node ns = ts.isNull() ? n : ts.getNode();
 147   return ns;
 148 }
 149
 150 void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
 151 {
 152   Assert(pppg != nullptr);
 153   d_pnm = pppg->getManager();
 154   d_exDefs.setProofNodeManager(d_pnm);
 155   d_propagator.setProof(d_pnm, d_context, pppg);
 156 }
 157
 158 }  // namespace smt
 159 }  // namespace CVC4