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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-01 08:07:14 -07:00
commit add8d26807
3 changed files with 23 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/qe/qe_lite.cpp
View file

@ -89,7 +89,7 @@ namespace eq {
var * v = vars[i]; var * v = vars[i];
expr * t = definitions[i]; expr * t = definitions[i];
if (t == nullptr || has_quantifiers(t) || occurs_var(v->get_idx(), t)) if (t == nullptr || has_quantifiers(t) || occurs_var(v->get_idx(), t))
definitions[i] = 0; definitions[i] = nullptr;
else else
found = true; // found at least one candidate found = true; // found at least one candidate
} }
@ -106,7 +106,7 @@ namespace eq {
unsigned vidx, num; unsigned vidx, num;
for (unsigned i = 0; i < definitions.size(); i++) { for (unsigned i = 0; i < definitions.size(); i++) {
if (definitions[i] == 0) if (definitions[i] == nullptr)
continue; continue;
var * v = vars[i]; var * v = vars[i];
SASSERT(v->get_idx() == i); SASSERT(v->get_idx() == i);
@ -116,7 +116,7 @@ namespace eq {
start: start:
frame & fr = todo.back(); frame & fr = todo.back();
expr * t = fr.first; expr * t = fr.first;
if (t->get_ref_count() > 1 && done.is_marked(t)) { if (done.is_marked(t)) {
todo.pop_back(); todo.pop_back();
continue; continue;
} }
@ -126,11 +126,11 @@ namespace eq {
if (fr.second == 0) { if (fr.second == 0) {
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula. // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
if (definitions.get(vidx, 0) != 0) { if (definitions.get(vidx, nullptr) != nullptr) {
if (visiting.is_marked(t)) { if (visiting.is_marked(t)) {
// cycle detected: remove t // cycle detected: remove t
visiting.reset_mark(t); visiting.reset_mark(t);
definitions[vidx] = 0; definitions[vidx] = nullptr;
} }
else { else {
visiting.mark(t); visiting.mark(t);
@ -142,17 +142,14 @@ namespace eq {
} }
else { else {
SASSERT(fr.second == 1); SASSERT(fr.second == 1);
if (definitions.get(vidx, 0) != 0) { visiting.reset_mark(t);
visiting.reset_mark(t); if (!done.is_marked(t)) {
order.push_back(vidx); if (definitions.get(vidx, nullptr) != nullptr)
} order.push_back(vidx);
else { done.mark(t);
// var was removed from the list of candidate vars to elim cycle
// do nothing
} }
} }
if (t->get_ref_count() > 1) done.mark(t);
done.mark(t);
todo.pop_back(); todo.pop_back();
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
@ -164,13 +161,11 @@ namespace eq {
while (fr.second < num) { while (fr.second < num) {
expr * arg = to_app(t)->get_arg(fr.second); expr * arg = to_app(t)->get_arg(fr.second);
fr.second++; fr.second++;
if (arg->get_ref_count() > 1 && done.is_marked(arg)) if (done.is_marked(arg)) continue;
continue;
todo.push_back(frame(arg, 0)); todo.push_back(frame(arg, 0));
goto start; goto start;
} }
if (t->get_ref_count() > 1) done.mark(t);
done.mark(t);
todo.pop_back(); todo.pop_back();
break; break;
default: default:
@ -574,12 +569,15 @@ namespace eq {
checkpoint(); checkpoint();
ptr_vector<var> vs; ptr_vector<var> vs;
expr_ref_vector ts(m); expr_ref_vector ts(m);
expr_ref t(m);
if (is_var_def(is_exists, args[i], vs, ts)) { if (is_var_def(is_exists, args[i], vs, ts)) {
for (unsigned j = 0; j < vs.size(); ++j) { for (unsigned j = 0; j < vs.size(); ++j) {
var* v = vs[j]; var* v = vs[j];
expr* t = ts[j].get(); t = ts.get(j);
m_rewriter(t);
if (t != ts.get(j)) m_new_exprs.push_back(t);
unsigned idx = v->get_idx(); unsigned idx = v->get_idx();
if (m_map.get(idx, 0) == 0) { if (m_map.get(idx, nullptr) == nullptr) {
m_map.reserve(idx + 1, 0); m_map.reserve(idx + 1, 0);
m_inx2var.reserve(idx + 1, 0); m_inx2var.reserve(idx + 1, 0);
m_map[idx] = t; m_map[idx] = t;
@ -2461,9 +2459,7 @@ public:
fmls[index] = fml; fmls[index] = fml;
return; return;
} }
TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) { TRACE("qe_lite", tout << fmls << "\n";);
tout << mk_pp(fmls[i].get(), m) << "\n";
});
is_variable_test is_var(index_set, index_of_bound); is_variable_test is_var(index_set, index_of_bound);
m_der.set_is_variable_proc(is_var); m_der.set_is_variable_proc(is_var);
m_fm.set_is_variable_proc(is_var); m_fm.set_is_variable_proc(is_var);

1
src/qe/qe_lite.h
View file

@ -57,7 +57,6 @@ public:
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml); void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs); void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
/** /**
\brief full rewriting based light-weight quantifier elimination round. \brief full rewriting based light-weight quantifier elimination round.
*/ */

6
src/smt/theory_str.cpp
View file

@ -6645,7 +6645,8 @@ namespace smt {
expr * sub1; expr * sub1;
expr * sub2; expr * sub2;
if (u.re.is_to_re(re, sub1)) { if (u.re.is_to_re(re, sub1)) {
SASSERT(u.str.is_string(sub1)); if (!u.str.is_string(sub1))
throw default_exception("regular expressions must be built from string literals");
zstring str; zstring str;
u.str.is_string(sub1, str); u.str.is_string(sub1, str);
return str.length(); return str.length();
@ -6842,7 +6843,8 @@ namespace smt {
expr * sub1; expr * sub1;
expr * sub2; expr * sub2;
if (u.re.is_to_re(re, sub1)) { if (u.re.is_to_re(re, sub1)) {
SASSERT(u.str.is_string(sub1)); if (!u.str.is_string(sub1))
throw default_exception("regular expressions must be built from string literals");
zstring str; zstring str;
u.str.is_string(sub1, str); u.str.is_string(sub1, str);
rational strlen(str.length()); rational strlen(str.length());