| # 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}}", |
| ] |
| } |
