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

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2012-11-26 21:03:47 +00:00
commit d1342ba7a9
2 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

15
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 context::bind_variables(expr* fml, bool is_forall) {
expr_ref result(m); expr_ref result(m);
app_ref_vector & vars = m_vars; app_ref_vector const & vars = m_vars;
if (vars.empty()) { if (vars.empty()) {
result = fml; result = fml;
} }
@ -352,14 +352,21 @@ namespace datalog {
else { else {
svector<symbol> names; svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) { 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]) { if (!sorts[i]) {
if (i < vars.size()) {
sorts[i] = vars[i]->get_decl()->get_range(); 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()); names.push_back(vars[i]->get_decl()->get_name());
} }
else {
names.push_back(symbol(i));
}
}
quantifier_ref q(m); quantifier_ref q(m);
sorts.reverse(); sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);

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) {} 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> { class select_elim_star : public rewriter_tpl<select_elim_cfg> {
select_elim_cfg m_cfg; select_elim_cfg m_cfg;
@ -1205,5 +1204,6 @@ namespace pdr {
template class rewriter_tpl<pdr::ite_hoister_cfg>; template class rewriter_tpl<pdr::ite_hoister_cfg>;
template class rewriter_tpl<pdr::select_elim_cfg>;