diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix clang compilation (Denys Duchier).

Browse Source
This commit is contained in:
Vítor Santos Costa 2012-06-29 22:24:12 +01:00
parent 0ed4e15925
commit e938c17748
1 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
packages/swi-minisat2/C/SolverTypes.h
View File

@ -119,11 +119,7 @@ public:
// -- use this function instead: // -- use this function instead:
template<class V> template<class V>
friend Clause* Clause_new(const V& ps, bool learnt = false) { friend Clause* Clause_new(const V& ps, bool learnt = false);
assert(sizeof(Lit) == sizeof(uint32_t));
assert(sizeof(float) == sizeof(uint32_t));
void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
return new (mem) Clause(ps, learnt); }
int size () const { return size_etc >> 3; } int size () const { return size_etc >> 3; }
void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); }
@ -147,6 +143,12 @@ public:
}; };
template<class V>
Clause* Clause_new(const V& ps, bool learnt) {
assert(sizeof(Lit) == sizeof(uint32_t));
assert(sizeof(float) == sizeof(uint32_t));
void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
return new (mem) Clause(ps, learnt); }
/*_________________________________________________________________________________________________ /*_________________________________________________________________________________________________
| |
| subsumes : (other : const Clause&) -> Lit | subsumes : (other : const Clause&) -> Lit