From 91050c4da5d2ed0b22bf935c09c46184f6fde77e Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 13 Nov 2020 11:23:49 -0800 Subject: 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. --- src/printer/cvc/cvc_printer.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/printer/cvc') diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 236c87b91..8b252d0ea 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1076,8 +1076,8 @@ void DeclareTypeNodeCommandToStream(std::ostream& out, TypeNode type_node = command.getType(); const std::vector* type_reps = model.getRepSet()->getTypeRepsOrNull(type_node); - if (options::modelUninterpDtEnum() && type_node.isSort() - && type_reps != nullptr) + if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum + && type_node.isSort() && type_reps != nullptr) { out << "DATATYPE" << std::endl; out << " " << command.getSymbol() << " = "; @@ -1147,7 +1147,8 @@ void DeclareFunctionNodeCommandToStream( // We get the value from the theory model directly, which notice // does not have to go through the standard SmtEngine::getValue interface. Node val = model.getValue(n); - if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) + if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum + && val.getKind() == kind::STORE) { TypeNode type_node = val[1].getType(); if (tn.isSort()) -- cgit v1.2.3