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