diff options
Diffstat (limited to 'src')
61 files changed, 306 insertions, 38 deletions
diff --git a/src/context/context.cpp b/src/context/context.cpp index 005c3bd6a..3635d0c07 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/context/context.h b/src/context/context.h index 6cc36ae9b..68667c223 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Context class and context manager. **/ #ifndef __CVC4__CONTEXT__CONTEXT_H diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 3b4089b25..d772b886f 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context_mm.cpp + ** Original author: barrett + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/context/context_mm.h b/src/context/context_mm.h index d48cbedc0..eeaa0a2c8 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** context_mm.h + ** Original author: barrett + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index 597be0fe7..7fa828237 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** attr_type.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Node attribute describing the type of a node. **/ #ifndef __CVC4__EXPR__ATTR_TYPE_H diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h index 13a2ec36f..a17a3ba18 100644 --- a/src/expr/attr_var_name.h +++ b/src/expr/attr_var_name.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** attr_type.h +/** attr_var_name.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The node attribute describing variable names. **/ #ifndef __CVC4__EXPR__ATTR_VAR_NAME_H diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index eacd1cb24..ee9334f3c 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -1,9 +1,17 @@ -/* - * expr.cpp - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr.cpp + ** Original author: dejan + ** Major contributors: 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) + ** 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 "expr/expr.h" #include "expr/node.h" diff --git a/src/expr/expr.h b/src/expr/expr.h index a0a646900..447c35f77 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -1,9 +1,17 @@ -/* - * expr.h - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): taking, mdeters + ** 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. + ** + ** Public-facing expression interface. + **/ #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index ea1649e12..ea1ade477 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** Original author: dejan + ** 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) + ** 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 ]] + **/ + /* * expr_manager.cpp * diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 645193ecf..ace8b2d1c 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -1,9 +1,17 @@ -/* - * expr_manager.h - * - * Created on: Dec 10, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** expr_manager.h + ** Original author: dejan + ** Major contributors: 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Public-facing expression manager interface. + **/ #ifndef __CVC4__EXPR_MANAGER_H #define __CVC4__EXPR_MANAGER_H diff --git a/src/expr/kind.h b/src/expr/kind.h index 624ab7337..ea9dbd662 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** kind.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Kinds of Nodes. **/ #ifndef __CVC4__KIND_H diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 334cf1b0e..9c73b982c 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node.h b/src/expr/node.h index aad0689bb..9bb138b21 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Reference-counted encapsulation of a pointer to an expression. + ** Reference-counted encapsulation of a pointer to node information. **/ #include "expr/node_value.h" diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h index 0b759efb4..021e64649 100644 --- a/src/expr/node_attribute.h +++ b/src/expr/node_attribute.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** expr_attribute.h +/** node_attribute.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Node attributes. **/ #ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 0a36421f2..9e24fa280 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_builder.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 63048c1ac..b974ecc67 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_builder.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A builder interface for nodes. **/ #ifndef __CVC4__NODE_BUILDER_H diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7e871d9c3..d752db88f 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_manager.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 643f09f11..827c6c1b7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_manager.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A manager for Nodes. **/ #ifndef __CVC4__NODE_MANAGER_H diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 42b7b05e4..6724b0771 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_value.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 75c694ec9..352be7d27 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** node_value.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index f1877781f..9cf9a182b 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc4_config.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Macros that should be defined everywhere during the building of + ** the libraries and driver binary. **/ #ifndef __CVC4_CONFIG_H diff --git a/src/main/about.h b/src/main/about.h index 592c09551..ec6f3dced 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** about.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 24c96f69a..c191b2a15 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** getopt.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/main/main.cpp b/src/main/main.cpp index 187a0f316..ba71b043f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** main.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/main/main.h b/src/main/main.h index 0141e2848..c44cd9d67 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** main.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/main/usage.h b/src/main/usage.h index d48c1c96d..e9d8aa983 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** usage.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/main/util.cpp b/src/main/util.cpp index 94a295d54..9bb96d853 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** util.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 1baaf2139..c42415c54 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** antlr_parser.cpp + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): cconway, mdeters + ** 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. + ** + ** [[ Add file-specific comments here ]] + **/ + /* * antlr_parser.cpp * diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index b2ef3f181..8a9dea5ad 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -1,9 +1,17 @@ -/* - * antlr_parser.h - * - * Created on: Nov 30, 2009 - * Author: dejan - */ +/********************* -*- C++ -*- */ +/** antlr_parser.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters, cconway + ** 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. + ** + ** Base for ANTLR parser classes. + **/ #ifndef CVC4_PARSER_H_ #define CVC4_PARSER_H_ diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp index adeb5761d..57d5e6c96 100644 --- a/src/parser/cvc/cvc_parser.cpp +++ b/src/parser/cvc/cvc_parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc_parser.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 9cb6b7594..82d659566 100644 --- a/src/parser/cvc/cvc_parser.h +++ b/src/parser/cvc/cvc_parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** cvc_parser.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8d4af5ba1..2ff409686 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.h b/src/parser/parser.h index 7755d65f0..b448cd2a6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index b2cf8bc55..3504eeba2 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** parser_exception.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Exception class. + ** Exception class for parse errors. **/ #ifndef __CVC4__PARSER__PARSER_EXCEPTION_H diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 65d36690c..8c5773e32 100644 --- a/src/parser/smt/smt_parser.cpp +++ b/src/parser/smt/smt_parser.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_parser.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index 6927888cf..21c278a37 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_parser.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_parser.h + ** Original author: mdeters + ** Major contributors: none + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 2c4f0e8b7..66d5727d6 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** symbol_table.h + ** Original author: cconway + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A symbol table for the parsers' use. **/ #ifndef __CVC4__PARSER__SYMBOL_TABLE_H diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index caf87428b..ffd335453 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ -/** prop_engine.h +/** prop_engine.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 21a6669d7..6cb818d10 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** prop_engine.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The PropEngine (proposiitonal engine); main interface point + ** between CVC4's SMT infrastructure and the SAT solver. **/ #ifndef __CVC4__PROP_ENGINE_H diff --git a/src/prop/sat.h b/src/prop/sat.h index 32ca9e983..9e216b126 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** sat.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** SAT Solver. **/ #ifndef __CVC4__PROP__SAT_H diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 23dc1153a..4c7f6a156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_engine.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index edcbdcca3..98cffb6de 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** smt_engine.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** SmtEngine: the main public entry point of libcvc4. **/ #ifndef __CVC4__SMT_ENGINE_H diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 024d192e6..c4b2b8d83 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Base for theory interface. **/ #include "theory/theory.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 21124375a..b695ca03d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Base of the theory interface. **/ #ifndef __CVC4__THEORY__THEORY_H diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6d0b9d91d..2289f2fea 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory_engine.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The theory engine. **/ #include "theory/theory_engine.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d6d8691b2..65a317433 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** theory_engine.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** The theory engine. **/ #ifndef __CVC4__THEORY_ENGINE_H diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index a86e2021a..337649039 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** Assert.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/util/Assert.h b/src/util/Assert.h index 26a1ee7d4..49c97e9b6 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** Assert.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/util/command.cpp b/src/util/command.cpp index 3911897f5..5a5b766cb 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -1,3 +1,18 @@ +/********************* -*- C++ -*- */ +/** command.cpp + ** Original author: mdeters + ** 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) + ** 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 ]] + **/ + /* * command.cpp * diff --git a/src/util/command.h b/src/util/command.h index 221c513f0..9cc009d01 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** command.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Implementation of the command pattern on SmtEngines. Generated by + ** the parser. **/ #ifndef __CVC4__COMMAND_H diff --git a/src/util/debug.h b/src/util/debug.h index 14dc0fbd1..800106764 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** debug.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,20 +10,27 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Debugging things. + ** + ** These are low-level assertions! Generally you should use + ** CVC4::Assert() instead (they throw an exception!). See + ** util/Assert.h. **/ #ifndef __CVC4__DEBUG_H #define __CVC4__DEBUG_H +#include "cvc4_config.h" + #include <cassert> -#ifdef DEBUG +#ifdef CVC4_ASSERTIONS // the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) +# define cvc4assert(x) assert(EXPECT_TRUE( x )) #else // TODO: use a compiler annotation when assertions are off ? // (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +# define cvc4assert(x) /*EXPECT_TRUE( x )*/ +#endif /* CVC4_ASSERTIONS */ #endif /* __CVC4__DEBUG_H */ diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index ae79f920d..36f99f4ac 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** decision_engine.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 3a093211c..58f9400b5 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** decision_engine.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A decision engine for CVC4. **/ #ifndef __CVC4__DECISION_ENGINE_H diff --git a/src/util/exception.h b/src/util/exception.h index d239f48de..8481a8504 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** exception.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,9 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Exception class. - ** - ** As many paragraphs as you like. + ** CVC4's exception base class and some associated utilities. **/ #ifndef __CVC4__EXCEPTION_H diff --git a/src/util/literal.h b/src/util/literal.h index 3ec216a6a..921a9ef0d 100644 --- a/src/util/literal.h +++ b/src/util/literal.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** literal.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A literal. **/ #ifndef __CVC4__LITERAL_H diff --git a/src/util/model.h b/src/util/model.h index cf006b3e1..b79032221 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** model.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A model. **/ #ifndef __CVC4__MODEL_H diff --git a/src/util/options.h b/src/util/options.h index 8d2d113a2..2bfbf675f 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** options.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Global (command-line or equivalent) tuning parameters. **/ #include <iostream> diff --git a/src/util/output.cpp b/src/util/output.cpp index 103a3d61a..05c74918c 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** output.cpp + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/util/output.h b/src/util/output.h index 43dfe8a40..57ce5f3ca 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** output.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences diff --git a/src/util/result.h b/src/util/result.h index 8d9b93a1e..87686d59c 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** result.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Encapsulation of the result of a query. **/ #ifndef __CVC4__RESULT_H diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 4ac80f772..633a544f0 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -1,5 +1,8 @@ /********************* -*- C++ -*- */ /** unique_id.h + ** Original author: mdeters + ** 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) ** Courant Institute of Mathematical Sciences @@ -7,6 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** A mechanism for getting a compile-time unique ID. **/ #ifndef __CVC4__UNIQUE_ID_H |