From f014ab959856d947a658f49a6177b184b6f84d84 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2012 19:00:01 -0800 Subject: [PATCH] use different symbols for named rules Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 12 +++++++++--- src/muz_qe/model2expr.h | 1 + 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index ecd9ee5cb..87a386251 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1683,7 +1683,8 @@ namespace datalog { for (unsigned i = 0; i < rules.size(); ++i) { out << (use_fixedpoint_extensions?"(rule ":"(assert "); expr* r = rules[i].get(); - if (symbol::null != names[i]) { + symbol nm = names[i]; + if (symbol::null != nm) { out << "(! "; } if (use_fixedpoint_extensions) { @@ -1692,8 +1693,13 @@ namespace datalog { else { out << mk_smt_pp(r, m); } - if (symbol::null != names[i]) { - out << " :named " << names[i] << ")"; + if (symbol::null != nm) { + while (fresh_names.contains(nm)) { + std::ostringstream s; + s << nm << "!"; + nm = symbol(s.str().c_str()); + } + out << " :named " << nm << ")"; } out << ")\n"; } diff --git a/src/muz_qe/model2expr.h b/src/muz_qe/model2expr.h index 9a63d6b8c..2c1ed8d15 100644 --- a/src/muz_qe/model2expr.h +++ b/src/muz_qe/model2expr.h @@ -36,6 +36,7 @@ public: mk_fresh_name(): m_char('A'), m_num(0) {} void add(ast* a); symbol next(); + bool contains(symbol const& s) const { return m_symbols.contains(s); } };