diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 16:18:08 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 18:06:11 -0500 |
| commit | 63ca7c0a10dcd6b3be42d4d513f842db76733392 (patch) | |
| tree | 58359725846197e3a471ff218bd4c593172d4fc8 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | d6a6ab61dbe64848b78b9ab8d07d95fc58b64e72 (diff) | |
Only put quantifier assertions in model equality engine if fullModel==true
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index a1f8e32fe..be6dd5b08 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -92,14 +92,16 @@ Node TheoryQuantifiers::getValue(TNode n) { } } -void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ - for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { - if((*i).assertion.getKind() == kind::NOT) { - Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; - m->assertPredicate((*i).assertion[0], false); - } else { - Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; - m->assertPredicate(*i, true); +void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { + if(fullModel) { + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + if((*i).assertion.getKind() == kind::NOT) { + Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; + m->assertPredicate((*i).assertion[0], false); + } else { + Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; + m->assertPredicate(*i, true); + } } } } |