mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix build problem, redo naming abstraction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-26 08:26:51 -08:00
parent 682a725e13
commit f7825755db
2 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

19
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();