Adding str.len to triggers (#5746)

This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 654b1fd12ae84a95aad2c04e23b6e40f21f777b3..a111e0221438056aa4a15d4f2ca9cc9943b35957 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -419,7 +419,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) {
          || k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET
          || k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO
          || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY
-         || k == SEQ_NTH;
+         || k == STRING_LENGTH || k == SEQ_NTH;
 }
 
 bool Trigger::isRelationalTrigger( Node n ) {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 62978220aa755c5177917af33f2916d84a3d7858..509427d45527931ff8f1989b6e3a7e253fa4afe1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -975,6 +975,7 @@ set(regress_0_tests
   regress0/seq/seq-nth.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/seq/seq-types.smt2
+  regress0/seq/quant_len_trigger.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
   regress0/sets/abt-te-exh2.smt2

diff --git a/test/regress/regress0/seq/quant_len_trigger.smt2 b/test/regress/regress0/seq/quant_len_trigger.smt2
new file mode 100644 (file)
index 0000000..08fdb4a
--- /dev/null
+++ b/test/regress/regress0/seq/quant_len_trigger.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+
+(set-option :strings-exp true)
+(set-logic ALL)
+
+(assert (forall ((x (Seq Int)) (xx (Seq Int)) ) (=> (and (= (seq.len x) (seq.len xx)) (forall ((i Int) )   (=> (and (<= 0 i) (< i (seq.len x))) (= (seq.nth x i) (seq.nth xx i))))) (= x xx))))
+
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+
+(assert (not (=> (= (seq.len x) (seq.len y)) (=> (forall ((i Int) )   (=> (and (<= 0 i) (< i (seq.len x))) (= (seq.nth x i) (seq.nth y i)))) (= x y)))))
+
+(check-sat)