MD downloads: implement (x) inside of search input
[chromium-blink-merge.git] / third_party / stp / stp.gyp
blobe938a02ea2b975c207c2af3d13a2f31bc5e72e43
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.
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   ],