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.

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 3f6943a72fafe10e3729f1d37cbc2489a5c8ca4e..9d84ea5757cf900b446ef34db48f8f34cac98f73 100644 (file)
--- 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 1a38518004f94c553fa9af4d6406abeed475b5a7..2893fd6860d0d9d9c78a0ec5b00a4173badb68e2 100644 (file)
--- 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 f91cda36b7ed8c7e63a00d9191301fe14ed0892e..0ed488891f9675fbee68068eba0934847f1d5a9d 100644 (file)
--- 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();