diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 31 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 33 |
3 files changed, 41 insertions, 30 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 39d76728a..85742feef 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -152,6 +152,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || @@ -187,7 +188,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ - + out << "Model()"; } static void toStream(std::ostream& out, const EmptyCommand* c) throw() { @@ -293,6 +294,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " >> )"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "GetModel()"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "GetAssignment()"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 5803ad23f..7f66d6fa0 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -98,7 +98,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo if(types) { // print the whole type, but not *its* type out << ":"; - n.getType().toStream(out, -1, false, language::output::LANG_CVC4); + n.getType().toStream(out, -1, false, false, language::output::LANG_CVC4); } return; } @@ -164,10 +164,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; default: - Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl; - out << n.getKind(); - break; + // fall back on whatever operator<< does on underlying type; we + // might luck out and print something reasonable + kind::metakind::NodeValueConstPrinter::toStream(out, n); } + return; } @@ -213,6 +214,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case kind::TUPLE: // no-op break; + case kind::LAMBDA: + op << "LAMBDA"; + opType = PREFIX; + break; case kind::APPLY: toStream(op, n.getOperator(), depth, types, true); break; @@ -225,6 +230,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } } break; + // BOOL case kind::AND: op << "AND"; @@ -691,6 +697,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || @@ -768,17 +775,7 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) }else{ out << tn; } - out << " = "; - if( tn.isFunction() || tn.isPredicate() ){ - out << "LAMBDA ("; - for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ - if( i>0 ) out << ", "; - out << "$x" << (i+1) << " : " << tn[i]; - } - out << "): "; - } - out << tm->getValue( n ); - out << ";" << std::endl; + out << " = " << tm->getValue( n ) << ";" << std::endl; /* //for table format (work in progress) @@ -920,6 +917,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " ))"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "% (get-model)"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "% (get-assignment)"; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9400b7732..8356f9e49 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -177,6 +177,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << n.getConst<Datatype>().getName(); break; + case kind::UNINTERPRETED_CONSTANT: { + const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>(); + out << '@' << uc; + break; + } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -480,6 +486,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || + tryToStream<GetModelCommand>(out, c) || tryToStream<GetAssignmentCommand>(out, c) || tryToStream<GetAssertionsCommand>(out, c) || tryToStream<SetBenchmarkStatusCommand>(out, c) || @@ -546,21 +553,15 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } }else if( c_type==Model::COMMAND_DECLARE_FUN ){ Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); - TypeNode tn = n.getType(); - out << "(define-fun " << n << " ("; - if( tn.isFunction() || tn.isPredicate() ){ - for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ - if( i>0 ) out << " "; - out << "($x" << (i+1) << " " << tn[i] << ")"; - } - out << ") " << tn.getRangeType(); - }else{ - out << ") " << tn; + Node val = tm->getValue( n ); + if(val.getKind() == kind::LAMBDA) { + out << "(define-fun " << n << " " << val[0] + << " " << n.getType().getRangeType() + << " " << val[1] << ")" << std::endl; + } else { + out << "(define-fun " << n << " () " + << n.getType() << " " << val << ")" << std::endl; } - out << " "; - out << tm->getValue( n ); - out << ")" << std::endl; - /* //for table format (work in progress) bool printedModel = false; @@ -713,6 +714,10 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << " ))"; } +static void toStream(std::ostream& out, const GetModelCommand* c) throw() { + out << "(get-model)"; +} + static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "(get-assignment)"; } |