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/theory | |
| parent | 200585e3ae407b138b0cec0b2930dfc00d26c0bd (diff) | |
Model API for domain elements (#3243)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_model.cpp | 21 | ||||
| -rw-r--r-- | src/theory/theory_model.h | 2 |
2 files changed, 23 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 8d6511854..168dc4c62 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -117,6 +117,27 @@ std::vector<std::pair<Expr, Expr> > TheoryModel::getApproximations() const return approx; } +std::vector<Expr> TheoryModel::getDomainElements(Type t) const +{ + // must be an uninterpreted sort + Assert(t.isSort()); + std::vector<Expr> elements; + TypeNode tn = TypeNode::fromType(t); + const std::vector<Node>* type_refs = d_rep_set.getTypeRepsOrNull(tn); + if (type_refs == nullptr || type_refs->empty()) + { + // This is called when t is a sort that does not occur in this model. + // Sorts are always interpreted as non-empty, thus we add a single element. + elements.push_back(t.mkGroundTerm()); + return elements; + } + for (const Node& n : *type_refs) + { + elements.push_back(n.toExpr()); + } + return elements; +} + Node TheoryModel::getValue(TNode n) const { //apply substitutions diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index baf3a401c..b120b4501 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -239,6 +239,8 @@ public: bool hasApproximations() const override; /** get approximations */ std::vector<std::pair<Expr, Expr> > getApproximations() const override; + /** get domain elements for uninterpreted sort t */ + std::vector<Expr> getDomainElements(Type t) const override; /** get the representative set object */ const RepSet* getRepSet() const { return &d_rep_set; } /** get the representative set object (FIXME: remove this, see #1199) */ |