summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp49
-rw-r--r--src/printer/ast/ast_printer.h2
-rw-r--r--src/printer/cvc/cvc_printer.cpp98
-rw-r--r--src/printer/cvc/cvc_printer.h2
-rw-r--r--src/printer/printer.cpp2
-rw-r--r--src/printer/printer.h2
-rw-r--r--src/printer/smt/smt_printer.cpp2
-rw-r--r--src/printer/smt/smt_printer.h2
-rw-r--r--src/printer/smt2/smt2_printer.cpp110
-rw-r--r--src/printer/smt2/smt2_printer.h2
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback