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

use different symbols for named rules

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-18 19:00:01 -08:00
parent 9c304d7642
commit f014ab9598
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz_qe/dl_context.cpp
View file

@ -1683,7 +1683,8 @@ namespace datalog {
for (unsigned i = 0; i < rules.size(); ++i) { for (unsigned i = 0; i < rules.size(); ++i) {
out << (use_fixedpoint_extensions?"(rule ":"(assert "); out << (use_fixedpoint_extensions?"(rule ":"(assert ");
expr* r = rules[i].get(); expr* r = rules[i].get();
if (symbol::null != names[i]) { symbol nm = names[i];
if (symbol::null != nm) {
out << "(! "; out << "(! ";
} }
if (use_fixedpoint_extensions) { if (use_fixedpoint_extensions) {
@ -1692,8 +1693,13 @@ namespace datalog {
else { else {
out << mk_smt_pp(r, m); out << mk_smt_pp(r, m);
} }
if (symbol::null != names[i]) { if (symbol::null != nm) {
out << " :named " << names[i] << ")"; while (fresh_names.contains(nm)) {
std::ostringstream s;
s << nm << "!";
nm = symbol(s.str().c_str());
}
out << " :named " << nm << ")";
} }
out << ")\n"; out << ")\n";
} }

1
src/muz_qe/model2expr.h
View file

@ -36,6 +36,7 @@ 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);
symbol next(); symbol next();
bool contains(symbol const& s) const { return m_symbols.contains(s); }
}; };