diff options
Diffstat (limited to 'src')
33 files changed, 89 insertions, 44 deletions
diff --git a/src/context/context.h b/src/context/context.h index 1af4480f9..403235bc9 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -2,7 +2,7 @@ /** context.h ** Original author: mdeters ** Major contributors: barrett - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 1d2705240..54500d0d5 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,7 +1,7 @@ -/********************* -*- C++ -*- */ +/********************* */ /** attribute.h ** Original author: mdeters - ** Major contributors: dejan + ** 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) diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 18c0fdbab..c29b7e448 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -1,8 +1,8 @@ /********************* */ /** expr.cpp ** Original author: dejan - ** Major contributors: taking - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr.h b/src/expr/expr.h index dd4d0e9d7..096094aff 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -2,7 +2,7 @@ /** expr.h ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): mdeters, taking + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 506c118bc..71368c101 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -1,7 +1,7 @@ /********************* */ /** expr_manager.cpp ** Original author: dejan - ** Major contributors: mdeters + ** 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) diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index edfc18c8d..d84cf76be 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -1,7 +1,7 @@ /********************* */ /** expr_manager.h ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: cconway, mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 79490d58e..90dd86712 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,8 +1,8 @@ /********************* */ /** node.cpp ** Original author: mdeters - ** Major contributors: taking, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 12a6d1732..c6aee3dea 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,8 +1,8 @@ /********************* */ /** node_manager.cpp ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Major contributors: dejan + ** 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 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 18a95f041..97f5ba9cd 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,8 +1,8 @@ /********************* */ /** node_manager.h ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): taking, dejan + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h index fe71a4d1a..0bf9b47cf 100644 --- a/src/expr/soft_node.h +++ b/src/expr/soft_node.h @@ -1,8 +1,8 @@ -/********************* -*- C++ -*- */ +/********************* */ /** soft_node.h ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type.cpp b/src/expr/type.cpp index d4662d420..368a3fe44 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -1,5 +1,5 @@ -/********************* -*- C++ -*- */ -/** type.h +/********************* */ +/** type.cpp ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none diff --git a/src/expr/type.h b/src/expr/type.h index 19d0c831e..fd485602e 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,8 +1,8 @@ -/********************* -*- C++ -*- */ +/********************* */ /** type.h ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 190f7bbf3..7ca889592 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -2,7 +2,7 @@ /** getopt.cpp ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan + ** Minor contributors (to current version): barrett, dejan, 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 diff --git a/src/main/main.cpp b/src/main/main.cpp index 6ebe895a5..a12c69df7 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -2,7 +2,7 @@ /** main.cpp ** Original author: mdeters ** Major contributors: barrett, dejan - ** Minor contributors (to current version): none + ** 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 diff --git a/src/main/usage.h b/src/main/usage.h index 9a8175e2a..6c44fef5a 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -2,7 +2,7 @@ /** usage.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** 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 diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 30fb33a32..0fdde07ff 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -1,8 +1,8 @@ /********************* */ /** antlr_parser.cpp ** Original author: dejan - ** Major contributors: mdeters, cconway - ** Minor contributors (to current version): none + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 0cdf9f36b..bfdc4c0f2 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -1,8 +1,8 @@ /* ******************* */ /* cvc_parser.g ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): cconway + ** Major contributors: cconway + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b9e2d576e..84796f093 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -2,7 +2,7 @@ /** parser.cpp ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** 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 diff --git a/src/parser/parser.h b/src/parser/parser.h index 170e1af31..da2c630ca 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -2,7 +2,7 @@ /** parser.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** 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 diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index d790a1c84..dd110c4c1 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -1,4 +1,4 @@ -/********************* -*- C++ -*- */ +/********************* */ /** symbol_table.h ** Original author: cconway ** Major contributors: dejan, mdeters diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 80a8819b9..5dd57610d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,8 +1,8 @@ /********************* */ /** prop_engine.cpp ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9aa1ecff8..d4007e73a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,8 +1,8 @@ /********************* */ /** prop_engine.h ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): dejan + ** Major contributors: taking, dejan + ** 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 diff --git a/src/prop/sat.h b/src/prop/sat.h index 350537d8f..a9696162a 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -1,7 +1,7 @@ /********************* */ /** sat.h ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** 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) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 36954ace4..bb3e8c058 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2,7 +2,7 @@ /** smt_engine.cpp ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0e7e951f8..838f9cd7a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -2,7 +2,7 @@ /** smt_engine.h ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/theory/theory.h b/src/theory/theory.h index dffc99053..831a185f8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -2,7 +2,7 @@ /** theory.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp index a22faf61e..cb7add487 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/ecdata.cpp @@ -1,3 +1,18 @@ +/********************* */ +/** ecdata.cpp + ** Original author: taking + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** [[ Add file-specific comments here ]] + **/ + #include "theory/uf/ecdata.h" using namespace CVC4; diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index fd0855bee..c8303a245 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -1,7 +1,7 @@ /********************* */ /** ecdata.h ** Original author: taking - ** Major contributors: barrett + ** 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) diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 840c7b51e..1f4d80b9b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -1,3 +1,18 @@ +/********************* */ +/** theory_uf.cpp + ** Original author: taking + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** [[ Add file-specific comments here ]] + **/ + #include "theory/uf/theory_uf.h" #include "theory/uf/ecdata.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 06b0ee4f8..0ab51ca2c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,3 +1,18 @@ +/********************* */ +/** theory_uf.h + ** Original author: taking + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** [[ Add file-specific comments here ]] + **/ + #ifndef __CVC4__THEORY__THEORY_UF_H #define __CVC4__THEORY__THEORY_UF_H diff --git a/src/util/configuration.h b/src/util/configuration.h index b761f1f22..20d00a5f8 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -2,7 +2,7 @@ /** configuration.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): taking + ** 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 diff --git a/src/util/options.h b/src/util/options.h index cad00a61b..404700a85 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,8 +1,8 @@ /********************* */ /** options.h ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking + ** Major contributors: cconway + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/output.h b/src/util/output.h index ad42416d8..d0db064f0 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -2,7 +2,7 @@ /** output.h ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences |