diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-23 17:00:56 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-23 17:06:59 -0500 |
| commit | 04d8d1a3336633b0665a29d4a6e25828a6674a36 (patch) | |
| tree | 11c8fc21c16ed5b1f3b18b5f0f435fbba030701b /src/theory/quantifiers | |
| parent | 298f2b1deb9b304c67f0a12fa9b834265ed5255c (diff) | |
partially address bug 486: allow some model inspection of quantifiers
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index b1a7c9927..b5287fff4 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -93,7 +93,9 @@ Node TheoryQuantifiers::getValue(TNode n) { } void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){ - + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + m->assertPredicate(*i, true); + } } void TheoryQuantifiers::check(Effort e) { |