diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 53 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 53 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 |
3 files changed, 78 insertions, 29 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e0d4656f4..0206c4252 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -21,7 +21,9 @@ #include "expr/command.h" #include "theory/substitutions.h" #include "smt/smt_engine.h" +#include "smt/options.h" #include "theory/model.h" +#include "theory/arrays/theory_arrays_rewriter.h" #include <iostream> #include <vector> @@ -813,21 +815,34 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t theory::TheoryModel& tm = (theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); - if( tn.isSort() ){ - // print the cardinality - if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; + 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 << " " << 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) { + out << "| "; + } + out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " "; } - } - out << c << std::endl; - if( tn.isSort() ){ - // print the representatives - if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ - if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ - out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl; - }else{ - out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + out << std::endl << "END;" << std::endl; + } else { + if( tn.isSort() ){ + // print the cardinality + if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + out << "% cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; + } + } + out << c << std::endl; + if( tn.isSort() ){ + // print the representatives + if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ + if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ + out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl; + }else{ + out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + } } } } @@ -850,7 +865,15 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t }else{ out << tn; } - out << " = " << Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr())) << ";" << std::endl; + Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr())); + if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) { + TypeNode tn = val[1].getType(); + if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size()); + val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard ); + } + } + out << " = " << val << ";" << std::endl; /* //for table format (work in progress) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5821fbc77..8541ca6ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -27,8 +27,10 @@ #include "theory/substitutions.h" #include "util/language.h" #include "smt/smt_engine.h" +#include "smt/options.h" #include "theory/model.h" +#include "theory/arrays/theory_arrays_rewriter.h" using namespace std; @@ -541,25 +543,41 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ +void Smt2Printer::toStream(std::ostream& out, Model& m) const throw() { + out << "(model" << std::endl; + this->Printer::toStream(out, m); + out << ")" << std::endl; +} + + void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() { theory::TheoryModel& tm = (theory::TheoryModel&) m; if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); - if( tn.isSort() ){ - //print the cardinality - if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; + if( options::modelUninterpDtEnum() && tn.isSort() && + tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " "; + for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ + out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")"; } - } - out << c << std::endl; - if( tn.isSort() ){ - //print the representatives - if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ - for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ - if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ - out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl; - }else{ - out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + out << ")))" << std::endl; + } else { + if( tn.isSort() ){ + //print the cardinality + if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl; + } + } + out << c << std::endl; + if( tn.isSort() ){ + //print the representatives + if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){ + if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){ + out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl; + }else{ + out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + } } } } @@ -576,6 +594,13 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const << " " << n.getType().getRangeType() << " " << val[1] << ")" << std::endl; } else { + if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) { + TypeNode tn = val[1].getType(); + if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){ + Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size()); + val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard ); + } + } out << "(define-fun " << n << " () " << n.getType() << " " << val << ")" << std::endl; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index c6d932457..32a0c94ba 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -30,6 +30,7 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); void toStream(std::ostream& out, Model& m, const Command* c) const throw(); + void toStream(std::ostream& out, Model& m) const throw(); public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); |