diff options
Diffstat (limited to 'src')
62 files changed, 144 insertions, 139 deletions
diff --git a/src/context/context.cpp b/src/context/context.cpp index a00364fe6..487dd97f8 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** context.cpp ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: barrett + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/context/context.h b/src/context/context.h index 2a4b2df2f..9e1eba644 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** context.h ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: barrett + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/context/context_mm.cpp b/src/context/context_mm.cpp index f282df96d..bc8e8772f 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -4,7 +4,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/context/context_mm.h b/src/context/context_mm.h index 8c870c603..45b2539ca 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/attr_type.h b/src/expr/attr_type.h index a4c8c41a9..966d69081 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/attr_var_name.h b/src/expr/attr_var_name.h index a17a3ba18..30f67fcf9 100644 --- a/src/expr/attr_var_name.h +++ b/src/expr/attr_var_name.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/expr.cpp b/src/expr/expr.cpp index 578eaf2f5..1df4012a6 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** expr.cpp ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): taking + ** Major contributors: taking + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/expr.h b/src/expr/expr.h index 0bbdcd09a..2210a6c0a 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -2,9 +2,9 @@ /** expr.h ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): taking, mdeters + ** Minor contributors (to current version): mdeters, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index ea1ade477..5b5f962bd 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** expr_manager.cpp ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/expr_manager.h b/src/expr/expr_manager.h index ace8b2d1c..97f2cd24d 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** expr_manager.h ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/kind.h b/src/expr/kind.h index 64991c71c..575a4790c 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -2,9 +2,9 @@ /** kind.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node.cpp b/src/expr/node.cpp index cd61b257f..8092348fe 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** node.cpp ** Original author: mdeters - ** Major contributors: dejan + ** Major contributors: taking, dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node.h b/src/expr/node.h index 46827d196..1d47f676b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_attribute.h b/src/expr/node_attribute.h index 021e64649..0d00a300f 100644 --- a/src/expr/node_attribute.h +++ b/src/expr/node_attribute.h @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_builder.cpp b/src/expr/node_builder.cpp index 9e24fa280..3629815b6 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_builder.h b/src/expr/node_builder.h index 77ff05ab5..1411024a9 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_manager.cpp b/src/expr/node_manager.cpp index c9a819751..df49800b6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_manager.h b/src/expr/node_manager.h index 3d95a4369..3c8dbdea7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** node_manager.h ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** Major contributors: none + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_value.cpp b/src/expr/node_value.cpp index 554655573..781747542 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/expr/node_value.h b/src/expr/node_value.h index 847b6b153..bf8b7cd79 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/include/cvc4_config.h b/src/include/cvc4_config.h index 9cf9a182b..bda26ebe0 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/about.h b/src/main/about.h index ec6f3dced..d00b1eaec 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/getopt.cpp b/src/main/getopt.cpp index 388e58a3b..6eb70a3e1 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): barrett, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/main.cpp b/src/main/main.cpp index 387d5ca97..02ebe8deb 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -4,7 +4,7 @@ ** Major contributors: barrett, dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/main.h b/src/main/main.h index c44cd9d67..9b2f4fcbe 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/usage.h b/src/main/usage.h index e9d8aa983..f6c089f1d 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/main/util.cpp b/src/main/util.cpp index 0b33b145d..df4ab803d 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 171da47e8..053eb8a11 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** antlr_parser.cpp ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): cconway, mdeters + ** Major contributors: mdeters, cconway + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/antlr_parser.h b/src/parser/antlr_parser.h index 0c6deb95a..aa32e4193 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** antlr_parser.h ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): mdeters, cconway + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index db40be3a8..2452b1002 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -1,16 +1,17 @@ -/* cvc_lexer.g - * Original author: dejan - * Major contributors: - * Minor contributors (to current version): none - * This file is part of the CVC4 prototype. - * Copyright (c) 2009 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 - * information. - * - * Lexer for CVC presentation language. - */ +/* ******************* -*- C++ -*- */ +/* cvc_lexer.g + ** Original author: dejan + ** Major contributors: mdeters + ** Minor contributors (to current version): cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 + ** information. + ** + ** Lexer for CVC presentation language. + **/ options { language = "Cpp"; // C++ output for antlr diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index ce61deae2..5832847fc 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -1,16 +1,18 @@ -/* cvc_parser.g - * Original author: dejan - * Major contributors: - * Minor contributors (to current version): none - * This file is part of the CVC4 prototype. - * Copyright (c) 2009 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 - * information. - * - * Parser for CVC presentation language. - */ +/* ******************* -*- C++ -*- */ +/* cvc_parser.g + ** Original author: dejan + ** Major contributors: mdeters + ** Minor contributors (to current version): cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 + ** information. + ** + ** + ** Parser for CVC presentation language. + **/ header "post_include_hpp" { #include "parser/antlr_parser.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 2f9ac6724..6a70b5181 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/parser.h b/src/parser/parser.h index 4f0502f24..98c7267c6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/parser_exception.h b/src/parser/parser_exception.h index 3504eeba2..85d50ba51 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index f1c01ea05..6c7e4be9d 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -1,16 +1,17 @@ -/* smt_lexer.g - * Original author: dejan - * Major contributors: - * Minor contributors (to current version): none - * This file is part of the CVC4 prototype. - * Copyright (c) 2009 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 - * information. - * - * Lexer for SMT-LIB input language. - */ +/* ******************* -*- C++ -*- */ +/* smt_lexer.g + ** Original author: dejan + ** Major contributors: cconway, mdeters + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Lexer for SMT-LIB input language. + **/ options { language = "Cpp"; // C++ output for antlr diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 65ebbb65a..fe98063cc 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -1,16 +1,17 @@ -/* smt_parser.g - * Original author: dejan - * Major contributors: - * Minor contributors (to current version): none - * This file is part of the CVC4 prototype. - * Copyright (c) 2009 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 - * information. - * - * Parser for SMT-LIB input language. - */ +/* ******************* -*- C++ -*- */ +/* smt_parser.g + ** Original author: dejan + ** Major contributors: mdeters, cconway + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Parser for SMT-LIB input language. + **/ header "post_include_hpp" { #include "parser/antlr_parser.h" diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index be2a958b8..7dc3783a5 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -4,7 +4,7 @@ ** Major contributors: dejan, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/cnf_conversion.h b/src/prop/cnf_conversion.h index 1d0ac50bb..0adbda2db 100644 --- a/src/prop/cnf_conversion.h +++ b/src/prop/cnf_conversion.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** cnf_conversion.h - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e758301d4..79182617e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** cnf_stream.cpp ** Original author: taking - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/cnf_stream.h b/src/prop/cnf_stream.h index 247a5b096..9be5efcd3 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** cnf_stream.h ** Original author: taking - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8485a6e32..047daace8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** prop_engine.cpp ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Major contributors: taking + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/prop_engine.h b/src/prop/prop_engine.h index 181c0288e..15664be75 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,10 +1,10 @@ /********************* -*- C++ -*- */ /** prop_engine.h ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/prop/sat.h b/src/prop/sat.h index 9e216b126..9a22dfb29 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e4a54b694..2d36da0f1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2,9 +2,9 @@ /** smt_engine.cpp ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/smt/smt_engine.h b/src/smt/smt_engine.h index 48365e129..904275c49 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -2,9 +2,9 @@ /** smt_engine.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/theory/interrupted.h b/src/theory/interrupted.h index 03bf466c9..17b54adda 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -1,6 +1,6 @@ /********************* -*- C++ -*- */ /** interrupted.h - ** Original author: + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 42e68b7a9..298be12bf 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -1,6 +1,6 @@ /********************* -*- C++ -*- */ /** output_channel.h - ** Original author: + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 337649039..c798b3d0a 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/Assert.h b/src/util/Assert.h index fa05ecaa5..7d2785d73 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/command.cpp b/src/util/command.cpp index f5a694a73..58f8b41bb 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/command.h b/src/util/command.h index 15104a5ea..81af801d1 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -4,7 +4,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/debug.h b/src/util/debug.h index 800106764..e99b1c48a 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/decision_engine.cpp b/src/util/decision_engine.cpp index 36f99f4ac..b163879b8 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/decision_engine.h b/src/util/decision_engine.h index 58f9400b5..a2392c104 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/exception.h b/src/util/exception.h index 8481a8504..8401b041e 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/literal.h b/src/util/literal.h index 921a9ef0d..b246d1289 100644 --- a/src/util/literal.h +++ b/src/util/literal.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/model.h b/src/util/model.h index b79032221..2d2419d0f 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/options.h b/src/util/options.h index ff156b595..82552553f 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -2,9 +2,9 @@ /** options.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/output.cpp b/src/util/output.cpp index b42fc77be..fb48a23a5 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/output.h b/src/util/output.h index 6a6c76d83..d11725fc5 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/result.h b/src/util/result.h index d4980c776..cac72aba7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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/util/unique_id.h b/src/util/unique_id.h index 633a544f0..8b5e1f31e 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -4,7 +4,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010 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 |