Fixing invalid API usage of CaDiCaL 3.0

marekpiotrow · marekpiotrow · commit d98f1b7147fe · 2026-01-19T17:42:26.000+01:00
diff --git a/CadicalWrap.h b/CadicalWrap.h
@@ -201,9 +201,9 @@ class SimpSolver {
         int ret = solver->solve();
         conflicts = solver->conflicts();
         if (ret == 10) {
-            int nv = solver->vars();
+            int nv = nvars;
             model.growTo(nv);
-            for (int v = 0 ; v < nv; v++) model[v] = solver->val(v + 1);
+            for (int v = 0 ; v < nv; v++) model[v] = solver->val(lit2val(mkLit(v)));
         }
         return ret == 10 ? l_True : (ret == 20 ? l_False : l_Undef);
     }
@@ -246,8 +246,7 @@ class SimpSolver {
     }
 
     lbool modelValue(Var v) {
-        int cvar = lit2val(mkLit(v));
-        int val = (cvar <= model.size() ? model[cvar - 1] : 0);
+        int val = (v < model.size() ? model[v] : 0);
         return val == 0 ? l_Undef : (val > 0 ? l_True : l_False);
     }
     lbool modelValue(Lit p) {

Original file line number	Diff line number	Diff line change
`@@ -201,9 +201,9 @@ class SimpSolver {`
`201`	`201`	`int ret = solver->solve();`
`202`	`202`	`conflicts = solver->conflicts();`
`203`	`203`	`if (ret == 10) {`
`204`		`- int nv = solver->vars();`
	`204`	`+ int nv = nvars;`
`205`	`205`	`model.growTo(nv);`
`206`		`- for (int v = 0 ; v < nv; v++) model[v] = solver->val(v + 1);`
	`206`	`+ for (int v = 0 ; v < nv; v++) model[v] = solver->val(lit2val(mkLit(v)));`
`207`	`207`	`}`
`208`	`208`	`return ret == 10 ? l_True : (ret == 20 ? l_False : l_Undef);`
`209`	`209`	`}`
`@@ -246,8 +246,7 @@ class SimpSolver {`
`246`	`246`	`}`
`247`	`247`
`248`	`248`	`lbool modelValue(Var v) {`
`249`		`- int cvar = lit2val(mkLit(v));`
`250`		`- int val = (cvar <= model.size() ? model[cvar - 1] : 0);`
	`249`	`+ int val = (v < model.size() ? model[v] : 0);`
`251`	`250`	`return val == 0 ? l_Undef : (val > 0 ? l_True : l_False);`
`252`	`251`	`}`
`253`	`252`	`lbool modelValue(Lit p) {`