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