Remove STP from third_party

Unresolved upstream issues have blocked my plans to use STP in
sandbox_linux_unittests for long enough that I've decided to abandon
them (at least for the foreseeable future), so no point in keeping
this unused code around at the moment.

BUG=414363
TBR=jln@chromium.org

Review URL: https://codereview.chromium.org/1308063009

Cr-Commit-Position: refs/heads/master@{#348314}

10 files changed, 0 insertions, 1268 deletions

diff --git a/third_party/stp/BUILD.gn b/third_party/stp/BUILD.gn
deleted file mode 100644
index 5463eec..0000000
--- a/third_party/stp/BUILD.gn
+++ /dev/null
@@ -1,397 +0,0 @@
-# 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}}",
-  ]
-}
diff --git a/third_party/stp/LICENSE b/third_party/stp/LICENSE
deleted file mode 100644
index d3d803c..0000000
--- a/third_party/stp/LICENSE
+++ /dev/null
@@ -1,331 +0,0 @@
-/********************************************************************
- * PROGRAM NAME: STP (Simple Theorem Prover)	
- *		
- * AUTHORS: Vijay Ganesh
- *	
- * BEGIN DATE: November, 2005
- ********************************************************************/
-
-The MIT License
-
-Copyright (c) 2008 Vijay Ganesh
-
-Permission is hereby granted, free of charge, to any person obtaining
-a copy of this software and associated documentation files (the
-"Software"), to deal in the Software without restriction, including
-without limitation the rights to use, copy, modify, merge, publish,
-distribute, sublicense, and/or sell copies of the Software, and to
-permit persons to whom the Software is furnished to do so, subject to
-the following conditions:
-
-The above copyright notice and this permission notice shall be
-included in all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
-LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
-OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
-WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-
-
-STP links to copyrighted librarys:
-	* Minisat Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson.
-	* Bit::Vector Copyright (c) 1995 - 2004 by Steffen Beyer. 
-	* CVC's SMT-LIB Parser  Copyright (C) 2004 by the Board of Trustees
-          of Leland Stanford Junior University and by New York University.
-	* CryptoMinisat Copyright (c) 2009 Mate Soos
-	* ABC by Alan Mishchenko
-	* Boost by various: http://www.boost.org/
-        * CryptoMiniSat4 in case it's installed
-
-MINISAT
-	MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-
-	Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-	associated documentation files (the "Software"), to deal in the Software without restriction,
-	including without limitation the rights to use, copy, modify, merge, publish, distribute,
-	sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-	furnished to do so, subject to the following conditions:
-
-	The above copyright notice and this permission notice shall be included in all copies or
-	substantial portions of the Software.
-
-	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-	NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-	NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-	DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-	OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-
-Bit::Vector
-	This library is free software; you can redistribute it and/or    
-	modify it under the terms of the GNU Library General Public      
-	License as published by the Free Software Foundation; either     
-	version 2 of the License, || (at your option) any later version. 
-	                                                                 
-	This library is distributed in the hope that it will be useful,  
-	but WITHOUT ANY WARRANTY; without even the implied warranty of   
-	MERCHANTABILITY || FITNESS FOR A PARTICULAR PURPOSE. See the GNU 
-	Library General Public License for more details.                 
-	                                                                 
-	You should have received a copy of the GNU Library General Public
-	License along with this library; if not, write to the            
-	Free Software Foundation, Inc.,                                  
-	59 Temple Place, Suite 330, Boston, MA 02111-1307 USA            
-	                                                                 
-	|| download a copy from ftp://ftp.gnu.org/pub/gnu/COPYING.LIB-2.0
-
-CVC's SMT-LIB Parser
-	\file smtlib.y
-	
-	Author: Sergey Berezin, Clark Barrett
-	
-	Created: Apr 30 2005
-	
-	Copyright (C) 2004 by the Board of Trustees of Leland Stanford
-	Junior University and by New York University. 
-	
-	License to use, copy, modify, sell and/or distribute this software
-	and its documentation for any purpose is hereby granted without
-	royalty, subject to the terms and conditions defined in the \ref
-	LICENSE file provided with this distribution.  In particular:
-	
-	- The above copyright notice and this permission notice must appear
-	in all copies of the software and related documentation.
-	
-	- THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
-	EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
-
-Cryptominisat2
-	CryptoMiniSat -- Copyright (c) 2009 Mate Soos
-
-	Permission is hereby granted, free of charge, to any person obtaining a
-	copy of this software and associated documentation files (the
-	"Software"), to deal in the Software without restriction, including
-	without limitation the rights to use, copy, modify, merge, publish,
-	distribute, sublicense, and/or sell copies of the Software, and to
-	permit persons to whom the Software is furnished to do so, subject to
-	the following conditions:
-
-	The above copyright notice and this permission notice shall be included
-	in all copies or substantial portions of the Software.
-
-	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
-	OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-	MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-	NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
-	LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
-	OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
-	WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-
-Cryptominisat4
-        Copyright (c) 2009-2014, Mate Soos. All rights reserved.
-        
-        This library is free software; you can redistribute it and/or
-        modify it under the terms of the GNU Lesser General Public
-        License as published by the Free Software Foundation; either
-        version 2.0 of the License.
-        
-        This library is distributed in the hope that it will be useful,
-        but WITHOUT ANY WARRANTY; without even the implied warranty of
-        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-        Lesser General Public License for more details.
-        
-        You should have received a copy of the GNU Lesser General Public
-        License along with this library; if not, write to the Free Software
-        Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
-        MA 02110-1301  USA
-
-ABC
-	Copyright (c) The Regents of the University of California. All rights reserved.
-
-	Permission is hereby granted, without written agreement and without license or
-	royalty fees, to use, copy, modify, and distribute this software and its
-	documentation for any purpose, provided that the above copyright notice and
-	the following two paragraphs appear in all copies of this software.
-
-	IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
-	DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
-	THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
-	CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-	THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
-	BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-	A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
-	AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
-	SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
-
-Boost
-	Boost Software License - Version 1.0 - August 17th, 2003
-
-	Permission is hereby granted, free of charge, to any person or organization
-	obtaining a copy of the software and accompanying documentation covered by
-	this license (the "Software") to use, reproduce, display, distribute,
-	execute, and transmit the Software, and to prepare derivative works of the
-	Software, and to permit third-parties to whom the Software is furnished to
-	do so, all subject to the following:
-
-	The copyright notices in the Software and this entire statement, including
-	the above license grant, this restriction and the following disclaimer,
-	must be included in all copies of the Software, in whole or in part, and
-	all derivative works of the Software, unless such copies or derivative
-	works are solely in the form of machine-executable object code generated by
-	a source language processor.
-
-	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-	IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-	FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
-	SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
-	FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
-	ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
-	DEALINGS IN THE SOFTWARE.
-
-Windows msc99hdr
-        Copyright (c) 2006-2008 Alexander Chemeris
-        Copyright (c) 2000 Jeroen Ruigrok van der Werven <asmodai@FreeBSD.org>
-        
-        Redistribution and use in source and binary forms, with or without
-        modification, are permitted provided that the following conditions are met:
-        
-          1. Redistributions of source code must retain the above copyright notice,
-             this list of conditions and the following disclaimer.
-        
-          2. Redistributions in binary form must reproduce the above copyright
-             notice, this list of conditions and the following disclaimer in the
-             documentation and/or other materials provided with the distribution.
-        
-          3. The name of the author may be used to endorse or promote products
-             derived from this software without specific prior written permission.
-        
-        THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
-        WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
-        MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO
-        EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-        SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-        PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
-        OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
-        WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
-        OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
-        ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-LLVM integration tester (llvm-lit)
-    University of Illinois/NCSA
-    Open Source License
-
-    Copyright (c) 2003-2014 University of Illinois at Urbana-Champaign.
-    All rights reserved.
-
-    Developed by:
-
-        LLVM Team
-
-        University of Illinois at Urbana-Champaign
-
-        http://llvm.org
-
-    Permission is hereby granted, free of charge, to any person obtaining a copy of
-    this software and associated documentation files (the "Software"), to deal with
-    the Software without restriction, including without limitation the rights to
-    use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
-    of the Software, and to permit persons to whom the Software is furnished to do
-    so, subject to the following conditions:
-
-        * Redistributions of source code must retain the above copyright notice,
-          this list of conditions and the following disclaimers.
-
-        * Redistributions in binary form must reproduce the above copyright notice,
-          this list of conditions and the following disclaimers in the
-          documentation and/or other materials provided with the distribution.
-
-        * Neither the names of the LLVM Team, University of Illinois at
-          Urbana-Champaign, nor the names of its contributors may be used to
-          endorse or promote products derived from this Software without specific
-          prior written permission.
-
-    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
-    FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
-    CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-    LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-    OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE
-    SOFTWARE.
-
-OutputCheck
-    Copyright (c) 2014, Daniel Liew All rights reserved.
-
-    Redistribution and use in source and binary forms, with or without modification,
-    are permitted provided that the following conditions are met:
-
-    1. Redistributions of source code must retain the above copyright notice, this
-    list of conditions and the following disclaimer.
-
-    2. Redistributions in binary form must reproduce the above copyright notice,
-    this list of conditions and the following disclaimer in the documentation and/or
-    other materials provided with the distribution.
-
-    3. Neither the name of the copyright holder nor the names of its contributors
-    may be used to endorse or promote products derived from this software without
-    specific prior written permission.
-
-    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
-    ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-    WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-    DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
-    ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-    (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
-    ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-    (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-    SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-GoogleTest framework
-    Copyright 2008, Google Inc.
-    All rights reserved.
-
-    Redistribution and use in source and binary forms, with or without
-    modification, are permitted provided that the following conditions are
-    met:
-
-        * Redistributions of source code must retain the above copyright
-    notice, this list of conditions and the following disclaimer.
-        * Redistributions in binary form must reproduce the above
-    copyright notice, this list of conditions and the following disclaimer
-    in the documentation and/or other materials provided with the
-    distribution.
-        * Neither the name of Google Inc. nor the names of its
-    contributors may be used to endorse or promote products derived from
-    this software without specific prior written permission.
-
-    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-    A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-    OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-    SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-    LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-    DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-    THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-    (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-    OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-MemoryPool
-    Copyright (c) 2013 Cosku Acay, http://www.coskuacay.com
-
-    Permission is hereby granted, free of charge, to any person obtaining a
-    copy of this software and associated documentation files (the "Software"),
-    to deal in the Software without restriction, including without limitation
-    the rights to use, copy, modify, merge, publish, distribute, sublicense,
-    and/or sell copies of the Software, and to permit persons to whom the
-    Software is furnished to do so, subject to the following conditions:
-
-    The above copyright notice and this permission notice shall be included in
-    all copies or substantial portions of the Software.
-
-    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-    AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-    LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-    FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
-    IN THE SOFTWARE.
diff --git a/third_party/stp/OWNERS b/third_party/stp/OWNERS
deleted file mode 100644
index 8f9b21c..0000000
--- a/third_party/stp/OWNERS
+++ /dev/null
@@ -1,2 +0,0 @@
-mdempsky@chromium.org
-jln@chromium.org
diff --git a/third_party/stp/README.chromium b/third_party/stp/README.chromium
deleted file mode 100644
index 4612322..0000000
--- a/third_party/stp/README.chromium
+++ /dev/null
@@ -1,18 +0,0 @@
-Name: STP Constraint Solver
-Short Name: stp
-URL: https://sites.google.com/site/stpfastprover
-Version: 0
-Date: 2014-11-14
-Revision: fc94a599207752ab4d64048204f0c88494811b62
-License: MIT, LGPL
-License File: LICENSE
-Security Critical: no
-
-Description:
-STP is a constraint solver (also referred to as a decision procedure
-or automated prover) aimed at solving constraints generated by program
-analysis tools, theorem provers, automated bug finders, biology,
-cryptography, intelligent fuzzers and model checkers.
-
-Local Modifications:
-None.
diff --git a/third_party/stp/README.security b/third_party/stp/README.security
deleted file mode 100644
index 2f0502f..0000000
--- a/third_party/stp/README.security
+++ /dev/null
@@ -1,4 +0,0 @@
-This code is not considered security critical because it is used only
-for unit testing, and is not linked into chrome.
-
-Contact security@chromium.org before adding new uses.
diff --git a/third_party/stp/bison.py b/third_party/stp/bison.py
deleted file mode 100644
index 947ea3f..0000000
--- a/third_party/stp/bison.py
+++ /dev/null
@@ -1,18 +0,0 @@
-# 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.
-
-import subprocess
-import sys
-
-(source, name, out,) = sys.argv[1:]
-
-subprocess.check_call([
-  "bison",
-  "--debug",
-  "-Wnone",
-  "-o", out + ".cpp",
-  "--defines=" + out + ".hpp",
-  "-p", name,
-  source,
-])
diff --git a/third_party/stp/config/stp/config.h b/third_party/stp/config/stp/config.h
deleted file mode 100644
index d1f2fc3..0000000
--- a/third_party/stp/config/stp/config.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/***********
-AUTHORS: Ryan Govostes, Dan Liew
-
-BEGIN DATE: Sept, 2013
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in
-all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECT
-**********************/
-
-
-#ifndef _CONFIG_H_
-#define _CONFIG_H_
-
-#if __cplusplus
-
-/* Where to find <hash_set> or <unordered_set>, if available. */
-#define HAVE_HASH_SET 0
-#define HASH_SET_H <unordered_set>
-#define HASH_SET_CLASS unordered_set
-#define HASH_SET_NAMESPACE std
-
-/* Where to find <hash_multiset> or <unordered_multiset>, if available. */
-#define HAVE_HASH_MULTISET 0
-#define HASH_MULTISET_H <unordered_set>
-#define HASH_MULTISET_CLASS unordered_multiset
-#define HASH_MULTISET_NAMESPACE std
-
-/* Where to find <hash_map> or <unordered_map>, if available. */
-#define HAVE_HASH_MAP 0
-#define HASH_MAP_H <unordered_map>
-#define HASH_MAP_CLASS unordered_map
-#define HASH_MAP_NAMESPACE std
-
-#endif
-
-#endif
diff --git a/third_party/stp/flex.py b/third_party/stp/flex.py
deleted file mode 100644
index 8eac4e0..0000000
--- a/third_party/stp/flex.py
+++ /dev/null
@@ -1,16 +0,0 @@
-# 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.
-
-import subprocess
-import sys
-
-(source, name, out,) = sys.argv[1:]
-
-subprocess.check_call([
-  "flex",
-  "-Cfe",
-  "-o", out + ".cpp",
-  "--prefix=" + name,
-  source,
-])
diff --git a/third_party/stp/genastkinds.py b/third_party/stp/genastkinds.py
deleted file mode 100644
index 93eb989..0000000
--- a/third_party/stp/genastkinds.py
+++ /dev/null
@@ -1,17 +0,0 @@
-# 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.
-
-import os
-import os.path
-import subprocess
-import sys
-
-(script, source, out,) = sys.argv[1:]
-
-subprocess.check_call([
-  "perl", script,
-  "--file", source,
-])
-os.rename("ASTKind.cpp", os.path.join(out, "src/lib/AST/ASTKind.cpp"))
-os.rename("ASTKind.h", os.path.join(out, "src/include/stp/AST/ASTKind.h"))
diff --git a/third_party/stp/stp.gyp b/third_party/stp/stp.gyp
deleted file mode 100644
index e938a02..0000000
--- a/third_party/stp/stp.gyp
+++ /dev/null
@@ -1,415 +0,0 @@
-# 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.
-
-{
-  'variables': {
-    'shared_generated_dir': '<(SHARED_INTERMEDIATE_DIR)/third_party/stp',
-  },
-  'targets': [
-    {
-      'target_name': 'stp',
-      'type': '<(component)',
-      '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',
-      ],
-      'direct_dependent_settings': {
-        'include_dirs': [
-          'src/include',
-        ],
-      },
-      'include_dirs': [
-        'config',
-        'src/include',
-        'src/lib',
-        'src/lib/Sat',
-        'src/lib/Sat/cryptominisat2/mtl',
-        'src/lib/extlib-abc',
-        '<(shared_generated_dir)/src/include',
-      ],
-      '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',
-        '<(shared_generated_dir)/src/include/stp/AST/ASTKind.h',
-        '<(shared_generated_dir)/src/lib/AST/ASTKind.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/lexcvc.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/lexsmt.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/lexsmt2.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsecvc.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsecvc.hpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsesmt.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsesmt.hpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsesmt2.cpp',
-        '<(shared_generated_dir)/src/lib/Parser/parsesmt2.hpp',
-      ],
-      'dependencies': [
-        'stp_generated_sources',
-      ],
-    },
-    {
-      'target_name': 'stp_generated_sources',
-      'type': 'none',
-      'sources': [
-        'src/lib/AST/ASTKind.kinds',
-        'src/lib/Parser/cvc.lex',
-        'src/lib/Parser/cvc.y',
-        'src/lib/Parser/smt.lex',
-        'src/lib/Parser/smt.y',
-        'src/lib/Parser/smt2.lex',
-        'src/lib/Parser/smt2.y',
-      ],
-      'actions': [
-        {
-          'action_name': 'generate_astkind',
-          'inputs': [
-            'genastkinds.py',
-            'src/lib/AST/ASTKind.kinds',
-            'src/lib/AST/genkinds.pl',
-          ],
-          'outputs': [
-            '<(shared_generated_dir)/src/include/stp/AST/ASTKind.h',
-            '<(shared_generated_dir)/src/lib/AST/ASTKind.cpp',
-          ],
-          'action': [
-            'python',
-            'genastkinds.py',
-            'src/lib/AST/genkinds.pl',
-            'src/lib/AST/ASTKind.kinds',
-            '<(shared_generated_dir)',
-          ],
-          'message': 'Generating ASTKind ...',
-        },
-      ],
-      'rules': [
-        {
-          'rule_name': 'generate_flex',
-          'extension': '.lex',
-          'inputs': [
-            'flex.py',
-          ],
-          'outputs': [
-            '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/lex<(RULE_INPUT_ROOT).cpp',
-          ],
-          'action': [
-            'python',
-            'flex.py',
-            '<(RULE_INPUT_PATH)',
-            '<(RULE_INPUT_ROOT)',
-            '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/lex<(RULE_INPUT_ROOT)',
-          ],
-          'message': 'Generating <(RULE_INPUT_ROOT) lexer ...',
-        },
-        {
-          'rule_name': 'generate_bison',
-          'extension': '.y',
-          'inputs': [
-            'bison.py',
-          ],
-          'outputs': [
-            '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT).cpp',
-            '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT).hpp',
-          ],
-          'action': [
-            'python',
-            'bison.py',
-            '<(RULE_INPUT_PATH)',
-            '<(RULE_INPUT_ROOT)',
-            '<(shared_generated_dir)/<(RULE_INPUT_DIRNAME)/parse<(RULE_INPUT_ROOT)',
-          ],
-          'message': 'Generating <(RULE_INPUT_ROOT) parser ...',
-        },
-      ],
-    },
-  ],
-}