Fix type issues with relevant domain computation (#5788)

This fixes 2 issues with relevant domain type computation, the first involving arithmetic INST_CONSTANT that do not belong to the current quantified formula being solved for in a monomial sum, the second involving parametric datatype selectors.

Fixes #5635. Both benchmarks on that issue are unsolved (one timeout, one unknown) but throw no assertion failure.

3 files changed, 15 insertions, 9 deletions

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 3f6943a72..9d84ea575 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -314,7 +314,9 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
                   << std::endl;
             }
             Assert(terms[i].isNull()
-                   || terms[i].getType().isComparableTo(ftypes[i]));
+                   || terms[i].getType().isComparableTo(ftypes[i]))
+                << "Incompatible type " << f << ", " << terms[i].getType()
+                << ", " << ftypes[i] << std::endl;
           }
           if (ie->addInstantiation(f, terms))
           {
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 1a3851800..2893fd686 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -19,12 +19,11 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 void RelevantDomain::RDomain::merge( RDomain * r ) {
   Assert(!d_parent);
@@ -261,7 +260,9 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
             Node var2;
             bool hasNonVar = false;
             for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-              if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
+              if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
+                  && tu->getInstConstAttr(it->first) == q)
+              {
                 if( var.isNull() ){
                   var = it->first;
                 }else if( var2.isNull() ){
@@ -329,3 +330,6 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
   }
 }
 
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f91cda36b..0ed488891 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -168,8 +168,8 @@ Node TermDb::getMatchOperator( Node n ) {
   //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 || k == SEQ_NTH)
+      || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || 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();