diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
commit | c3e9112157320111c18b2984052abd9cd17127dc (patch) | |
tree | 1fa4ff944c86630034357994dd602486f609899e /src/theory/theory_engine.cpp | |
parent | c33c9d3699597abe2fbeaacb6799ba05f11f8e93 (diff) |
New model code, mostly workin
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0db71aba4..61b66ba3e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -590,6 +590,17 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ d_theoryTable[theoryId]->collectModelInfo( m, fullModel ); } } + // Get the Boolean variables + vector<TNode> boolVars; + d_propEngine->getBooleanVariables(boolVars); + vector<TNode>::iterator it, iend = boolVars.end(); + bool hasValue, value; + for (it = boolVars.begin(); it != iend; ++it) { + TNode var = *it; + hasValue = d_propEngine->hasValue(var, value); + // TODO: Assert that hasValue is true? + m->assertPredicate(var, hasValue ? value : false); + } } /* get model */ |