1 /******************************************************************************
2 * Top contributors (to current version):
3 * Liana Hadarean, Mathias Preiner, Andres Noetzli
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * AIG Bitblaster based on ABC.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
19 #define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
21 #include "theory/bv/bitblast/bitblaster.h"
24 typedef Abc_Obj_t_ Abc_Obj_t
;
27 typedef Abc_Ntk_t_ Abc_Ntk_t
;
30 typedef Abc_Aig_t_ Abc_Aig_t
;
33 typedef Cnf_Dat_t_ Cnf_Dat_t
;
44 class AigBitblaster
: public TBitblaster
<Abc_Obj_t
*>
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();
59 typedef std::unordered_map
<TNode
, Abc_Obj_t
*> TNodeAigMap
;
60 typedef std::unordered_map
<Node
, Abc_Obj_t
*> NodeAigMap
;
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
;
68 NodeAigMap d_nodeToAigInput
;
69 // the thing we are checking for sat
70 Abc_Obj_t
* d_aigOutputNode
;
72 std::unique_ptr
<MinisatEmptyNotify
> d_notify
;
74 void addAtom(TNode atom
);
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
91 prop::SatSolver
* getSatSolver() override
{ return d_satSolver
.get(); }
97 IntStat d_numVariables
;
98 TimerStat d_simplificationTime
;
99 TimerStat d_cnfConversionTime
;
100 TimerStat d_solveTime
;
104 Statistics d_statistics
;
107 #else /* CVC5_USE_ABC */
110 * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we
111 * can declare `std::unique_ptr<AigBitblaster>` without ABC.
113 class AigBitblaster
: public TBitblaster
<Abc_Obj_t
*>
115 AigBitblaster() = delete;
118 #endif /* CVC5_USE_ABC */
121 } // namespace theory
124 #endif // CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H