diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-05 21:40:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-05 21:40:50 -0500 |
| commit | dbb5fdf2f295f231da050a59c2ab63cf4742a97c (patch) | |
| tree | 5d11d5f5ec21126e022f2652a0fe9faca3856a13 /src/smt/model.h | |
| parent | 200585e3ae407b138b0cec0b2930dfc00d26c0bd (diff) | |
Model API for domain elements (#3243)
Diffstat (limited to 'src/smt/model.h')
| -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 { |