diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-20 15:56:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-20 15:56:26 -0600 |
commit | af7107611a37d45d495d0d40c50b67c08fc7de9c (patch) | |
tree | 81873b37a540158ae07476d4cee0b729d12cb6b1 /src/theory/quantifiers/relevant_domain.cpp | |
parent | 273219488df1068a1abd444fc677bee57748bc32 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
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 |