From c26a0f8fd971a72e8e9bdf058930c06587856604 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Oct 2018 00:31:57 -0500 Subject: Fix string ext inference for rewrites that introduce negation (#2618) --- src/theory/strings/theory_strings.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/theory') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 26ff9188f..fb25e1348 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1778,18 +1778,21 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef Node conc = nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); conc = Rewriter::rewrite(conc); + conc = conc.negate(); bool do_infer = false; - if (conc.getKind() == EQUAL) + bool pol = conc.getKind() != NOT; + Node lit = pol ? conc : conc[0]; + if (lit.getKind() == EQUAL) { - do_infer = !areDisequal(conc[0], conc[1]); + do_infer = pol ? !areEqual(lit[0], lit[1]) + : !areDisequal(lit[0], lit[1]); } else { - do_infer = !areEqual(conc, d_false); + do_infer = !areEqual(lit, pol ? d_true : d_false); } if (do_infer) { - conc = conc.negate(); std::vector exp_c; exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; -- cgit v1.2.3