mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 01:27:41 +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-26 14:18:26 -08:00
commit 4f7dd08c38
88 changed files with 1503 additions and 1201 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/muz_qe/dl_context.cpp
View file

@ -338,7 +338,7 @@ namespace datalog {
expr_ref context::bind_variables(expr* fml, bool is_forall) {
expr_ref result(m);
app_ref_vector & vars = m_vars;
app_ref_vector const & vars = m_vars;
if (vars.empty()) {
result = fml;
}
@ -352,13 +352,20 @@ namespace datalog {
else {
svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) {
if (vars.size() == i) {
vars.push_back(m.mk_fresh_const("x", m.mk_bool_sort()));
}
if (!sorts[i]) {
sorts[i] = vars[i]->get_decl()->get_range();
if (i < vars.size()) {
sorts[i] = vars[i]->get_decl()->get_range();
}
else {
sorts[i] = m.mk_bool_sort();
}
}
if (i < vars.size()) {
names.push_back(vars[i]->get_decl()->get_name());
}
else {
names.push_back(symbol(i));
}
names.push_back(vars[i]->get_decl()->get_name());
}
quantifier_ref q(m);
sorts.reverse();
@ -987,6 +994,7 @@ namespace datalog {
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
@ -1643,6 +1651,9 @@ namespace datalog {
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
bool print_low_level = m_params.get_bool(":print-low-level-smt2", true);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
get_rules_as_formulas(rules, names);
@ -1677,18 +1688,18 @@ namespace datalog {
obj_hashtable<sort>& sorts = visitor.sorts();
obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
for (; sit != send; ++sit) {
ast_smt2_pp(out, *sit, env, params);
PP(*sit);
}
for (; it != end; ++it) {
func_decl* f = *it;
ast_smt2_pp(out, f, env, params);
PP(f);
out << "\n";
}
it = rels.begin(); end = rels.end();
for (; it != end; ++it) {
func_decl* f = *it;
out << "(declare-rel " << f->get_name() << " (";
for (unsigned i = 0; i < f->get_arity(); ++i) {
for (unsigned i = 0; i < f->get_arity(); ++i) {
ast_smt2_pp(out, f->get_domain(i), env, params);
if (i + 1 < f->get_arity()) {
out << " ";
@ -1707,7 +1718,7 @@ namespace datalog {
for (unsigned i = 0; i < num_axioms; ++i) {
out << "(assert ";
ast_smt2_pp(out, axioms[i], env, params);
PP(axioms[i]);
out << ")\n";
}
for (unsigned i = 0; i < rules.size(); ++i) {
@ -1717,12 +1728,7 @@ namespace datalog {
if (symbol::null != nm) {
out << "(! ";
}
if (use_fixedpoint_extensions) {
ast_smt2_pp(out, r, env, params);
}
else {
out << mk_smt_pp(r, m);
}
PP(r);
if (symbol::null != nm) {
while (fresh_names.contains(nm)) {
std::ostringstream s;
@ -1737,7 +1743,7 @@ namespace datalog {
if (use_fixedpoint_extensions) {
for (unsigned i = 0; i < num_queries; ++i) {
out << "(query ";
ast_smt2_pp(out, queries[i], env, params);
PP(queries[i]);
out << ")\n";
}
}
@ -1747,7 +1753,7 @@ namespace datalog {
out << "(assert ";
expr_ref q(m);
q = m.mk_not(queries[i]);
ast_smt2_pp(out, q, env, params);
PP(q);
out << ")\n";
out << "(check-sat)\n";
if (num_queries > 1) out << "(pop)\n";

2
src/muz_qe/pdr_util.cpp
View file

@ -119,7 +119,6 @@ namespace pdr {
select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {}
};
template class rewriter_tpl<select_elim_cfg>;
class select_elim_star : public rewriter_tpl<select_elim_cfg> {
select_elim_cfg m_cfg;
@ -1206,5 +1205,6 @@ namespace pdr {
template class rewriter_tpl<pdr::ite_hoister_cfg>;
template class rewriter_tpl<pdr::select_elim_cfg>;