From ca9705cf0785e3a81fc25995df0bc3dc76e3bd9f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Feb 2021 15:55:32 -0600 Subject: Fix disequality between seq.unit terms (#5880) This adds a missing inference for disequality between seq.unit terms, which was not handled previously. Fixes #5666. --- src/theory/strings/core_solver.cpp | 92 +++++++++++++++++++++++++++++++------- src/theory/strings/core_solver.h | 2 +- src/theory/strings/infer_info.cpp | 1 + src/theory/strings/infer_info.h | 7 +++ 4 files changed, 85 insertions(+), 17 deletions(-) (limited to 'src/theory/strings') diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 6f7c97037..e95e79d68 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1987,6 +1987,65 @@ void CoreSolver::processDeq(Node ni, Node nj) if (nfni.d_nf.size() <= 1 && nfnj.d_nf.size() <= 1) { + // If normal forms have size <=1, then we are comparing either: + // (1) variable to variable, + // (2) variable to constant-like (empty, constant string/seq or SEQ_UNIT), + // (3) SEQ_UNIT to constant-like. + // We only have to process (3) here, since disequalities of the form of (1) + // and (2) are satisfied by construction. + for (size_t i = 0; i < 2; i++) + { + NormalForm& nfc = i == 0 ? nfni : nfnj; + if (nfc.d_nf.size() == 0 || nfc.d_nf[0].getKind() != SEQ_UNIT) + { + // may need to look at the other side + continue; + } + Node u = nfc.d_nf[0]; + // if the other side is constant like + NormalForm& nfo = i == 0 ? nfnj : nfni; + if (nfo.d_nf.size() == 0 || !utils::isConstantLike(nfo.d_nf[0])) + { + break; + } + // v is the other side (a possibly constant seq.unit term) + Node v = nfo.d_nf[0]; + Node vc; + if (v.isConst()) + { + // get the list of characters (strings of length 1) + std::vector vchars = Word::getChars(v); + if (vchars.size() != 1) + { + // constant of size != 1, disequality is satisfied + break; + } + // get the element of the character + vc = vchars[0].getConst().getVec()[0]; + } + else + { + Assert(v.getKind() == SEQ_UNIT); + vc = v[0]; + } + Assert(u[0].getType() == vc.getType()); + // if already disequal, we are done + if (d_state.areDisequal(u[0], vc)) + { + break; + } + // seq.unit(x) != seq.unit(y) => x != y + // Notice this is a special case, since the code below would justify this + // disequality by reasoning that a component is disequal. However, the + // disequality components are the entire disequality. + Node deq = u.eqNode(v).notNode(); + std::vector premises; + premises.push_back(deq); + Node conc = u[0].eqNode(vc).notNode(); + d_im.sendInference(premises, conc, Inference::UNIT_INJ_DEQ, false, true); + return; + } + Trace("strings-solve-debug") << "...trivial" << std::endl; return; } @@ -2015,6 +2074,7 @@ void CoreSolver::processDeq(Node ni, Node nj) if (processReverseDeq(nfi, nfj, ni, nj)) { + Trace("strings-solve-debug") << "...processed reverse" << std::endl; return; } @@ -2026,6 +2086,7 @@ void CoreSolver::processDeq(Node ni, Node nj) { if (processSimpleDeq(nfi, nfj, ni, nj, index, false)) { + Trace("strings-solve-debug") << "...processed simple" << std::endl; return; } @@ -2495,24 +2556,23 @@ void CoreSolver::checkNormalFormsDeq() // if both are constants, they should be distinct, and its trivial Assert(cols[i][j] != cols[i][k]); } - else + else if (d_state.areDisequal(cols[i][j], cols[i][k])) { - if (d_state.areDisequal(cols[i][j], cols[i][k])) + Assert(!d_state.isInConflict()); + if (Trace.isOn("strings-solve")) { - Assert(!d_state.isInConflict()); - if (Trace.isOn("strings-solve")) - { - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf, "strings-solve"); - Trace("strings-solve") << " against " << cols[i][k] << " "; - utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf, "strings-solve"); - Trace("strings-solve") << "..." << std::endl; - } - processDeq(cols[i][j], cols[i][k]); - if (d_im.hasProcessed()) - { - return; - } + Trace("strings-solve") << "- Compare " << cols[i][j] << ", nf "; + utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf, + "strings-solve"); + Trace("strings-solve") << " against " << cols[i][k] << ", nf "; + utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf, + "strings-solve"); + Trace("strings-solve") << "..." << std::endl; + } + processDeq(cols[i][j], cols[i][k]); + if (d_im.hasProcessed()) + { + return; } } } diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index b1c302935..6e536cbfa 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -78,7 +78,7 @@ class CoreInferInfo class CoreSolver { friend class InferenceManager; - typedef context::CDHashMap NodeIntMap; + using NodeIntMap = context::CDHashMap; public: CoreSolver(SolverState& s, diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 15d8bbde7..4cb072efb 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -31,6 +31,7 @@ const char* toString(Inference i) case Inference::I_NORM: return "I_NORM"; case Inference::UNIT_INJ: return "UNIT_INJ"; case Inference::UNIT_CONST_CONFLICT: return "UNIT_CONST_CONFLICT"; + case Inference::UNIT_INJ_DEQ: return "UNIT_INJ_DEQ"; case Inference::CARD_SP: return "CARD_SP"; case Inference::CARDINALITY: return "CARDINALITY"; case Inference::I_CYCLE_E: return "I_CYCLE_E"; diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 863f1ab06..a6c4776eb 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -69,9 +69,16 @@ enum class Inference : uint32_t // y = "" ^ z = "" => x ++ y = z ++ x I_NORM, // injectivity of seq.unit + // (seq.unit x) = (seq.unit y) => x=y, or + // (seq.unit x) = (seq.unit c) => x=c UNIT_INJ, // unit constant conflict + // (seq.unit x) = C => false if |C| != 1. UNIT_CONST_CONFLICT, + // injectivity of seq.unit for disequality + // (seq.unit x) != (seq.unit y) => x != y, or + // (seq.unit x) != (seq.unit c) => x != c + UNIT_INJ_DEQ, // A split due to cardinality CARD_SP, // The cardinality inference for strings, see Liang et al CAV 2014. -- cgit v1.2.3