From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Oct 2020 16:58:37 +0000 (-0500)
Subject: Make seq.nth a trigger kind (#5314)
X-Git-Tag: cvc5-1.0.0~2686
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e6e153a78843b134d943f5d1ec33e254d0fb2fe;p=cvc5.git

Make seq.nth a trigger kind (#5314)

This makes seq.nth a trigger kind, analogous to select in arrays.

This fixes a timeout in seq-unsolved-ematch.smt2, fixing the nightlies.
---

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 545dab701..95ab0674f 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -408,7 +408,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) {
          || k == APPLY_SELECTOR_TOTAL || 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 == INT_TO_BITVECTOR || k == HO_APPLY || k == SEQ_NTH;
 }
 
 bool Trigger::isRelationalTrigger( Node n ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3e8201144..42677fa3f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -166,8 +166,11 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
 Node TermDb::getMatchOperator( Node n ) {
   Kind k = n.getKind();
   //datatype operators may be parametric, always assume they are
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
-      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){
+  if (k == SELECT || k == STORE || k == UNION || k == INTERSECTION
+      || k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON
+      || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == SEP_PTO
+      || k == HO_APPLY || k == SEQ_NTH)
+  {
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();