1 /******************************************
2 Copyright (c) 2016, Mate Soos
3 
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10 
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13 
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22 
23 #ifndef CLAUSEALLOCATOR_H
24 #define CLAUSEALLOCATOR_H
25 
26 
27 #include "constants.h"
28 #include "cloffset.h"
29 #include "watched.h"
30 #include "clause.h"
31 #include "watcharray.h"
32 
33 #include <stdlib.h>
34 #include <map>
35 #include <vector>
36 
37 namespace CMSat {
38 
39 class Clause;
40 class Solver;
41 class PropEngine;
42 
43 using std::map;
44 using std::vector;
45 
46 /**
47 @brief Allocates memory for (xor) clauses
48 
49 This class allocates memory in large chunks, then distributes it to clauses when
50 needed. When instructed, it consolidates the unused space (i.e. clauses free()-ed).
51 Essentially, it is a stack-like allocator for clauses. It is useful to have
52 this, because this way, we can address clauses according to their number,
53 which is 32-bit, instead of their address, which might be 64-bit
54 */
55 class ClauseAllocator {
56     public:
57         ClauseAllocator();
58         ~ClauseAllocator();
59 
60         template<class T>
Clause_new(const T & ps,const uint32_t conflictNum,const int64_t ID)61         Clause* Clause_new(const T& ps, const uint32_t conflictNum
62             #ifdef STATS_NEEDED
63             , const int64_t ID
64             #endif
65         ) {
66             if (ps.size() > (0x01UL << 28)) {
67                 throw CMSat::TooLongClauseError();
68             }
69 
70             void* mem = allocEnough(ps.size());
71             Clause* real = new (mem) Clause(ps, conflictNum
72             #ifdef STATS_NEEDED
73             , ID
74             #endif
75             );
76 
77             return real;
78         }
79 
80         ClOffset get_offset(const Clause* ptr) const;
81 
ptr(const ClOffset offset)82         inline Clause* ptr(const ClOffset offset) const
83         {
84             return (Clause*)(&dataStart[offset]);
85         }
86 
87         void clauseFree(Clause* c);
88         void clauseFree(ClOffset offset);
89 
90         void consolidate(
91             Solver* solver
92             , const bool force = false
93             , bool lower_verb = false
94         );
95 
96         size_t mem_used() const;
97 
98     private:
99         void update_offsets(
100             vector<ClOffset>& offsets,
101             ClOffset* newDataStart,
102             ClOffset*& new_ptr
103         );
104         void move_one_watchlist(
105             watch_subarray& ws, ClOffset* newDataStart, ClOffset*& new_ptr);
106 
107         ClOffset move_cl(
108             ClOffset* newDataStart
109             , ClOffset*& new_ptr
110             , Clause* old
111         ) const;
112 
113         BASE_DATA_TYPE* dataStart; ///<Stack starts at these positions
114         uint64_t size; ///<The number of BASE_DATA_TYPE datapieces currently used in each stack
115         /**
116         @brief Clauses in the stack had this size when they were allocated
117         This my NOT be their current size: the clauses may be shrinked during
118         the running of the solver. Therefore, it is imperative that their orignal
119         size is saved. This way, we can later move clauses around.
120         */
121         uint64_t capacity; ///<The number of BASE_DATA_TYPE datapieces allocated
122         /**
123         @brief The estimated used size of the stack
124         This is incremented by clauseSize each time a clause is allocated, and
125         decremetented by clauseSize each time a clause is deallocated. The
126         problem is, that clauses can shrink, and thus this value will be an
127         overestimation almost all the time
128         */
129         uint64_t currentlyUsedSize;
130 
131         void* allocEnough(const uint32_t num_lits);
132 };
133 
134 } //end namespace
135 
136 #endif //CLAUSEALLOCATOR_H
137