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 545dab7011e86a6d4f1711cc0fc27c146ba815cd..95ab0674f28ddb8ca8b4575bde804e9cbd930bf4 100644 (file)
--- 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 3e8201144c3ef6ade282de9550fa3b5f2c2b62d6..42677fa3fcde7226b08c1208f9f70c63df3fb007 100644 (file)
--- 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();