third_party/stp/BUILD.gn

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