report the correct number of variables in unsat nnf

QuMuLab / dsharp

MIT License

16 stars 5 forks source link

report the correct number of variables in unsat nnf #14

Closed symphorien closed 3 years ago

symphorien commented 3 years ago

I should have seen it while reviewing #13

haz commented 3 years ago

Hrmz...do satisfiable theories with un-smooth outputs include the correct variable count? Now I'm wondering if it only reports the number of variables that actually appear in the d-DNNF...

symphorien commented 3 years ago

Yes:

$  cat foo.cnf
p cnf 10 1
1 0
$  ./dsharp -Fnnf nnf -Fgraph graph foo.cnf  
$  cat nnf 
nnf 1 1 10
L 1