From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 5 Jan 2021 19:19:34 +0000 (-0800)
Subject: Adding str.len to triggers (#5746)
X-Git-Tag: cvc5-1.0.0~2399
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d2ee68b75d1fd3ea0d523b44815d2dc63529e54;p=cvc5.git

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 654b1fd12..a111e0221 100644
--- 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 62978220a..509427d45 100644
--- 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
index 000000000..08fdb4a43
--- /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)