From 86e7f83e061c2353b16021ca592335bf59f909ff Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 11 Jul 2017 13:24:48 -0400 Subject: [PATCH 1/4] proper theory_arith integration in theory_str::get_arith_value() --- src/smt/theory_str.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2e928af37..bcb91b884 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4664,7 +4664,19 @@ namespace smt { if (!tha) { return false; } - TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); + + // first query theory_arith directly + + expr_ref ival(m); + if (ctx.e_internalized(e) && tha->get_value(ctx.get_enode(e), ival) + && m_autil.is_numeral(ival, val) && val.is_int()) { + TRACE("str", tout << "theory_arith: " << mk_pp(e, m) << " = " << val << std::endl;); + return true; + } + + // if this fails, fall back to checking eqc + + TRACE("str", tout << "no result in theory_arith! checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); expr_ref _val(m); enode * en_e = ctx.get_enode(e); enode * it = en_e; From c6707688ba7ebfb70610e8c6a10c13831e431953 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 18 Jul 2017 13:11:03 -0400 Subject: [PATCH 2/4] improved get_arith_value() in theory_str Since the root of the eqc of an integer term should be a constant if there is a constant in that eqc, we can ask for it directly without either iterating over the entire eqc or asking the arithmetic solver (and receiving potentially stale info). --- src/smt/theory_str.cpp | 32 +++++++++++++------------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index bcb91b884..89687c4ed 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4653,30 +4653,23 @@ namespace smt { } bool theory_str::get_arith_value(expr* e, rational& val) const { - if (opt_DisableIntegerTheoryIntegration) { - TRACE("str", 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); - if (!tha) { + + // if an integer constant exists in the eqc, it should be the root + enode * en_e = ctx.get_enode(e); + enode * root_e = en_e->get_root(); + if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) { + TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;); + return true; + } else { + TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;); return false; } - // first query theory_arith directly - - expr_ref ival(m); - if (ctx.e_internalized(e) && tha->get_value(ctx.get_enode(e), ival) - && m_autil.is_numeral(ival, val) && val.is_int()) { - TRACE("str", tout << "theory_arith: " << mk_pp(e, m) << " = " << val << std::endl;); - return true; - } - - // if this fails, fall back to checking eqc - - TRACE("str", tout << "no result in theory_arith! checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); + // fallback code: iterate over eqc (slow for large cases, e.g. many terms with length 0) + /* + TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); expr_ref _val(m); enode * en_e = ctx.get_enode(e); enode * it = en_e; @@ -4693,6 +4686,7 @@ namespace smt { } while (it != en_e); TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;); return false; + */ } bool theory_str::lower_bound(expr* _e, rational& lo) { From 69f0ed9b1f5bcd864ff5ae9940909f06bc469a6b Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 18 Jul 2017 13:13:12 -0400 Subject: [PATCH 3/4] remove disabled code block in get_arith_value() --- src/smt/theory_str.cpp | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 89687c4ed..1007ee662 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4666,27 +4666,6 @@ namespace smt { TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;); return false; } - - // fallback code: iterate over eqc (slow for large cases, e.g. many terms with length 0) - /* - TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); - expr_ref _val(m); - enode * en_e = ctx.get_enode(e); - enode * it = en_e; - do { - if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) { - // found an arithmetic term - TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )" - << std::endl;); - return true; - } else { - TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;); - } - it = it->get_next(); - } while (it != en_e); - TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;); - return false; - */ } bool theory_str::lower_bound(expr* _e, rational& lo) { From 7ddb940f77582babb2cd1e799c7c2f815bb80b82 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 19 Jul 2017 10:15:38 -0400 Subject: [PATCH 4/4] add e_internalized() check in theory_str::get_arith_value() --- src/smt/theory_str.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1007ee662..89e0123a8 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4656,6 +4656,11 @@ namespace smt { context& ctx = get_context(); ast_manager & m = get_manager(); + // safety + if (!ctx.e_internalized(e)) { + return false; + } + // if an integer constant exists in the eqc, it should be the root enode * en_e = ctx.get_enode(e); enode * root_e = en_e->get_root();