mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-11-19 05:21:15 -08:00
commit b30fc79bf1
2 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/dl_context.cpp
View file

@ -1697,8 +1697,9 @@ namespace datalog {
while (fresh_names.contains(nm)) { while (fresh_names.contains(nm)) {
std::ostringstream s; std::ostringstream s;
s << nm << "!"; s << nm << "!";
nm = symbol(s.str().c_str()); nm = symbol(s.str().c_str());
} }
fresh_names.add(nm);
out << " :named " << nm << ")"; out << " :named " << nm << ")";
} }
out << ")\n"; out << ")\n";

1
src/muz_qe/model2expr.h
View file

@ -35,6 +35,7 @@ class mk_fresh_name {
public: public:
mk_fresh_name(): m_char('A'), m_num(0) {} mk_fresh_name(): m_char('A'), m_num(0) {}
void add(ast* a); void add(ast* a);
void add(symbol const& s) { m_symbols.insert(s); }
symbol next(); symbol next();
bool contains(symbol const& s) const { return m_symbols.contains(s); } bool contains(symbol const& s) const { return m_symbols.contains(s); }
}; };