From f98e107d0e3b8a73d258aa723f2586af98de6efc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2012 20:11:48 -0800 Subject: [PATCH] insert fresh name Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 3 ++- src/muz_qe/model2expr.h | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 87a386251..13008d059 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1697,8 +1697,9 @@ namespace datalog { while (fresh_names.contains(nm)) { std::ostringstream s; s << nm << "!"; - nm = symbol(s.str().c_str()); + nm = symbol(s.str().c_str()); } + fresh_names.add(nm); out << " :named " << nm << ")"; } out << ")\n"; diff --git a/src/muz_qe/model2expr.h b/src/muz_qe/model2expr.h index 2c1ed8d15..3fd2e4524 100644 --- a/src/muz_qe/model2expr.h +++ b/src/muz_qe/model2expr.h @@ -35,6 +35,7 @@ class mk_fresh_name { public: mk_fresh_name(): m_char('A'), m_num(0) {} void add(ast* a); + void add(symbol const& s) { m_symbols.insert(s); } symbol next(); bool contains(symbol const& s) const { return m_symbols.contains(s); } };