mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
512aa0e8d3
commit
b352d43e50
|
@ -1048,6 +1048,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
|
|||
return s2;
|
||||
}
|
||||
std::ostringstream buffer;
|
||||
SASSERT(false);
|
||||
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
|
||||
throw ast_exception(buffer.str().c_str());
|
||||
}
|
||||
|
|
|
@ -584,6 +584,9 @@ bool theory_seq::check_extensionality() {
|
|||
for (unsigned i = 0; i < seqs.size(); ++i) {
|
||||
enode* n2 = get_enode(seqs[i]);
|
||||
expr* o2 = n2->get_owner();
|
||||
if (m.get_sort(o1) != m.get_sort(o2)) {
|
||||
continue;
|
||||
}
|
||||
if (m_exclude.contains(o1, o2)) {
|
||||
continue;
|
||||
}
|
||||
|
@ -720,6 +723,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
|
|||
context& ctx = get_context();
|
||||
expr_ref_vector lhs(m), rhs(m);
|
||||
bool changed = false;
|
||||
TRACE("seq", tout << ls << " = " << rs << "\n";);
|
||||
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
|
||||
// equality is inconsistent.
|
||||
TRACE("seq", tout << ls << " != " << rs << "\n";);
|
||||
|
@ -739,7 +743,6 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
|
|||
expr_ref li(lhs[i].get(), m);
|
||||
expr_ref ri(rhs[i].get(), m);
|
||||
if (solve_unit_eq(li, ri, deps)) {
|
||||
// skip
|
||||
}
|
||||
else if (m_util.is_seq(li) || m_util.is_re(li)) {
|
||||
m_eqs.push_back(mk_eqdep(li, ri, deps));
|
||||
|
@ -1534,6 +1537,9 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
|
|||
else if (m_util.str.is_contains(e, e1, e2)) {
|
||||
result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
|
||||
}
|
||||
else if (m_util.str.is_unit(e, e1)) {
|
||||
result = m_util.str.mk_unit(expand(e1, deps));
|
||||
}
|
||||
else {
|
||||
result = e;
|
||||
}
|
||||
|
|
|
@ -190,14 +190,14 @@ public:
|
|||
}
|
||||
|
||||
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
|
||||
m_check_sat_executed = true;
|
||||
|
||||
m_check_sat_executed = true;
|
||||
m_use_solver1_results = false;
|
||||
|
||||
if (get_num_assumptions() != 0 ||
|
||||
num_assumptions > 0 || // assumptions were provided
|
||||
m_ignore_solver1) {
|
||||
// must use incremental solver
|
||||
switch_inc_mode();
|
||||
m_use_solver1_results = false;
|
||||
return m_solver2->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
|
@ -206,7 +206,6 @@ public:
|
|||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
|
||||
lbool r = m_solver2->check_sat(0, 0);
|
||||
if (r != l_undef || !use_solver1_when_undef()) {
|
||||
m_use_solver1_results = false;
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
@ -219,7 +218,6 @@ public:
|
|||
r = m_solver2->check_sat(0, 0);
|
||||
}
|
||||
if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
|
||||
m_use_solver1_results = false;
|
||||
return r;
|
||||
}
|
||||
if (eh.m_canceled) {
|
||||
|
@ -227,7 +225,6 @@ public:
|
|||
}
|
||||
}
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
|
||||
|
||||
}
|
||||
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
|
||||
|
|
Loading…
Reference in a new issue