2.Cadical-代码解读arena类型

arena.hpp文件内容

#ifndef _arena_hpp_INCLUDED
#define _arena_hpp_INCLUDED

namespace CaDiCaL {

/*

This memory allocation arena provides fixed size pre-allocated memory for the moving garbage collector 'copy_non_garbage_clauses' in 'collect.cpp' to hold clauses which should survive garbage collection.

译文：这个内存分配领域为‘collect’中的移动垃圾收集器‘copy_non_garbage_clauses’提供了固定大小的预分配内存。保存那些在垃圾收集中幸存下来的子句。

The advantage of using a pre-allocated arena is that the allocation order  of the clauses can be adapted in such a way that clauses watched by the  same literal are allocated consecutively. This improves locality during propagation and thus is more cache friendly.

译文：使用预先分配的arena的好处是，可以调整子句的分配顺序，使相同文字监视的子句被连续分配。这改善了传播期间的局部性，因此对缓存更友好.

A similar technique is  implemented in MiniSAT and Glucose and gives substantial speed-up in  propagations per second even though it might even almost double peek  memory usage. Note that in MiniSAT this arena is  ctually required for  MiniSAT to be able to use 32 bit clauses references instead of 64 bit  pointers. This would restrict the maximum number of clauses and thus is  a restriction we do not want to use anymore.

译文：在MiniSAT和Glucose中实现了一项类似的技术，它极大地提高了每秒的传播速度，尽管它甚至可能使peek内存使用量几乎翻倍。请注意，在MiniSAT中，为了能够使用32位子句引用而不是64位指针，这个arena实际上是必需的。这将限制子句的最大数量，因此我们不想再使用这个限制.

New learned clauses are allocated in CaDiCaL outside of this arena and moved to the arena during garbage collection. The additional 'to' space required for such a moving garbage collector is only allocated for those  clauses surviving garbage collection, which usually needs much less  memory than all clauses.

译文：新的学习子句被分配到这个竞技场之外的CaDiCaL中，并在垃圾收集期间移动到竞技场中。这种移动垃圾收集器所需要的额外的“to”空间只分配给那些在垃圾收集中幸存的子句，这通常比所有子句所需的内存要少得多。

The net effect is that in our implementation the moving garbage collector using this arena only needs roughly 50% more  memory than allocating the clauses directly. Both implementations can be  compared by varying the 'opts.arenatype' option (which also controls the  allocation order of clauses during moving them).

译文：最终结果是，在我们的实现中，使用这个平台的移动垃圾收集器只需要比直接分配子句多大约50%的内存。两种实现都可以通过改变'opts.arenatype'选项进行比较。(该选项还控制子句在移动时的分配顺序)。

// The standard sequence of using the arena is as follows:
//
// Arena arena;
// ...
// arena.prepare (bytes);
// q1 = arena.copy (p1, bytes1);
// ...
// qn = arena.copy (pn, bytesn);
// assert (bytes1 + ... + bytesn <= bytes);
// arena.swap ();
// ...
// if (!arena.contains (q)) delete q;
// ...
// arena.prepare (bytes);
// q1 = arena.copy (p1, bytes1);
// ...
// qn = arena.copy (pn, bytesn);
// assert (bytes1 + ... + bytesn <= bytes);
// arena.swap ();
// ...
//
// One has to be really careful with 'qi' references to arena memory.译文：一个人必须非常小心使用“qi”来引用竞技场内存。

*/

//arena类型声明-------见下面代码

.......

#endif

 1 struct Internal;
 2 
 3 class Arena {
 4 
 5   Internal * internal;
 6 
 7   struct { char * start, * top, * end; } from, to;
 8 
 9 public:
10 
11   Arena (Internal *);
12   ~Arena ();
13 
14   // Prepare 'to' space to hold that amount of memory.  Precondition is that
15   // the 'to' space is empty.  The following sequence of 'copy' operations
16   // can use as much memory in sum as pre-allocated here.
17   // 准备“to”空间来容纳这些内存。前提条件是“to”空间是空的。
        下面的“复制”操作序列可以使用这里预先分配的全部内存。
18   void prepare (size_t bytes);
19 
20   // Does the memory pointed to by 'p' belong to this arena? More precisely
21   // to the 'from' space, since that is the only one remaining after 'swap'.
22   //p指向的记忆属于这个竞技场吗?更准确地说，是“from”空间，因为它是“swap”之后唯一剩下的空间。
23   bool contains (void * p) const {
24     char * c = (char *) p;
25     return from.start <= c && c < from.top;
26   }
27 
28   // Allocate that amount of memory in 'to' space.  This assumes the 'to'
29   // space has been prepared to hold enough memory with 'prepare'.  Then
30   // copy the memory pointed to by 'p' of size 'bytes'.  Note that it does
31   // not matter whether 'p' is in 'from' or allocated outside of the arena.
32   //
        在“到”空间中分配内存。这假设“to”空间已经准备好使用“prepare”来容纳足够的内存。
        然后复制大小为字节的“p”所指向的内存。注意，“p”是在“from”中还是在arena之外分配并不重要。

33   char * copy (const char * p, size_t bytes) {
34     char * res = to.top;
35     to.top += bytes;
36     assert (to.top <= to.end);
37     memcpy (res, p, bytes);
38     return res;
39   }
40 
41   // Completely delete 'from' space and then replace 'from' by 'to' (by
42   // pointer swapping).  Everything previously allocated (in 'from') and not
43   // explicitly copied to 'to' with 'copy' becomes invalid.
44   //
       完全删除'from'空间，然后替换'from' by 'to'(通过指针交换)。
       以前分配的(在'from'中)和没有显式地用'copy'复制到'to'的所有内容都将无效。
45   void swap ();
46 };

 1 #include "internal.hpp"
 2 
 3 namespace CaDiCaL {
 4 
 5 Arena::Arena (Internal * i) {
 6   memset (this, 0, sizeof *this);
 7   internal = i;
 8 }
 9 
10 Arena::~Arena () {
11   delete [] from.start;
12   delete [] to.start;
13 }
14 
15 void Arena::prepare (size_t bytes) {
16   LOG ("preparing 'to' space of arena with %zd bytes", bytes);
17   assert (!to.start);
18   to.top = to.start = new char[bytes];
19   to.end = to.start + bytes;
20 }
21 
22 void Arena::swap () {
23   delete [] from.start;
24   LOG ("delete 'from' space of arena with %zd bytes",
25     (size_t) (from.end - from.start));
26   from = to;
27   to.start = to.top = to.end = 0;
28 }
29 
30 }