luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #425 from MyskYko/fix3 

fix cadical
This commit is contained in:
alanminko 2025-07-07 03:44:24 -07:00 committed by GitHub
parent beff7f1b34 6e130c15a3
commit 0dc5524b80
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 15 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/sat/cadical/cadicalSolver.c
View File

@ -103,7 +103,7 @@ int cadical_solver_addclause(cadical_solver* s, int* begin, int* end) {
Synopsis [solve with resource limits]
Description [assumptions and inspection limits are not supported.]
Description [inspection limits are not supported.]
SideEffects []
@ -193,7 +193,7 @@ int cadical_solver_final(cadical_solver* s, int** ppArray) {
Synopsis [get number of variables]
Description [emulated using "nVars".]
Description [also update "nVars" if added by BVA.]
SideEffects []
@ -201,6 +201,9 @@ int cadical_solver_final(cadical_solver* s, int** ppArray) {
***********************************************************************/
int cadical_solver_nvars(cadical_solver* s) {
if(s->nVars < ccadical_vars((CCaDiCaL*)s->p)) {
s->nVars = ccadical_vars((CCaDiCaL*)s->p);
}
return s->nVars;
}
@ -208,7 +211,7 @@ int cadical_solver_nvars(cadical_solver* s) {
Synopsis [add new variable]
Description [emulated using "nVars".]
Description [also update "nVars" if added by BVA.]
SideEffects []
@ -216,6 +219,9 @@ int cadical_solver_nvars(cadical_solver* s) {
***********************************************************************/
int cadical_solver_addvar(cadical_solver* s) {
if(s->nVars < ccadical_vars((CCaDiCaL*)s->p)) {
s->nVars = ccadical_vars((CCaDiCaL*)s->p);
}
return s->nVars++;
}
@ -223,7 +229,9 @@ int cadical_solver_addvar(cadical_solver* s) {
Synopsis [set number of variables]
Description [not only emulate with "nVars" but also reserve memory.]
Description [emulate with "nVars". also reserve as many variables only
when no variables have been added yet, as it destroys a
satisfying assignment in incremental solving.]
SideEffects []
@ -232,7 +240,9 @@ int cadical_solver_addvar(cadical_solver* s) {
***********************************************************************/
void cadical_solver_setnvars(cadical_solver* s,int n) {
s->nVars = n;
ccadical_reserve((CCaDiCaL*)s->p, n);
if(ccadical_vars((CCaDiCaL*)s->p) == 0) {
ccadical_reserve((CCaDiCaL*)s->p, n);
}
}
/**Function*************************************************************