diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 23:57:56 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 23:57:56 +0100 |
commit | 9d677333439c15677b6891ee8f6bd368a5df9f0a (patch) | |
tree | 07768d701e98e3ec39b4a37fa40681e61658eb97 /src/theory/theory_model.h | |
parent | 081351e87edeb52facba0d0abc2e933433480444 (diff) |
Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder. Fix bug in fmf-empty-sorts.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 8ee4e843d..e609bf703 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -130,8 +130,10 @@ public: private: TypeSetMap d_typeSet; TypeToTypeEnumMap d_teMap; + TypeEnumeratorProperties * d_tep; public: + TypeSet() : d_tep(NULL) {} ~TypeSet() { iterator it; for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) { @@ -146,7 +148,7 @@ private: } } } - + void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; } void add(TypeNode t, TNode n) { iterator it = d_typeSet.find(t); @@ -175,7 +177,7 @@ private: TypeEnumerator* te; TypeToTypeEnumMap::iterator it = d_teMap.find(t); if (it == d_teMap.end()) { - te = new TypeEnumerator(t); + te = new TypeEnumerator(t, d_tep); d_teMap[t] = te; } else { |