src/theory/bv/bitblast/aig_bitblaster.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Liana Hadarean, Mathias Preiner, Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * AIG Bitblaster based on ABC.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
  19 #define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
  20
  21 #include "theory/bv/bitblast/bitblaster.h"
  22
  23 class Abc_Obj_t_;
  24 typedef Abc_Obj_t_ Abc_Obj_t;
  25
  26 class Abc_Ntk_t_;
  27 typedef Abc_Ntk_t_ Abc_Ntk_t;
  28
  29 class Abc_Aig_t_;
  30 typedef Abc_Aig_t_ Abc_Aig_t;
  31
  32 class Cnf_Dat_t_;
  33 typedef Cnf_Dat_t_ Cnf_Dat_t;
  34
  35 namespace cvc5 {
  36 namespace prop {
  37 class SatSolver;
  38 }
  39 namespace theory {
  40 namespace bv {
  41
  42 #ifdef CVC5_USE_ABC
  43
  44 class AigBitblaster : public TBitblaster<Abc_Obj_t*>
  45 {
  46  public:
  47   AigBitblaster();
  48   ~AigBitblaster();
  49
  50   void makeVariable(TNode node, Bits& bits) override;
  51   void bbTerm(TNode node, Bits& bits) override;
  52   void bbAtom(TNode node) override;
  53   Abc_Obj_t* bbFormula(TNode formula);
  54   bool solve(TNode query);
  55   static Abc_Aig_t* currentAigM();
  56   static Abc_Ntk_t* currentAigNtk();
  57
  58  private:
  59   typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap;
  60   typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap;
  61
  62   static thread_local Abc_Ntk_t* s_abcAigNetwork;
  63   std::unique_ptr<context::Context> d_nullContext;
  64   std::unique_ptr<prop::SatSolver> d_satSolver;
  65   TNodeAigMap d_aigCache;
  66   NodeAigMap d_bbAtoms;
  67
  68   NodeAigMap d_nodeToAigInput;
  69   // the thing we are checking for sat
  70   Abc_Obj_t* d_aigOutputNode;
  71
  72   std::unique_ptr<MinisatEmptyNotify> d_notify;
  73
  74   void addAtom(TNode atom);
  75   void simplifyAig();
  76   void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
  77   Abc_Obj_t* getBBAtom(TNode atom) const override;
  78   bool hasBBAtom(TNode atom) const override;
  79   void cacheAig(TNode node, Abc_Obj_t* aig);
  80   bool hasAig(TNode node);
  81   Abc_Obj_t* getAig(TNode node);
  82   Abc_Obj_t* mkInput(TNode input);
  83   bool hasInput(TNode input);
  84   void convertToCnfAndAssert();
  85   void assertToSatSolver(Cnf_Dat_t* pCnf);
  86   Node getModelFromSatSolver(TNode a, bool fullModel) override
  87   {
  88     Unreachable();
  89   }
  90
  91   prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
  92
  93   class Statistics
  94   {
  95    public:
  96     IntStat d_numClauses;
  97     IntStat d_numVariables;
  98     TimerStat d_simplificationTime;
  99     TimerStat d_cnfConversionTime;
 100     TimerStat d_solveTime;
 101     Statistics();
 102   };
 103
 104   Statistics d_statistics;
 105 };
 106
 107 #else /* CVC5_USE_ABC */
 108
 109 /**
 110  * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we
 111  * can declare `std::unique_ptr<AigBitblaster>` without ABC.
 112  */
 113 class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 114 {
 115   AigBitblaster() = delete;
 116 };
 117
 118 #endif /* CVC5_USE_ABC */
 119
 120 }  // namespace bv
 121 }  // namespace theory
 122 }  // namespace cvc5
 123
 124 #endif  //  CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H