diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 49 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 98 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 | ||||
-rw-r--r-- | src/printer/printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.h | 2 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 2 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 110 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 2 |
10 files changed, 211 insertions, 60 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 5863ded9f..082765765 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -112,9 +112,12 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<QuitCommand>(out, c) || + tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || - tryToStream<DeclarationCommand>(out, c) || + tryToStream<DeclareFunctionCommand>(out, c) || tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DeclareTypeCommand>(out, c) || + tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || @@ -126,7 +129,8 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c)) { + tryToStream<DatatypeDeclarationCommand>(out, c) || + tryToStream<CommentCommand>(out, c)) { return; } @@ -167,6 +171,16 @@ static void toStream(std::ostream& out, const QuitCommand* c) { out << "Quit()"; } +static void toStream(std::ostream& out, const DeclarationSequence* c) { + out << "DeclarationSequence[" << endl; + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } + out << "]"; +} + static void toStream(std::ostream& out, const CommandSequence* c) { out << "CommandSequence[" << endl; for(CommandSequence::const_iterator i = c->begin(); @@ -177,13 +191,8 @@ static void toStream(std::ostream& out, const CommandSequence* c) { out << "]"; } -static void toStream(std::ostream& out, const DeclarationCommand* c) { - const vector<string>& declaredSymbols = c->getDeclaredSymbols(); - out << "Declare(["; - copy( declaredSymbols.begin(), declaredSymbols.end() - 1, - ostream_iterator<string>(out, ", ") ); - out << declaredSymbols.back(); - out << "])"; +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { + out << "Declare(" << c->getSymbol() << "," << c->getType() << ")"; } static void toStream(std::ostream& out, const DefineFunctionCommand* c) { @@ -199,6 +208,22 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "], << " << formula << " >> )"; } +static void toStream(std::ostream& out, const DeclareTypeCommand* c) { + out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << "," + << c->getType() << ")"; +} + +static void toStream(std::ostream& out, const DefineTypeCommand* c) { + const vector<Type>& params = c->getParameters(); + out << "DefineType(" << c->getSymbol() << ",["; + if(params.size() > 0) { + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(out, ", ") ); + out << params.back(); + } + out << "]," << c->getType() << ")"; +} + static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); @@ -252,6 +277,10 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { out << "])"; } +static void toStream(std::ostream& out, const CommentCommand* c) { + out << "CommentCommand([" << c->getComment() << "])"; +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { if(typeid(*c) == typeid(T)) { diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index ddc3c50b8..69c39915b 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8e089a8a3..0f3d635bd 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -28,6 +28,7 @@ #include <typeinfo> #include <algorithm> #include <iterator> +#include <stack> using namespace std; @@ -172,6 +173,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { switch(n.getKind()) { + case kind::SORT_TYPE: { + std::string name; + if(n.getAttribute(expr::VarNameAttr(), name)) { + out << name; + } else { + goto default_case; + } + break; + } case kind::BITVECTOR_EXTRACT: out << n[0] << n.getOperator().getConst<BitVectorExtract>(); break; @@ -192,6 +202,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, break; default: + default_case: out << n.getOperator(); if(n.getNumChildren() > 0) { out << '('; @@ -231,9 +242,24 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::SELECT: out << n[0] << '[' << n[1] << ']'; break; - case kind::STORE: - out << n[0] << " WITH [" << n[1] << "] = " << n[2]; + case kind::STORE: { + stack<TNode> stk; + stk.push(n); + while(stk.top()[0].getKind() == kind::STORE) { + stk.push(stk.top()[0]); + } + out << '('; + TNode x = stk.top(); + out << x[0] << " WITH [" << x[1] << "] := " << x[2]; + stk.pop(); + while(!stk.empty()) { + x = stk.top(); + out << ", [" << x[1] << "] := " << x[2]; + stk.pop(); + } + out << ')'; break; + } case kind::TUPLE_TYPE: out << '['; @@ -301,7 +327,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, // infix binary operator out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')'; } else if(n.getKind() == kind::AND || - n.getKind() == kind::OR) { + n.getKind() == kind::OR || + n.getKind() == kind::PLUS || + n.getKind() == kind::MULT) { // infix N-ary operator TNode::iterator i = n.begin(); out << '(' << *i++; @@ -347,9 +375,12 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<QuitCommand>(out, c) || + tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || - tryToStream<DeclarationCommand>(out, c) || + tryToStream<DeclareFunctionCommand>(out, c) || tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DeclareTypeCommand>(out, c) || + tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || @@ -361,7 +392,8 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c)) { + tryToStream<DatatypeDeclarationCommand>(out, c) || + tryToStream<CommentCommand>(out, c)) { return; } @@ -385,16 +417,22 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "CHECKSAT " << e << ";"; + } else { + out << "CHECKSAT;"; } - out << "CHECKSAT;"; } static void toStream(std::ostream& out, const QueryCommand* c) { - out << "QUERY " << c->getExpr() << ";"; + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "QUERY " << e << ";"; + } else { + out << "QUERY TRUE;"; + } } static void toStream(std::ostream& out, const QuitCommand* c) { - Unhandled("quit command"); + //out << "EXIT;"; } static void toStream(std::ostream& out, const CommandSequence* c) { @@ -405,14 +443,22 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclarationCommand* c) { - const vector<string>& declaredSymbols = c->getDeclaredSymbols(); - Type declaredType = c->getDeclaredType(); - Assert(declaredSymbols.size() > 0); - copy( declaredSymbols.begin(), declaredSymbols.end() - 1, - ostream_iterator<string>(out, ", ") ); - out << declaredSymbols.back(); - out << " : " << declaredType << ";"; +static void toStream(std::ostream& out, const DeclarationSequence* c) { + DeclarationSequence::const_iterator i = c->begin(); + for(;;) { + DeclarationDefinitionCommand* dd = + static_cast<DeclarationDefinitionCommand*>(*i++); + if(i != c->end()) { + out << dd->getSymbol() << ", "; + } else { + out << *dd; + break; + } + } +} + +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { + out << c->getSymbol() << " : " << c->getType() << ";"; } static void toStream(std::ostream& out, const DefineFunctionCommand* c) { @@ -430,6 +476,22 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "): " << formula << ";"; } +static void toStream(std::ostream& out, const DeclareTypeCommand* c) { + if(c->getArity() > 0) { + Unhandled("Don't know how to print parameterized type declaration " + "in CVC language:\n%s", c->toString().c_str()); + } + out << c->getSymbol() << " : TYPE;"; +} + +static void toStream(std::ostream& out, const DefineTypeCommand* c) { + if(c->getParameters().size() > 0) { + Unhandled("Don't know how to print parameterized type definition " + "in CVC language:\n%s", c->toString().c_str()); + } + out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; +} + static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { toStream(out, static_cast<const DefineFunctionCommand*>(c)); } @@ -484,6 +546,10 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { } } +static void toStream(std::ostream& out, const CommentCommand* c) { + out << "% " << c->getComment(); +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { if(typeid(*c) == typeid(T)) { diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index d794c82e8..fd478dbe5 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index ca5935bec..6714d355e 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/printer.h b/src/printer/printer.h index eae2fc48f..7294ab231 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index de22a04c1..ed7f8febf 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 058a6b18c..14d6c09e1 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5ce571904..5758b1101 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -23,6 +23,8 @@ #include <string> #include <typeinfo> +#include "util/boolean_simplification.h" + using namespace std; namespace CVC4 { @@ -64,6 +66,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // constant if(n.getMetaKind() == kind::metakind::CONSTANT) { switch(n.getKind()) { + case kind::TYPE_CONSTANT: + switch(n.getConst<TypeConstant>()) { + case BOOLEAN_TYPE: out << "Boolean"; break; + case REAL_TYPE: out << "Real"; break; + case INTEGER_TYPE: out << "Int"; break; + default: + // fall back on whatever operator<< does on underlying type; we + // might luck out and be SMT-LIB v2 compliant + kind::metakind::NodeValueConstPrinter::toStream(out, n); + } + break; case kind::BITVECTOR_TYPE: out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")"; break; @@ -91,11 +104,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } + if(n.getKind() == kind::SORT_TYPE) { + std::string name; + if(n.getAttribute(expr::VarNameAttr(), name)) { + out << name; + return; + } + } + bool stillNeedToPrintParams = true; // operator out << '('; switch(n.getKind()) { // builtin theory + case kind::APPLY: break; case kind::EQUAL: out << "= "; break; case kind::DISTINCT: out << "distinct "; break; case kind::TUPLE: break; @@ -111,7 +133,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // uf theory case kind::APPLY_UF: break; - case kind::SORT_TYPE: break; // arith theory case kind::PLUS: out << "+ "; break; @@ -127,6 +148,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // arrays theory case kind::SELECT: out << "select "; break; case kind::STORE: out << "store "; break; + case kind::ARRAY_TYPE: out << "Array "; break; // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; @@ -253,8 +275,10 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<QueryCommand>(out, c) || tryToStream<QuitCommand>(out, c) || tryToStream<CommandSequence>(out, c) || - tryToStream<DeclarationCommand>(out, c) || + tryToStream<DeclareFunctionCommand>(out, c) || tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DeclareTypeCommand>(out, c) || + tryToStream<DefineTypeCommand>(out, c) || tryToStream<DefineNamedFunctionCommand>(out, c) || tryToStream<SimplifyCommand>(out, c) || tryToStream<GetValueCommand>(out, c) || @@ -266,7 +290,8 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || - tryToStream<DatatypeDeclarationCommand>(out, c)) { + tryToStream<DatatypeDeclarationCommand>(out, c) || + tryToStream<CommentCommand>(out, c)) { return; } @@ -289,13 +314,25 @@ static void toStream(std::ostream& out, const PopCommand* c) { static void toStream(std::ostream& out, const CheckSatCommand* c) { BoolExpr e = c->getExpr(); if(!e.isNull()) { - out << "(assert " << e << ")"; + out << PushCommand() << endl + << AssertCommand(e) << endl + << CheckSatCommand() << endl + << PopCommand() << endl; + } else { + out << "(check-sat)"; } - out << "(check-sat)"; } static void toStream(std::ostream& out, const QueryCommand* c) { - Unhandled("query command"); + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << PushCommand() << endl + << AssertCommand(BooleanSimplification::negate(e)) << endl + << CheckSatCommand() << endl + << PopCommand() << endl; + } else { + out << "(check-sat)"; + } } static void toStream(std::ostream& out, const QuitCommand* c) { @@ -310,26 +347,21 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclarationCommand* c) { - const vector<string>& declaredSymbols = c->getDeclaredSymbols(); - Type declaredType = c->getDeclaredType(); - for(vector<string>::const_iterator i = declaredSymbols.begin(); - i != declaredSymbols.end(); - ++i) { - if(declaredType.isFunction()) { - FunctionType ft = declaredType; - out << "(declare-fun " << *i << " ("; - const vector<Type> argTypes = ft.getArgTypes(); - if(argTypes.size() > 0) { - copy( argTypes.begin(), argTypes.end() - 1, - ostream_iterator<Type>(out, " ") ); - out << argTypes.back(); - } - out << ") " << ft.getRangeType() << ")"; - } else { - out << "(declare-fun " << *i << " () " << declaredType << ")"; +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { + Type type = c->getType(); + out << "(declare-fun " << c->getSymbol() << " ("; + if(type.isFunction()) { + FunctionType ft = type; + const vector<Type> argTypes = ft.getArgTypes(); + if(argTypes.size() > 0) { + copy( argTypes.begin(), argTypes.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << argTypes.back(); } + type = ft.getRangeType(); } + + out << ") " << type << ")"; } static void toStream(std::ostream& out, const DefineFunctionCommand* c) { @@ -337,14 +369,34 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); out << "(define-fun " << func << " ("; - for(vector<Expr>::const_iterator i = formals.begin(); - i != formals.end(); - ++i) { + vector<Expr>::const_iterator i = formals.begin(); + for(;;) { out << "(" << (*i) << " " << (*i).getType() << ")"; + ++i; + if(i != formals.end()) { + out << " "; + } else { + break; + } } out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; } +static void toStream(std::ostream& out, const DeclareTypeCommand* c) { + out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")"; +} + +static void toStream(std::ostream& out, const DefineTypeCommand* c) { + const vector<Type>& params = c->getParameters(); + out << "(define-sort " << c->getSymbol() << " ("; + if(params.size() > 0) { + copy( params.begin(), params.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << params.back(); + } + out << ") " << c->getType() << ")"; +} + static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); @@ -406,6 +458,10 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { Unhandled("datatype declaration command"); } +static void toStream(std::ostream& out, const CommentCommand* c) { + out << "(set-info :notes \"" << c->getComment() << "\")"; +} + template <class T> static bool tryToStream(std::ostream& out, const Command* c) { if(typeid(*c) == typeid(T)) { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 4bae8a2e1..2086370ae 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing |