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

fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-15 21:17:00 -08:00
parent f47671931f
commit c3f67f3b5f
4 changed files with 24 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -4373,7 +4373,7 @@ namespace smt {
void context::add_rec_funs_to_model() { void context::add_rec_funs_to_model() {
ast_manager& m = m_manager; ast_manager& m = m_manager;
SASSERT(m_model); SASSERT(m_model);
for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) { for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
expr* e = m_asserted_formulas.get_formula(i); expr* e = m_asserted_formulas.get_formula(i);
if (is_quantifier(e)) { if (is_quantifier(e)) {
TRACE("context", tout << mk_pp(e, m) << "\n";); TRACE("context", tout << mk_pp(e, m) << "\n";);

5
src/smt/smt_context.h
View file

@ -209,7 +209,12 @@ namespace smt {
~scoped_mk_model() { ~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) { if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model(); m_ctx.m_model = m_ctx.m_proto_model->mk_model();
try {
m_ctx.add_rec_funs_to_model(); m_ctx.add_rec_funs_to_model();
}
catch (...) {
// no op
}
m_ctx.m_proto_model = 0; // proto_model is not needed anymore. m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
} }
} }

19
src/smt/theory_str.cpp
View file

@ -47,6 +47,8 @@ namespace smt {
sLevel(0), sLevel(0),
finalCheckProgressIndicator(false), finalCheckProgressIndicator(false),
m_trail(m), m_trail(m),
m_factory(nullptr),
m_unused_id(0),
m_delayed_axiom_setup_terms(m), m_delayed_axiom_setup_terms(m),
tmpStringVarCount(0), tmpStringVarCount(0),
tmpXorVarCount(0), tmpXorVarCount(0),
@ -4648,14 +4650,17 @@ namespace smt {
// We only check m_find for a string constant. // We only check m_find for a string constant.
expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) { expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
expr * curr = n; theory_var curr = m_find.find(get_var(n));
theory_var first = curr;
do { do {
if (u.str.is_string(curr)) { expr* a = get_ast(curr);
if (u.str.is_string(a)) {
hasEqcValue = true; hasEqcValue = true;
return curr; return a;
} }
curr = get_eqc_next(curr); curr = m_find.next(curr);
} while (curr != n); }
while (curr != first && curr != null_theory_var);
hasEqcValue = false; hasEqcValue = false;
return n; return n;
} }
@ -10584,7 +10589,9 @@ namespace smt {
return alloc(expr_wrapper_proc, val); return alloc(expr_wrapper_proc, val);
} else { } else {
TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**"))); std::ostringstream unused;
unused << "**UNUSED**" << (m_unused_id++);
return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
} }
} }

4
src/smt/theory_str.h
View file

@ -267,6 +267,10 @@ protected:
str_value_factory * m_factory; str_value_factory * m_factory;
// Unique identifier appended to unused variables to ensure that model construction
// does not introduce equalities when they weren't enforced.
unsigned m_unused_id;
// terms we couldn't go through set_up_axioms() with because they weren't internalized // terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms; expr_ref_vector m_delayed_axiom_setup_terms;