diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-03 16:17:24 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-03 16:17:24 -0600 |
| commit | f81c51ca8af1c38126336f0c31a33fba72614dc1 (patch) | |
| tree | 33cab3539b7ecc7b81dcb6890fd612e15d528e70 /src/theory/uf/theory_uf.cpp | |
| parent | 72986ccf378dcdbede11d93c70601fdcc5b438ed (diff) | |
Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e4a3ac78c..35aee5305 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -246,7 +246,12 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { } void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ - m->assertEqualityEngine( &d_equalityEngine ); + set<Node> termSet; + + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + + m->assertEqualityEngine( &d_equalityEngine, &termSet ); // if( fullModel ){ // std::map< TypeNode, TypeEnumerator* > type_enums; // //must choose proper representatives |