diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
| commit | a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 (patch) | |
| tree | 8b95b65fad71aab9b0baee4b6bfc976b731f9502 /src/util/util_model.h | |
| parent | dba60e91f02ae9ca3c3126c76d79a09c95f95a45 (diff) | |
fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const.
Diffstat (limited to 'src/util/util_model.h')
| -rw-r--r-- | src/util/util_model.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/util_model.h b/src/util/util_model.h index bb40c9ba4..e67485ce7 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -53,9 +53,9 @@ public: public: /** get value for expression */ - virtual Expr getValue(Expr expr) = 0; + virtual Expr getValue(Expr expr) const = 0; /** get cardinality for sort */ - virtual Cardinality getCardinality(Type t) = 0; + virtual Cardinality getCardinality(Type t) const = 0; };/* class Model */ class ModelBuilder { |