diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/printer/cvc | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/printer/cvc')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2cfeaafc1..524344612 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( options::modelUninterpDtEnum() && tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - out << "DATATYPE " << std::endl; + out << "DATATYPE" << std::endl; out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = "; for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ if (i>0) { @@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << ',' << endl; } const Datatype& dt = (*i).getDatatype(); - out << " " << dt.getName() << " = "; + out << " " << dt.getName(); + if(dt.isParametric()) { + out << '['; + for(size_t j = 0; j < dt.getNumParameters(); ++j) { + if(j > 0) { + out << ','; + } + out << dt.getParameter(j); + } + out << ']'; + } + out << " = "; bool firstConstructor = true; for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { if(! firstConstructor) { |