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

api for accessing dl_rule name

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-20 22:08:52 -04:00
parent 7840f6cead
commit 50f794c4f5
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/muz/base/dl_rule.h
View file

@ -298,7 +298,7 @@ namespace datalog {
static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }
rule() : m_ref_cnt(0) {} rule() : m_ref_cnt(0), m_name(symbol::null) {}
~rule() {} ~rule() {}
void deallocate(ast_manager & m); void deallocate(ast_manager & m);
@ -355,7 +355,12 @@ namespace datalog {
void display(context & ctx, std::ostream & out) const; void display(context & ctx, std::ostream & out) const;
symbol const& name() const { return m_name; } /**
\brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.
This possibly returns a ";"-separated list of names.
*/
symbol const& name() const { return m_name; } ;
unsigned hash() const; unsigned hash() const;