lib/linguist/samples.json in github-linguist-4.5.6 vs lib/linguist/samples.json in github-linguist-4.5.8
- old
+ new
@@ -821,10 +821,14 @@
".sas"
],
"SCSS": [
".scss"
],
+ "SMT": [
+ ".smt",
+ ".smt2"
+ ],
"SPARQL": [
".sparql"
],
"SQF": [
".hqf",
@@ -1190,10 +1194,13 @@
],
"INI": [
".editorconfig",
".gitconfig"
],
+ "Isabelle ROOT": [
+ "ROOT"
+ ],
"Linker Script": [
"ld.script"
],
"Makefile": [
"Kbuild",
@@ -1268,12 +1275,12 @@
],
"YAML": [
".gemrc"
]
},
- "tokens_total": 941132,
- "languages_total": 1339,
+ "tokens_total": 967294,
+ "languages_total": 1345,
"tokens": {
"ABAP": {
"*/**": 1,
"*": 58,
"The": 2,
@@ -41802,10 +41809,451 @@
"qed": 1,
"fastforce": 1,
"intro": 1,
"end": 1
},
+ "Isabelle ROOT": {
+ "chapter": 1,
+ "HOL": 59,
+ "session": 13,
+ "(": 5,
+ "main": 2,
+ ")": 6,
+ "Pure": 2,
+ "+": 14,
+ "description": 12,
+ "{": 21,
+ "*": 23,
+ "Classical": 2,
+ "Higher": 2,
+ "-": 123,
+ "order": 2,
+ "Logic.": 1,
+ "}": 17,
+ "options": 10,
+ "[": 14,
+ "document_graph": 7,
+ "]": 14,
+ "global_theories": 1,
+ "Main": 2,
+ "Complex_Main": 1,
+ "files": 2,
+ "document_files": 9,
+ "with": 3,
+ "explicit": 1,
+ "proof": 2,
+ "terms.": 1,
+ "document": 6,
+ "false": 8,
+ "quick_and_dirty": 2,
+ "theories": 14,
+ "Proofs": 1,
+ "in": 15,
+ "Library": 3,
+ "Logic": 2,
+ "batteries": 1,
+ "included.": 1,
+ "List_lexord": 1,
+ "Sublist_Order": 1,
+ "Product_Lexorder": 1,
+ "Product_Order": 1,
+ "Finite_Lattice": 1,
+ "AList_Mapping": 1,
+ "Code_Binary_Nat": 1,
+ "Code_Char": 1,
+ "Code_Prolog": 1,
+ "Code_Real_Approx_By_Float": 1,
+ "Code_Target_Numeral": 1,
+ "DAList": 1,
+ "DAList_Multiset": 1,
+ "RBT_Mapping": 1,
+ "RBT_Set": 1,
+ "Refute": 1,
+ "Old_Datatype": 1,
+ "Old_Recdef": 1,
+ "Old_SMT": 1,
+ "Hahn_Banach": 1,
+ "Author": 4,
+ "Gertrud": 1,
+ "Bauer": 1,
+ "TU": 2,
+ "Munich": 1,
+ "The": 5,
+ "Hahn": 3,
+ "Banach": 3,
+ "theorem": 4,
+ "for": 4,
+ "real": 2,
+ "vector": 1,
+ "spaces.": 1,
+ "This": 4,
+ "is": 4,
+ "the": 5,
+ "of": 21,
+ "vectorspaces": 1,
+ "following": 1,
+ "H.": 1,
+ "Heuser": 1,
+ "Funktionalanalysis": 1,
+ "p.": 1,
+ "one": 1,
+ "fundamental": 1,
+ "theorems": 1,
+ "functional": 2,
+ "analysis.": 1,
+ "It": 1,
+ "a": 11,
+ "conclusion": 1,
+ "Zorn": 1,
+ "s": 3,
+ "Theorem": 4,
+ "some": 2,
+ "lemmas": 1,
+ "Quadratic": 1,
+ "Reciprocity.": 1,
+ "Pocklington": 1,
+ "Gauss": 1,
+ "Number_Theory": 1,
+ "Euclidean_Algorithm": 1,
+ "Old_Number_Theory": 1,
+ "Fundamental": 1,
+ "Arithmetic": 1,
+ "Chinese": 1,
+ "Remainder": 1,
+ "Fermat/Euler": 1,
+ "Wilson": 1,
+ "Bij": 1,
+ "Divisibility": 1,
+ "IntRing": 1,
+ "UnivPoly": 1,
+ "Auth": 1,
+ "A": 2,
+ "new": 1,
+ "approach": 1,
+ "to": 2,
+ "verifying": 1,
+ "authentication": 1,
+ "protocols.": 1,
+ "Auth_Shared": 1,
+ "Auth_Public": 1,
+ "UNITY": 1,
+ "Lawrence": 1,
+ "C": 1,
+ "Paulson": 1,
+ "Cambridge": 2,
+ "University": 2,
+ "Computer": 1,
+ "Laboratory": 1,
+ "Copyright": 2,
+ "Verifying": 1,
+ "security": 1,
+ "protocols": 2,
+ "using": 1,
+ "Chandy": 1,
+ "and": 15,
+ "Misra": 1,
+ "Notation.": 1,
+ "defines": 1,
+ "lambda": 1,
+ "calculus": 1,
+ "terms": 1,
+ "de": 1,
+ "Bruijn": 1,
+ "indixes": 1,
+ "proves": 1,
+ "confluence": 1,
+ "beta": 2,
+ "eta": 1,
+ "eta.": 1,
+ "paper": 1,
+ "describes": 1,
+ "whole": 1,
+ "theory": 2,
+ "see": 2,
+ "http": 1,
+ "//www.in.tum.de/": 1,
+ "nipkow/pubs/jar2001.html": 1,
+ ".": 1,
+ "print_mode": 1,
+ "parallel_proofs": 1,
+ "Eta": 1,
+ "StrongNorm": 1,
+ "Standardization": 1,
+ "WeakNorm": 1,
+ "Prolog": 3,
+ "David": 1,
+ "von": 1,
+ "Oheimb": 1,
+ "based": 1,
+ "on": 4,
+ "lecture": 1,
+ "Lambda": 3,
+ "by": 1,
+ "Nadathur": 1,
+ "bare": 1,
+ "bones": 1,
+ "implementation": 2,
+ "Prolog.": 1,
+ "simple": 1,
+ "exploratory": 1,
+ "including": 2,
+ "minimal": 1,
+ "examples": 1,
+ "Test.thy": 1,
+ "more": 1,
+ "typical": 1,
+ "example": 1,
+ "little": 1,
+ "language": 1,
+ "its": 2,
+ "type": 2,
+ "system.": 1,
+ "Test": 1,
+ "Type": 1,
+ "MicroJava": 2,
+ "Formalization": 1,
+ "fragment": 2,
+ "Java": 1,
+ "together": 1,
+ "corresponding": 1,
+ "virtual": 1,
+ "machine": 1,
+ "specification": 1,
+ "bytecode": 2,
+ "verifier": 2,
+ "lightweight": 1,
+ "proofs": 2,
+ "safety.": 1,
+ "NanoJava": 1,
+ "Hoare": 1,
+ "tiny": 1,
+ "Java.": 1,
+ "Example": 1,
+ "Bali": 1,
+ "AxExample": 1,
+ "AxSound": 1,
+ "AxCompl": 1,
+ "Trans": 1,
+ "IOA": 6,
+ "Tobias": 2,
+ "Nipkow": 4,
+ "Konrad": 2,
+ "Slind": 3,
+ "Olaf": 2,
+ "M": 2,
+ "ller": 1,
+ "Muenchen": 1,
+ "meta": 1,
+ "I/O": 2,
+ "Automata": 2,
+ "HOL.": 1,
+ "formalization": 1,
+ "has": 1,
+ "been": 2,
+ "significantly": 1,
+ "changed": 1,
+ "extended": 1,
+ "HOLCF/IOA.": 1,
+ "There": 1,
+ "are": 1,
+ "also": 1,
+ "two": 1,
+ "communication": 1,
+ "which": 1,
+ "formerly": 1,
+ "have": 1,
+ "here.": 1,
+ "@inproceedings": 2,
+ "author": 2,
+ "title": 1,
+ "Isabelle/HOL": 1,
+ "booktitle": 1,
+ "Proc.": 1,
+ "TYPES": 1,
+ "Workshop": 1,
+ "publisher": 1,
+ "Springer": 1,
+ "series": 1,
+ "LNCS": 1,
+ "note": 1,
+ "To": 1,
+ "appear": 1,
+ "ftp": 1,
+ "//ftp.informatik.tu": 1,
+ "muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz": 1,
+ "Mueller": 1,
+ "Lattice": 1,
+ "root.tex": 15,
+ "ex": 4,
+ "/src/HOL/Library/State_Monad": 1,
+ "/src/HOL/Library/FuncSet": 1,
+ "/src/HOL/Library/FinFun_Syntax": 1,
+ "/src/HOL/Library/Refute": 1,
+ "/src/HOL/Library/Transitive_Closure_Table": 1,
+ "root.bib": 5,
+ "Isar_Examples": 1,
+ "/src/HOL/Library/Lattice_Syntax": 1,
+ "../Number_Theory/Primes": 1,
+ "style.tex": 1,
+ "SET_Protocol": 1,
+ "/src/HOL/Library/Nat_Bijection": 2,
+ "Matrix_LP": 1,
+ "TLA": 7,
+ "Inc": 1,
+ "TLA/Inc": 1,
+ "Buffer": 2,
+ "TLA/Buffer": 1,
+ "Memory": 1,
+ "TLA/Memory": 1,
+ "TPTP": 1,
+ "Multivariate_Analysis": 2,
+ "Probability": 2,
+ "/src/HOL/Library/Countable": 2,
+ "/src/HOL/Library/Permutation": 1,
+ "/src/HOL/Library/Order_Continuity": 1,
+ "/src/HOL/Library/Diagonal_Subsequence": 1,
+ "ex/Dining_Cryptographers": 1,
+ "ex/Koepf_Duermuth_Countermeasure": 1,
+ "Nominal": 3,
+ "Examples": 4,
+ "Nominal/Examples": 1,
+ "Cardinals": 1,
+ "intro.tex": 2,
+ "Datatype_Examples": 1,
+ "/src/HOL/Library/Old_Datatype": 1,
+ "Derivation_Trees/Gram_Lang": 1,
+ "Derivation_Trees/Parallel": 1,
+ "Word": 6,
+ "Word/Examples": 1,
+ "Statespace": 1,
+ "NSA": 3,
+ "NSA/Examples": 1,
+ "Mirabelle": 3,
+ "Mirabelle/ex": 1,
+ "SMT_Examples": 1,
+ "Boogie_Dijkstra.certs": 1,
+ "Boogie_Max.certs": 1,
+ "SMT_Examples.certs": 1,
+ "SMT_Word_Examples.certs": 1,
+ "VCC_Max.certs": 1,
+ "SPARK": 6,
+ "SPARK/Examples": 1,
+ "Gcd/Greatest_Common_Divisor": 1,
+ "Liseq/Longest_Increasing_Subsequence": 1,
+ "RIPEMD": 36,
+ "/F": 1,
+ "/Hash": 1,
+ "/K_L": 1,
+ "/K_R": 1,
+ "/R_L": 1,
+ "/Round": 1,
+ "/R_R": 1,
+ "/S_L": 1,
+ "/S_R": 1,
+ "Sqrt/Sqrt": 1,
+ "Gcd/greatest_common_divisor/g_c_d.fdl": 1,
+ "Gcd/greatest_common_divisor/g_c_d.rls": 1,
+ "Gcd/greatest_common_divisor/g_c_d.siv": 1,
+ "Liseq/liseq/liseq_length.fdl": 1,
+ "Liseq/liseq/liseq_length.rls": 1,
+ "Liseq/liseq/liseq_length.siv": 1,
+ "/rmd/f.fdl": 1,
+ "/rmd/f.rls": 1,
+ "/rmd/f.siv": 1,
+ "/rmd/hash.fdl": 1,
+ "/rmd/hash.rls": 1,
+ "/rmd/hash.siv": 1,
+ "/rmd/k_l.fdl": 1,
+ "/rmd/k_l.rls": 1,
+ "/rmd/k_l.siv": 1,
+ "/rmd/k_r.fdl": 1,
+ "/rmd/k_r.rls": 1,
+ "/rmd/k_r.siv": 1,
+ "/rmd/r_l.fdl": 1,
+ "/rmd/r_l.rls": 1,
+ "/rmd/r_l.siv": 1,
+ "/rmd/round.fdl": 1,
+ "/rmd/round.rls": 1,
+ "/rmd/round.siv": 1,
+ "/rmd/r_r.fdl": 1,
+ "/rmd/r_r.rls": 1,
+ "/rmd/r_r.siv": 1,
+ "/rmd/s_l.fdl": 1,
+ "/rmd/s_l.rls": 1,
+ "/rmd/s_l.siv": 1,
+ "/rmd/s_r.fdl": 1,
+ "/rmd/s_r.rls": 1,
+ "/rmd/s_r.siv": 1,
+ "Manual": 1,
+ "SPARK/Manual": 1,
+ "complex_types_app/initialize.fdl": 1,
+ "complex_types_app/initialize.rls": 1,
+ "complex_types_app/initialize.siv": 1,
+ "loop_invariant/proc1.fdl": 1,
+ "loop_invariant/proc1.rls": 1,
+ "loop_invariant/proc1.siv": 1,
+ "loop_invariant/proc2.fdl": 1,
+ "loop_invariant/proc2.rls": 1,
+ "loop_invariant/proc2.siv": 1,
+ "simple_greatest_common_divisor/g_c_d.fdl": 1,
+ "simple_greatest_common_divisor/g_c_d.rls": 1,
+ "simple_greatest_common_divisor/g_c_d.siv": 1,
+ "complex_types.ads": 1,
+ "complex_types_app.adb": 1,
+ "complex_types_app.ads": 1,
+ "Gcd.adb": 1,
+ "Gcd.ads": 1,
+ "loop_invariant.adb": 1,
+ "loop_invariant.ads": 1,
+ "Simple_Gcd.adb": 1,
+ "Simple_Gcd.ads": 1,
+ "Mutabelle": 1,
+ "Quickcheck_Examples": 1,
+ "Quickcheck_Benchmark": 1,
+ "Quotient_Examples": 1,
+ "Predicate_Compile_Examples": 1,
+ "ISABELLE_SWIPL": 2,
+ "HOLCF": 5,
+ "Tutorial": 1,
+ "HOLCF/Tutorial": 1,
+ "HOLCF/Library": 1,
+ "IMP": 1,
+ "HOLCF/IMP": 1,
+ "HOLCF/ex": 1,
+ "FOCUS": 2,
+ "HOLCF/FOCUS": 1,
+ "Design": 1,
+ "Distributed": 1,
+ "Systems": 2,
+ "An": 1,
+ "Introduction": 1,
+ "Specification": 2,
+ "Refinement": 2,
+ "Length": 1,
+ "One": 1,
+ "Development": 1,
+ "Interactive": 1,
+ "Focus": 1,
+ "Streams": 1,
+ "Interfaces": 1,
+ "HOLCF/IOA": 1,
+ "meta_theory/Abstraction": 1,
+ "ABP": 1,
+ "HOLCF/IOA/ABP": 1,
+ "NTP": 1,
+ "HOLCF/IOA/NTP": 1,
+ "Storage": 1,
+ "HOLCF/IOA/Storage": 1,
+ "HOLCF/IOA/ex": 1,
+ "Record_Benchmark": 3,
+ "Some": 1,
+ "benchmark": 1,
+ "large": 1,
+ "record.": 1,
+ "condition": 1,
+ "ISABELLE_FULL_TEST": 1
+ },
"J": {
"NB.": 7,
"From": 1,
".": 1,
"See": 1,
@@ -73580,11 +74028,11 @@
"PHP_URL_PATH": 1,
"path.": 1,
"getParameters": 1,
"getFiles": 3,
"getServer": 1,
- "<?php>": 4,
+ "<?php>": 5,
"CakePHP": 6,
"tm": 6,
"Rapid": 2,
"Development": 2,
"Framework": 2,
@@ -73665,11 +74113,11 @@
"methods": 5,
"These": 1,
"are": 5,
"on": 4,
"that": 2,
- "not": 2,
+ "not": 3,
"prefixed": 1,
"with": 5,
"_": 1,
"Each": 1,
"serves": 1,
@@ -74286,11 +74734,15 @@
"autoload": 1,
"config": 3,
"application": 2,
"_SERVER": 1,
"_GET": 1,
- "var": 1
+ "var": 1,
+ "I": 1,
+ "am": 1,
+ "Isabelle": 1,
+ "ROOT": 1
},
"PLSQL": {
"create": 5,
"or": 6,
"replace": 4,
@@ -75037,12 +75489,12 @@
},
"Perl": {
"package": 17,
"App": 131,
"Ack": 136,
- ";": 1420,
- "use": 98,
+ ";": 1421,
+ "use": 99,
"warnings": 19,
"strict": 22,
"File": 56,
"Next": 27,
"Plugin": 2,
@@ -77077,22 +77529,23 @@
"convert": 1,
"formats": 1,
"<+3M>": 1,
"reference.": 1,
"AUTHOR": 1,
- "Test": 2,
+ "Test": 3,
"Base": 1,
+ "More": 1,
"__DATA__": 1,
"Strict": 1,
"Mojolicious": 1,
"Lite": 1,
"experimental": 1
},
"Perl6": {
"use": 55,
"v6": 13,
- ";": 1063,
+ ";": 1062,
"Test": 11,
"begin": 6,
"pod": 106,
"handling": 1,
"of": 94,
@@ -77112,20 +77565,20 @@
"Ibar": 1,
"should": 6,
"make": 1,
"<@*INC>": 3,
"look": 1,
- "like": 10,
+ "like": 3,
"foo": 6,
"bar": 1,
"...": 5,
"Duplication": 1,
"directories": 1,
"on": 12,
"the": 33,
"command": 9,
- "line": 8,
+ "line": 5,
"is": 271,
"mirrored": 1,
"in": 24,
"variable": 4,
"so": 3,
@@ -77140,12 +77593,12 @@
".": 27,
"end": 6,
"my": 310,
"fragment": 1,
"@tests": 2,
- "(": 852,
- ")": 871,
+ "(": 844,
+ ")": 863,
"plan": 7,
"@tests*2": 1,
"diag": 3,
"pugs": 25,
"redir": 2,
@@ -77156,12 +77609,12 @@
"any": 3,
"<MSWin32>": 1,
"mingw": 1,
"msys": 1,
"cygwin": 1,
- "{": 623,
- "}": 617,
+ "{": 620,
+ "}": 615,
"sub": 97,
"nonce": 2,
"return": 71,
".pick": 1,
"run_pugs": 3,
@@ -77220,11 +77673,11 @@
"%": 127,
"*": 15,
"_": 71,
"./": 1,
"<": 15,
- "A": 15,
+ "A": 12,
"key": 7,
"can": 2,
"be": 10,
"string": 14,
"rosebud": 1,
@@ -77318,15 +77771,15 @@
"style": 1,
"bold": 3,
"text1": 1,
"onMouseUp": 1,
"sun1.opacity": 2,
- "a": 64,
+ "a": 56,
"implement": 1,
"no": 4,
"stinkin": 1,
- "single": 5,
+ "single": 2,
"quote": 2,
"<[\"\\ttab\\tcharacter>": 1,
"unquoted_key": 1,
"@n": 2,
"i": 12,
@@ -77454,22 +77907,22 @@
"using": 3,
"ANSI": 1,
"escape": 5,
"sequences": 3,
"SYNOPSIS": 1,
- "say": 47,
+ "say": 46,
"DESCRIPTION": 2,
"provides": 2,
"interface": 1,
"terminals.": 1,
"following": 4,
"functions": 1,
"available": 5,
"head2": 5,
"<color()>": 4,
"Given": 2,
- "with": 30,
+ "with": 22,
"names": 11,
"produced": 1,
"by": 26,
"sets": 1,
"terminal": 1,
@@ -77588,11 +78041,11 @@
"app.context.env": 1,
"match": 6,
"app.find_route": 1,
"app.response.content": 2,
"r.value.": 2,
- "|": 28,
+ "|": 25,
"match.list": 1,
"app.response": 1,
"psgi": 2,
".psgi": 1,
"baile": 1,
@@ -77602,11 +78055,11 @@
".run": 1,
"test_lines": 3,
"@lines": 8,
"SHEBANG#!#!rakudo": 1,
"@lines.elems": 1,
- "#": 57,
+ "#": 50,
"niecza": 6,
"skip": 12,
"fh": 6,
"open": 5,
"count": 3,
@@ -77644,11 +78097,11 @@
"uc": 1,
"@things": 2,
"separator": 2,
".uc.join": 1,
"Failure": 1,
- "role": 12,
+ "role": 4,
"X": 47,
"Comp": 12,
"ControlFlow": 2,
"Exception": 13,
"has": 49,
@@ -78087,11 +78540,11 @@
"_.key": 4,
"#L": 1,
"S04/The": 1,
"<for>": 1,
"statement/implicit": 1,
- "block": 20,
+ "block": 18,
"read/write": 1,
"_.WHAT.gist": 3,
"Int.gist": 1,
"Array.gist": 2,
"h": 4,
@@ -78450,11 +78903,11 @@
"re": 1,
"list": 4,
"via": 1,
"IsSpace": 1,
"fly.": 1,
- "Of": 2,
+ "Of": 1,
"course": 1,
"contain": 1,
"whitespace.": 1,
"<\\xA0>": 1,
"specifically": 1,
@@ -78734,18 +79187,10 @@
"Hooray": 1,
"<now>": 1,
"more": 1,
"Hash.new": 1,
"highlighted": 1,
- "table": 1,
- "things": 1,
- "declarator": 7,
- "keyword": 7,
- "Another": 2,
- "brace": 1,
- "More": 2,
- "blocks": 2,
"don": 2,
"Rob": 1,
"food": 1,
"something": 1,
"some": 2,
@@ -88620,10 +89065,614 @@
"}": 2,
".border": 1,
"padding": 1,
"/": 2
},
+ "SMT": {
+ "(": 5805,
+ "set": 17,
+ "-": 647,
+ "logic": 4,
+ "QF_LIA": 1,
+ ")": 5814,
+ "info": 13,
+ "source": 3,
+ "|": 280,
+ "SMT": 2,
+ "COMP": 1,
+ "organizers": 1,
+ "smt": 3,
+ "lib": 3,
+ "version": 3,
+ "category": 3,
+ "status": 3,
+ "unsat": 1,
+ "notes": 1,
+ "This": 1,
+ "benchmark": 1,
+ "is": 2,
+ "designed": 1,
+ "to": 5,
+ "check": 5,
+ "if": 2,
+ "the": 1,
+ "DP": 1,
+ "supports": 1,
+ "bignumbers.": 1,
+ "declare": 64,
+ "fun": 345,
+ "x1": 65,
+ "Int": 18,
+ "x2": 53,
+ "x3": 49,
+ "x4": 37,
+ "x5": 37,
+ "x6": 36,
+ "assert": 9,
+ "and": 18,
+ "or": 8,
+ "<": 2,
+ "<=>": 11,
+ "8000": 1,
+ "sat": 6,
+ "exit": 3,
+ "AUFLIRA": 1,
+ "Buggy": 1,
+ "list": 1,
+ "theorem": 1,
+ "sort": 27,
+ "List": 17,
+ "cons": 8,
+ "Real": 7,
+ "nil": 3,
+ "car": 2,
+ "cdr": 2,
+ "len": 4,
+ "forall": 5,
+ "x": 974,
+ "y": 895,
+ "+": 1,
+ "append": 4,
+ "y1": 3,
+ "y2": 3,
+ "not": 140,
+ "QF_IDL": 1,
+ "Queens": 1,
+ "benchmarks": 1,
+ "generated": 1,
+ "by": 1,
+ "Hyondeuk": 1,
+ "Kim": 1,
+ "in": 13,
+ "LIB": 1,
+ "format.": 1,
+ "x0": 60,
+ "x7": 32,
+ "x8": 20,
+ "x9": 20,
+ "x10": 11,
+ "let": 174,
+ "v_0": 3,
+ "v_1": 3,
+ "v_2": 3,
+ "v_3": 3,
+ "v_4": 3,
+ "v_5": 3,
+ "v_6": 3,
+ "v_7": 3,
+ "v_8": 3,
+ "v_9": 3,
+ "v_10": 3,
+ "v_11": 3,
+ "v_12": 3,
+ "v_13": 3,
+ "v_14": 3,
+ "v_15": 3,
+ "v_16": 3,
+ "v_17": 3,
+ "v_18": 3,
+ "v_19": 3,
+ "v_20": 3,
+ "v_21": 3,
+ "v_22": 3,
+ "v_23": 3,
+ "v_24": 3,
+ "v_25": 3,
+ "v_26": 3,
+ "v_27": 3,
+ "v_28": 3,
+ "v_29": 3,
+ "v_30": 3,
+ "v_31": 3,
+ "v_32": 3,
+ "v_33": 3,
+ "v_34": 3,
+ "v_35": 3,
+ "v_36": 3,
+ "v_37": 3,
+ "v_38": 3,
+ "v_39": 3,
+ "v_40": 3,
+ "v_41": 3,
+ "v_42": 3,
+ "v_43": 3,
+ "v_44": 3,
+ "v_45": 3,
+ "v_46": 3,
+ "v_47": 3,
+ "v_48": 3,
+ "v_49": 3,
+ "v_50": 3,
+ "v_51": 3,
+ "v_52": 3,
+ "v_53": 3,
+ "v_54": 3,
+ "9": 10,
+ "QF_ABV": 1,
+ "define": 308,
+ "Address": 30,
+ "_": 318,
+ "BitVec": 178,
+ "Byte": 2,
+ "Mem": 34,
+ "Array": 25,
+ "I8": 3,
+ "I16": 3,
+ "I32": 3,
+ "I64": 3,
+ "I128": 3,
+ ";": 490,
+ "constants": 1,
+ "zero": 7,
+ "bv0": 84,
+ "one": 5,
+ "bv1": 7,
+ "two": 8,
+ "bv2": 1,
+ "three": 3,
+ "bv3": 2,
+ "four": 8,
+ "bv4": 7,
+ "five": 1,
+ "bv5": 1,
+ "six": 1,
+ "bv6": 1,
+ "seven": 1,
+ "bv7": 1,
+ "eight": 8,
+ "bv8": 3,
+ "Write": 6,
+ "a": 31,
+ "little": 14,
+ "endian": 14,
+ "bit": 14,
+ "value": 12,
+ "aligned": 2,
+ "at": 13,
+ "address": 13,
+ "mem": 42,
+ "write1": 1,
+ "v": 18,
+ "Bool": 30,
+ "store": 107,
+ "ite": 3,
+ "#x01": 1,
+ "#x00": 2,
+ "write8": 1,
+ "write16": 1,
+ "b0": 16,
+ "extract": 32,
+ "b1": 16,
+ "bvadd": 70,
+ "write32": 9,
+ "b2": 4,
+ "b3": 4,
+ "write64": 4,
+ "write128": 1,
+ "Read": 6,
+ "returns": 1,
+ "Boolean": 1,
+ "true": 4,
+ "what": 1,
+ "s": 1,
+ "stored": 1,
+ "non": 1,
+ "read1": 1,
+ "select": 1478,
+ "read8": 1,
+ "read16": 1,
+ "concat": 11,
+ "read32": 13,
+ "read64": 7,
+ "read128": 1,
+ "Vectors": 30,
+ "of": 32,
+ "int4": 7,
+ "elements": 35,
+ "vector_1_4": 4,
+ "vundef_1_4": 2,
+ "int8": 7,
+ "vector_1_8": 43,
+ "vundef_1_8": 2,
+ "int16": 7,
+ "vector_1_16": 43,
+ "vundef_1_16": 2,
+ "int32": 7,
+ "vector_1_32": 45,
+ "vundef_1_32": 4,
+ "int64": 7,
+ "vector_1_64": 45,
+ "vundef_1_64": 2,
+ "vector_2_4": 4,
+ "vundef_2_4": 2,
+ "vector_2_8": 43,
+ "vundef_2_8": 2,
+ "vector_2_16": 43,
+ "vundef_2_16": 2,
+ "vector_2_32": 45,
+ "vundef_2_32": 2,
+ "vector_2_64": 43,
+ "vundef_2_64": 2,
+ "vector_3_4": 4,
+ "vundef_3_4": 2,
+ "vector_3_8": 43,
+ "vundef_3_8": 2,
+ "vector_3_16": 43,
+ "vundef_3_16": 2,
+ "vector_3_32": 43,
+ "vundef_3_32": 2,
+ "vector_3_64": 43,
+ "vundef_3_64": 2,
+ "Special": 1,
+ "case": 1,
+ "where": 1,
+ "we": 1,
+ "use": 1,
+ "rather": 1,
+ "than": 1,
+ "bitvectors": 1,
+ "size": 1,
+ "vector_1_1": 3,
+ "vundef_1_1": 2,
+ "vmake_1_1": 1,
+ "#b0": 112,
+ "#b1": 112,
+ "vector_2_1": 3,
+ "vundef_2_1": 2,
+ "vmake_2_1": 1,
+ "#b00": 111,
+ "#b01": 111,
+ "#b10": 111,
+ "#b11": 111,
+ "vector_3_1": 3,
+ "vundef_3_1": 2,
+ "vmake_3_1": 1,
+ "#b000": 110,
+ "#b001": 110,
+ "#b010": 110,
+ "#b011": 110,
+ "#b100": 110,
+ "#b101": 110,
+ "#b110": 110,
+ "#b111": 110,
+ "i.e.": 15,
+ "vmake_1_4": 2,
+ "vmake_2_4": 2,
+ "vmake_3_4": 2,
+ "vectors": 6,
+ "with": 13,
+ "vzero_1_4": 1,
+ "vzero_2_4": 1,
+ "vzero_3_4": 1,
+ "vmake_1_8": 15,
+ "vmake_2_8": 15,
+ "vmake_3_8": 15,
+ "vzero_1_8": 1,
+ "vzero_2_8": 1,
+ "vzero_3_8": 1,
+ "vmake_1_16": 15,
+ "vmake_2_16": 15,
+ "vmake_3_16": 15,
+ "vzero_1_16": 1,
+ "vzero_2_16": 1,
+ "vzero_3_16": 1,
+ "vmake_1_32": 16,
+ "vmake_2_32": 16,
+ "vmake_3_32": 15,
+ "vzero_1_32": 3,
+ "vzero_2_32": 1,
+ "vzero_3_32": 1,
+ "vmake_1_64": 16,
+ "vmake_2_64": 15,
+ "vmake_3_64": 15,
+ "vzero_1_64": 1,
+ "vzero_2_64": 1,
+ "vzero_3_64": 1,
+ "vbvadd_1_8": 1,
+ "z0": 318,
+ "z1": 318,
+ "vbvadd_1_16": 1,
+ "vbvadd_1_32": 1,
+ "vbvadd_1_64": 1,
+ "vbvsub_1_8": 1,
+ "bvsub": 63,
+ "vbvsub_1_16": 1,
+ "vbvsub_1_32": 1,
+ "vbvsub_1_64": 1,
+ "vbvmul_1_8": 1,
+ "bvmul": 56,
+ "vbvmul_1_16": 1,
+ "vbvmul_1_32": 1,
+ "vbvmul_1_64": 1,
+ "vbvshl_1_8": 1,
+ "bvshl": 56,
+ "vbvshl_1_16": 1,
+ "vbvshl_1_32": 1,
+ "vbvshl_1_64": 1,
+ "vbvsdiv_1_8": 1,
+ "bvsdiv": 56,
+ "vbvsdiv_1_16": 1,
+ "vbvsdiv_1_32": 1,
+ "vbvsdiv_1_64": 1,
+ "vbvudiv_1_8": 1,
+ "bvudiv": 56,
+ "vbvudiv_1_16": 1,
+ "vbvudiv_1_32": 1,
+ "vbvudiv_1_64": 1,
+ "vbvlshr_1_8": 1,
+ "bvlshr": 56,
+ "vbvlshr_1_16": 1,
+ "vbvlshr_1_32": 1,
+ "vbvlshr_1_64": 1,
+ "vbvashr_1_8": 1,
+ "bvashr": 56,
+ "vbvashr_1_16": 1,
+ "vbvashr_1_32": 1,
+ "vbvashr_1_64": 1,
+ "vbvurem_1_8": 1,
+ "bvurem": 56,
+ "vbvurem_1_16": 1,
+ "vbvurem_1_32": 1,
+ "vbvurem_1_64": 1,
+ "vbvsrem_1_8": 1,
+ "bvsrem": 56,
+ "vbvsrem_1_16": 1,
+ "vbvsrem_1_32": 1,
+ "vbvsrem_1_64": 1,
+ "vbvand_1_8": 1,
+ "bvand": 56,
+ "vbvand_1_16": 1,
+ "vbvand_1_32": 1,
+ "vbvand_1_64": 1,
+ "vbvor_1_8": 1,
+ "bvor": 56,
+ "vbvor_1_16": 1,
+ "vbvor_1_32": 1,
+ "vbvor_1_64": 1,
+ "vbvxor_1_8": 1,
+ "bvxor": 56,
+ "vbvxor_1_16": 1,
+ "vbvxor_1_32": 1,
+ "vbvxor_1_64": 1,
+ "vbvadd_2_8": 1,
+ "z2": 210,
+ "z3": 210,
+ "vbvadd_2_16": 1,
+ "vbvadd_2_32": 1,
+ "vbvadd_2_64": 1,
+ "vbvsub_2_8": 1,
+ "vbvsub_2_16": 1,
+ "vbvsub_2_32": 1,
+ "vbvsub_2_64": 1,
+ "vbvmul_2_8": 1,
+ "vbvmul_2_16": 1,
+ "vbvmul_2_32": 1,
+ "vbvmul_2_64": 1,
+ "vbvshl_2_8": 1,
+ "vbvshl_2_16": 1,
+ "vbvshl_2_32": 1,
+ "vbvshl_2_64": 1,
+ "vbvsdiv_2_8": 1,
+ "vbvsdiv_2_16": 1,
+ "vbvsdiv_2_32": 1,
+ "vbvsdiv_2_64": 1,
+ "vbvudiv_2_8": 1,
+ "vbvudiv_2_16": 1,
+ "vbvudiv_2_32": 1,
+ "vbvudiv_2_64": 1,
+ "vbvlshr_2_8": 1,
+ "vbvlshr_2_16": 1,
+ "vbvlshr_2_32": 1,
+ "vbvlshr_2_64": 1,
+ "vbvashr_2_8": 1,
+ "vbvashr_2_16": 1,
+ "vbvashr_2_32": 1,
+ "vbvashr_2_64": 1,
+ "vbvurem_2_8": 1,
+ "vbvurem_2_16": 1,
+ "vbvurem_2_32": 1,
+ "vbvurem_2_64": 1,
+ "vbvsrem_2_8": 1,
+ "vbvsrem_2_16": 1,
+ "vbvsrem_2_32": 1,
+ "vbvsrem_2_64": 1,
+ "vbvand_2_8": 1,
+ "vbvand_2_16": 1,
+ "vbvand_2_32": 1,
+ "vbvand_2_64": 1,
+ "vbvor_2_8": 1,
+ "vbvor_2_16": 1,
+ "vbvor_2_32": 1,
+ "vbvor_2_64": 1,
+ "vbvxor_2_8": 1,
+ "vbvxor_2_16": 1,
+ "vbvxor_2_32": 1,
+ "vbvxor_2_64": 1,
+ "vbvadd_3_8": 1,
+ "z4": 104,
+ "z5": 104,
+ "z6": 104,
+ "z7": 104,
+ "vbvadd_3_16": 1,
+ "vbvadd_3_32": 1,
+ "vbvadd_3_64": 1,
+ "vbvsub_3_8": 1,
+ "vbvsub_3_16": 1,
+ "vbvsub_3_32": 1,
+ "vbvsub_3_64": 1,
+ "vbvmul_3_8": 1,
+ "vbvmul_3_16": 1,
+ "vbvmul_3_32": 1,
+ "vbvmul_3_64": 1,
+ "vbvshl_3_8": 1,
+ "vbvshl_3_16": 1,
+ "vbvshl_3_32": 1,
+ "vbvshl_3_64": 1,
+ "vbvsdiv_3_8": 1,
+ "vbvsdiv_3_16": 1,
+ "vbvsdiv_3_32": 1,
+ "vbvsdiv_3_64": 1,
+ "vbvudiv_3_8": 1,
+ "vbvudiv_3_16": 1,
+ "vbvudiv_3_32": 1,
+ "vbvudiv_3_64": 1,
+ "vbvlshr_3_8": 1,
+ "vbvlshr_3_16": 1,
+ "vbvlshr_3_32": 1,
+ "vbvlshr_3_64": 1,
+ "vbvashr_3_8": 1,
+ "vbvashr_3_16": 1,
+ "vbvashr_3_32": 1,
+ "vbvashr_3_64": 1,
+ "vbvurem_3_8": 1,
+ "vbvurem_3_16": 1,
+ "vbvurem_3_32": 1,
+ "vbvurem_3_64": 1,
+ "vbvsrem_3_8": 1,
+ "vbvsrem_3_16": 1,
+ "vbvsrem_3_32": 1,
+ "vbvsrem_3_64": 1,
+ "vbvand_3_8": 1,
+ "vbvand_3_16": 1,
+ "vbvand_3_32": 1,
+ "vbvand_3_64": 1,
+ "vbvor_3_8": 1,
+ "vbvor_3_16": 1,
+ "vbvor_3_32": 1,
+ "vbvor_3_64": 1,
+ "vbvxor_3_8": 1,
+ "vbvxor_3_16": 1,
+ "vbvxor_3_32": 1,
+ "vbvxor_3_64": 1,
+ "conversion": 3,
+ "from": 3,
+ "Bitvector": 3,
+ "this": 2,
+ "assumes": 2,
+ "representation": 2,
+ "cast_vector_1_32_to_bits": 1,
+ "cast_bits_to_vector_1_32": 1,
+ "w": 11,
+ "cast_vector_2_32_to_bits": 1,
+ "cast_bits_to_vector_2_32": 1,
+ "i64": 3,
+ "cast_vector_1_64_to_bits": 1,
+ "cast_bits_to_vector_1_64": 1,
+ "end": 1,
+ "prelude": 1,
+ "@.str": 3,
+ "[": 4,
+ "i8": 4,
+ "]": 4,
+ "c": 2,
+ "@.str1": 3,
+ "@lhs": 21,
+ "@rhs": 15,
+ "@main": 71,
+ "@atoi": 4,
+ "@printf": 4,
+ "Function": 5,
+ "i32": 63,
+ "%": 221,
+ "b": 18,
+ "memory1": 1,
+ "rsp1": 1,
+ "BLOCK": 8,
+ "index": 8,
+ "rank": 8,
+ "Predecessors": 8,
+ "@lhs_block_0_entry_condition": 2,
+ "insertelement": 4,
+ "<2>": 12,
+ "undef": 4,
+ "shufflevector": 2,
+ "<i32>": 2,
+ "1": 2,
+ "0": 2,
+ "extractelement": 2,
+ "ret": 3,
+ "No": 8,
+ "backward": 8,
+ "arrows": 8,
+ "@lhs_result": 2,
+ "memory2": 1,
+ "rsp2": 1,
+ "@rhs_block_0_entry_condition": 2,
+ "@rhs_result": 2,
+ "argc": 4,
+ "i8**": 7,
+ "argv": 4,
+ "memory3": 2,
+ "rsp3": 2,
+ "@main_block_0_entry_condition": 4,
+ "alloca": 7,
+ "align": 27,
+ "rsp4": 3,
+ "rsp5": 3,
+ "rsp6": 3,
+ "rsp7": 3,
+ "rsp8": 3,
+ "lhs": 10,
+ "rsp9": 3,
+ "rhs": 8,
+ "rsp10": 2,
+ "i32*": 16,
+ "memory4": 2,
+ "memory5": 2,
+ "i8***": 3,
+ "memory6": 4,
+ "load": 14,
+ "icmp": 2,
+ "eq": 2,
+ "br": 5,
+ "i1": 2,
+ "label": 7,
+ "@main_block_1_entry_condition": 4,
+ "Memory": 5,
+ "PHI": 5,
+ "memory7": 4,
+ "getelementptr": 4,
+ "inbounds": 4,
+ "call": 6,
+ "i8*": 8,
+ "memory8": 4,
+ "bv16": 1,
+ "memory9": 4,
+ "memory10": 4,
+ "memory11": 5,
+ "@main_block_2_entry_condition": 3,
+ "memory12": 3,
+ "...": 3,
+ "*": 4,
+ "@main_block_3_entry_condition": 4,
+ "memory13": 4,
+ "@main_block_4_entry_condition": 4,
+ "memory14": 2,
+ "@main_block_5_entry_condition": 2,
+ "memory15": 1,
+ "@main_result": 1
+ },
"SPARQL": {
"PREFIX": 4,
"foaf": 4,
"<http://xmlns.com/foaf/0.1/>": 1,
"SELECT": 3,
@@ -105071,10 +106120,11 @@
"Idris": 148,
"Inform 7": 75,
"Inno Setup": 478,
"Ioke": 2,
"Isabelle": 136,
+ "Isabelle ROOT": 1046,
"J": 104,
"JFlex": 1780,
"JSON": 183,
"JSON5": 57,
"JSONLD": 18,
@@ -105149,20 +106199,20 @@
"Org": 358,
"Ox": 1006,
"Oxygene": 157,
"Oz": 116,
"PAWN": 3261,
- "PHP": 20771,
+ "PHP": 20777,
"PLSQL": 828,
"PLpgSQL": 2512,
"Pan": 130,
"Papyrus": 560,
"Parrot Assembly": 6,
"Parrot Internal Representation": 5,
"Pascal": 955,
- "Perl": 21047,
- "Perl6": 12283,
+ "Perl": 21051,
+ "Perl6": 12184,
"PicoLisp": 589,
"PigLatin": 30,
"Pike": 1848,
"Pod": 658,
"PogoScript": 250,
@@ -105191,10 +106241,11 @@
"RobotFramework": 483,
"Ruby": 4610,
"Rust": 3566,
"SAS": 1777,
"SCSS": 39,
+ "SMT": 25205,
"SPARQL": 253,
"SQF": 196,
"SQL": 1530,
"SQLPL": 503,
"STON": 100,
@@ -105362,10 +106413,11 @@
"Idris": 1,
"Inform 7": 2,
"Inno Setup": 1,
"Ioke": 1,
"Isabelle": 1,
+ "Isabelle ROOT": 1,
"J": 1,
"JFlex": 2,
"JSON": 4,
"JSON5": 2,
"JSONLD": 1,
@@ -105440,11 +106492,11 @@
"Org": 1,
"Ox": 3,
"Oxygene": 1,
"Oz": 1,
"PAWN": 1,
- "PHP": 12,
+ "PHP": 13,
"PLSQL": 5,
"PLpgSQL": 5,
"Pan": 1,
"Papyrus": 3,
"Parrot Assembly": 1,
@@ -105482,10 +106534,11 @@
"RobotFramework": 3,
"Ruby": 27,
"Rust": 1,
"SAS": 3,
"SCSS": 1,
+ "SMT": 4,
"SPARQL": 2,
"SQF": 2,
"SQL": 10,
"SQLPL": 6,
"STON": 7,
@@ -105545,7 +106598,7 @@
"eC": 1,
"edn": 1,
"fish": 3,
"wisp": 1
},
- "md5": "c4d168927a1c67e75a3352fa4b169ecd"
+ "md5": "a04f5b0f937c6a5a9675da45afc03016"
}
\ No newline at end of file