diff options
Diffstat (limited to 'src/context')
| -rw-r--r-- | src/context/backtrackable.h | 29 | ||||
| -rw-r--r-- | src/context/cddense_set.h | 35 | ||||
| -rw-r--r-- | src/context/cdhashmap.h | 158 | ||||
| -rw-r--r-- | src/context/cdhashmap_forward.h | 42 | ||||
| -rw-r--r-- | src/context/cdhashset.h | 29 | ||||
| -rw-r--r-- | src/context/cdhashset_forward.h | 43 | ||||
| -rw-r--r-- | src/context/cdinsert_hashmap.h | 63 | ||||
| -rw-r--r-- | src/context/cdinsert_hashmap_forward.h | 44 | ||||
| -rw-r--r-- | src/context/cdlist.h | 32 | ||||
| -rw-r--r-- | src/context/cdlist_forward.h | 55 | ||||
| -rw-r--r-- | src/context/cdmaybe.h | 36 | ||||
| -rw-r--r-- | src/context/cdo.h | 29 | ||||
| -rw-r--r-- | src/context/cdqueue.h | 42 | ||||
| -rw-r--r-- | src/context/cdtrail_queue.h | 36 | ||||
| -rw-r--r-- | src/context/context.cpp | 29 | ||||
| -rw-r--r-- | src/context/context.h | 29 | ||||
| -rw-r--r-- | src/context/context_mm.cpp | 29 | ||||
| -rw-r--r-- | src/context/context_mm.h | 32 |
18 files changed, 391 insertions, 401 deletions
diff --git a/src/context/backtrackable.h b/src/context/backtrackable.h index b128313a6..0c1081266 100644 --- a/src/context/backtrackable.h +++ b/src/context/backtrackable.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file backtrackable.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Contains a backtrackable list - ** - ** Contains a backtrackable list. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Contains a backtrackable list. + */ #include "cvc4_private.h" diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h index 095d14156..5b45e9f58 100644 --- a/src/context/cddense_set.h +++ b/src/context/cddense_set.h @@ -1,21 +1,20 @@ -/********************* */ -/*! \file cddense_set.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This is an abstraction of a set of unsigned integers. - ** - ** This is an abstraction of a set of unsigned integers. - ** This class is designed to provide constant time insertion, element_of, - ** and fast iteration. This is done by storing backing vectors of size greater - ** than the maximum key. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * This is an abstraction of a set of unsigned integers. + * + * This class is designed to provide constant time insertion, element_of, + * and fast iteration. This is done by storing backing vectors of size greater + * than the maximum key. + */ #include "cvc4_private.h" diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 9a8ae925f..32b0cc8cc 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -1,82 +1,82 @@ -/********************* */ -/*! \file cdhashmap.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent map class. - ** - ** Context-dependent map class. Generic templated class for a map - ** which must be saved and restored as contexts are pushed and - ** popped. Requires that operator= be defined for the data class, - ** and operator== for the key class. For key types that don't have a - ** std::hash<>, you should provide an explicit HashFcn. - ** - ** See also: - ** CDInsertHashMap : An "insert-once" CD hash map. - ** CDTrailHashMap : A lightweight CD hash map with poor iteration - ** characteristics and some quirks in usage. - ** - ** Internal documentation: - ** - ** CDHashMap<> is something of a work in progress at present (26 May - ** 2010), due to some recent discoveries of problems with its - ** internal state. Here are some notes on the internal use of - ** CDOhash_maps that may be useful in figuring out this mess: - ** - ** So you have a CDHashMap<>. - ** - ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> - ** and goes on a doubly-linked list headed by map.d_first and - ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed - ** with a NULL d_map pointer, but then immediately call - ** makeCurrent() and set the d_map pointer back to the map. At - ** context level 0, this doesn't lead to anything special. In - ** higher context levels, this stores away a CDOhash_map with a NULL - ** map pointer at level 0, and a non-NULL map pointer in the - ** current context level. (Remember that for later.) - ** - ** When a key is associated to a new value in a CDHashMap, its - ** associated CDOhash_map calls makeCurrent(), then sets the new - ** value. The save object is also a CDOhash_map (allocated in context - ** memory). - ** - ** Now, CDOhash_maps disappear in a variety of ways. - ** - ** First, you might pop beyond a "modification of the value" - ** scope level, requiring a re-association of the key to an old - ** value. This is easy. CDOhash_map::restore() does the work, and - ** the context memory of the save object is reclaimed as usual. - ** - ** Second, you might pop beyond a "insert the key" scope level, - ** requiring that the key be completely removed from the map and - ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored - ** to a "NULL-map" state (see above), signaling it to remove - ** itself from the map completely and put itself on a "trash - ** list" for its scope. - ** - ** Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). - ** This first calls destroy(), as per ContextObj contract, but - ** cdhashmapdoesn't save/restore itself, so that does nothing at the - ** CDHashMap-level. Then, for each element in the map, it marks it as being - ** "part of a complete map destruction", which essentially short-circuits - ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates - ** it. - ** - ** Fourth, you might clear() the CDHashMap. This does exactly the - ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() - ** on itself. - ** - ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then - ** frees the memory associated to the CDOhash_map. - ** CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as - ** possible. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context-dependent map class. + * + * Generic templated class for a map which must be saved and restored as + * contexts are pushed and popped. Requires that operator= be defined for the + * data class, and operator== for the key class. For key types that don't have + * a std::hash<>, you should provide an explicit HashFcn. + * + * See also: + * CDInsertHashMap : An "insert-once" CD hash map. + * CDTrailHashMap : A lightweight CD hash map with poor iteration + * characteristics and some quirks in usage. + * + * Internal documentation: + * + * CDHashMap<> is something of a work in progress at present (26 May + * 2010), due to some recent discoveries of problems with its + * internal state. Here are some notes on the internal use of + * CDOhash_maps that may be useful in figuring out this mess: + * + * So you have a CDHashMap<>. + * + * You insert some (key,value) pairs. Each allocates a CDOhash_map<> + * and goes on a doubly-linked list headed by map.d_first and + * threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed + * with a NULL d_map pointer, but then immediately call + * makeCurrent() and set the d_map pointer back to the map. At + * context level 0, this doesn't lead to anything special. In + * higher context levels, this stores away a CDOhash_map with a NULL + * map pointer at level 0, and a non-NULL map pointer in the + * current context level. (Remember that for later.) + * + * When a key is associated to a new value in a CDHashMap, its + * associated CDOhash_map calls makeCurrent(), then sets the new + * value. The save object is also a CDOhash_map (allocated in context + * memory). + * + * Now, CDOhash_maps disappear in a variety of ways. + * + * First, you might pop beyond a "modification of the value" + * scope level, requiring a re-association of the key to an old + * value. This is easy. CDOhash_map::restore() does the work, and + * the context memory of the save object is reclaimed as usual. + * + * Second, you might pop beyond a "insert the key" scope level, + * requiring that the key be completely removed from the map and + * its CDOhash_map object memory freed. Here, the CDOhash_map is restored + * to a "NULL-map" state (see above), signaling it to remove + * itself from the map completely and put itself on a "trash + * list" for its scope. + * + * Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). + * This first calls destroy(), as per ContextObj contract, but + * cdhashmapdoesn't save/restore itself, so that does nothing at the + * CDHashMap-level. Then, for each element in the map, it marks it as being + * "part of a complete map destruction", which essentially short-circuits + * CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates + * it. + * + * Fourth, you might clear() the CDHashMap. This does exactly the + * same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() + * on itself. + * + * ContextObj::deleteSelf() calls the CDOhash_map destructor, then + * frees the memory associated to the CDOhash_map. + * CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as + * possible. + */ #include "cvc4_private.h" diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h index e7ca68bb4..ef7b9a6a4 100644 --- a/src/context/cdhashmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -1,25 +1,23 @@ -/********************* */ -/*! \file cdhashmap_forward.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This is a forward declaration header to declare the CDHashMap<> - ** template - ** - ** This is a forward declaration header to declare the CDHashMap<> - ** template. It's useful if you want to forward-declare CDHashMap<> - ** without including the full cdhashmap.h header, for example, in a - ** public header context. - ** - ** For CDHashMap<> in particular, it's difficult to forward-declare it - ** yourself, because it has a default template argument. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Morgan Deters, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * This is a forward declaration header to declare the CDHashMap<> + * template + * + * It's useful if you want to forward-declare CDHashMap<> without including the + * full cdhashmap.h header, for example, in a public header context. + * + * For CDHashMap<> in particular, it's difficult to forward-declare it + * yourself, because it has a default template argument. + */ #include "cvc4_public.h" diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index b7e9b051b..416806e09 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdhashset.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent set class. - ** - ** Context-dependent set class. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context-dependent set class. + */ #include "cvc4_private.h" diff --git a/src/context/cdhashset_forward.h b/src/context/cdhashset_forward.h index 2601dfed8..978576de6 100644 --- a/src/context/cdhashset_forward.h +++ b/src/context/cdhashset_forward.h @@ -1,25 +1,24 @@ -/********************* */ -/*! \file cdhashset_forward.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This is a forward declaration header to declare the CDSet<> - ** template - ** - ** This is a forward declaration header to declare the CDSet<> - ** template. It's useful if you want to forward-declare CDSet<> - ** without including the full cdset.h header, for example, in a - ** public header context. - ** - ** For CDSet<> in particular, it's difficult to forward-declare it - ** yourself, because it has a default template argument. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Tim King, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * This is a forward declaration header to declare the CDSet<> + * template + * + * It's useful if you want to forward-declare CDSet<> without including the + * full cdset.h header, for example, in a public header context. + * + * For CDSet<> in particular, it's difficult to forward-declare it + * yourself, because it has a default template argument. + */ #include "cvc4_public.h" diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index 903acdaf0..2b7712924 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -1,34 +1,35 @@ -/********************* */ -/*! \file cdinsert_hashmap.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent insert only hashmap built using trail of edits - ** - ** Context-dependent hashmap that only allows for one insertion per element. - ** This can be viewed as a highly restricted version of CDHashMap. - ** It is significantly lighter in memory usage than CDHashMap. - ** - ** See also: - ** CDTrailHashMap : A lightweight CD hash map with poor iteration - ** characteristics and some quirks in usage. - ** CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>) - ** - ** Notes: - ** - To iterate efficiently over the elements use the key_iterators. - ** - operator[] is only supported as a const derefence (must succeed). - ** - insert(k) must always work. - ** - Use insert_safe if you want to check if the element has been inserted - ** and only insert if it has not yet been. - ** - Does not accept TNodes as keys. - ** - Supports insertAtContextLevelZero() if the element is not in the map. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Mathias Preiner, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context-dependent insert only hashmap built using trail of edits + * + * Context-dependent hashmap that only allows for one insertion per element. + * This can be viewed as a highly restricted version of CDHashMap. + * It is significantly lighter in memory usage than CDHashMap. + * + * See also: + * CDTrailHashMap : A lightweight CD hash map with poor iteration + * characteristics and some quirks in usage. + * CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>) + * + * Notes: + * - To iterate efficiently over the elements use the key_iterators. + * - operator[] is only supported as a const derefence (must succeed). + * - insert(k) must always work. + * - Use insert_safe if you want to check if the element has been inserted + * and only insert if it has not yet been. + * - Does not accept TNodes as keys. + * - Supports insertAtContextLevelZero() if the element is not in the map. + */ #include "cvc4_private.h" diff --git a/src/context/cdinsert_hashmap_forward.h b/src/context/cdinsert_hashmap_forward.h index 5b9c0eb78..1c1bcae76 100644 --- a/src/context/cdinsert_hashmap_forward.h +++ b/src/context/cdinsert_hashmap_forward.h @@ -1,25 +1,25 @@ -/********************* */ -/*! \file cdinsert_hashmap_forward.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This is a forward declaration header to declare the CDInsertHashMap<> - ** template - ** - ** This is a forward declaration header to declare the CDInsertHashMap<> - ** template. It's useful if you want to forward-declare CDInsertHashMap<> - ** without including the full cdinsert_hashmap.h header, for example, in a - ** public header context. - ** - ** For CDInsertHashMap<> in particular, it's difficult to forward-declare it - ** yourself, because it has a default template argument. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * This is a forward declaration header to declare the CDInsertHashMap<> + * template + * + * It's useful if you want to forward-declare CDInsertHashMap<> without + * including the full cdinsert_hashmap.h header, for example, in a public + * header context. + * + * For CDInsertHashMap<> in particular, it's difficult to forward-declare it + * yourself, because it has a default template argument. + */ #include "cvc4_public.h" diff --git a/src/context/cdlist.h b/src/context/cdlist.h index c379e21c8..14f99e03e 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -1,19 +1,19 @@ -/********************* */ -/*! \file cdlist.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent list class (only supports append) - ** - ** Context-dependent list class. This list only supports appending - ** to the list; on backtrack, the list is simply shortened. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * Context-dependent list class (only supports append). + * + * This list only supports appending to the list; on backtrack, the list is + * simply shortened. + */ #include "cvc4_private.h" diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h index cf912a93a..d8a583922 100644 --- a/src/context/cdlist_forward.h +++ b/src/context/cdlist_forward.h @@ -1,31 +1,30 @@ -/********************* */ -/*! \file cdlist_forward.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This is a forward declaration header to declare the - ** CDList<> template - ** - ** This is a forward declaration header to declare the CDList<> - ** template. It's useful if you want to forward-declare CDList<> - ** without including the full cdlist.h or cdlist_context_memory.h - ** header, for example, in a public header context, or to keep - ** compile times low when only a forward declaration is needed. - ** - ** Note that all specializations of the template should be listed - ** here as well, since different specializations are defined in - ** different headers (cdlist.h and cdlist_context_memory.h). - ** Explicitly declaring both specializations here ensure that if you - ** define one, you'll get an error if you didn't include the correct - ** header (avoiding different, incompatible instantiations in - ** different compilation units). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Morgan Deters, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * This is a forward declaration header to declare the + * CDList<> template + * + * It's useful if you want to forward-declare CDList<> without including the + * full cdlist.h or cdlist_context_memory.h header, for example, in a public + * header context, or to keep compile times low when only a forward declaration + * is needed. + * + * Note that all specializations of the template should be listed + * here as well, since different specializations are defined in + * different headers (cdlist.h and cdlist_context_memory.h). + * Explicitly declaring both specializations here ensure that if you + * define one, you'll get an error if you didn't include the correct + * header (avoiding different, incompatible instantiations in + * different compilation units). + */ #include "cvc4_public.h" diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h index 4913c2dd5..f89313af1 100644 --- a/src/context/cdmaybe.h +++ b/src/context/cdmaybe.h @@ -1,21 +1,21 @@ -/********************* */ -/*! \file cdmaybe.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A context-dependent "maybe" template type - ** - ** This implements a CDMaybe. - ** This has either been set in the context or it has not. - ** Template parameter T must have a default constructor and support - ** assignment. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * A context-dependent "maybe" template type + * + * This implements a CDMaybe. + * This has either been set in the context or it has not. + * Template parameter T must have a default constructor and support + * assignment. + */ #include "cvc4_private.h" diff --git a/src/context/cdo.h b/src/context/cdo.h index 7e3d892d7..5fdf3fd6d 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdo.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Clark Barrett, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A context-dependent object. - ** - ** A context-dependent object. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Clark Barrett, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A context-dependent object. + */ #include "cvc4_private.h" diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index acd31020a..dc7994957 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -1,24 +1,24 @@ -/********************* */ -/*! \file cdqueue.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Francois Bobot, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent queue class - ** - ** Context-dependent First-In-First-Out queue class. - ** This implementation may discard elements which are enqueued and dequeued - ** at the same context level. - ** - ** The implementation is based on a CDList with one additional size_t - ** for tracking the next element to dequeue from the list and additional - ** size_t for tracking the previous size of the list. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Francois Bobot, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context-dependent First-In-First-Out queue class. + * + * This implementation may discard elements which are enqueued and dequeued + * at the same context level. + * + * The implementation is based on a CDList with one additional size_t + * for tracking the next element to dequeue from the list and additional + * size_t for tracking the previous size of the list. + */ #include "cvc4_private.h" diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h index 1cc8b1f70..09aa9a29e 100644 --- a/src/context/cdtrail_queue.h +++ b/src/context/cdtrail_queue.h @@ -1,21 +1,21 @@ -/********************* */ -/*! \file cdtrail_queue.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context-dependent queue class with an explicit trail of elements - ** - ** Context-dependent First-In-First-Out queue class. - ** The implementation is based on a combination of CDList and a CDO<size_t> - ** for tracking the next element to dequeue from the list. - ** The implementation is currently not full featured. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Mathias Preiner, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context-dependent queue class with an explicit trail of elements + * + * The implementation is based on a combination of CDList and a CDO<size_t> + * for tracking the next element to dequeue from the list. + * The implementation is currently not full featured. + */ #include "cvc4_private.h" diff --git a/src/context/context.cpp b/src/context/context.cpp index 6dfab3de2..7e49b49ab 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context.cpp - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of base context operations. - ** - ** Implementation of base context operations. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Morgan Deters, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of base context operations. + */ #include <iostream> #include <string> diff --git a/src/context/context.h b/src/context/context.h index d6b458701..1ccddfa59 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Context class and context manager. - ** - ** Context class and context manager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Morgan Deters, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Context class and context manager. + */ #include "cvc4_private.h" diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 30306d254..9df5c357d 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context_mm.cpp - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of Context Memory Manager. - ** - ** Implementation of Context Memory Manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Andres Noetzli, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of Context Memory Manager + */ #include <cstdlib> #include <deque> diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 75b3a2fbf..725f713ac 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -1,19 +1,19 @@ -/********************* */ -/*! \file context_mm.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Region-based memory manager with stack-based push and pop. - ** - ** Region-based memory manager with stack-based push and pop. Designed - ** for use by ContextManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Morgan Deters, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Region-based memory manager with stack-based push and pop. + * + * Designed for use by ContextManager. + */ #include "cvc4_private.h" |