Fix LFSC proof construction for concat clash of sequences (#8739)

Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences.

Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting.

diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp
index f849047ff60ca2bf7d47b832ff770808c22d0995..9fe57823053510de60481eacb1aff485d803d6a0 100644 (file)
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -366,34 +366,17 @@ bool LfscProofPostprocessCallback::update(Node res,
     break;
     case PfRule::CONCAT_CONFLICT:
     {
-      Assert(children.size() == 1);
-      Assert(children[0].getKind() == EQUAL);
-      if (children[0][0].getType().isString())
+      if (children.size() == 1)
       {
         // no need to change
         return false;
       }
-      bool isRev = args[0].getConst<bool>();
-      std::vector<Node> tvec;
-      std::vector<Node> svec;
-      theory::strings::utils::getConcat(children[0][0], tvec);
-      theory::strings::utils::getConcat(children[0][1], svec);
-      Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
-      Node s0 = svec[isRev ? svec.size() - 1 : 0];
-      Assert(t0.isConst() && s0.isConst());
-      // We introduce an explicit disequality for the constants:
-      // ------------------- EVALUATE
-      // (= (= c1 c2) false)
-      // ------------------- FALSE_ELIM
-      // (not (= c1 c2))
+      Assert(children.size() == 2);
+      Assert(children[0].getKind() == EQUAL);
+      Assert(children[0][0].getType().isSequence());
+      // must use the sequences version of the rule
       Node falsen = nm->mkConst(false);
-      Node eq = t0.eqNode(s0);
-      Node eqEqFalse = eq.eqNode(falsen);
-      cdp->addStep(eqEqFalse, PfRule::EVALUATE, {}, {eq});
-      Node deq = eq.notNode();
-      cdp->addStep(deq, PfRule::FALSE_ELIM, {eqEqFalse}, {});
-      addLfscRule(
-          cdp, falsen, {children[0], deq}, LfscRule::CONCAT_CONFLICT_DEQ, args);
+      addLfscRule(cdp, falsen, children, LfscRule::CONCAT_CONFLICT_DEQ, args);
     }
     break;
     default: return false; break;

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index be1d7b040d1bb4fc7095e1d4567b0b49d3af5ce2..c6f2b9a16a26703cd96a93c77067c64c2e47e3ec 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -1436,7 +1436,20 @@ enum class PfRule : uint32_t
    * where :math:`b` indicates if the direction is reversed, :math:`c_1,\,c_2`
    * are constants such that :math:`\texttt{Word::splitConstant}(c_1,c_2,
    * \mathit{index},b)` is null, in other words, neither is a prefix of the
-   * other.
+   * other. Note it may be the case that one side of the equality denotes the
+   * empty string.
+   *
+   * Alternatively, if the equality is between sequences, this rule has the
+   * form:
+   *
+   * .. math::
+   *
+   *   \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot}
+   *
+   * where t_1 and s_1 are constants of length one, or otherwise one side
+   * of the equality is the empty sequence and t_1 or s_1 corresponding to
+   * that side is the empty sequence.
+   *
    * \endverbatim
    */
   CONCAT_CONFLICT,

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 8d57068e672e795af586f710669f2650105dbc94..212bc56d3afa82bf61915abbbf3e43b76366c1f2 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -392,6 +392,13 @@ void InferProofCons::convert(InferenceId infer,
         // fail
         break;
       }
+      // get the heads of the equality
+      std::vector<Node> tvec;
+      std::vector<Node> svec;
+      theory::strings::utils::getConcat(mainEqCeq[0], tvec);
+      theory::strings::utils::getConcat(mainEqCeq[1], svec);
+      Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
+      Node s0 = svec[isRev ? svec.size() - 1 : 0];
       // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
       // inference involved t and s.
       if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ
@@ -427,10 +434,20 @@ void InferProofCons::convert(InferenceId infer,
         // should be a constant conflict
         std::vector<Node> childrenC;
         childrenC.push_back(mainEqCeq);
+        // if it is between sequences, we require the explicit disequality
+        if (mainEqCeq[0].getType().isSequence())
+        {
+          Assert(t0.isConst() && s0.isConst());
+          // We introduce an explicit disequality for the constants
+          Node deq = t0.eqNode(s0).notNode();
+          psb.addStep(PfRule::MACRO_SR_PRED_INTRO, {}, {deq}, deq);
+          Assert(!deq.isNull());
+          childrenC.push_back(deq);
+        }
         std::vector<Node> argsC;
         argsC.push_back(nodeIsRev);
-        Node mainEqC = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC);
-        if (mainEqC == conc)
+        Node conflict = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC);
+        if (conflict == conc)
         {
           useBuffer = true;
           Trace("strings-ipc-core") << "...success!" << std::endl;
@@ -457,12 +474,6 @@ void InferProofCons::convert(InferenceId infer,
       }
       else
       {
-        std::vector<Node> tvec;
-        std::vector<Node> svec;
-        utils::getConcat(mainEqCeq[0], tvec);
-        utils::getConcat(mainEqCeq[1], svec);
-        Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
-        Node s0 = svec[isRev ? svec.size() - 1 : 0];
         bool applySym = false;
         // may need to apply symmetry
         if ((infer == InferenceId::STRINGS_SSPLIT_CST

diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index a938a120fc3899359e247cd6f0e43a2cb4724957..0b7f84fc3eb1696e80ed95f25eb81608caadd6f8 100644 (file)
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -181,7 +181,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     }
     else if (id == PfRule::CONCAT_CONFLICT)
     {
-      Assert(children.size() == 1);
+      Assert(children.size() >= 1 && children.size() <= 2);
       if (!t0.isConst() || !s0.isConst())
       {
         // not constants
@@ -195,6 +195,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
         // versa.
         return Node::null();
       }
+      // if a disequality was provided, ensure that it is correct
+      if (children.size() == 2)
+      {
+        if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
+            || children[1][0][0] != t0 || children[1][0][1] != s0)
+        {
+          return Node::null();
+        }
+      }
+      else if (t0.getType().isSequence())
+      {
+        // we require the disequality for sequences
+        return Node::null();
+      }
       return nm->mkConst(false);
     }
     else if (id == PfRule::CONCAT_SPLIT)

diff --git a/test/regress/cli/regress0/seq/seq-types.smt2 b/test/regress/cli/regress0/seq/seq-types.smt2
index f8d8aa8b3a6e977b49c2407c7d2a70e199aa7e13..3facf688ab91f9c2827ac0d02adb3f565ea6a0e6 100644 (file)
--- a/test/regress/cli/regress0/seq/seq-types.smt2
+++ b/test/regress/cli/regress0/seq/seq-types.smt2
@@ -1,4 +1,3 @@
-; DISABLE-TESTER: lfsc
 ; COMMAND-LINE: --strings-exp
 ;EXPECT: unsat
 (set-logic ALL)