mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
add option to disable integer theory integration in theory_str; this is currently ENABLED
This commit is contained in:
parent
02a66c425e
commit
f555074e27
|
@ -34,6 +34,7 @@ theory_str::theory_str(ast_manager & m):
|
|||
opt_VerifyFinalCheckProgress(true),
|
||||
opt_LCMUnrollStep(2),
|
||||
opt_NoQuickReturn_Concat_IntegerTheory(true),
|
||||
opt_DisableIntegerTheoryIntegration(true),
|
||||
/* Internal setup */
|
||||
search_started(false),
|
||||
m_autil(m),
|
||||
|
@ -3747,6 +3748,11 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
|
|||
}
|
||||
|
||||
bool theory_str::get_value(expr* e, rational& val) const {
|
||||
if (opt_DisableIntegerTheoryIntegration) {
|
||||
TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
|
||||
return false;
|
||||
}
|
||||
|
||||
context& ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
|
||||
|
@ -3773,6 +3779,11 @@ bool theory_str::get_value(expr* e, rational& val) const {
|
|||
}
|
||||
|
||||
bool theory_str::lower_bound(expr* _e, rational& lo) {
|
||||
if (opt_DisableIntegerTheoryIntegration) {
|
||||
TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
|
||||
return false;
|
||||
}
|
||||
|
||||
context& ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
|
||||
|
@ -3782,6 +3793,11 @@ bool theory_str::lower_bound(expr* _e, rational& lo) {
|
|||
}
|
||||
|
||||
bool theory_str::upper_bound(expr* _e, rational& hi) {
|
||||
if (opt_DisableIntegerTheoryIntegration) {
|
||||
TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
|
||||
return false;
|
||||
}
|
||||
|
||||
context& ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
|
||||
|
@ -3791,6 +3807,11 @@ bool theory_str::upper_bound(expr* _e, rational& hi) {
|
|||
}
|
||||
|
||||
bool theory_str::get_len_value(expr* e, rational& val) {
|
||||
if (opt_DisableIntegerTheoryIntegration) {
|
||||
TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;);
|
||||
return false;
|
||||
}
|
||||
|
||||
context& ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
theory* th = ctx.get_theory(m_autil.get_family_id());
|
||||
|
|
|
@ -100,9 +100,25 @@ namespace smt {
|
|||
* will not return from the function after asserting their axioms.
|
||||
* This means that control will fall through to the type 1-6 axioms,
|
||||
* causing those to be added as well.
|
||||
* The default behaviour of Z3str2 is to set this to 'false'.
|
||||
*/
|
||||
bool opt_NoQuickReturn_Concat_IntegerTheory;
|
||||
|
||||
/*
|
||||
* If DisableIntegerTheoryIntegration is set to true,
|
||||
* ALL calls to the integer theory integration methods
|
||||
* (get_value, get_len_value, lower_bound, upper_bound)
|
||||
* will ignore what the arithmetic solver believes about length terms,
|
||||
* and will return no information.
|
||||
*
|
||||
* This reduces performance significantly, but can be useful to enable
|
||||
* if it is suspected that string-integer integration, or the arithmetic solver itself,
|
||||
* might have a bug.
|
||||
*
|
||||
* The default behaviour of Z3str2 is to set this to 'false'.
|
||||
*/
|
||||
bool opt_DisableIntegerTheoryIntegration;
|
||||
|
||||
bool search_started;
|
||||
arith_util m_autil;
|
||||
str_util m_strutil;
|
||||
|
|
Loading…
Reference in a new issue