Fix related to preregistering boolean term variables in strings (#5331)

We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences).

This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index b5b2a5a137c29f4e4eff9d6cb36cfc79e45001f6..2b5daa476103a958a7ee95f433f59c938d7d8cf4 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -203,8 +203,12 @@ void TermRegistry::preRegisterTerm(TNode n)
   }
   else if (tn.isBoolean())
   {
-    // Get triggered for both equal and dis-equal
-    ee->addTriggerPredicate(n);
+    // All kinds that we do congruence over that may return a Boolean go here
+    if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH)
+    {
+      // Get triggered for both equal and dis-equal
+      ee->addTriggerPredicate(n);
+    }
   }
   else
   {

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index e48e91cd0069cdcadf884cfe295e5db90391830b..fdb80e878d11931cd9995c0d956aa383b236e897 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1739,7 +1739,7 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) {
     return addTriggerEquality(predicate);
   }
   Assert(d_congruenceKinds.tst(predicate.getKind()))
-      << "No point in adding non-congruence predicates";
+      << "No point in adding non-congruence predicates, kind is " << predicate.getKind();
 
   if (d_done) {
     return;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6c2c51dfb9cf9443e8cb87763a11beccbbad3a42..4653f1c3e0b818ef0e4ca603c9681caa512195c2 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -883,6 +883,7 @@ set(regress_0_tests
   regress0/sep/wand-crash.smt2
   regress0/seq/intseq.smt2
   regress0/seq/intseq_dt.smt2
+  regress0/seq/issue4370-bool-terms.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2

diff --git a/test/regress/regress0/seq/issue4370-bool-terms.smt2 b/test/regress/regress0/seq/issue4370-bool-terms.smt2
new file mode 100644 (file)
index 0000000..8f6a16b
--- /dev/null
+++ b/test/regress/regress0/seq/issue4370-bool-terms.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --strings-exp --no-check-models
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((a 0)) (((b))))
+(define-fun v () (Seq Bool) (as seq.empty (Seq Bool)))
+(declare-fun e () (Seq a))
+(define-fun w () Int (seq.len e))
+(define-fun x () (Seq a) (seq.extract e 1 (- w 1)))
+(define-fun i () (Seq a) (seq.extract x 1 (- (seq.len x) 1)))
+(define-fun y () (Seq Bool) (ite (= 0 (seq.len i)) v (seq.unit true)))
+(define-fun m () (Seq Bool) (seq.++ (seq.unit false) y))
+(define-fun n () (Seq Bool) (ite (= 0 (seq.len x)) v m))
+(define-fun o () (Seq Bool) (seq.++ (seq.unit false) n))
+(define-fun p () (Seq Bool) (ite (= 0 w) v o))
+(define-fun s () (Seq Bool) (seq.extract p 1 (- (seq.len p) 1)))
+(define-fun u () (Seq Bool) (seq.extract s 1 (- (seq.len s) 1)))
+(assert (not (seq.nth u 0)))
+(check-sat)