From: Andrew Reynolds Date: Mon, 8 Feb 2021 21:55:32 +0000 (-0600) Subject: Fix disequality between seq.unit terms (#5880) X-Git-Tag: cvc5-1.0.0~2306 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca9705cf0785e3a81fc25995df0bc3dc76e3bd9f;p=cvc5.git 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. --- 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. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 82ef8702a..ddf810b0c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1108,6 +1108,8 @@ set(regress_0_tests regress0/strings/issue5428-re-diff-assoc.smt2 regress0/strings/issue5542-strings-seq-mix.smt2 regress0/strings/issue5608-eager-pp.smt2 + regress0/strings/issue5666-orig-unit-deq.smt2 + regress0/strings/issue5666-unit-deq.smt2 regress0/strings/issue5745-eager-pp.smt2 regress0/strings/issue5767-eager-pp.smt2 regress0/strings/issue5771-eager-pp.smt2 diff --git a/test/regress/regress0/strings/issue5666-orig-unit-deq.smt2 b/test/regress/regress0/strings/issue5666-orig-unit-deq.smt2 new file mode 100644 index 000000000..ae4cd046b --- /dev/null +++ b/test/regress/regress0/strings/issue5666-orig-unit-deq.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun i5 () Int) +(declare-fun seq2 () (Seq Int)) +(assert (< 1 i5)) +(assert (xor (seq.prefixof seq2 seq2) (seq.suffixof (seq.unit 2) (seq.unit i5)))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5666-unit-deq.smt2 b/test/regress/regress0/strings/issue5666-unit-deq.smt2 new file mode 100644 index 000000000..3a83bfb12 --- /dev/null +++ b/test/regress/regress0/strings/issue5666-unit-deq.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun s () (Seq Int)) +(declare-fun x () Int) +(assert (= s (seq.unit 0))) +(assert (not (= s (seq.unit x)))) +(check-sat)