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

pretty print rules with quoted symbols

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-29 19:17:01 -08:00
parent 646ace6842
commit 654c02701c
2 changed files with 30 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/muz_qe/dl_context.cpp
View file

@ -1626,6 +1626,23 @@ namespace datalog {
void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
expr_ref fml(m);
datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rule_refs(rm);
// ensure that rules are all using bound variables.
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
ptr_vector<sort> sorts;
get_free_vars(m_rule_fmls[i].get(), sorts);
if (!sorts.empty()) {
rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]);
m_rule_fmls[i] = m_rule_fmls.back();
m_rule_names[i] = m_rule_names.back();
m_rule_fmls.pop_back();
m_rule_names.pop_back();
--i;
}
}
add_rules(rule_refs);
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
@ -1732,13 +1749,20 @@ namespace datalog {
}
PP(r);
if (symbol::null != nm) {
out << " :named ";
while (fresh_names.contains(nm)) {
std::ostringstream s;
s << nm << "!";
nm = symbol(s.str().c_str());
}
fresh_names.add(nm);
out << " :named " << nm << ")";
if (is_smt2_quoted_symbol(nm)) {
out << mk_smt2_quoted_symbol(nm);
}
else {
out << nm;
}
out << ")";
}
out << ")\n";
}

5
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -461,6 +461,11 @@ namespace datalog {
{
rule_ref r(r0, m_context.get_rule_manager());
if (r->has_quantifiers()) {
res = r;
return false;
}
start:
unsigned u_len = r->get_uninterpreted_tail_size();
unsigned len = r->get_tail_size();