From a5156f257e172185695aba1d10a9c15c5899b377 Mon Sep 17 00:00:00 2001 From: MyskYko Date: Fri, 20 Jun 2025 13:40:04 -0700 Subject: [PATCH 1/3] fix cadical --- src/sat/cadical/cadicalSolver.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index 9caea6605..677f32fe7 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -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; } @@ -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++; } From 9ea1aaa3cf00ed94dcf359d6b86472f8afc068c6 Mon Sep 17 00:00:00 2001 From: MyskYko Date: Fri, 20 Jun 2025 14:45:50 -0700 Subject: [PATCH 2/3] fix comments --- src/sat/cadical/cadicalSolver.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index 677f32fe7..4b3230bad 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -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 [] @@ -211,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 [] @@ -229,7 +229,7 @@ int cadical_solver_addvar(cadical_solver* s) { Synopsis [set number of variables] - Description [not only emulate with "nVars" but also reserve memory.] + Description [set "nVars" and reserve as many variables.] SideEffects [] From 6e130c15a37a1addd70c0519b93577d1a65706b7 Mon Sep 17 00:00:00 2001 From: MyskYko Date: Fri, 20 Jun 2025 15:28:27 -0700 Subject: [PATCH 3/3] fix setnvars --- src/sat/cadical/cadicalSolver.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index 4b3230bad..bf6df9512 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -229,7 +229,9 @@ int cadical_solver_addvar(cadical_solver* s) { Synopsis [set number of variables] - Description [set "nVars" and reserve as many variables.] + 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 [] @@ -238,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*************************************************************