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