diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-27 08:34:59 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-27 08:35:14 -0600 |
| commit | 251fd73a759a8e5e94103e9b76a06491a92e425b (patch) | |
| tree | 193cd049c7422b30c6a65ce119f1ac18615037f9 /src/theory/quantifiers/relevant_domain.cpp | |
| parent | 7a6c462b0ce3adf52a9d44a5f98c53065fedc33d (diff) | |
Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the default QCF setting. Bug fix to prevent non-ground terms from entering relevant domains.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 0452278f2..952f3409a 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -190,7 +190,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ - rds[varCh]->addTerm( n[oCh] ); + rds[varCh]->addTerm( n[oCh], ng ); } //the positive occurence adds other terms if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ |