diff options
Diffstat (limited to 'src/sat/glucose2/SolverTypes.h')
-rw-r--r-- | src/sat/glucose2/SolverTypes.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/sat/glucose2/SolverTypes.h b/src/sat/glucose2/SolverTypes.h index b15c887f..ea0f76d0 100644 --- a/src/sat/glucose2/SolverTypes.h +++ b/src/sat/glucose2/SolverTypes.h @@ -38,6 +38,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose2/Map.h" #include "sat/glucose2/Alloc.h" +#include "sat/glucose2/CGlucose.h" + ABC_NAMESPACE_CXX_HEADER_START namespace Gluco2 { @@ -145,6 +147,10 @@ class Clause { friend class ClauseAllocator; + #ifdef CGLUCOSE_EXP + friend class Solver; + #endif + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template<class V> Clause(const V& ps, bool use_extra, bool learnt) { @@ -306,9 +312,15 @@ class OccLists } void clear(bool free = true){ - occs .clear(free); - dirty .clear(free); - dirties.clear(free); + if(free){ + occs .clear(free); + dirty .clear(free); + dirties.clear(free); + } else { + occs .shrink_(occs .size()); + dirty .shrink_(dirty .size()); + dirties.shrink_(dirties.size()); + } } }; |