diff options
Diffstat (limited to 'src/expr')
41 files changed, 95 insertions, 66 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index cde261463..2cd884bba 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic, Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/attribute.h b/src/expr/attribute.h index d203b75ad..0bca760ef 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 0a3d389e7..dae11fd74 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index 3a52d7a89..45dc368a5 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9f502c2ea..16484a320 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -519,7 +519,9 @@ std::string DeclarationDefinitionCommand::getSymbol() const throw() { DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : DeclarationDefinitionCommand(id), d_func(func), - d_type(t) { + d_type(t), + d_printInModel(true), + d_printInModelSetByUser(false){ } Expr DeclareFunctionCommand::getFunction() const throw() { @@ -530,18 +532,37 @@ Type DeclareFunctionCommand::getType() const throw() { return d_type; } +bool DeclareFunctionCommand::getPrintInModel() const throw() { + return d_printInModel; +} + +bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { + return d_printInModelSetByUser; +} + +void DeclareFunctionCommand::setPrintInModel( bool p ) { + d_printInModel = p; + d_printInModelSetByUser = true; +} + void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = CommandSuccess::instance(); } Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), + d_type.exportTo(exprManager, variableMap)); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } Command* DeclareFunctionCommand::clone() const { - return new DeclareFunctionCommand(d_symbol, d_func, d_type); + DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); + dfc->d_printInModel = d_printInModel; + dfc->d_printInModelSetByUser = d_printInModelSetByUser; + return dfc; } std::string DeclareFunctionCommand::getCommandName() const throw() { diff --git a/src/expr/command.h b/src/expr/command.h index ed6be86de..606618d21 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -351,11 +351,16 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Expr d_func; Type d_type; + bool d_printInModel; + bool d_printInModelSetByUser; public: DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); ~DeclareFunctionCommand() throw() {} Expr getFunction() const throw(); Type getType() const throw(); + bool getPrintInModel() const throw(); + bool getPrintInModelSetByUser() const throw(); + void setPrintInModel( bool p ); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h index 93b8d460d..0c3b690b2 100644 --- a/src/expr/convenience_node_builders.h +++ b/src/expr/convenience_node_builders.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index ea5452eac..a8e8f04be 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 147ad3723..7ce51ecdd 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic, Christopher L. Conway ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f5e01d545..49094c593 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): Andrew Reynolds, Tim King, Christopher L. Conway + ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h index edfa4ba07..20977011c 100644 --- a/src/expr/expr_stream.h +++ b/src/expr/expr_stream.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 60f34867c..809064413 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -2,10 +2,10 @@ /*! \file expr_template.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: Dejan Jovanovic - ** Minor contributors (to current version): Tim King, Christopher L. Conway, Kshitij Bansal + ** Major contributors: Dejan Jovanovic, Kshitij Bansal + ** Minor contributors (to current version): Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 828b1923c..c5e8e77de 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/kind.i b/src/expr/kind.i index 95c350cf3..189c94f1f 100644 --- a/src/expr/kind.i +++ b/src/expr/kind.i @@ -8,6 +8,9 @@ %ignore CVC4::theory::operator++(TheoryId&); +%rename(apply) CVC4::kind::KindHashFunction::operator()(::CVC4::Kind) const; +%rename(apply) CVC4::TypeConstantHashFunction::operator()(TypeConstant) const; + %rename(Kind) CVC4::kind::Kind_t; %include "expr/kind.h" diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index e66f8c3b3..d3ed43e1c 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index b98a9a373..f93df4132 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index ea9a598c0..73f48ba04 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 34a72e106..deceda840 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node.h b/src/expr/node.h index ba139748e..35f94b9e3 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett, Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -439,7 +439,7 @@ public: * explicit Expr(Node) constructor---but that dirties the public * interface. */ - inline Expr toExpr(); + inline Expr toExpr() const; /** * Convert an Expr into a Node. @@ -1451,7 +1451,7 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, } template <bool ref_count> -inline Expr NodeTemplate<ref_count>::toExpr() { +inline Expr NodeTemplate<ref_count>::toExpr() const { assertTNodeNotExpired(); return NodeManager::currentNM()->toExpr(*this); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 0be97b24a..bea51b576 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4c61550b9..be3749021 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Dejan Jovanovic ** Major contributors: Morgan Deters - ** Minor contributors (to current version): ACSYS, Tim King, Christopher L. Conway + ** Minor contributors (to current version): ACSYS, Kshitij Bansal, Tim King, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f75ed9559..0aa222294 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Dejan Jovanovic ** Major contributors: Christopher L. Conway, Morgan Deters - ** Minor contributors (to current version): ACSYS, Tianyi Liang, Tim King + ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index ab55baa6e..41086ac21 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index e1cca1aef..401cc6152 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index d5b08bc18..8af056f62 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 85abca524..a6e7a6053 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Christopher L. Conway, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h index 1959c10c4..e2a92ade7 100644 --- a/src/expr/options_handlers.h +++ b/src/expr/options_handlers.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index e80e20fc8..6f47f9207 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h index beff1f8a9..acf0dccdd 100644 --- a/src/expr/pickle_data.h +++ b/src/expr/pickle_data.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -49,27 +49,27 @@ const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; const unsigned NBITS_CONSTBLOCKS = 32; struct BlockHeader { - unsigned d_kind : NBITS_KIND; + uint64_t d_kind : NBITS_KIND; };/* struct BlockHeader */ struct BlockHeaderOperator { - unsigned d_kind : NBITS_KIND; - unsigned d_nchildren : NBITS_NCHILDREN; - unsigned long : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); + uint64_t d_kind : NBITS_KIND; + uint64_t d_nchildren : NBITS_NCHILDREN; + uint64_t : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); };/* struct BlockHeaderOperator */ struct BlockHeaderConstant { - unsigned d_kind : NBITS_KIND; - unsigned long d_constblocks : NBITS_BLOCK - NBITS_KIND; + uint64_t d_kind : NBITS_KIND; + uint64_t d_constblocks : NBITS_BLOCK - NBITS_KIND; };/* struct BlockHeaderConstant */ struct BlockHeaderVariable { - unsigned d_kind : NBITS_KIND; - unsigned long : NBITS_BLOCK - NBITS_KIND; + uint64_t d_kind : NBITS_KIND; + uint64_t : NBITS_BLOCK - NBITS_KIND; };/* struct BlockHeaderVariable */ struct BlockBody { - unsigned long d_data : NBITS_BLOCK; + uint64_t d_data : NBITS_BLOCK; };/* struct BlockBody */ union Block { diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 065805a65..20e8859e3 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/pickler.h b/src/expr/pickler.h index afaf72600..f1cdd1c65 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index e36219a81..ce7d571db 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 63a7e299b..a9ab43cfe 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type.cpp b/src/expr/type.cpp index d0fe77aae..5810e1f4f 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Christopher L. Conway ** Major contributors: Dejan Jovanovic, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds + ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type.h b/src/expr/type.h index b4761e1d6..7674ff9d0 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Christopher L. Conway ** Major contributors: Dejan Jovanovic, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds + ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 491b44347..4b04adfc9 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 87361e991..061e1b4e0 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index eb5c8a6f8..9dbcb628f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -2,10 +2,10 @@ /*! \file type_node.cpp ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Tim King, Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett + ** Major contributors: Kshitij Bansal, Morgan Deters + ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type_node.h b/src/expr/type_node.h index a49ae31bf..289395a34 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Dejan Jovanovic ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Tim King + ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index fc68fcf8c..b54fd8809 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 416850622..59ce5c606 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |