From a9f52b0069bf31d316f3485731b13897551aee43 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 Dec 2022 10:04:01 -0800
Subject: [PATCH] doc fixes
---
doc/mk_tactic_doc.py | 17 +++++++++++++----
src/ast/simplifiers/card2bv.cpp | 2 +-
src/tactic/arith/card2bv_tactic.h | 2 +-
3 files changed, 15 insertions(+), 6 deletions(-)
diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index 37b77ef52..e4c71341a 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -53,15 +53,24 @@ def extract_tactic_doc(ous, f):
if is_doc.search(line):
generate_tactic_doc(ous, f, ins)
+def presort_files():
+ tac_files = []
+ for root, dirs, files in os.walk(doc_path("../src")):
+ for f in files:
+ if f.endswith("tactic.h"):
+ tac_files += [(f, os.path.join(root, f))]
+ tac_files = sorted(tac_files, key = lambda x: x[0])
+ return tac_files
+
def help(ous):
+ presort_files()
ous.write("---\n")
ous.write("title: Tactics Summary\n")
ous.write("sidebar_position: 5\n")
ous.write("---\n")
- for root, dirs, files in os.walk(doc_path("../src")):
- for f in files:
- if f.endswith("tactic.h"):
- extract_tactic_doc(ous, os.path.join(root, f))
+ tac_files = presort_files()
+ for file, path in tac_files:
+ extract_tactic_doc(ous, path)
def mk_dir(d):
if not os.path.exists(d):
diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp
index b2fece21e..d2d482aa3 100644
--- a/src/ast/simplifiers/card2bv.cpp
+++ b/src/ast/simplifiers/card2bv.cpp
@@ -55,7 +55,7 @@ void card2bv::collect_statistics(statistics& st) const {
}
void card2bv::collect_param_descrs(param_descrs& r) {
- r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver");
+ r.insert("keep_cardinality_constraints", CPK_BOOL, "retain cardinality constraints for solver", "true");
pb2bv_rewriter rw(m, m_params);
rw.collect_param_descrs(r);
}
diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h
index d28326514..f3cd4e2c8 100644
--- a/src/tactic/arith/card2bv_tactic.h
+++ b/src/tactic/arith/card2bv_tactic.h
@@ -11,7 +11,7 @@ Author:
Tactic Documentation:
-## Tactic car2bv
+## Tactic card2bv
### Short Description