mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

patch UNSAT to UNKNOWN in cmd_context for theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-09-02 19:04:20 -04:00
parent d3062a8eff
commit 2b8f165cc4
2 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/smt_context.cpp
View file

@ -37,6 +37,7 @@ Revision History:
#include"model_pp.h" #include"model_pp.h"
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
#include"ast_translation.h" #include"ast_translation.h"
#include"theory_str.h"
namespace smt { namespace smt {
@ -3086,6 +3087,25 @@ namespace smt {
if (r == l_true && get_cancel_flag()) { if (r == l_true && get_cancel_flag()) {
r = l_undef; r = l_undef;
} }
// PATCH for theory_str:
// UNSAT + overlapping variables => UNKNOWN
if (r == l_false) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
theory * th = *it;
if (strcmp(th->get_name(), "strings") == 0) {
theory_str * str = (theory_str*)th;
if (str->overlapping_variables_detected()) {
TRACE("t_str", tout << "WARNING: overlapping variables detected, UNSAT changed to UNKNOWN!" << std::endl;);
r = l_undef;
}
break;
}
}
}
return r; return r;
} }

2
src/smt/theory_str.h
View file

@ -457,6 +457,8 @@ namespace smt {
virtual char const * get_name() const { return "strings"; } virtual char const * get_name() const { return "strings"; }
virtual void display(std::ostream & out) const; virtual void display(std::ostream & out) const;
bool overlapping_variables_detected() const { return loopDetected; }
protected: protected:
virtual bool internalize_atom(app * atom, bool gate_ctx); virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term); virtual bool internalize_term(app * term);