diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
| commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
| tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) | |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 74d8269f9..5016bd87f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -73,6 +73,15 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { } +void TheoryQuantifiers::finishInit() +{ + // quantifiers are not evaluated in getModelValue + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setUnevaluatedKind(EXISTS); + tm->setUnevaluatedKind(FORALL); +} + void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; if( n.getKind()==FORALL ){ |