diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 33 |
1 files changed, 19 insertions, 14 deletions
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)"; } |