From 16dc2788a7bfe29b87d505f092a20bc2315e2762 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Oct 2019 12:43:17 -0700 Subject: [PATCH] compiler warnings Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 2 +- src/smt/theory_str.cpp | 31 ++++++++++++++++++------------- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index de036a46b..264af8bc7 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1622,7 +1622,7 @@ namespace nlsat { del_clauses(m_valids); if (m_check_lemmas) { for (clause* c : m_learned) { - //check_lemma(c->size(), c->c_ptr(), false, nullptr); + check_lemma(c->size(), c->c_ptr(), false, nullptr); } } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 46c60b621..a30dbd551 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1920,19 +1920,23 @@ namespace smt { u.str.is_string(range2, range2val); return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); } else if (u.re.is_loop(a_regex)) { - expr * body; - unsigned lo, hi; - // There are two variants of loop: a 2-argument version and a 3-argument version. - if (u.re.is_loop(a_regex, body, lo, hi)) { - rational rLo(lo); - rational rHi(hi); - zstring bodyStr = get_std_regex_str(body); - return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})"); - } else if (u.re.is_loop(a_regex, body, lo)) { - rational rLo(lo); - zstring bodyStr = get_std_regex_str(body); - return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring("+") + zstring("})"); - } + expr * body; + unsigned lo, hi; + // There are two variants of loop: a 2-argument version and a 3-argument version. + if (u.re.is_loop(a_regex, body, lo, hi)) { + rational rLo(lo); + rational rHi(hi); + zstring bodyStr = get_std_regex_str(body); + return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})"); + } else if (u.re.is_loop(a_regex, body, lo)) { + rational rLo(lo); + zstring bodyStr = get_std_regex_str(body); + return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring("+") + zstring("})"); + } + else { + TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); + UNREACHABLE(); return zstring(""); + } } else if (u.re.is_full_seq(a_regex)) { return zstring("(.*)"); } else if (u.re.is_full_char(a_regex)) { @@ -1941,6 +1945,7 @@ namespace smt { TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); UNREACHABLE(); return zstring(""); } + } void theory_str::instantiate_axiom_RegexIn(enode * e) {