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

remove the option to bypass check_regex_in in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-08-17 21:12:19 -04:00
parent 6263391c11
commit 54d7e4bbb5
2 changed files with 2 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_str.cpp
View file

@ -35,7 +35,6 @@ theory_str::theory_str(ast_manager & m):
opt_LCMUnrollStep(2), opt_LCMUnrollStep(2),
opt_NoQuickReturn_IntegerTheory(false), opt_NoQuickReturn_IntegerTheory(false),
opt_DisableIntegerTheoryIntegration(false), opt_DisableIntegerTheoryIntegration(false),
opt_NoCheckRegexIn(false),
/* Internal setup */ /* Internal setup */
search_started(false), search_started(false),
m_autil(m), m_autil(m),
@ -1645,12 +1644,8 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
} }
if (!regex_in_bool_map.empty()) { if (!regex_in_bool_map.empty()) {
if (opt_NoCheckRegexIn) { TRACE("t_str", tout << "checking regex consistency" << std::endl;);
TRACE("t_str", tout << "WARNING: skipping check_regex_in()" << std::endl;); check_regex_in(lhs, rhs);
} else {
TRACE("t_str", tout << "checking regex consistency" << std::endl;);
check_regex_in(lhs, rhs);
}
} }
// okay, all checks here passed // okay, all checks here passed

8
src/smt/theory_str.h
View file

@ -138,14 +138,6 @@ namespace smt {
*/ */
bool opt_DisableIntegerTheoryIntegration; bool opt_DisableIntegerTheoryIntegration;
/*
* If NoCheckRegexIn is set to true,
* an expensive regular expression membership test is skipped.
* This option is for experiment purposes only and should be set to 'false'
* as skipping this check impacts the correctness of the solver.
*/
bool opt_NoCheckRegexIn;
bool search_started; bool search_started;
arith_util m_autil; arith_util m_autil;
str_util m_strutil; str_util m_strutil;