| blob | e938a02ea2b975c207c2af3d13a2f31bc5e72e43 |
1 # Copyright 2014 The Chromium Authors. All rights reserved.
2 # Use of this source code is governed by a BSD-style license that can be
3 # found in the LICENSE file.
5 {
6 'variables': {
7 'shared_generated_dir': '<(SHARED_INTERMEDIATE_DIR)/third_party/stp',
8 },
9 'targets': [
10 {
11 'target_name': 'stp',
12 'type': '<(component)',
13 'cflags': [
14 '-U_DEBUG',
15 '-Wno-dangling-else',
16 '-Wno-empty-body',
17 '-Wno-header-guard',
18 '-Wno-implicit-function-declaration',
19 '-Wno-mismatched-tags',
20 '-Wno-overloaded-virtual',
21 '-Wno-parentheses-equality',
22 '-Wno-return-type',
23 '-Wno-sign-compare',
24 '-Wno-sometimes-uninitialized',
25 '-Wno-string-conversion',
26 '-Wno-tautological-constant-out-of-range-compare',
27 '-Wno-unused-const-variable',
28 '-Wno-unused-function',
29 '-Wno-unused-private-field',
30 ],
31 'cflags_cc': [
32 '-fexceptions',
33 ],
34 'direct_dependent_settings': {
35 'include_dirs': [
36 'src/include',
37 ],
38 },
39 'include_dirs': [
40 'config',
41 'src/include',
42 'src/lib',
43 'src/lib/Sat',
44 'src/lib/Sat/cryptominisat2/mtl',
45 'src/lib/extlib-abc',
46 '<(shared_generated_dir)/src/include',
47 ],
48 'sources': [
49 'config/stp/config.h',
50 'src/include/stp/AbsRefineCounterExample/AbsRefine_CounterExample.h',
51 'src/include/stp/AST/ArrayTransformer.h',
52 'src/include/stp/AST/ASTBVConst.h',
53 'src/include/stp/AST/AST.h',
54 'src/include/stp/AST/ASTInterior.h',
55 'src/include/stp/AST/ASTInternal.h',
56 'src/include/stp/AST/ASTInternalWithChildren.h',
57 'src/include/stp/AST/ASTNode.h',
58 'src/include/stp/AST/ASTSymbol.h',
59 'src/include/stp/AST/NodeFactory/HashingNodeFactory.h',
60 'src/include/stp/AST/NodeFactory/NodeFactory.h',
61 'src/include/stp/AST/NodeFactory/SimplifyingNodeFactory.h',
62 'src/include/stp/AST/NodeFactory/TypeChecker.h',
63 'src/include/stp/AST/RunTimes.h',
64 'src/include/stp/AST/STLport_config.h',
65 'src/include/stp/AST/UsefulDefs.h',
66 'src/include/stp/c_interface.h',
67 'src/include/stp/cpp_interface.h',
68 'src/include/stp/Globals/Globals.h',
69 'src/include/stp/Interface/fdstream.h',
70 'src/include/stp/Parser/LetMgr.h',
71 'src/include/stp/Parser/parser.h',
72 'src/include/stp/Printer/AssortedPrinters.h',
73 'src/include/stp/Printer/printers.h',
74 'src/include/stp/Printer/SMTLIBPrinter.h',
75 'src/include/stp/Sat/CryptoMinisat.h',
76 'src/include/stp/Sat/MinisatCore.h',
77 'src/include/stp/Sat/MinisatCore_prop.h',
78 'src/include/stp/Sat/SATSolver.h',
79 'src/include/stp/Sat/SimplifyingMinisat.h',
80 'src/include/stp/Simplifier/AIGSimplifyPropositionalCore.h',
81 'src/include/stp/Simplifier/AlwaysTrue.h',
82 'src/include/stp/Simplifier/bvsolver.h',
83 'src/include/stp/Simplifier/constantBitP/ConstantBitP_MaxPrecision.h',
84 'src/include/stp/Simplifier/constantBitP/ConstantBitPropagation.h',
85 'src/include/stp/Simplifier/constantBitP/ConstantBitP_TransferFunctions.h',
86 'src/include/stp/Simplifier/constantBitP/ConstantBitP_Utility.h',
87 'src/include/stp/Simplifier/constantBitP/Dependencies.h',
88 'src/include/stp/Simplifier/constantBitP/FixedBits.h',
89 'src/include/stp/Simplifier/constantBitP/MersenneTwister.h',
90 'src/include/stp/Simplifier/constantBitP/multiplication/ColumnCounts.h',
91 'src/include/stp/Simplifier/constantBitP/multiplication/ColumnStats.h',
92 'src/include/stp/Simplifier/constantBitP/MultiplicationStats.h',
93 'src/include/stp/Simplifier/constantBitP/NodeToFixedBitsMap.h',
94 'src/include/stp/Simplifier/constantBitP/WorkList.h',
95 'src/include/stp/Simplifier/EstablishIntervals.h',
96 'src/include/stp/Simplifier/FindPureLiterals.h',
97 'src/include/stp/Simplifier/MutableASTNode.h',
98 'src/include/stp/Simplifier/PropagateEqualities.h',
99 'src/include/stp/Simplifier/RemoveUnconstrained.h',
100 'src/include/stp/Simplifier/simplifier.h',
101 'src/include/stp/Simplifier/SubstitutionMap.h',
102 'src/include/stp/Simplifier/Symbols.h',
103 'src/include/stp/Simplifier/UseITEContext.h',
104 'src/include/stp/Simplifier/VariablesInExpression.h',
105 'src/include/stp/STPManager/DifficultyScore.h',
106 'src/include/stp/STPManager/NodeIterator.h',
107 'src/include/stp/STPManager/STP.h',
108 'src/include/stp/STPManager/STPManager.h',
109 'src/include/stp/STPManager/UserDefinedFlags.h',
110 'src/include/stp/ToSat/AIG/BBNodeAIG.h',
111 'src/include/stp/ToSat/AIG/BBNodeManagerAIG.h',
112 'src/include/stp/ToSat/AIG/ToCNFAIG.h',
113 'src/include/stp/ToSat/AIG/ToSATAIG.h',
114 'src/include/stp/ToSat/ASTNode/BBNodeManagerASTNode.h',
115 'src/include/stp/ToSat/ASTNode/ClauseList.h',
116 'src/include/stp/ToSat/ASTNode/ToCNF.h',
117 'src/include/stp/ToSat/ASTNode/ToSAT.h',
118 'src/include/stp/ToSat/BitBlaster.h',
119 'src/include/stp/ToSat/ToSATBase.h',
120 'src/lib/AbsRefineCounterExample/AbstractionRefinement.cpp',
121 'src/lib/AbsRefineCounterExample/CounterExample.cpp',
122 'src/lib/AST/ArrayTransformer.cpp',
123 'src/lib/AST/ASTBVConst.cpp',
124 'src/lib/AST/ASTInterior.cpp',
125 'src/lib/AST/ASTmisc.cpp',
126 'src/lib/AST/ASTNode.cpp',
127 'src/lib/AST/ASTSymbol.cpp',
128 'src/lib/AST/ASTUtil.cpp',
129 'src/lib/AST/NodeFactory/HashingNodeFactory.cpp',
130 'src/lib/AST/NodeFactory/NodeFactory.cpp',
131 'src/lib/AST/NodeFactory/SimplifyingNodeFactory.cpp',
132 'src/lib/AST/NodeFactory/TypeChecker.cpp',
133 'src/lib/AST/RunTimes.cpp',
134 'src/lib/extlib-abc/aig/aig/aigCheck.c',
135 'src/lib/extlib-abc/aig/aig/aigDfs.c',
136 'src/lib/extlib-abc/aig/aig/aigFanout.c',
137 'src/lib/extlib-abc/aig/aig/aigMan.c',
138 'src/lib/extlib-abc/aig/aig/aigMem.c',
139 'src/lib/extlib-abc/aig/aig/aigMffc.c',
140 'src/lib/extlib-abc/aig/aig/aigObj.c',
141 'src/lib/extlib-abc/aig/aig/aigOper.c',
142 'src/lib/extlib-abc/aig/aig/aigOrder.c',
143 'src/lib/extlib-abc/aig/aig/aigPart.c',
144 'src/lib/extlib-abc/aig/aig/aigRepr.c',
145 'src/lib/extlib-abc/aig/aig/aigRet.c',
146 'src/lib/extlib-abc/aig/aig/aigScl.c',
147 'src/lib/extlib-abc/aig/aig/aigSeq.c',
148 'src/lib/extlib-abc/aig/aig/aigShow.c',
149 'src/lib/extlib-abc/aig/aig/aigTable.c',
150 'src/lib/extlib-abc/aig/aig/aigTime.c',
151 'src/lib/extlib-abc/aig/aig/aigTiming.c',
152 'src/lib/extlib-abc/aig/aig/aigTruth.c',
153 'src/lib/extlib-abc/aig/aig/aigTsim.c',
154 'src/lib/extlib-abc/aig/aig/aigUtil.c',
155 'src/lib/extlib-abc/aig/aig/aigWin.c',
156 'src/lib/extlib-abc/aig/cnf/cnfCore.c',
157 'src/lib/extlib-abc/aig/cnf/cnfCut.c',
158 'src/lib/extlib-abc/aig/cnf/cnfData.c',
159 'src/lib/extlib-abc/aig/cnf/cnfMan.c',
160 'src/lib/extlib-abc/aig/cnf/cnfMap.c',
161 'src/lib/extlib-abc/aig/cnf/cnfPost.c',
162 'src/lib/extlib-abc/aig/cnf/cnfUtil.c',
163 'src/lib/extlib-abc/aig/cnf/cnfWrite.c',
164 'src/lib/extlib-abc/aig/dar/darBalance.c',
165 'src/lib/extlib-abc/aig/dar/darCore.c',
166 'src/lib/extlib-abc/aig/dar/darCut.c',
167 'src/lib/extlib-abc/aig/dar/darData.c',
168 'src/lib/extlib-abc/aig/dar/darLib.c',
169 'src/lib/extlib-abc/aig/dar/darMan.c',
170 'src/lib/extlib-abc/aig/dar/darPrec.c',
171 'src/lib/extlib-abc/aig/dar/darRefact.c',
172 'src/lib/extlib-abc/aig/dar/darScript.c',
173 'src/lib/extlib-abc/aig.h',
174 'src/lib/extlib-abc/aig/kit/kitAig.c',
175 'src/lib/extlib-abc/aig/kit/kitGraph.c',
176 'src/lib/extlib-abc/aig/kit/kitIsop.c',
177 'src/lib/extlib-abc/aig/kit/kitSop.c',
178 'src/lib/extlib-abc/aig/kit/kitTruth.c',
179 'src/lib/extlib-abc/cnf.h',
180 'src/lib/extlib-abc/cnf_short.h',
181 'src/lib/extlib-abc/dar.h',
182 'src/lib/extlib-abc/darInt.h',
183 'src/lib/extlib-abc/kit.h',
184 'src/lib/extlib-abc/leaks.h',
185 'src/lib/extlib-abc/vecFlt.h',
186 'src/lib/extlib-abc/vec.h',
187 'src/lib/extlib-abc/vecInt.h',
188 'src/lib/extlib-abc/vecPtr.h',
189 'src/lib/extlib-abc/vecStr.h',
190 'src/lib/extlib-abc/vecVec.h',
191 'src/lib/extlib-constbv/constantbv.cpp',
192 'src/lib/extlib-constbv/constantbv.h',
193 'src/lib/Globals/Globals.cpp',
194 'src/lib/Interface/c_interface.cpp',
195 'src/lib/Interface/cpp_interface.cpp',
196 'src/lib/Parser/LetMgr.cpp',
197 'src/lib/Printer/AssortedPrinters.cpp',
198 'src/lib/Printer/BenchPrinter.cpp',
199 'src/lib/Printer/CPrinter.cpp',
200 'src/lib/Printer/dotPrinter.cpp',
201 'src/lib/Printer/GDLPrinter.cpp',
202 'src/lib/Printer/LispPrinter.cpp',
203 'src/lib/Printer/PLPrinter.cpp',
204 'src/lib/Printer/SMTLIB1Printer.cpp',
205 'src/lib/Printer/SMTLIB2Printer.cpp',
206 'src/lib/Printer/SMTLIBPrinter.cpp',
207 'src/lib/Sat/cryptominisat2/BitArray.h',
208 'src/lib/Sat/cryptominisat2/BoundedQueue.h',
209 'src/lib/Sat/cryptominisat2/ClauseAllocator.cpp',
210 'src/lib/Sat/cryptominisat2/ClauseAllocator.h',
211 'src/lib/Sat/cryptominisat2/ClauseCleaner.cpp',
212 'src/lib/Sat/cryptominisat2/ClauseCleaner.h',
213 'src/lib/Sat/cryptominisat2/Clause.h',
214 'src/lib/Sat/cryptominisat2/constants.h',
215 'src/lib/Sat/cryptominisat2/CSet.h',
216 'src/lib/Sat/cryptominisat2/FailedVarSearcher.cpp',
217 'src/lib/Sat/cryptominisat2/FailedVarSearcher.h',
218 'src/lib/Sat/cryptominisat2/FindUndef.cpp',
219 'src/lib/Sat/cryptominisat2/FindUndef.h',
220 'src/lib/Sat/cryptominisat2/GaussianConfig.h',
221 'src/lib/Sat/cryptominisat2/Gaussian.cpp',
222 'src/lib/Sat/cryptominisat2/Gaussian.h',
223 'src/lib/Sat/cryptominisat2/Logger.cpp',
224 'src/lib/Sat/cryptominisat2/Logger.h',
225 'src/lib/Sat/cryptominisat2/MatrixFinder.cpp',
226 'src/lib/Sat/cryptominisat2/MatrixFinder.h',
227 'src/lib/Sat/cryptominisat2/MemoryPool/MemoryPool.h',
228 'src/lib/Sat/cryptominisat2/MemoryPool/MemoryPool.tcc',
229 'src/lib/Sat/cryptominisat2/MersenneTwister.h',
230 'src/lib/Sat/cryptominisat2/msvc/stdint.h',
231 'src/lib/Sat/cryptominisat2/mtl/Alg.h',
232 'src/lib/Sat/cryptominisat2/mtl/BasicHeap.h',
233 'src/lib/Sat/cryptominisat2/mtl/BoxedVec.h',
234 'src/lib/Sat/cryptominisat2/mtl/Heap.h',
235 'src/lib/Sat/cryptominisat2/mtl/Map.h',
236 'src/lib/Sat/cryptominisat2/mtl/Queue.h',
237 'src/lib/Sat/cryptominisat2/mtl/Vec.h',
238 'src/lib/Sat/cryptominisat2/OnlyNonLearntBins.cpp',
239 'src/lib/Sat/cryptominisat2/OnlyNonLearntBins.h',
240 'src/lib/Sat/cryptominisat2/PackedMatrix.h',
241 'src/lib/Sat/cryptominisat2/PackedRow.cpp',
242 'src/lib/Sat/cryptominisat2/PackedRow.h',
243 'src/lib/Sat/cryptominisat2/PartFinder.cpp',
244 'src/lib/Sat/cryptominisat2/PartFinder.h',
245 'src/lib/Sat/cryptominisat2/PartHandler.cpp',
246 'src/lib/Sat/cryptominisat2/PartHandler.h',
247 'src/lib/Sat/cryptominisat2/RestartTypeChooser.cpp',
248 'src/lib/Sat/cryptominisat2/RestartTypeChooser.h',
249 'src/lib/Sat/cryptominisat2/Solver.cpp',
250 'src/lib/Sat/cryptominisat2/Solver.h',
251 'src/lib/Sat/cryptominisat2/SolverTypes.h',
252 'src/lib/Sat/cryptominisat2/StateSaver.cpp',
253 'src/lib/Sat/cryptominisat2/StateSaver.h',
254 'src/lib/Sat/cryptominisat2/Subsumer.cpp',
255 'src/lib/Sat/cryptominisat2/Subsumer.h',
256 'src/lib/Sat/cryptominisat2/time_mem.cpp',
257 'src/lib/Sat/cryptominisat2/time_mem.h',
258 'src/lib/Sat/cryptominisat2/UselessBinRemover.cpp',
259 'src/lib/Sat/cryptominisat2/UselessBinRemover.h',
260 'src/lib/Sat/cryptominisat2/VarReplacer.cpp',
261 'src/lib/Sat/cryptominisat2/VarReplacer.h',
262 'src/lib/Sat/cryptominisat2/XorFinder.cpp',
263 'src/lib/Sat/cryptominisat2/XorFinder.h',
264 'src/lib/Sat/cryptominisat2/XorSubsumer.cpp',
265 'src/lib/Sat/cryptominisat2/XorSubsumer.h',
266 'src/lib/Sat/cryptominisat2/XSet.h',
267 'src/lib/Sat/CryptoMinisat.cpp',
268 'src/lib/Sat/MinisatCore.cpp',
269 'src/lib/Sat/minisat/core/Dimacs.h',
270 'src/lib/Sat/MinisatCore_prop.cpp',
271 'src/lib/Sat/minisat/core_prop/Solver_prop.cc',
272 'src/lib/Sat/minisat/core_prop/Solver_prop.h',
273 'src/lib/Sat/minisat/core/Solver.cc',
274 'src/lib/Sat/minisat/core/Solver.h',
275 'src/lib/Sat/minisat/core/SolverTypes.h',
276 'src/lib/Sat/minisat/mtl/Alg.h',
277 'src/lib/Sat/minisat/mtl/Alloc.h',
278 'src/lib/Sat/minisat/mtl/BasicHeap.h',
279 'src/lib/Sat/minisat/mtl/BoxedVec.h',
280 'src/lib/Sat/minisat/mtl/Heap.h',
281 'src/lib/Sat/minisat/mtl/IntTypesMtl.h',
282 'src/lib/Sat/minisat/mtl/Map.h',
283 'src/lib/Sat/minisat/mtl/Queue.h',
284 'src/lib/Sat/minisat/mtl/Sort.h',
285 'src/lib/Sat/minisat/mtl/Vec.h',
286 'src/lib/Sat/minisat/mtl/XAlloc.h',
287 'src/lib/Sat/minisat/simp/SimpSolver.cc',
288 'src/lib/Sat/minisat/simp/SimpSolver.h',
289 'src/lib/Sat/minisat/utils/Options.h',
290 'src/lib/Sat/minisat/utils/ParseUtils.h',
291 'src/lib/Sat/minisat/utils/System.cc',
292 'src/lib/Sat/minisat/utils/System.h',
293 'src/lib/Sat/SimplifyingMinisat.cpp',
294 'src/lib/Simplifier/bvsolver.cpp',
295 'src/lib/Simplifier/constantBitP/ConstantBitP_Arithmetic.cpp',
296 'src/lib/Simplifier/constantBitP/ConstantBitP_Boolean.cpp',
297 'src/lib/Simplifier/constantBitP/ConstantBitP_Comparison.cpp',
298 'src/lib/Simplifier/constantBitP/ConstantBitP_Division.cpp',
299 'src/lib/Simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp',
300 'src/lib/Simplifier/constantBitP/ConstantBitP_Multiplication.cpp',
301 'src/lib/Simplifier/constantBitP/ConstantBitPropagation.cpp',
302 'src/lib/Simplifier/constantBitP/ConstantBitP_Shifting.cpp',
303 'src/lib/Simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp',
304 'src/lib/Simplifier/constantBitP/ConstantBitP_Utility.cpp',
305 'src/lib/Simplifier/constantBitP/FixedBits.cpp',
306 'src/lib/Simplifier/consteval.cpp',
307 'src/lib/Simplifier/MutableASTNode.cpp',
308 'src/lib/Simplifier/PropagateEqualities.cpp',
309 'src/lib/Simplifier/RemoveUnconstrained.cpp',
310 'src/lib/Simplifier/simplifier.cpp',
311 'src/lib/Simplifier/SubstitutionMap.cpp',
312 'src/lib/Simplifier/VariablesInExpression.cpp',
313 'src/lib/STPManager/STP.cpp',
314 'src/lib/STPManager/STPManager.cpp',
315 'src/lib/ToSat/AIG/BBNodeManagerAIG.cpp',
316 'src/lib/ToSat/AIG/ToCNFAIG.cpp',
317 'src/lib/ToSat/AIG/ToSATAIG.cpp',
318 'src/lib/ToSat/ASTNode/ClauseList.cpp',
319 'src/lib/ToSat/ASTNode/SimpBool.cpp',
320 'src/lib/ToSat/ASTNode/ToCNF.cpp',
321 'src/lib/ToSat/ASTNode/ToSAT.cpp',
322 'src/lib/ToSat/BitBlaster.cpp',
323 'src/lib/ToSat/ToSATBase.cpp',
324 '<(shared_generated_dir)/src/include/stp/AST/ASTKind.h',
325 '<(shared_generated_dir)/src/lib/AST/ASTKind.cpp',
326 '<(shared_generated_dir)/src/lib/Parser/lexcvc.cpp',
327 '<(shared_generated_dir)/src/lib/Parser/lexsmt.cpp',
328 '<(shared_generated_dir)/src/lib/Parser/lexsmt2.cpp',
329 '<(shared_generated_dir)/src/lib/Parser/parsecvc.cpp',
330 '<(shared_generated_dir)/src/lib/Parser/parsecvc.hpp',
331 '<(shared_generated_dir)/src/lib/Parser/parsesmt.cpp',
332 '<(shared_generated_dir)/src/lib/Parser/parsesmt.hpp',
333 '<(shared_generated_dir)/src/lib/Parser/parsesmt2.cpp',
334 '<(shared_generated_dir)/src/lib/Parser/parsesmt2.hpp',
335 ],
336 'dependencies': [
337 'stp_generated_sources',
338 ],
339 },
340 {
341 'target_name': 'stp_generated_sources',
342 'type': 'none',
343 'sources': [
344 'src/lib/AST/ASTKind.kinds',
345 'src/lib/Parser/cvc.lex',
346 'src/lib/Parser/cvc.y',
347 'src/lib/Parser/smt.lex',
348 'src/lib/Parser/smt.y',
349 'src/lib/Parser/smt2.lex',
350 'src/lib/Parser/smt2.y',
351 ],
352 'actions': [
353 {
354 'action_name': 'generate_astkind',
355 'inputs': [
356 'genastkinds.py',
357 'src/lib/AST/ASTKind.kinds',
358 'src/lib/AST/genkinds.pl',
359 ],
360 'outputs': [
361 '<(shared_generated_dir)/src/include/stp/AST/ASTKind.h',
362 '<(shared_generated_dir)/src/lib/AST/ASTKind.cpp',
363 ],
364 'action': [
365 'python',
366 'genastkinds.py',
367 'src/lib/AST/genkinds.pl',
368 'src/lib/AST/ASTKind.kinds',
369 '<(shared_generated_dir)',
370 ],
371 'message': 'Generating ASTKind ...',
372 },
373 ],
374 'rules': [
375 {
376 'rule_name': 'generate_flex',
377 'extension': '.lex',
378 'inputs': [
379 'flex.py',
380 ],
381 'outputs': [
382 '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/lex<(RULE_INPUT_ROOT).cpp',
383 ],
384 'action': [
385 'python',
386 'flex.py',
387 '<(RULE_INPUT_PATH)',
388 '<(RULE_INPUT_ROOT)',
389 '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/lex<(RULE_INPUT_ROOT)',
390 ],
391 'message': 'Generating <(RULE_INPUT_ROOT) lexer ...',
392 },
393 {
394 'rule_name': 'generate_bison',
395 'extension': '.y',
396 'inputs': [
397 'bison.py',
398 ],
399 'outputs': [
400 '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT).cpp',
401 '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT).hpp',
402 ],
403 'action': [
404 'python',
405 'bison.py',
406 '<(RULE_INPUT_PATH)',
407 '<(RULE_INPUT_ROOT)',
408 '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT)',
409 ],
410 'message': 'Generating <(RULE_INPUT_ROOT) parser ...',
411 },
412 ],
413 },
414 ],
415 }