diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-11-13 11:23:49 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-13 13:23:49 -0600 |
| commit | 91050c4da5d2ed0b22bf935c09c46184f6fde77e (patch) | |
| tree | 00a8ae99e9e5fe7e119d3dcce0c38cff65411db6 /src/printer/smt2 | |
| parent | 74be116f3956dab6be0b8e3e18f723957a351fbf (diff) | |
Model declarations printing options (#5432)
This PR relates to #4987 .
Our plan is to:
delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.
The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.
Diffstat (limited to 'src/printer/smt2')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index feef73217..d44842633 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1365,7 +1365,8 @@ void Smt2Printer::toStream(std::ostream& out, else { std::vector<Node> elements = theory_model->getDomainElements(tn); - if (options::modelUninterpDtEnum()) + if (options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DtEnum) { if (isVariant_2_6(d_variant)) { @@ -1385,7 +1386,11 @@ void Smt2Printer::toStream(std::ostream& out, { // print the cardinality out << "; cardinality of " << tn << " is " << elements.size() << endl; - out << (*dtc) << endl; + if (options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DeclSortAndFun) + { + out << (*dtc) << endl; + } // print the representatives for (const Node& trn : elements) { @@ -1432,7 +1437,9 @@ void Smt2Printer::toStream(std::ostream& out, } else { - if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) + if (options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DtEnum + && val.getKind() == kind::STORE) { TypeNode tn = val[1].getType(); const std::vector<Node>* type_refs = |