Compiling the pseudo-boolean constraints checker
cliqueCompileScript.sml: Compiles the max clique + PB checker
cnfCompileScript.sml: Compiles the CNF + PB checker
mccisCompileScript.sml: Compiles the MCCIS + PB checker
mcisCompileScript.sml: Compiles the MCIS + PB checker
npbc_fullCompileScript.sml: Compiles the PB checker example by evaluation inside the logic of HOL
proofs: Prove end-to-end correctness theorem for PB checker with arrays
proofsARM8: Prove end-to-end correctness theorem for PB checker with arrays
subgraph_isoCompileScript.sml: Compiles the encoder
wcnfCompileScript.sml: Compiles the WCNF + PB checker