diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/model.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/model.h b/src/smt/model.h index b435fb5e2..06b616f9b 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -96,6 +96,14 @@ class Model { * is a predicate over t that indicates a property that t satisfies. */ virtual std::vector<std::pair<Expr, Expr> > getApproximations() const = 0; + /** get the domain elements for uninterpreted sort t + * + * This method gets the interpretation of an uninterpreted sort t. + * All models interpret uninterpreted sorts t as finite sets + * of domain elements v_1, ..., v_n. This method returns this list for t in + * this model. + */ + virtual std::vector<Expr> getDomainElements(Type t) const = 0; };/* class Model */ class ModelBuilder { |