summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/cnf/cnfData.c2
-rw-r--r--src/sat/msat/msatVec.c4
-rw-r--r--src/sat/satoko/solver.c2
-rw-r--r--src/sat/satoko/solver_api.c2
-rw-r--r--src/sat/satoko/utils/vec/vec_char.h4
-rw-r--r--src/sat/satoko/utils/vec/vec_flt.h4
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_int.h4
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_sdbl.h4
-rwxr-xr-xsrc/sat/satoko/utils/vec/vec_uint.h4
-rw-r--r--src/sat/xsat/xsatSolver.c2
10 files changed, 16 insertions, 16 deletions
diff --git a/src/sat/cnf/cnfData.c b/src/sat/cnf/cnfData.c
index 3d3cdf37..797066e7 100644
--- a/src/sat/cnf/cnfData.c
+++ b/src/sat/cnf/cnfData.c
@@ -4737,7 +4737,7 @@ int Aig_ManDeriveCnfTest2()
Counter += CountCur;
pNums[uTruth] = CountCur;
pSops[uTruth] = ALLOC( char, CountCur );
- memcpy( pSops[uTruth], Sop, CountCur );
+ memcpy( pSops[uTruth], Sop, (size_t)CountCur );
pLines[nLines++] = Counter;
}
fclose( pFile );
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 7144b213..d443cb0a 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -442,10 +442,10 @@ int Msat_IntVecPop( Msat_IntVec_t * p )
void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse )
{
if ( fReverse )
- qsort( (void *)p->pArray, p->nSize, sizeof(int),
+ qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(int),
(int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
else
- qsort( (void *)p->pArray, p->nSize, sizeof(int),
+ qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(int),
(int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
}
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index b1596345..8f7dd875 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -173,7 +173,7 @@ static inline void clause_realloc(struct cdb *dest, struct cdb *src, unsigned *c
}
new_cref = cdb_append(dest, 3 + old_clause->f_learnt + old_clause->size);
new_clause = cdb_handler(dest, new_cref);
- memcpy(new_clause, old_clause, (3 + old_clause->f_learnt + old_clause->size) * 4);
+ memcpy(new_clause, old_clause, (size_t)((3 + old_clause->f_learnt + old_clause->size) * 4));
old_clause->f_reallocd = 1;
old_clause->size = (unsigned) new_cref;
*cref = new_cref;
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 0193b1c3..4775e445 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -259,7 +259,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
unsigned max_var;
unsigned cref;
- qsort((void *) lits, size, sizeof(unsigned), stk_uint_compare);
+ qsort((void *) lits, (size_t)size, sizeof(unsigned), stk_uint_compare);
max_var = lit2var(lits[size - 1]);
while (max_var >= vec_act_size(s->activity))
satoko_add_variable(s, SATOKO_LIT_FALSE);
diff --git a/src/sat/satoko/utils/vec/vec_char.h b/src/sat/satoko/utils/vec/vec_char.h
index 7d5732ec..4d780b22 100644
--- a/src/sat/satoko/utils/vec/vec_char.h
+++ b/src/sat/satoko/utils/vec/vec_char.h
@@ -233,10 +233,10 @@ static inline int vec_char_desc_compare(const void *p1, const void *p2)
static inline void vec_char_sort(vec_char_t *p, int ascending)
{
if (ascending)
- qsort((void *) p->data, p->size, sizeof(char),
+ qsort((void *) p->data, (size_t)p->size, sizeof(char),
(int (*)(const void *, const void *)) vec_char_asc_compare);
else
- qsort((void*) p->data, p->size, sizeof(char),
+ qsort((void*) p->data, (size_t)p->size, sizeof(char),
(int (*)(const void *, const void *)) vec_char_desc_compare);
}
diff --git a/src/sat/satoko/utils/vec/vec_flt.h b/src/sat/satoko/utils/vec/vec_flt.h
index d7c896d9..8dd7b2ac 100644
--- a/src/sat/satoko/utils/vec/vec_flt.h
+++ b/src/sat/satoko/utils/vec/vec_flt.h
@@ -220,10 +220,10 @@ static inline int vec_flt_desc_compare(const void* p1, const void* p2)
static inline void vec_flt_sort(vec_flt_t* p, int ascending)
{
if (ascending)
- qsort((void *) p->data, p->size, sizeof(float),
+ qsort((void *) p->data, (size_t)p->size, sizeof(float),
(int (*)(const void*, const void*)) vec_flt_asc_compare);
else
- qsort((void *) p->data, p->size, sizeof(float),
+ qsort((void *) p->data, (size_t)p->size, sizeof(float),
(int (*)(const void*, const void*)) vec_flt_desc_compare);
}
diff --git a/src/sat/satoko/utils/vec/vec_int.h b/src/sat/satoko/utils/vec/vec_int.h
index 75c5d134..d310fd45 100755
--- a/src/sat/satoko/utils/vec/vec_int.h
+++ b/src/sat/satoko/utils/vec/vec_int.h
@@ -214,10 +214,10 @@ static inline int vec_int_desc_compare(const void* p1, const void* p2)
static inline void vec_int_sort(vec_int_t* p, int ascending)
{
if (ascending)
- qsort((void *) p->data, p->size, sizeof(int),
+ qsort((void *) p->data, (size_t)p->size, sizeof(int),
(int (*)(const void*, const void*)) vec_int_asc_compare);
else
- qsort((void *) p->data, p->size, sizeof(int),
+ qsort((void *) p->data, (size_t)p->size, sizeof(int),
(int (*)(const void*, const void*)) vec_int_desc_compare);
}
diff --git a/src/sat/satoko/utils/vec/vec_sdbl.h b/src/sat/satoko/utils/vec/vec_sdbl.h
index ec1c731c..89127412 100755
--- a/src/sat/satoko/utils/vec/vec_sdbl.h
+++ b/src/sat/satoko/utils/vec/vec_sdbl.h
@@ -227,10 +227,10 @@ static inline int vec_sdbl_desc_compare(const void* p1, const void* p2)
static inline void vec_sdbl_sort(vec_sdbl_t* p, int ascending)
{
if (ascending)
- qsort((void *) p->data, p->size, sizeof(sdbl_t),
+ qsort((void *) p->data, (size_t)p->size, sizeof(sdbl_t),
(int (*)(const void*, const void*)) vec_sdbl_asc_compare);
else
- qsort((void *) p->data, p->size, sizeof(sdbl_t),
+ qsort((void *) p->data, (size_t)p->size, sizeof(sdbl_t),
(int (*)(const void*, const void*)) vec_sdbl_desc_compare);
}
diff --git a/src/sat/satoko/utils/vec/vec_uint.h b/src/sat/satoko/utils/vec/vec_uint.h
index e6719ca3..ef094236 100755
--- a/src/sat/satoko/utils/vec/vec_uint.h
+++ b/src/sat/satoko/utils/vec/vec_uint.h
@@ -242,10 +242,10 @@ static inline int vec_uint_desc_compare(const void *p1, const void *p2)
static inline void vec_uint_sort(vec_uint_t *p, int ascending)
{
if (ascending)
- qsort((void *) p->data, p->size, sizeof(unsigned),
+ qsort((void *) p->data, (size_t)p->size, sizeof(unsigned),
(int (*)(const void *, const void *)) vec_uint_asc_compare);
else
- qsort((void*) p->data, p->size, sizeof(unsigned),
+ qsort((void*) p->data, (size_t)p->size, sizeof(unsigned),
(int (*)(const void *, const void *)) vec_uint_desc_compare);
}
diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c
index 4844ca1d..abf0809a 100644
--- a/src/sat/xsat/xsatSolver.c
+++ b/src/sat/xsat/xsatSolver.c
@@ -944,7 +944,7 @@ void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, unsigned * pC
}
nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
- memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 );
+ memcpy( pNewCla, pOldCla, (size_t)(( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4) );
pOldCla->fReallocd = 1;
pOldCla->nSize = ( unsigned ) nNewCRef;
*pCRef = nNewCRef;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:36:11 +0000