src/theory/bv/bv_solver_lazy.h

   1 /*********************                                                        */
   2 /*! \file bv_solver_lazy.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Liana Hadarean, 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 Lazy bit-vector solver.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
  18 #define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
  19
  20 #include <unordered_map>
  21 #include <unordered_set>
  22
  23 #include "context/cdhashset.h"
  24 #include "context/cdlist.h"
  25 #include "context/context.h"
  26 #include "theory/bv/bv_solver.h"
  27 #include "theory/bv/bv_subtheory.h"
  28 #include "theory/bv/theory_bv.h"
  29 #include "util/hash.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace bv {
  34
  35 class CoreSolver;
  36 class InequalitySolver;
  37 class AlgebraicSolver;
  38 class BitblastSolver;
  39 class EagerBitblastSolver;
  40 class AbstractionModule;
  41
  42 class BVSolverLazy : public BVSolver
  43 {
  44   /** Back reference to TheoryBV */
  45   TheoryBV& d_bv;
  46
  47   /** The context we are using */
  48   context::Context* d_context;
  49
  50   /** Context dependent set of atoms we already propagated */
  51   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
  52   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
  53
  54   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
  55   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
  56       d_subtheoryMap;
  57
  58  public:
  59   BVSolverLazy(TheoryBV& bv,
  60                context::Context* c,
  61                context::UserContext* u,
  62                ProofNodeManager* pnm = nullptr,
  63                std::string name = "");
  64
  65   ~BVSolverLazy();
  66
  67   //--------------------------------- initialization
  68
  69   /**
  70    * Returns true if we need an equality engine. If so, we initialize the
  71    * information regarding how it should be setup. For details, see the
  72    * documentation in Theory::needsEqualityEngine.
  73    */
  74   bool needsEqualityEngine(EeSetupInfo& esi) override;
  75
  76   /** finish initialization */
  77   void finishInit() override;
  78   //--------------------------------- end initialization
  79
  80   void preRegisterTerm(TNode n) override;
  81
  82   bool preCheck(Theory::Effort e) override;
  83
  84   bool needsCheckLastEffort() override;
  85
  86   void propagate(Theory::Effort e) override;
  87
  88   TrustNode explain(TNode n) override;
  89
  90   bool collectModelValues(TheoryModel* m,
  91                           const std::set<Node>& termSet) override;
  92
  93   std::string identify() const override { return std::string("BVSolverLazy"); }
  94
  95   Theory::PPAssertStatus ppAssert(
  96       TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
  97
  98   TrustNode ppRewrite(TNode t) override;
  99
 100   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 101
 102   void presolve() override;
 103
 104   bool applyAbstraction(const std::vector<Node>& assertions,
 105                         std::vector<Node>& new_assertions) override;
 106
 107   bool isLeaf(TNode node) { return d_bv.isLeaf(node); }
 108
 109  private:
 110   class Statistics
 111   {
 112    public:
 113     AverageStat d_avgConflictSize;
 114     IntStat d_solveSubstitutions;
 115     TimerStat d_solveTimer;
 116     IntStat d_numCallsToCheckFullEffort;
 117     IntStat d_numCallsToCheckStandardEffort;
 118     TimerStat d_weightComputationTimer;
 119     IntStat d_numMultSlice;
 120     Statistics();
 121     ~Statistics();
 122   };
 123
 124   Statistics d_statistics;
 125
 126   void check(Theory::Effort e);
 127   void spendResource(ResourceManager::Resource r);
 128
 129   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 130   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 131   NodeSet d_staticLearnCache;
 132
 133   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
 134
 135   context::CDO<bool> d_lemmasAdded;
 136
 137   // Are we in conflict?
 138   context::CDO<bool> d_conflict;
 139
 140   // Invalidate the model cache if check was called
 141   context::CDO<bool> d_invalidateModelCache;
 142
 143   /** The conflict node */
 144   Node d_conflictNode;
 145
 146   /** Literals to propagate */
 147   context::CDList<Node> d_literalsToPropagate;
 148
 149   /** Index of the next literal to propagate */
 150   context::CDO<unsigned> d_literalsToPropagateIndex;
 151
 152   /**
 153    * Keeps a map from nodes to the subtheory that propagated it so that we can
 154    * explain it properly.
 155    */
 156   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
 157   PropagatedMap d_propagatedBy;
 158
 159   std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
 160   std::unique_ptr<AbstractionModule> d_abstractionModule;
 161   bool d_calledPreregister;
 162
 163   bool wasPropagatedBySubtheory(TNode literal) const
 164   {
 165     return d_propagatedBy.find(literal) != d_propagatedBy.end();
 166   }
 167
 168   SubTheory getPropagatingSubtheory(TNode literal) const
 169   {
 170     Assert(wasPropagatedBySubtheory(literal));
 171     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 172     return (*find).second;
 173   }
 174
 175   /** Should be called to propagate the literal.  */
 176   bool storePropagation(TNode literal, SubTheory subtheory);
 177
 178   /**
 179    * Explains why this literal (propagated by subtheory) is true by adding
 180    * assumptions.
 181    */
 182   void explain(TNode literal, std::vector<TNode>& assumptions);
 183
 184   void notifySharedTerm(TNode t) override;
 185
 186   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
 187
 188   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 189
 190   Node getModelValue(TNode var);
 191
 192   inline std::string indent()
 193   {
 194     std::string indentStr(d_context->getLevel(), ' ');
 195     return indentStr;
 196   }
 197
 198   void setConflict(Node conflict = Node::null());
 199
 200   bool inConflict() { return d_conflict; }
 201
 202   void sendConflict();
 203
 204   void lemma(TNode node)
 205   {
 206     d_im.lemma(node, InferenceId::UNKNOWN);
 207     d_lemmasAdded = true;
 208   }
 209
 210   void checkForLemma(TNode node);
 211
 212   size_t numAssertions() { return d_bv.numAssertions(); }
 213
 214   theory::Assertion get() { return d_bv.get(); }
 215
 216   bool done() { return d_bv.done(); }
 217
 218   friend class LazyBitblaster;
 219   friend class TLazyBitblaster;
 220   friend class EagerBitblaster;
 221   friend class BitblastSolver;
 222   friend class EqualitySolver;
 223   friend class CoreSolver;
 224   friend class InequalitySolver;
 225   friend class AlgebraicSolver;
 226   friend class EagerBitblastSolver;
 227 }; /* class BVSolverLazy */
 228
 229 }  // namespace bv
 230 }  // namespace theory
 231
 232 }  // namespace CVC4
 233
 234 #endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */