diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 08:39:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 08:39:27 +0000 |
commit | 7293554b109742697d4d928ed7b58acadc6de947 (patch) | |
tree | 73e057306fac266b5c9ca9cf12ae050f73c43bdf /src/include | |
parent | acd68152ff9600bdff208376f2cd43f09d45cdc8 (diff) |
another pass
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/assert.h | 6 | ||||
-rw-r--r-- | src/include/attr_type.h | 6 | ||||
-rw-r--r-- | src/include/command.h | 6 | ||||
-rw-r--r-- | src/include/context.h | 6 | ||||
-rw-r--r-- | src/include/debug.h | 6 | ||||
-rw-r--r-- | src/include/decision_engine.h | 10 | ||||
-rw-r--r-- | src/include/exception.h | 9 | ||||
-rw-r--r-- | src/include/expr.h | 9 | ||||
-rw-r--r-- | src/include/expr_attribute.h | 6 | ||||
-rw-r--r-- | src/include/expr_builder.h | 6 | ||||
-rw-r--r-- | src/include/expr_manager.h | 6 | ||||
-rw-r--r-- | src/include/expr_value.h | 11 | ||||
-rw-r--r-- | src/include/kind.h | 6 | ||||
-rw-r--r-- | src/include/literal.h | 6 | ||||
-rw-r--r-- | src/include/model.h | 6 | ||||
-rw-r--r-- | src/include/parser.h | 9 | ||||
-rw-r--r-- | src/include/parser_exception.h | 11 | ||||
-rw-r--r-- | src/include/prop_engine.h | 6 | ||||
-rw-r--r-- | src/include/prover.h | 6 | ||||
-rw-r--r-- | src/include/result.h | 6 | ||||
-rw-r--r-- | src/include/sat.h | 6 | ||||
-rw-r--r-- | src/include/theory.h | 6 | ||||
-rw-r--r-- | src/include/theory_engine.h | 6 | ||||
-rw-r--r-- | src/include/unique_id.h | 6 | ||||
-rw-r--r-- | src/include/vc.h | 6 |
25 files changed, 109 insertions, 64 deletions
diff --git a/src/include/assert.h b/src/include/assert.h index 473cd21f1..a66503641 100644 --- a/src/include/assert.h +++ b/src/include/assert.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** assert.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_ASSERT_H diff --git a/src/include/attr_type.h b/src/include/attr_type.h index e5eb222fe..d24385f8e 100644 --- a/src/include/attr_type.h +++ b/src/include/attr_type.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** attr_type.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_ATTR_TYPE_H diff --git a/src/include/command.h b/src/include/command.h index 45b59a95b..944b9c621 100644 --- a/src/include/command.h +++ b/src/include/command.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** command.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_COMMAND_H diff --git a/src/include/context.h b/src/include/context.h index 1997e63d6..fce2f0b8d 100644 --- a/src/include/context.h +++ b/src/include/context.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** context.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_CONTEXT_H diff --git a/src/include/debug.h b/src/include/debug.h index 95e705bcb..36942d1ae 100644 --- a/src/include/debug.h +++ b/src/include/debug.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** debug.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_DEBUG_H diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h index 8745adad5..ec0172535 100644 --- a/src/include/decision_engine.h +++ b/src/include/decision_engine.h @@ -1,17 +1,19 @@ /********************* -*- C++ -*- */ /** decision_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ -#include "literal.h" - #ifndef __CVC4_DECISION_ENGINE_H #define __CVC4_DECISION_ENGINE_H +#include "literal.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) diff --git a/src/include/exception.h b/src/include/exception.h index ce19b0d68..792a98701 100644 --- a/src/include/exception.h +++ b/src/include/exception.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** exception.h ** This file is part of the CVC4 prototype. - ** - ** Exception class. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** + ** Exception class. **/ #ifndef __CVC4_EXCEPTION_H diff --git a/src/include/expr.h b/src/include/expr.h index 9ca449ce7..e92ece93d 100644 --- a/src/include/expr.h +++ b/src/include/expr.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** expr.h ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** + ** Reference-counted encapsulation of a pointer to an expression. **/ #ifndef __CVC4_EXPR_H diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h index 1c10a6663..77700096e 100644 --- a/src/include/expr_attribute.h +++ b/src/include/expr_attribute.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_attribute.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_EXPR_ATTRIBUTE_H diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h index 342834e37..a95ecb2e3 100644 --- a/src/include/expr_builder.h +++ b/src/include/expr_builder.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_builder.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_EXPR_BUILDER_H diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h index 5dae5b854..59a3eb7a3 100644 --- a/src/include/expr_manager.h +++ b/src/include/expr_manager.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** expr_manager.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_EXPR_MANAGER_H diff --git a/src/include/expr_value.h b/src/include/expr_value.h index c15241ebf..ea14c3fa7 100644 --- a/src/include/expr_value.h +++ b/src/include/expr_value.h @@ -1,16 +1,17 @@ -/********************* +/********************* -*- C++ -*- */ /** expr_value.h ** 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. ** ** An expression node. ** ** Instances of this class are generally referenced through ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the ** reference count on ExprValue instances and - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ #ifndef __CVC4_EXPR_VALUE_H diff --git a/src/include/kind.h b/src/include/kind.h index a015a6b71..5d99330ca 100644 --- a/src/include/kind.h +++ b/src/include/kind.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** kind.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_KIND_H diff --git a/src/include/literal.h b/src/include/literal.h index 93855edb8..8b147c640 100644 --- a/src/include/literal.h +++ b/src/include/literal.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** literal.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_LITERAL_H diff --git a/src/include/model.h b/src/include/model.h index 205dcf18f..c07b75dfa 100644 --- a/src/include/model.h +++ b/src/include/model.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** model.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_MODEL_H diff --git a/src/include/parser.h b/src/include/parser.h index 63a448b28..e30b31b1c 100644 --- a/src/include/parser.h +++ b/src/include/parser.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** parser.h ** This file is part of the CVC4 prototype. - ** - ** Parser abstraction. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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 abstraction. **/ #ifndef __CVC4_PARSER_H diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h index 8bad801f4..debb75e70 100644 --- a/src/include/parser_exception.h +++ b/src/include/parser_exception.h @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ -/** exception.h +/** parser_exception.h ** This file is part of the CVC4 prototype. - ** - ** Exception class. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** + ** Exception class. **/ #ifndef __CVC4_PARSER_EXCEPTION_H diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h index 90d07a47b..de25c5594 100644 --- a/src/include/prop_engine.h +++ b/src/include/prop_engine.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** prop_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_PROP_ENGINE_H diff --git a/src/include/prover.h b/src/include/prover.h index e48d6336c..de29f48c0 100644 --- a/src/include/prover.h +++ b/src/include/prover.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** prover.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_PROVER_H diff --git a/src/include/result.h b/src/include/result.h index cfabd3be2..50f488682 100644 --- a/src/include/result.h +++ b/src/include/result.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** result.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_RESULT_H diff --git a/src/include/sat.h b/src/include/sat.h index 13578ec8d..00a94c142 100644 --- a/src/include/sat.h +++ b/src/include/sat.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** sat.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_SAT_H diff --git a/src/include/theory.h b/src/include/theory.h index 5c50c7a37..935c23b08 100644 --- a/src/include/theory.h +++ b/src/include/theory.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** theory.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_THEORY_H diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h index f4e36f604..2a0841d8d 100644 --- a/src/include/theory_engine.h +++ b/src/include/theory_engine.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** theory_engine.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_THEORY_ENGINE_H diff --git a/src/include/unique_id.h b/src/include/unique_id.h index 55fa24e51..1a6f3427a 100644 --- a/src/include/unique_id.h +++ b/src/include/unique_id.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** unique_id.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_UNIQUE_ID_H diff --git a/src/include/vc.h b/src/include/vc.h index 57d8a957e..845d1eb6d 100644 --- a/src/include/vc.h +++ b/src/include/vc.h @@ -1,10 +1,12 @@ /********************* -*- C++ -*- */ /** vc.h ** This file is part of the CVC4 prototype. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** 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. + ** **/ #ifndef __CVC4_VC_H |