src/theory/bv/theory_bv.h

   1 /*********************                                                        */
   2 /*! \file theory_bv.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Dejan Jovanovic, Liana Hadarean
   6  ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds, Martin Brain <>
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Bitvector theory.
  13  **
  14  ** Bitvector theory.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__BV__THEORY_BV_H
  20 #define __CVC4__THEORY__BV__THEORY_BV_H
  21
  22 #include "context/cdhashset.h"
  23 #include "context/cdlist.h"
  24 #include "context/context.h"
  25 #include "theory/bv/bv_subtheory.h"
  26 #include "theory/bv/theory_bv_utils.h"
  27 #include "theory/theory.h"
  28 #include "util/hash.h"
  29 #include "util/statistics_registry.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
  40 class EagerBitblastSolver;
  41
  42 class AbstractionModule;
  43
  44 class TheoryBV : public Theory {
  45
  46   /** The context we are using */
  47   context::Context* d_context;
  48
  49   /** Context dependent set of atoms we already propagated */
  50   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
  51   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
  52
  53   std::vector<SubtheorySolver*> d_subtheories;
  54   __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
  55
  56 public:
  57
  58   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
  59            Valuation valuation, const LogicInfo& logicInfo);
  60
  61   ~TheoryBV();
  62
  63   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  64
  65   Node expandDefinition(LogicRequest &logicRequest, Node node);
  66
  67   void mkAckermanizationAsssertions(std::vector<Node>& assertions);
  68
  69   void preRegisterTerm(TNode n);
  70
  71   void check(Effort e);
  72
  73   void propagate(Effort e);
  74
  75   Node explain(TNode n);
  76
  77   void collectModelInfo( TheoryModel* m, bool fullModel );
  78
  79   std::string identify() const { return std::string("TheoryBV"); }
  80
  81   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
  82
  83   void enableCoreTheorySlicer();
  84
  85   Node ppRewrite(TNode t);
  86
  87   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
  88
  89   void presolve();
  90
  91   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
  92
  93   void setProofLog( BitVectorProof * bvp );
  94
  95 private:
  96
  97   class Statistics {
  98   public:
  99     AverageStat d_avgConflictSize;
 100     IntStat     d_solveSubstitutions;
 101     TimerStat   d_solveTimer;
 102     IntStat     d_numCallsToCheckFullEffort;
 103     IntStat     d_numCallsToCheckStandardEffort;
 104     TimerStat   d_weightComputationTimer;
 105     IntStat     d_numMultSlice;
 106     Statistics();
 107     ~Statistics();
 108   };
 109
 110   Statistics d_statistics;
 111
 112   void spendResource(unsigned ammount) throw(UnsafeInterruptException);
 113
 114   /**
 115    * Return the uninterpreted function symbol corresponding to division-by-zero
 116    * for this particular bit-width
 117    * @param k should be UREM or UDIV
 118    * @param width
 119    *
 120    * @return
 121    */
 122   Node getBVDivByZero(Kind k, unsigned width);
 123
 124   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
 125   void collectNumerators(TNode term, TNodeSet& seen);
 126
 127   typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 128   NodeSet d_staticLearnCache;
 129
 130   /**
 131    * Maps from bit-vector width to division-by-zero uninterpreted
 132    * function symbols.
 133    */
 134   __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
 135   __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
 136
 137   /**
 138    * Maps from bit-vector width to numerators
 139    * of uninterpreted function symbol
 140    */
 141   typedef __gnu_cxx::hash_map<unsigned, TNodeSet > WidthToNumerators;
 142
 143   WidthToNumerators d_BVDivByZeroAckerman;
 144   WidthToNumerators d_BVRemByZeroAckerman;
 145
 146   context::CDO<bool> d_lemmasAdded;
 147
 148   // Are we in conflict?
 149   context::CDO<bool> d_conflict;
 150
 151   // Invalidate the model cache if check was called
 152   context::CDO<bool> d_invalidateModelCache;
 153
 154   /** The conflict node */
 155   Node d_conflictNode;
 156
 157   /** Literals to propagate */
 158   context::CDList<Node> d_literalsToPropagate;
 159
 160   /** Index of the next literal to propagate */
 161   context::CDO<unsigned> d_literalsToPropagateIndex;
 162
 163   /**
 164    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
 165    * properly.
 166    */
 167   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
 168   PropagatedMap d_propagatedBy;
 169
 170   EagerBitblastSolver* d_eagerSolver;
 171   AbstractionModule* d_abstractionModule;
 172   bool d_isCoreTheory;
 173   bool d_calledPreregister;
 174
 175   bool wasPropagatedBySubtheory(TNode literal) const {
 176     return d_propagatedBy.find(literal) != d_propagatedBy.end();
 177   }
 178
 179   SubTheory getPropagatingSubtheory(TNode literal) const {
 180     Assert(wasPropagatedBySubtheory(literal));
 181     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
 182     return (*find).second;
 183   }
 184
 185   /** Should be called to propagate the literal.  */
 186   bool storePropagation(TNode literal, SubTheory subtheory);
 187
 188   /**
 189    * Explains why this literal (propagated by subtheory) is true by adding assumptions.
 190    */
 191   void explain(TNode literal, std::vector<TNode>& assumptions);
 192
 193   void addSharedTerm(TNode t);
 194
 195   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
 196
 197   EqualityStatus getEqualityStatus(TNode a, TNode b);
 198
 199   Node getModelValue(TNode var);
 200
 201   inline std::string indent()
 202   {
 203     std::string indentStr(getSatContext()->getLevel(), ' ');
 204     return indentStr;
 205   }
 206
 207   void setConflict(Node conflict = Node::null());
 208
 209   bool inConflict() {
 210     return d_conflict;
 211   }
 212
 213   void sendConflict();
 214
 215   void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 216
 217   void checkForLemma(TNode node);
 218
 219   friend class LazyBitblaster;
 220   friend class TLazyBitblaster;
 221   friend class EagerBitblaster;
 222   friend class BitblastSolver;
 223   friend class EqualitySolver;
 224   friend class CoreSolver;
 225   friend class InequalitySolver;
 226   friend class AlgebraicSolver;
 227   friend class EagerBitblastSolver;
 228 };/* class TheoryBV */
 229
 230 }/* CVC4::theory::bv namespace */
 231 }/* CVC4::theory namespace */
 232
 233 }/* CVC4 namespace */
 234
 235 #endif /* __CVC4__THEORY__BV__THEORY_BV_H */