mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

updated doc generation script

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-30 22:52:32 -08:00
parent 6022c17131
commit 5794d080b5
1 changed files with 32 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
doc/mk_tactic_doc.py
View file

@ -18,6 +18,7 @@ def doc_path(path):
is_doc = re.compile("Tactic Documentation") is_doc = re.compile("Tactic Documentation")
is_doc_end = re.compile("\-\-\*\/") is_doc_end = re.compile("\-\-\*\/")
is_tac_name = re.compile("## Tactic (.*)") is_tac_name = re.compile("## Tactic (.*)")
is_simplifier = re.compile("ADD_SIMPLIFIER\(.*\"([^\"]*)\".*,.*\"([^\"]*)\".*,.*\"([^\"]*)\"\.*\)")
def is_ws(s): def is_ws(s):
return all([0 for ch in s if ch != ' ' and ch != '\n']) return all([0 for ch in s if ch != ' ' and ch != '\n'])
@ -53,6 +54,19 @@ def extract_tactic_doc(ous, f):
if is_doc.search(line): if is_doc.search(line):
generate_tactic_doc(ous, f, ins) generate_tactic_doc(ous, f, ins)
def generate_simplifier_doc(ous, name, desc):
ous.write("## Simplifier [" + name + "](tactic-summary/#" + name + ")\n")
ous.write("### Description\n" + desc + "\n")
def extract_simplifier_doc(ous, f):
with open(f) as ins:
for line in ins:
m = is_simplifier.search(line)
if m:
generate_simplifier_doc(ous, m.group(1), m.group(2))
return
def find_tactic_name(path): def find_tactic_name(path):
with open(path) as ins: with open(path) as ins:
for line in ins: for line in ins:
@ -66,13 +80,15 @@ def presort_files():
tac_files = [] tac_files = []
for root, dirs, files in os.walk(doc_path("../src")): for root, dirs, files in os.walk(doc_path("../src")):
for f in files: for f in files:
if f.endswith("tactic.h"): if f.endswith("~"):
continue
if f.endswith("tactic.h") or "simplifiers" in root:
tac_files += [(f, os.path.join(root, f))] tac_files += [(f, os.path.join(root, f))]
tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1])) tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1]))
return tac_files return tac_files
def help(ous): def help(ous):
presort_files()
ous.write("---\n") ous.write("---\n")
ous.write("title: Tactics Summary\n") ous.write("title: Tactics Summary\n")
ous.write("sidebar_position: 5\n") ous.write("sidebar_position: 5\n")
@ -81,6 +97,17 @@ def help(ous):
for file, path in tac_files: for file, path in tac_files:
extract_tactic_doc(ous, path) extract_tactic_doc(ous, path)
def help_simplifier(ous):
ous.write("---\n")
ous.write("title: Simplifier Summary\n")
ous.write("sidebar_position: 6\n")
ous.write("---\n")
tac_files = presort_files()
for file, path in tac_files:
extract_simplifier_doc(ous, path)
def mk_dir(d): def mk_dir(d):
if not os.path.exists(d): if not os.path.exists(d):
os.makedirs(d) os.makedirs(d)
@ -89,3 +116,6 @@ mk_dir(os.path.join(OUTPUT_DIRECTORY, 'md'))
with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous: with open(OUTPUT_DIRECTORY + "/md/tactics-summary.md",'w') as ous:
help(ous) help(ous)
with open(OUTPUT_DIRECTORY + "/md/simplifier-summary.md",'w') as ous:
help_simplifier(ous)