src/theory/bv/bv_subtheory_bitblast.h

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_bitblast.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Liana Hadarean
   6  ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Clark Barrett
   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 Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #pragma once
  20
  21 #include "theory/bv/bv_subtheory.h"
  22 #include "theory/bv/bitblaster_template.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace bv {
  27
  28 class LazyBitblaster;
  29 class AbstractionModule;
  30 class BVQuickCheck;
  31 class QuickXPlain;
  32
  33 /**
  34  * BitblastSolver
  35  */
  36 class BitblastSolver : public SubtheorySolver {
  37   struct Statistics {
  38     IntStat d_numCallstoCheck;
  39     IntStat d_numBBLemmas;
  40     Statistics();
  41     ~Statistics();
  42   };
  43   /** Bitblaster */
  44   TLazyBitblaster* d_bitblaster;
  45
  46   /** Nodes that still need to be bit-blasted */
  47   context::CDQueue<TNode> d_bitblastQueue;
  48   Statistics d_statistics;
  49
  50   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
  51   NodeMap d_modelCache;
  52   context::CDO<bool> d_validModelCache;
  53
  54   /** Queue for bit-blasting lemma atoms only in full check if we are sat */
  55   context::CDQueue<TNode> d_lemmaAtomsQueue;
  56   bool  d_useSatPropagation;
  57   AbstractionModule* d_abstractionModule;
  58   BVQuickCheck* d_quickCheck;
  59   QuickXPlain* d_quickXplain;
  60   //  Node getModelValueRec(TNode node);
  61   void setConflict(TNode conflict);
  62 public:
  63   BitblastSolver(context::Context* c, TheoryBV* bv);
  64   ~BitblastSolver();
  65
  66   void  preRegister(TNode node);
  67   bool  check(Theory::Effort e);
  68   void  explain(TNode literal, std::vector<TNode>& assumptions);
  69   EqualityStatus getEqualityStatus(TNode a, TNode b);
  70   void collectModelInfo(TheoryModel* m, bool fullModel);
  71   Node getModelValue(TNode node);
  72   bool isComplete() { return true; }
  73   void bitblastQueue();
  74   void setAbstraction(AbstractionModule* module);
  75   uint64_t computeAtomWeight(TNode atom);
  76 };
  77
  78 }
  79 }
  80 }