summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp7
-rw-r--r--src/printer/cvc/cvc_printer.cpp31
-rw-r--r--src/printer/smt2/smt2_printer.cpp33
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)";
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback