Generalize concat conflict for sequences in LFSC (#8625)

This ensures LFSC proofs are correct when using CONCAT_CONFLICT for sequences.

In detail, to justify why (seq.++ (seq.unit c1) t1) = (seq.++ (seq.unit c2) t2) is a conflict, where c1 and c2 are constants, we require an explicit step to evalute (seq.unit c1) = (seq.unit c2) to false, since c1 and c2 are theory-specific constants.

Note this is different from (str.++ (char n1) t1) = (str.++ (char n2) t2) where a syntactic check of n1 and n2 suffices.

This fixes proof checking for regress0/seq/seq-types.smt2.

diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf
index eb7351e0c6cc9549b289d5457c4952371d62e523..e280bc77bfa8cf0750adf11cb8b2152d0bc36de0 100644 (file)
--- a/proofs/lfsc/signatures/strings_programs.plf
+++ b/proofs/lfsc/signatures/strings_programs.plf
@@ -36,7 +36,7 @@
 (program sc_skolem_first_ctn_post ((s term) (t term)) term 
   (sc_skolem_suffix_rem s (a.+ (str.len (sc_skolem_first_ctn_pre s t)) (a.+ (str.len t) (int 0)))))
 
-; Head and tail for string concatenation.
+; Head and tail for string concatenation. Fails if not a concatentation term.
 (program sc_string_head ((t term)) term (nary_head f_str.++ t))
 (program sc_string_tail ((t term)) term (nary_tail f_str.++ t))
 
@@ -242,7 +242,8 @@
     ((apply t1 t2)
       (let t12 (getarg f_str.++ t1)
       (match t12
-        ((char n) t12))))
+        ((char n) t12)
+        ((apply t121 t122) (ifequal t121 f_seq.unit t12 (fail term))))))
     (default (ifequal t (sc_mk_emptystr u) t (fail term)))))
 
 ; Flatten constants in str.++ application s. Notice that the rewritten form

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index 5f945f465dee42da19f1d25a18b32128a4f4dc10..46c6f67e8e235212c95293a6798ae1392ab378ac 100644 (file)
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -111,6 +111,32 @@
                          (! r (^ (sc_concat_conflict s t rev u) ok)
                             (holds false))))))))
 
+; For sequences, we use a variant of the PfRule::CONCAT_CONFLICT rule where the
+; justification for the clashing characters is given in the form of a
+; disequality. This is due to the fact that check whether a term is value is
+; not a simple syntactic check for some types.
+(program sc_concat_conflict_deq ((s term) (t term) (sc term) (tc term) (rev flag) (u sort)) Ok
+  (match (sc_strip_prefix
+           (sc_string_to_flat_form s rev u)
+           (sc_string_to_flat_form t rev u) u)
+    ((pair ss ts)
+      (ifequal (sc_string_first_char_or_empty s u) sc
+        (ifequal (sc_string_first_char_or_empty t u) tc
+          ok
+          (fail Ok))
+        (fail Ok)))))
+
+(declare concat_conflict_deq (! s term
+                             (! t term
+                             (! sc term
+                             (! tc term
+                             (! rev flag
+                             (! u sort
+                             (! p (holds (= s t))
+                             (! pc (holds (not (= sc tc)))
+                             (! r (^ (sc_concat_conflict_deq s t sc tc rev u) ok)
+                                (holds false)))))))))))
+
 (program sc_string_length_pos ((t term) (u sort)) term
   (or (and (= (str.len t) (int 0)) (and (= t (sc_mk_emptystr u)) true)) (or (a.> (str.len t) (int 0)) false))
 )

diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp
index df902e6d69a88476738b85be5edf8aaa6db9eea5..37f97b905853c52d44776f19b3983e4bda42dbe4 100644 (file)
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -22,6 +22,7 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "proof/proof_node_updater.h"
+#include "theory/strings/theory_strings_utils.h"
 
 using namespace cvc5::internal::kind;
 
@@ -363,6 +364,38 @@ 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())
+      {
+        // 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))
+      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);
+    }
+    break;
     default: return false; break;
   }
   AlwaysAssert(cdp->getProofFor(res)->getRule() != PfRule::ASSUME);

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index a2cabd7b6706304550059f44fe58bdfcf2f8efb0..59230870b4c73885955cb7f43a3288b15f815ea1 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -704,6 +704,11 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
         case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break;
         case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break;
         case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break;
+        case LfscRule::CONCAT_CONFLICT_DEQ:
+          pf << h << h << h << h << as[2].getConst<bool>()
+             << d_tproc.convertType(children[0]->getResult()[0].getType())
+             << cs[0] << cs[1];
+          break;
         default: return false; break;
       }
     }

diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp
index c38470a52bed80b8790d6de83363ad81d2c67fb3..de8fad30620e618edaa781ae6d5b2f7e3a629b64 100644 (file)
--- a/src/proof/lfsc/lfsc_util.cpp
+++ b/src/proof/lfsc/lfsc_util.cpp
@@ -35,6 +35,7 @@ const char* toString(LfscRule id)
     case LfscRule::NOT_AND_REV: return "not_and_rev";
     case LfscRule::PROCESS_SCOPE: return "process_scope";
     case LfscRule::ARITH_SUM_UB: return "arith_sum_ub";
+    case LfscRule::CONCAT_CONFLICT_DEQ: return "concat_conflict_deq";
     case LfscRule::INSTANTIATE: return "instantiate";
     case LfscRule::SKOLEMIZE: return "skolemize";
     case LfscRule::LAMBDA: return "\\";

diff --git a/src/proof/lfsc/lfsc_util.h b/src/proof/lfsc/lfsc_util.h
index 761d9edb77ead17c33a6de6ee27688bff6fc0752..9a0d96fa03ebe32b34be9d46c35169d2812be23a 100644 (file)
--- a/src/proof/lfsc/lfsc_util.h
+++ b/src/proof/lfsc/lfsc_util.h
@@ -53,6 +53,9 @@ enum class LfscRule : uint32_t
   PROCESS_SCOPE,
   // arithmetic
   ARITH_SUM_UB,
+  // sequences uses a different form of the concat conflict rule which takes
+  // an explicit disequality
+  CONCAT_CONFLICT_DEQ,
 
   // form of quantifier rules varies from internal calculus
   INSTANTIATE,