Revision ee040783039b63af686d93be09a1f82df25e36e6 authored by Fabian Kunze on 01 February 2021, 11:08:31 UTC, committed by Fabian Kunze on 01 February 2021, 11:08:31 UTC
1 parent 93f57c3
count-lines.sh
#!/bin/bash
printf "Basic complexity\n"
coqwc\
theories/Complexity/Definitions.v\
theories/Complexity/EncodableP.v\
theories/Complexity/LinTimeDecodable.v\
theories/Complexity/Monotonic.v\
theories/Complexity/NP.v\
theories/Complexity/ONotation.v\
theories/Complexity/PolyTimeComputable.v\
theories/Complexity/Subtypes.v
printf "Problem definitions - non-flat\n"
coqwc \
theories/NP/SAT/SharedSAT.v\
theories/NP/SAT/SAT.v\
theories/NP/SAT/kSAT.v\
theories/NP/SAT/FSAT/FSAT.v\
theories/NP/SAT/CookLevin/Subproblems/BinaryCC.v\
theories/NP/SAT/CookLevin/Subproblems/CC.v\
theories/NP/SAT/CookLevin/Subproblems/TM_single.v\
theories/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.v\
theories/NP/TM/TMGenNP_fixed_mTM.v\
theories/NP/TM/TMGenNP.v\
theories/NP/L/GenNP.v\
theories/NP/L/GenNPBool.v\
theories/NP/L/CanEnumTerm.v\
theories/NP/L/GenNP_is_hard.v\
theories/NP/L/LMGenNP.v
printf "Problem definitions - additional flat variants\n"
# note: we omit the flat variants of Turing machines already available in the library of undecidable problems
coqwc\
theories/NP/SAT/CookLevin/Subproblems/FlatCC.v\
theories/NP/SAT/CookLevin/Subproblems/FlatTCC.v
printf "\n\nReductions\n\n"
printf "L to LM\n"
coqwc\
theories/NP/TM/L_to_LM.v
printf "LM to mTM\n"
coqwc\
theories/NP/TM/LM_to_mTM.v\
theories/NP/TM/M_LM2TM.v
printf "mTM to TMGenNP\n"
coqwc\
theories/NP/TM/M_multi2mono.v\
theories/NP/TM/mTM_to_singleTapeTM.v
printf "TM to CC\n"
coqwc\
theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v\
theories/NP/SAT/CookLevin/Reductions/PTCC_Preludes.v\
theories/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.v\
theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v\
theories/NP/SAT/CookLevin/Reductions/TCC_to_CC.v\
theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v
printf "CC to BCC\n"
coqwc\
theories/NP/SAT/CookLevin/Reductions/CC_homomorphisms.v\
theories/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.v\
theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v
printf "BinaryCC to FSAT\n"
coqwc\
theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v\
theories/NP/SAT/FSAT/FormulaEncoding.v
printf "FSAT to SAT\n"
coqwc\
theories/NP/SAT/FSAT/FSAT_to_SAT.v
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...