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/printer/smt2/smt2_printer.cpp | |
parent | 200585e3ae407b138b0cec0b2930dfc00d26c0bd (diff) |
Model API for domain elements (#3243)
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 65 |
1 files changed, 34 insertions, 31 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index dbb89d857..e02d308da 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1368,47 +1368,50 @@ void Smt2Printer::toStream(std::ostream& out, dynamic_cast<const DeclareTypeCommand*>(command)) { // print out the DeclareTypeCommand - TypeNode tn = TypeNode::fromType((*dtc).getType()); - const std::vector<Node>* type_refs = - theory_model->getRepSet()->getTypeRepsOrNull(tn); - if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr) + Type t = (*dtc).getType(); + if (!t.isSort()) { - if (isVariant_2_6(d_variant)) - { - out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) ("; - } - else - { - out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " "; - } - for (Node type_ref : *type_refs) - { - out << "(" << type_ref << ")"; - } - out << ")))" << endl; + out << (*dtc) << endl; } - else if (tn.isSort() && type_refs != nullptr) + else { - // print the cardinality - out << "; cardinality of " << tn << " is " << type_refs->size() << endl; - out << (*dtc) << endl; - // print the representatives - for (Node type_ref : *type_refs) + std::vector<Expr> elements = theory_model->getDomainElements(t); + if (options::modelUninterpDtEnum()) { - if (type_ref.isVar()) + if (isVariant_2_6(d_variant)) { - out << "(declare-fun " << quoteSymbol(type_ref) << " () " << tn << ")" - << endl; + out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) ("; } else { - out << "; rep: " << type_ref << endl; + out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " "; + } + for (const Expr& type_ref : elements) + { + out << "(" << type_ref << ")"; + } + out << ")))" << endl; + } + else + { + // print the cardinality + out << "; cardinality of " << t << " is " << elements.size() << endl; + out << (*dtc) << endl; + // print the representatives + for (const Expr& type_ref : elements) + { + Node trn = Node::fromExpr(type_ref); + if (trn.isVar()) + { + out << "(declare-fun " << quoteSymbol(trn) << " () " << t << ")" + << endl; + } + else + { + out << "; rep: " << trn << endl; + } } } - } - else - { - out << (*dtc) << endl; } } else if (const DeclareFunctionCommand* dfc = |