Ticket #31312: fix-clause-creator.diff

File fix-clause-creator.diff, 1.6 KB (added by gjasny@…, 12 years ago)
  • packages/swi-minisat2/C/SolverTypes.h

    old new  
    9797//=================================================================================================
    9898// Clause -- a simple class for representing a clause:
    9999
    100 
    101100class Clause {
    102101    uint32_t size_etc;
    103102    union { float act; uint32_t abst; } extra;
     
    116115        size_etc = (ps.size() << 3) | (uint32_t)learnt;
    117116        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
    118117        if (learnt) extra.act = 0; else calcAbstraction(); }
    119 
    120118    // -- use this function instead:
    121     template<class V>
    122     friend Clause* Clause_new(const V& ps, bool learnt = false) {
    123         assert(sizeof(Lit)      == sizeof(uint32_t));
    124         assert(sizeof(float)    == sizeof(uint32_t));
    125         void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
    126         return new (mem) Clause(ps, learnt); }
    127119
    128120    int          size        ()      const   { return size_etc >> 3; }
    129121    void         shrink      (int i)         { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
     
    146138    void         strengthen  (Lit p);
    147139};
    148140
     141template<class V>
     142Clause* Clause_new(const V& ps, bool learnt = false) {
     143    assert(sizeof(Lit)      == sizeof(uint32_t));
     144    assert(sizeof(float)    == sizeof(uint32_t));
     145    void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
     146    return new (mem) Clause(ps, learnt);
     147}
     148
    149149
    150150/*_________________________________________________________________________________________________
    151151|