From af7107611a37d45d495d0d40c50b67c08fc7de9c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Jan 2021 15:56:26 -0600 Subject: 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. --- src/theory/quantifiers/inst_strategy_enumerative.cpp | 4 +++- src/theory/quantifiers/relevant_domain.cpp | 16 ++++++++++------ src/theory/quantifiers/term_database.cpp | 4 ++-- 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(); -- cgit v1.2.3