diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 158 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 3 | ||||
-rw-r--r-- | src/printer/printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 53 |
4 files changed, 128 insertions, 91 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 77d8f14de..8412ecc2c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -661,6 +661,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << n.getOperator().getConst<BitVectorExtract>(); opType = POSTFIX; break; + case kind::BITVECTOR_BITOF: + op << n.getOperator().getConst<BitVectorBitOf>(); + opType = POSTFIX; + break; case kind::BITVECTOR_REPEAT: out << "BVREPEAT("; toStream(out, n[0], depth, types, false); @@ -776,7 +780,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo }/* CvcPrinter::toStream(TNode) */ template <class T> -static bool tryToStream(std::ostream& out, const Command* c) throw(); +static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw(); void CvcPrinter::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { @@ -784,35 +788,35 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, expr::ExprPrintTypes::Scope ptScope(out, types); expr::ExprDag::Scope dagScope(out, dag); - if(tryToStream<AssertCommand>(out, c) || - tryToStream<PushCommand>(out, c) || - tryToStream<PopCommand>(out, c) || - tryToStream<CheckSatCommand>(out, c) || - tryToStream<QueryCommand>(out, c) || - tryToStream<QuitCommand>(out, c) || - tryToStream<DeclarationSequence>(out, c) || - tryToStream<CommandSequence>(out, c) || - tryToStream<DeclareFunctionCommand>(out, c) || - tryToStream<DeclareTypeCommand>(out, c) || - tryToStream<DefineTypeCommand>(out, c) || - tryToStream<DefineNamedFunctionCommand>(out, c) || - tryToStream<DefineFunctionCommand>(out, c) || - tryToStream<SimplifyCommand>(out, c) || - tryToStream<GetValueCommand>(out, c) || - tryToStream<GetModelCommand>(out, c) || - tryToStream<GetAssignmentCommand>(out, c) || - tryToStream<GetAssertionsCommand>(out, c) || - tryToStream<GetProofCommand>(out, c) || - tryToStream<SetBenchmarkStatusCommand>(out, c) || - tryToStream<SetBenchmarkLogicCommand>(out, c) || - tryToStream<SetInfoCommand>(out, c) || - tryToStream<GetInfoCommand>(out, c) || - tryToStream<SetOptionCommand>(out, c) || - tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c) || - tryToStream<CommentCommand>(out, c) || - tryToStream<EmptyCommand>(out, c) || - tryToStream<EchoCommand>(out, c)) { + if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) || + tryToStream<PushCommand>(out, c, d_cvc3Mode) || + tryToStream<PopCommand>(out, c, d_cvc3Mode) || + tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) || + tryToStream<QueryCommand>(out, c, d_cvc3Mode) || + tryToStream<QuitCommand>(out, c, d_cvc3Mode) || + tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) || + tryToStream<CommandSequence>(out, c, d_cvc3Mode) || + tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) || + tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) || + tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) || + tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) || + tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) || + tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) || + tryToStream<GetValueCommand>(out, c, d_cvc3Mode) || + tryToStream<GetModelCommand>(out, c, d_cvc3Mode) || + tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) || + tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) || + tryToStream<GetProofCommand>(out, c, d_cvc3Mode) || + tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) || + tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) || + tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) || + tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) || + tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) || + tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) || + tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) || + tryToStream<CommentCommand>(out, c, d_cvc3Mode) || + tryToStream<EmptyCommand>(out, c, d_cvc3Mode) || + tryToStream<EchoCommand>(out, c, d_cvc3Mode)) { return; } @@ -826,13 +830,13 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { } template <class T> -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); +static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw(); void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { - if(tryToStream<CommandSuccess>(out, s) || - tryToStream<CommandFailure>(out, s) || - tryToStream<CommandUnsupported>(out, s)) { + if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) || + tryToStream<CommandFailure>(out, s, d_cvc3Mode) || + tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)) { return; } @@ -933,41 +937,53 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c } } -static void toStream(std::ostream& out, const AssertCommand* c) throw() { +static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode) throw() { out << "ASSERT " << c->getExpr() << ";"; } -static void toStream(std::ostream& out, const PushCommand* c) throw() { +static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode) throw() { out << "PUSH;"; } -static void toStream(std::ostream& out, const PopCommand* c) throw() { +static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode) throw() { out << "POP;"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { +static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) throw() { Expr e = c->getExpr(); + if(cvc3Mode) { + out << "PUSH; "; + } if(!e.isNull()) { out << "CHECKSAT " << e << ";"; } else { out << "CHECKSAT;"; } + if(cvc3Mode) { + out << " POP;"; + } } -static void toStream(std::ostream& out, const QueryCommand* c) throw() { +static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) throw() { Expr e = c->getExpr(); + if(cvc3Mode) { + out << "PUSH; "; + } if(!e.isNull()) { out << "QUERY " << e << ";"; } else { out << "QUERY TRUE;"; } + if(cvc3Mode) { + out << " POP;"; + } } -static void toStream(std::ostream& out, const QuitCommand* c) throw() { +static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() { //out << "EXIT;"; } -static void toStream(std::ostream& out, const CommandSequence* c) throw() { +static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode) throw() { for(CommandSequence::const_iterator i = c->begin(); i != c->end(); ++i) { @@ -975,7 +991,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() { } } -static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { +static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3Mode) throw() { DeclarationSequence::const_iterator i = c->begin(); for(;;) { DeclarationDefinitionCommand* dd = @@ -989,11 +1005,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { } } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c, bool cvc3Mode) throw() { out << c->getSymbol() << " : " << c->getType() << ";"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { +static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc3Mode) throw() { Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -1012,7 +1028,7 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() out << formula << ";"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { +static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() { if(c->getArity() > 0) { out << "ERROR: Don't know how to print parameterized type declaration " "in CVC language:" << endl << c->toString() << endl; @@ -1021,7 +1037,7 @@ static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { } } -static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { +static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mode) throw() { if(c->getParameters().size() > 0) { out << "ERROR: Don't know how to print parameterized type definition " "in CVC language:" << endl << c->toString() << endl; @@ -1030,15 +1046,15 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { } } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { - toStream(out, static_cast<const DefineFunctionCommand*>(c)); +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() { + toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode); } -static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { +static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode) throw() { out << "TRANSFORM " << c->getTerm() << ";"; } -static void toStream(std::ostream& out, const GetValueCommand* c) throw() { +static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode) throw() { const vector<Expr>& terms = c->getTerms(); Assert(!terms.empty()); out << "GET_VALUE "; @@ -1046,51 +1062,51 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << terms.back() << ";"; } -static void toStream(std::ostream& out, const GetModelCommand* c) throw() { +static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode) throw() { out << "COUNTERMODEL;"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { +static void toStream(std::ostream& out, const GetAssignmentCommand* c, bool cvc3Mode) throw() { out << "% (get-assignment)"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { +static void toStream(std::ostream& out, const GetAssertionsCommand* c, bool cvc3Mode) throw() { out << "WHERE;"; } -static void toStream(std::ostream& out, const GetProofCommand* c) throw() { +static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode) throw() { out << "DUMP_PROOF;"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, bool cvc3Mode) throw() { out << "% (set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool cvc3Mode) throw() { out << "OPTION \"logic\" \"" << c->getLogic() << "\";"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { +static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() { out << "% (set-info " << c->getFlag() << " "; toStream(out, c->getSExpr()); out << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { +static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) throw() { out << "% (get-info " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { +static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() { out << "OPTION \"" << c->getFlag() << "\" "; toStream(out, c->getSExpr()); out << ";"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { +static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode) throw() { out << "% (get-option " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "DATATYPE" << endl; bool firstDatatype = true; @@ -1140,44 +1156,44 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << endl << "END;"; } -static void toStream(std::ostream& out, const CommentCommand* c) throw() { +static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() { out << "% " << c->getComment(); } -static void toStream(std::ostream& out, const EmptyCommand* c) throw() { +static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) throw() { } -static void toStream(std::ostream& out, const EchoCommand* c) throw() { +static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode) throw() { out << "ECHO \"" << c->getOutput() << "\";"; } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) throw() { +static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw() { if(typeid(*c) == typeid(T)) { - toStream(out, dynamic_cast<const T*>(c)); + toStream(out, dynamic_cast<const T*>(c), cvc3Mode); return true; } return false; } -static void toStream(std::ostream& out, const CommandSuccess* s) throw() { +static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) throw() { if(Command::printsuccess::getPrintSuccess(out)) { out << "OK" << endl; } } -static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { +static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mode) throw() { out << "UNSUPPORTED" << endl; } -static void toStream(std::ostream& out, const CommandFailure* s) throw() { +static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() { out << s->getMessage() << endl; } template <class T> -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { +static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw() { if(typeid(*s) == typeid(T)) { - toStream(out, dynamic_cast<const T*>(s)); + toStream(out, dynamic_cast<const T*>(s), cvc3Mode); return true; } return false; diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 15b04488d..ec08b36b1 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -28,10 +28,13 @@ namespace printer { namespace cvc { class CvcPrinter : public CVC4::Printer { + bool d_cvc3Mode; + void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw(); void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); public: using CVC4::Printer::toStream; + CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { } 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(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index a68c3ca7f..24b9f274d 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -37,7 +37,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { - case LANG_SMTLIB_V1: + case LANG_SMTLIB_V1: // TODO the printer return new printer::smt1::Smt1Printer(); case LANG_SMTLIB_V2: @@ -55,6 +55,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_AST: return new printer::ast::AstPrinter(); + case LANG_CVC3: + return new printer::cvc::CvcPrinter(/* cvc3-mode = */ true); + default: Unhandled(lang); } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bc2cb1ec9..270e0dba0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -250,6 +250,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::DISTINCT: out << smtKindString(k) << " "; break; case kind::CHAIN: break; case kind::TUPLE: break; + case kind::FUNCTION_TYPE: + for(size_t i = 0; i < n.getNumChildren() - 1; ++i) { + if(i > 0) { + out << ' '; + } + out << n[i]; + } + out << ") " << n[n.getNumChildren() - 1]; + return; case kind::SEXPR: break; // bool theory @@ -455,7 +464,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ) { out << '('; - toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0); out << ' '; out << (*i).getType(); // The following code do stange things @@ -759,9 +768,9 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { - out << "(model" << std::endl; + out << "(model" << endl; this->Printer::toStream(out, m); - out << ")" << std::endl; + out << ")" << endl; } @@ -775,23 +784,23 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) 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 << ")))" << std::endl; + out << ")))" << 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 << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl; } } - out << c << std::endl; + out << c << 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 " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << std::endl; + out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl; }else{ - out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl; + out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl; } } } @@ -812,7 +821,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) if(val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] << " " << n.getType().getRangeType() - << " " << val[1] << ")" << std::endl; + << " " << val[1] << ")" << endl; } else { if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) { TypeNode tn = val[1].getType(); @@ -822,7 +831,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } } out << "(define-fun " << n << " () " - << n.getType() << " " << val << ")" << std::endl; + << n.getType() << " " << val << ")" << endl; } /* //for table format (work in progress) @@ -848,7 +857,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } */ }else{ - out << c << std::endl; + out << c << endl; } } @@ -878,7 +887,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { out << PushCommand() << endl << AssertCommand(e) << endl << CheckSatCommand() << endl - << PopCommand() << endl; + << PopCommand(); } else { out << "(check-sat)"; } @@ -890,7 +899,7 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() { out << PushCommand() << endl << AssertCommand(BooleanSimplification::negate(e)) << endl << CheckSatCommand() << endl - << PopCommand() << endl; + << PopCommand(); } else { out << "(check-sat)"; } @@ -901,10 +910,16 @@ static void toStream(std::ostream& out, const QuitCommand* c) throw() { } static void toStream(std::ostream& out, const CommandSequence* c) throw() { - for(CommandSequence::const_iterator i = c->begin(); - i != c->end(); - ++i) { - out << *i << endl; + CommandSequence::const_iterator i = c->begin(); + if(i != c->end()) { + for(;;) { + out << *i; + if(++i != c->end()) { + out << endl; + } else { + break; + } + } } } @@ -988,7 +1003,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "(get-value ( "; const vector<Expr>& terms = c->getTerms(); copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " ")); - out << " ))"; + out << "))"; } static void toStream(std::ostream& out, const GetModelCommand* c) throw() { @@ -1050,7 +1065,7 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr const Datatype & d = i->getDatatype(); - out << "(" << maybeQuoteSymbol(d.getName()) << " "; + out << "(" << maybeQuoteSymbol(d.getName()) << " "; for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); ctor != ctor_end; ++ctor){ if( ctor!=d.begin() ) out << " "; |