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/theory_model.cpp | |
parent | 200585e3ae407b138b0cec0b2930dfc00d26c0bd (diff) |
Model API for domain elements (#3243)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 21 |
1 files changed, 21 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 |