diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/kind_template.cpp | 10 | ||||
-rw-r--r-- | src/expr/kind_template.h | 1 | ||||
-rwxr-xr-x | src/expr/mkkind | 5 |
3 files changed, 16 insertions, 0 deletions
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index 5f92af622..aa9107a18 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -91,5 +91,15 @@ ${type_constant_to_theory_id} throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant"); } +std::string getStatsPrefix(TheoryId theoryId) { + switch(theoryId) { +${theory_stats_prefixes} +#line 98 "${template}" + default: + break; + } + return "unknown"; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 9247f50dd..6ebbb32c2 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -99,6 +99,7 @@ CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) { std::ostream& operator<<(std::ostream& out, TheoryId theoryId); TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; +std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/expr/mkkind b/src/expr/mkkind index 2b1901f5d..5e5be7c45 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -75,6 +75,7 @@ seen_theory_builtin=false theory_enum= theory_descriptions= +theory_stats_prefixes= function theory { # theory ID T header @@ -109,6 +110,9 @@ function theory { " theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " + prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]') + theory_stats_prefixes="${theory_stats_prefixes} case ${theory_id}: return \"theory::${prefix#theory_}\"; break; +" } function alternate { @@ -416,6 +420,7 @@ for var in \ type_constant_groundterms \ type_properties_includes \ theory_descriptions \ + theory_stats_prefixes \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" |