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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
|
# Copyright 2014 The Chromium Authors. All rights reserved.
# Use of this source code is governed by a BSD-style license that can be
# found in the LICENSE file.
config("stp_config") {
include_dirs = [
"config",
"src/include",
"src/lib",
"src/lib/Sat",
"src/lib/Sat/cryptominisat2/mtl",
"src/lib/extlib-abc",
"$target_gen_dir/src/include",
]
cflags = [
"-U_DEBUG",
"-Wno-dangling-else",
"-Wno-empty-body",
"-Wno-header-guard",
"-Wno-implicit-function-declaration",
"-Wno-mismatched-tags",
"-Wno-overloaded-virtual",
"-Wno-parentheses-equality",
"-Wno-return-type",
"-Wno-sign-compare",
"-Wno-sometimes-uninitialized",
"-Wno-string-conversion",
"-Wno-tautological-constant-out-of-range-compare",
"-Wno-unused-const-variable",
"-Wno-unused-function",
"-Wno-unused-private-field",
]
cflags_cc = [ "-fexceptions" ]
}
config("stp_public_config") {
include_dirs = [ "src/include" ]
}
component("stp") {
configs += [ ":stp_config" ]
public_configs = [ ":stp_public_config" ]
# Generated with:
# find src/include src/lib -name '*.[ch]' -o -name '*.cc' \
# -o -name '*.cpp' -o -name 'MemoryPool.tcc' \
# | grep -v -e /CryptoMinisat4 -e /TestAST/ -e /Util/ \
# | sort
sources = [
"config/stp/config.h",
"src/include/stp/AbsRefineCounterExample/AbsRefine_CounterExample.h",
"src/include/stp/AST/ArrayTransformer.h",
"src/include/stp/AST/ASTBVConst.h",
"src/include/stp/AST/AST.h",
"src/include/stp/AST/ASTInterior.h",
"src/include/stp/AST/ASTInternal.h",
"src/include/stp/AST/ASTInternalWithChildren.h",
"src/include/stp/AST/ASTNode.h",
"src/include/stp/AST/ASTSymbol.h",
"src/include/stp/AST/NodeFactory/HashingNodeFactory.h",
"src/include/stp/AST/NodeFactory/NodeFactory.h",
"src/include/stp/AST/NodeFactory/SimplifyingNodeFactory.h",
"src/include/stp/AST/NodeFactory/TypeChecker.h",
"src/include/stp/AST/RunTimes.h",
"src/include/stp/AST/STLport_config.h",
"src/include/stp/AST/UsefulDefs.h",
"src/include/stp/c_interface.h",
"src/include/stp/cpp_interface.h",
"src/include/stp/Globals/Globals.h",
"src/include/stp/Interface/fdstream.h",
"src/include/stp/Parser/LetMgr.h",
"src/include/stp/Parser/parser.h",
"src/include/stp/Printer/AssortedPrinters.h",
"src/include/stp/Printer/printers.h",
"src/include/stp/Printer/SMTLIBPrinter.h",
"src/include/stp/Sat/CryptoMinisat.h",
"src/include/stp/Sat/MinisatCore.h",
"src/include/stp/Sat/MinisatCore_prop.h",
"src/include/stp/Sat/SATSolver.h",
"src/include/stp/Sat/SimplifyingMinisat.h",
"src/include/stp/Simplifier/AIGSimplifyPropositionalCore.h",
"src/include/stp/Simplifier/AlwaysTrue.h",
"src/include/stp/Simplifier/bvsolver.h",
"src/include/stp/Simplifier/constantBitP/ConstantBitP_MaxPrecision.h",
"src/include/stp/Simplifier/constantBitP/ConstantBitPropagation.h",
"src/include/stp/Simplifier/constantBitP/ConstantBitP_TransferFunctions.h",
"src/include/stp/Simplifier/constantBitP/ConstantBitP_Utility.h",
"src/include/stp/Simplifier/constantBitP/Dependencies.h",
"src/include/stp/Simplifier/constantBitP/FixedBits.h",
"src/include/stp/Simplifier/constantBitP/MersenneTwister.h",
"src/include/stp/Simplifier/constantBitP/multiplication/ColumnCounts.h",
"src/include/stp/Simplifier/constantBitP/multiplication/ColumnStats.h",
"src/include/stp/Simplifier/constantBitP/MultiplicationStats.h",
"src/include/stp/Simplifier/constantBitP/NodeToFixedBitsMap.h",
"src/include/stp/Simplifier/constantBitP/WorkList.h",
"src/include/stp/Simplifier/EstablishIntervals.h",
"src/include/stp/Simplifier/FindPureLiterals.h",
"src/include/stp/Simplifier/MutableASTNode.h",
"src/include/stp/Simplifier/PropagateEqualities.h",
"src/include/stp/Simplifier/RemoveUnconstrained.h",
"src/include/stp/Simplifier/simplifier.h",
"src/include/stp/Simplifier/SubstitutionMap.h",
"src/include/stp/Simplifier/Symbols.h",
"src/include/stp/Simplifier/UseITEContext.h",
"src/include/stp/Simplifier/VariablesInExpression.h",
"src/include/stp/STPManager/DifficultyScore.h",
"src/include/stp/STPManager/NodeIterator.h",
"src/include/stp/STPManager/STP.h",
"src/include/stp/STPManager/STPManager.h",
"src/include/stp/STPManager/UserDefinedFlags.h",
"src/include/stp/ToSat/AIG/BBNodeAIG.h",
"src/include/stp/ToSat/AIG/BBNodeManagerAIG.h",
"src/include/stp/ToSat/AIG/ToCNFAIG.h",
"src/include/stp/ToSat/AIG/ToSATAIG.h",
"src/include/stp/ToSat/ASTNode/BBNodeManagerASTNode.h",
"src/include/stp/ToSat/ASTNode/ClauseList.h",
"src/include/stp/ToSat/ASTNode/ToCNF.h",
"src/include/stp/ToSat/ASTNode/ToSAT.h",
"src/include/stp/ToSat/BitBlaster.h",
"src/include/stp/ToSat/ToSATBase.h",
"src/lib/AbsRefineCounterExample/AbstractionRefinement.cpp",
"src/lib/AbsRefineCounterExample/CounterExample.cpp",
"src/lib/AST/ArrayTransformer.cpp",
"src/lib/AST/ASTBVConst.cpp",
"src/lib/AST/ASTInterior.cpp",
"src/lib/AST/ASTmisc.cpp",
"src/lib/AST/ASTNode.cpp",
"src/lib/AST/ASTSymbol.cpp",
"src/lib/AST/ASTUtil.cpp",
"src/lib/AST/NodeFactory/HashingNodeFactory.cpp",
"src/lib/AST/NodeFactory/NodeFactory.cpp",
"src/lib/AST/NodeFactory/SimplifyingNodeFactory.cpp",
"src/lib/AST/NodeFactory/TypeChecker.cpp",
"src/lib/AST/RunTimes.cpp",
"src/lib/extlib-abc/aig/aig/aigCheck.c",
"src/lib/extlib-abc/aig/aig/aigDfs.c",
"src/lib/extlib-abc/aig/aig/aigFanout.c",
"src/lib/extlib-abc/aig/aig/aigMan.c",
"src/lib/extlib-abc/aig/aig/aigMem.c",
"src/lib/extlib-abc/aig/aig/aigMffc.c",
"src/lib/extlib-abc/aig/aig/aigObj.c",
"src/lib/extlib-abc/aig/aig/aigOper.c",
"src/lib/extlib-abc/aig/aig/aigOrder.c",
"src/lib/extlib-abc/aig/aig/aigPart.c",
"src/lib/extlib-abc/aig/aig/aigRepr.c",
"src/lib/extlib-abc/aig/aig/aigRet.c",
"src/lib/extlib-abc/aig/aig/aigScl.c",
"src/lib/extlib-abc/aig/aig/aigSeq.c",
"src/lib/extlib-abc/aig/aig/aigShow.c",
"src/lib/extlib-abc/aig/aig/aigTable.c",
"src/lib/extlib-abc/aig/aig/aigTime.c",
"src/lib/extlib-abc/aig/aig/aigTiming.c",
"src/lib/extlib-abc/aig/aig/aigTruth.c",
"src/lib/extlib-abc/aig/aig/aigTsim.c",
"src/lib/extlib-abc/aig/aig/aigUtil.c",
"src/lib/extlib-abc/aig/aig/aigWin.c",
"src/lib/extlib-abc/aig/cnf/cnfCore.c",
"src/lib/extlib-abc/aig/cnf/cnfCut.c",
"src/lib/extlib-abc/aig/cnf/cnfData.c",
"src/lib/extlib-abc/aig/cnf/cnfMan.c",
"src/lib/extlib-abc/aig/cnf/cnfMap.c",
"src/lib/extlib-abc/aig/cnf/cnfPost.c",
"src/lib/extlib-abc/aig/cnf/cnfUtil.c",
"src/lib/extlib-abc/aig/cnf/cnfWrite.c",
"src/lib/extlib-abc/aig/dar/darBalance.c",
"src/lib/extlib-abc/aig/dar/darCore.c",
"src/lib/extlib-abc/aig/dar/darCut.c",
"src/lib/extlib-abc/aig/dar/darData.c",
"src/lib/extlib-abc/aig/dar/darLib.c",
"src/lib/extlib-abc/aig/dar/darMan.c",
"src/lib/extlib-abc/aig/dar/darPrec.c",
"src/lib/extlib-abc/aig/dar/darRefact.c",
"src/lib/extlib-abc/aig/dar/darScript.c",
"src/lib/extlib-abc/aig.h",
"src/lib/extlib-abc/aig/kit/kitAig.c",
"src/lib/extlib-abc/aig/kit/kitGraph.c",
"src/lib/extlib-abc/aig/kit/kitIsop.c",
"src/lib/extlib-abc/aig/kit/kitSop.c",
"src/lib/extlib-abc/aig/kit/kitTruth.c",
"src/lib/extlib-abc/cnf.h",
"src/lib/extlib-abc/cnf_short.h",
"src/lib/extlib-abc/dar.h",
"src/lib/extlib-abc/darInt.h",
"src/lib/extlib-abc/kit.h",
"src/lib/extlib-abc/leaks.h",
"src/lib/extlib-abc/vecFlt.h",
"src/lib/extlib-abc/vec.h",
"src/lib/extlib-abc/vecInt.h",
"src/lib/extlib-abc/vecPtr.h",
"src/lib/extlib-abc/vecStr.h",
"src/lib/extlib-abc/vecVec.h",
"src/lib/extlib-constbv/constantbv.cpp",
"src/lib/extlib-constbv/constantbv.h",
"src/lib/Globals/Globals.cpp",
"src/lib/Interface/c_interface.cpp",
"src/lib/Interface/cpp_interface.cpp",
"src/lib/Parser/LetMgr.cpp",
"src/lib/Printer/AssortedPrinters.cpp",
"src/lib/Printer/BenchPrinter.cpp",
"src/lib/Printer/CPrinter.cpp",
"src/lib/Printer/dotPrinter.cpp",
"src/lib/Printer/GDLPrinter.cpp",
"src/lib/Printer/LispPrinter.cpp",
"src/lib/Printer/PLPrinter.cpp",
"src/lib/Printer/SMTLIB1Printer.cpp",
"src/lib/Printer/SMTLIB2Printer.cpp",
"src/lib/Printer/SMTLIBPrinter.cpp",
"src/lib/Sat/cryptominisat2/BitArray.h",
"src/lib/Sat/cryptominisat2/BoundedQueue.h",
"src/lib/Sat/cryptominisat2/ClauseAllocator.cpp",
"src/lib/Sat/cryptominisat2/ClauseAllocator.h",
"src/lib/Sat/cryptominisat2/ClauseCleaner.cpp",
"src/lib/Sat/cryptominisat2/ClauseCleaner.h",
"src/lib/Sat/cryptominisat2/Clause.h",
"src/lib/Sat/cryptominisat2/constants.h",
"src/lib/Sat/cryptominisat2/CSet.h",
"src/lib/Sat/cryptominisat2/FailedVarSearcher.cpp",
"src/lib/Sat/cryptominisat2/FailedVarSearcher.h",
"src/lib/Sat/cryptominisat2/FindUndef.cpp",
"src/lib/Sat/cryptominisat2/FindUndef.h",
"src/lib/Sat/cryptominisat2/GaussianConfig.h",
"src/lib/Sat/cryptominisat2/Gaussian.cpp",
"src/lib/Sat/cryptominisat2/Gaussian.h",
"src/lib/Sat/cryptominisat2/Logger.cpp",
"src/lib/Sat/cryptominisat2/Logger.h",
"src/lib/Sat/cryptominisat2/MatrixFinder.cpp",
"src/lib/Sat/cryptominisat2/MatrixFinder.h",
"src/lib/Sat/cryptominisat2/MemoryPool/MemoryPool.h",
"src/lib/Sat/cryptominisat2/MemoryPool/MemoryPool.tcc",
"src/lib/Sat/cryptominisat2/MersenneTwister.h",
"src/lib/Sat/cryptominisat2/msvc/stdint.h",
"src/lib/Sat/cryptominisat2/mtl/Alg.h",
"src/lib/Sat/cryptominisat2/mtl/BasicHeap.h",
"src/lib/Sat/cryptominisat2/mtl/BoxedVec.h",
"src/lib/Sat/cryptominisat2/mtl/Heap.h",
"src/lib/Sat/cryptominisat2/mtl/Map.h",
"src/lib/Sat/cryptominisat2/mtl/Queue.h",
"src/lib/Sat/cryptominisat2/mtl/Vec.h",
"src/lib/Sat/cryptominisat2/OnlyNonLearntBins.cpp",
"src/lib/Sat/cryptominisat2/OnlyNonLearntBins.h",
"src/lib/Sat/cryptominisat2/PackedMatrix.h",
"src/lib/Sat/cryptominisat2/PackedRow.cpp",
"src/lib/Sat/cryptominisat2/PackedRow.h",
"src/lib/Sat/cryptominisat2/PartFinder.cpp",
"src/lib/Sat/cryptominisat2/PartFinder.h",
"src/lib/Sat/cryptominisat2/PartHandler.cpp",
"src/lib/Sat/cryptominisat2/PartHandler.h",
"src/lib/Sat/cryptominisat2/RestartTypeChooser.cpp",
"src/lib/Sat/cryptominisat2/RestartTypeChooser.h",
"src/lib/Sat/cryptominisat2/Solver.cpp",
"src/lib/Sat/cryptominisat2/Solver.h",
"src/lib/Sat/cryptominisat2/SolverTypes.h",
"src/lib/Sat/cryptominisat2/StateSaver.cpp",
"src/lib/Sat/cryptominisat2/StateSaver.h",
"src/lib/Sat/cryptominisat2/Subsumer.cpp",
"src/lib/Sat/cryptominisat2/Subsumer.h",
"src/lib/Sat/cryptominisat2/time_mem.cpp",
"src/lib/Sat/cryptominisat2/time_mem.h",
"src/lib/Sat/cryptominisat2/UselessBinRemover.cpp",
"src/lib/Sat/cryptominisat2/UselessBinRemover.h",
"src/lib/Sat/cryptominisat2/VarReplacer.cpp",
"src/lib/Sat/cryptominisat2/VarReplacer.h",
"src/lib/Sat/cryptominisat2/XorFinder.cpp",
"src/lib/Sat/cryptominisat2/XorFinder.h",
"src/lib/Sat/cryptominisat2/XorSubsumer.cpp",
"src/lib/Sat/cryptominisat2/XorSubsumer.h",
"src/lib/Sat/cryptominisat2/XSet.h",
"src/lib/Sat/CryptoMinisat.cpp",
"src/lib/Sat/MinisatCore.cpp",
"src/lib/Sat/minisat/core/Dimacs.h",
"src/lib/Sat/MinisatCore_prop.cpp",
"src/lib/Sat/minisat/core_prop/Solver_prop.cc",
"src/lib/Sat/minisat/core_prop/Solver_prop.h",
"src/lib/Sat/minisat/core/Solver.cc",
"src/lib/Sat/minisat/core/Solver.h",
"src/lib/Sat/minisat/core/SolverTypes.h",
"src/lib/Sat/minisat/mtl/Alg.h",
"src/lib/Sat/minisat/mtl/Alloc.h",
"src/lib/Sat/minisat/mtl/BasicHeap.h",
"src/lib/Sat/minisat/mtl/BoxedVec.h",
"src/lib/Sat/minisat/mtl/Heap.h",
"src/lib/Sat/minisat/mtl/IntTypesMtl.h",
"src/lib/Sat/minisat/mtl/Map.h",
"src/lib/Sat/minisat/mtl/Queue.h",
"src/lib/Sat/minisat/mtl/Sort.h",
"src/lib/Sat/minisat/mtl/Vec.h",
"src/lib/Sat/minisat/mtl/XAlloc.h",
"src/lib/Sat/minisat/simp/SimpSolver.cc",
"src/lib/Sat/minisat/simp/SimpSolver.h",
"src/lib/Sat/minisat/utils/Options.h",
"src/lib/Sat/minisat/utils/ParseUtils.h",
"src/lib/Sat/minisat/utils/System.cc",
"src/lib/Sat/minisat/utils/System.h",
"src/lib/Sat/SimplifyingMinisat.cpp",
"src/lib/Simplifier/bvsolver.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Arithmetic.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Boolean.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Comparison.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Division.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Multiplication.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitPropagation.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Shifting.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp",
"src/lib/Simplifier/constantBitP/ConstantBitP_Utility.cpp",
"src/lib/Simplifier/constantBitP/FixedBits.cpp",
"src/lib/Simplifier/consteval.cpp",
"src/lib/Simplifier/MutableASTNode.cpp",
"src/lib/Simplifier/PropagateEqualities.cpp",
"src/lib/Simplifier/RemoveUnconstrained.cpp",
"src/lib/Simplifier/simplifier.cpp",
"src/lib/Simplifier/SubstitutionMap.cpp",
"src/lib/Simplifier/VariablesInExpression.cpp",
"src/lib/STPManager/STP.cpp",
"src/lib/STPManager/STPManager.cpp",
"src/lib/ToSat/AIG/BBNodeManagerAIG.cpp",
"src/lib/ToSat/AIG/ToCNFAIG.cpp",
"src/lib/ToSat/AIG/ToSATAIG.cpp",
"src/lib/ToSat/ASTNode/ClauseList.cpp",
"src/lib/ToSat/ASTNode/SimpBool.cpp",
"src/lib/ToSat/ASTNode/ToCNF.cpp",
"src/lib/ToSat/ASTNode/ToSAT.cpp",
"src/lib/ToSat/BitBlaster.cpp",
"src/lib/ToSat/ToSATBase.cpp",
"$target_gen_dir/src/include/stp/AST/ASTKind.h",
"$target_gen_dir/src/lib/AST/ASTKind.cpp",
"$target_gen_dir/src/lib/Parser/lexcvc.cpp",
"$target_gen_dir/src/lib/Parser/lexsmt.cpp",
"$target_gen_dir/src/lib/Parser/lexsmt2.cpp",
"$target_gen_dir/src/lib/Parser/parsecvc.cpp",
"$target_gen_dir/src/lib/Parser/parsecvc.hpp",
"$target_gen_dir/src/lib/Parser/parsesmt.cpp",
"$target_gen_dir/src/lib/Parser/parsesmt.hpp",
"$target_gen_dir/src/lib/Parser/parsesmt2.cpp",
"$target_gen_dir/src/lib/Parser/parsesmt2.hpp",
]
deps = [
":generate_astkinds",
":generate_lexer",
":generate_parser",
]
}
action("generate_astkinds") {
script = "genastkinds.py"
sources = [
"src/lib/AST/ASTKind.kinds",
]
inputs = [
"src/lib/AST/genkinds.pl",
]
outputs = [
"$target_gen_dir/src/include/stp/AST/ASTKind.h",
"$target_gen_dir/src/lib/AST/ASTKind.cpp",
]
args = [
rebase_path("src/lib/AST/genkinds.pl", root_build_dir),
rebase_path("src/lib/AST/ASTKind.kinds", root_build_dir),
rebase_path(target_gen_dir, root_build_dir),
]
}
action_foreach("generate_lexer") {
script = "flex.py"
sources = [
"src/lib/Parser/cvc.lex",
"src/lib/Parser/smt.lex",
"src/lib/Parser/smt2.lex",
]
outputs = [
"{{source_gen_dir}}/lex{{source_name_part}}.cpp",
]
args = [
"{{source}}",
"{{source_name_part}}",
"{{source_gen_dir}}/lex{{source_name_part}}",
]
}
action_foreach("generate_parser") {
script = "bison.py"
sources = [
"src/lib/Parser/cvc.y",
"src/lib/Parser/smt.y",
"src/lib/Parser/smt2.y",
]
outputs = [
"{{source_gen_dir}}/parse{{source_name_part}}.cpp",
"{{source_gen_dir}}/parse{{source_name_part}}.hpp",
]
args = [
"{{source}}",
"{{source_name_part}}",
"{{source_gen_dir}}/parse{{source_name_part}}",
]
}
|
