Minor fixes to CakePB

developers/build-sequence

@@ -173,6 +173,12 @@ examples/pseudo_bool/array
 examples/pseudo_bool/array/compilation
 examples/pseudo_bool/array/compilation/proofs
 examples/pseudo_bool/array/compilation/proofsARM8
+examples/pseudo_bool/cnf_encoding/array
+examples/pseudo_bool/cnf_encoding/array/compilation
+examples/pseudo_bool/cnf_encoding/array/compilation/proofs
+examples/pseudo_bool/graph_encoding/array
+examples/pseudo_bool/graph_encoding/array/compilation
+examples/pseudo_bool/graph_encoding/array/compilation/proofs
 examples/pseudo_bool/cp_encoding
 examples/pseudo_bool/cp_encoding/array
 examples/pseudo_bool/cp_encoding/array/compilation

examples/cnf/README.md

@@ -9,11 +9,14 @@ A concrete CNF representation as lists of integers that will be packed.
 [cnfScript.sml](cnfScript.sml):
 Syntax and semantics of CNF
 
+[dimacsScript.sml](dimacsScript.sml):
+Syntax and semantics of CNF in the DIMACS format
+
 [dist](dist):
 An distributed RUP checker
 
 [lrup](lrup):
-An LRUP checker
+An LRUP checker for compressed (variable-byte encoded) proofs
 
 [syntax_helperScript.sml](syntax_helperScript.sml):
 Syntactic print/parse helper files

examples/cnf/ccnfScript.sml

@@ -85,131 +85,6 @@ Proof
   `F` by intLib.ARITH_TAC
 QED
 
-(* Canonical form for a clause: sorted, with repeated literals removed.
-  Nothing in this development canonicalises; the contract exported here is
-  MEM_canon_clause and canon_clause_ALL_DISTINCT.
-
-  Note a 0 literal is left in place: satisfies_ilit never satisfies it. *)
-Definition sorted_nub_aux_def:
-  (sorted_nub_aux h [] acc = (h::acc)) ∧
-  (sorted_nub_aux (h:ilit) (i::is) acc =
-    if i = h then sorted_nub_aux h is acc
-    else sorted_nub_aux i is (h::acc))
-End
-
-Definition sorted_nub_def:
-  (sorted_nub [] = []) ∧
-  (sorted_nub (x::xs) =
-    sorted_nub_aux x xs [])
-End
-
-Definition canon_clause_def:
-  canon_clause (ls:cclause) =
-    let ils = sort ($<=) ls in
-    sorted_nub ils
-End
-
-Theorem sorted_nub_aux_SORTED_strict:
-  ∀ls h acc.
-  SORTED ($>) (h::acc) ∧
-  SORTED ($<=) (h::ls) ⇒
-  SORTED ($>) (sorted_nub_aux h ls acc)
-Proof
-  Induct>>rw[sorted_nub_aux_def]>>
-  first_x_assum irule>>
-  simp[]>>
-  intLib.ARITH_TAC
-QED
-
-Theorem sorted_nub_SORTED_strict:
-  SORTED ($<=) ls ⇒
-  SORTED ($>) (sorted_nub ls)
-Proof
-  rw[oneline sorted_nub_def]>>
-  TOP_CASE_TAC>>gvs[]>>
-  irule sorted_nub_aux_SORTED_strict>>
-  simp[]
-QED
-
-Theorem MEM_sorted_nub_aux:
-  ∀ls x h acc.
-  MEM x ls ∨ x = h ∨ MEM x acc ⇔
-  MEM x (sorted_nub_aux h ls acc)
-Proof
-  Induct>>rw[sorted_nub_aux_def]>>
-  metis_tac[MEM]
-QED
-
-Theorem MEM_sorted_nub:
-  MEM x (sorted_nub ls) ⇔
-  MEM x ls
-Proof
-  rw[oneline sorted_nub_def]>>
-  Cases_on`ls`>>gvs[]>>
-  metis_tac[MEM_sorted_nub_aux,MEM]
-QED
-
-Theorem canon_clause_ALL_DISTINCT:
-  ALL_DISTINCT (canon_clause ls)
-Proof
-  rw[canon_clause_def]>>
-  irule SORTED_ALL_DISTINCT>>
-  irule_at Any sorted_nub_SORTED_strict>>
-  irule_at Any sort_SORTED>>
-  simp[transitive_def,total_def,irreflexive_def]>>
-  intLib.ARITH_TAC
-QED
-
-Theorem MEM_canon_clause[simp]:
-  MEM x (canon_clause ls) ⇔ MEM x ls
-Proof
-  rw[canon_clause_def,MEM_sorted_nub]
-QED
-
-Theorem canon_clause_eq_nil[simp]:
-  canon_clause ls = [] ⇔ ls = []
-Proof
-  `∀l:cclause. l = [] ⇔ ∀x. ¬MEM x l` by
-    (Cases>>simp[]>>metis_tac[])>>
-  metis_tac[MEM_canon_clause]
-QED
-
-Definition canon_vcc_def:
-  canon_vcc v = Vector (canon_clause (toList v))
-End
-
-Theorem toList_canon_vcc[simp]:
-  toList (canon_vcc v) = canon_clause (toList v)
-Proof
-  rw[canon_vcc_def,toList_thm]
-QED
-
-Theorem ALL_DISTINCT_canon_vcc:
-  ALL_DISTINCT (toList (canon_vcc v))
-Proof
-  simp[canon_clause_ALL_DISTINCT]
-QED
-
-Theorem canon_vcc_eq_emp[simp]:
-  canon_vcc v = Vector [] ⇔ v = Vector []
-Proof
-  Cases_on`v`>>rw[canon_vcc_def,toList_thm]
-QED
-
-Theorem satisfies_vcclause_canon_vcc[simp]:
-  satisfies_vcclause w (canon_vcc v) ⇔
-  satisfies_vcclause w v
-Proof
-  rw[satisfies_vcclause_def,satisfies_cclause_def]
-QED
-
-Theorem satisfies_vcfml_IMAGE_canon_vcc[simp]:
-  satisfies_vcfml w (IMAGE canon_vcc cs) ⇔
-  satisfies_vcfml w cs
-Proof
-  rw[satisfies_vcfml_def,satisfies_fml_gen_def,PULL_EXISTS]
-QED
-
 Definition insert_vcc_def:
   insert_vcc fml n v = fml |+ (n, v)
 End

examples/cnf/lrup/lrup_cnfScript.sml → examples/cnf/dimacsScript.sml

@@ -1,9 +1,9 @@
 (*
   Syntax and semantics of CNF in the DIMACS format
 *)
-Theory lrup_cnf
+Theory dimacs
 Ancestors
-  misc cnf ccnf syntax_helper mlstring mlint
+  misc cnf syntax_helper mlstring mlint
 Libs
   preamble
 
@@ -30,53 +30,6 @@ Definition parse_cnf_def:
   | SOME (nvars, nclauses, ls) => SOME ls
 End
 
-(* The same parse, delivered in the checker's clause representation *)
-Definition parse_vcnf_toks_def:
-  parse_vcnf_toks tokss = parse_dimacs_toks_gen parse_vclause tokss
-End
-
-Theorem parse_vcnf_toks:
-  parse_vcnf_toks tokss =
-  OPTION_MAP (λ(v,n,cs). (v,n,conv_cfml cs)) (parse_cnf_toks tokss)
-Proof
-  rw[parse_vcnf_toks_def,parse_cnf_toks_def,
-    parse_dimacs_toks_gen_parse_vclause]
-QED
-
-val cnf_raw = ``[
-  «c this is a comment»;
-  «p cnf 5 4 »;
-  «    1  4 0»;
-  «c this is a comment»;
-  «»;
-  «    2  2  4 0»;
-  «-1 -2 -3 0»;
-  «   -4 -5 0»;
-  ]``;
-
-val test = rconc (EVAL ``THE (parse_cnf ^(cnf_raw))``);
-
-(* Blank lines are skipped, and a clause is stored as it was written,
-  repeated literal and all *)
-Theorem parse_vcnf_toks_test[local]:
-  parse_vcnf_toks (MAP toks ^(cnf_raw)) =
-  SOME (5,4,
-    [Vector [1; 4]; Vector [2; 2; 4]; Vector [-1; -2; -3]; Vector [-4; -5]])
-Proof
-  EVAL_TAC
-QED
-
-(* A run that echoes its input prints unconv_cfml of what it stored, so
-  the echoed formula is the one that was written, repeated literal and all *)
-Theorem unconv_cfml_test[local]:
-  OPTION_MAP (λ(mv,ncl,vcfml). unconv_cfml vcfml)
-    (parse_vcnf_toks (MAP toks ^(cnf_raw))) =
-  SOME [[Pos 1; Pos 4]; [Pos 2; Pos 2; Pos 4];
-        [Neg 1; Neg 2; Neg 3]; [Neg 4; Neg 5]]
-Proof
-  EVAL_TAC
-QED
-
 (* CNF printer *)
 
 (* The variable count declared in the printed header *)
@@ -90,8 +43,6 @@ Definition print_cnf_def:
   MAP (print_lits #"\n") cs
 End
 
-val test2 = rconc (EVAL ``(print_cnf ^(test))``);
-
 (***
   Round trip: parsing the printed formula returns it unchanged
  ***)

examples/cnf/lrup/README.md

@@ -5,6 +5,3 @@ Array-based implementation of the LRUP checker
 
 [lrupScript.sml](lrupScript.sml):
 Specification of an LRUP checker for CNF
-
-[lrup_cnfScript.sml](lrup_cnfScript.sml):
-Syntax and semantics of CNF in the DIMACS format

examples/cnf/lrup/array/compilation/proofs/lrupProofScript.sml

@@ -6,7 +6,7 @@
 Theory lrupProof
 Ancestors
   semanticsProps backendProof x64_configProof TextIOProof
-  lrup_cnf lrup lrup_arrayFullProg lrupCompile
+  dimacs lrup lrup_arrayFullProg lrupCompile
 Libs
   preamble
 

examples/cnf/lrup/array/lrup_arrayFullProgScript.sml

@@ -4,7 +4,7 @@
 Theory lrup_arrayFullProg
 Ancestors
   misc UnsafeProof cnf ccnf ccnf_list ccnf_arrayProg ccnf_parseProg
-  syntax_helper lrup lrup_cnf lrup_list lrup_arrayProg
+  syntax_helper dimacs lrup lrup_list lrup_arrayProg
   basis_ffi
 Libs
   preamble basis

examples/cnf/lrup/array/lrup_arrayProgScript.sml

@@ -4,7 +4,7 @@
 Theory lrup_arrayProg
 Ancestors
   misc mllist UnsafeProof ccnf_arrayProg ccnf_parseProg cnf ccnf ccnf_list
-  syntax_helper lrup_cnf lrup lrup_list
+  syntax_helper lrup lrup_list
   mlint mlvector
 Libs
   preamble basis

examples/cnf/lrup/array/lrup_listScript.sml

@@ -3,7 +3,7 @@
 *)
 Theory lrup_list
 Ancestors
-  cnf ccnf lrup_cnf lrup ccnf_list mlstring mlvector
+  cnf ccnf lrup ccnf_list mlstring mlvector
 Libs
   preamble
 

examples/cnf/lrup/lrupScript.sml

@@ -3,10 +3,66 @@
 *)
 Theory lrup
 Ancestors
-  cnf ccnf syntax_helper lrup_cnf mlstring mlvector
+  cnf ccnf syntax_helper dimacs mlstring mlvector
 Libs
   preamble
 
+(***
+  The CNF input, delivered in the checker's clause representation
+ ***)
+
+Definition parse_vcnf_toks_def:
+  parse_vcnf_toks tokss = parse_dimacs_toks_gen parse_vclause tokss
+End
+
+Theorem parse_vcnf_toks:
+  parse_vcnf_toks tokss =
+  OPTION_MAP (λ(v,n,cs). (v,n,conv_cfml cs)) (parse_cnf_toks tokss)
+Proof
+  rw[parse_vcnf_toks_def,parse_cnf_toks_def,
+    parse_dimacs_toks_gen_parse_vclause]
+QED
+
+val cnf_raw = ``[
+  «c this is a comment»;
+  «p cnf 5 4 »;
+  «    1  4 0»;
+  «c this is a comment»;
+  «»;
+  «    2  2  4 0»;
+  «-1 -2 -3 0»;
+  «   -4 -5 0»;
+  ]``;
+
+val test = rconc (EVAL ``THE (parse_cnf ^(cnf_raw))``);
+
+val test2 = rconc (EVAL ``(print_cnf ^(test))``);
+
+(* Blank lines are skipped, and a clause is stored as it was written,
+  repeated literal and all *)
+Theorem parse_vcnf_toks_test[local]:
+  parse_vcnf_toks (MAP toks ^(cnf_raw)) =
+  SOME (5,4,
+    [Vector [1; 4]; Vector [2; 2; 4]; Vector [-1; -2; -3]; Vector [-4; -5]])
+Proof
+  EVAL_TAC
+QED
+
+(* A run that echoes its input prints unconv_cfml of what it stored, so
+  the echoed formula is the one that was written, repeated literal and all *)
+Theorem unconv_cfml_test[local]:
+  OPTION_MAP (λ(mv,ncl,vcfml). unconv_cfml vcfml)
+    (parse_vcnf_toks (MAP toks ^(cnf_raw))) =
+  SOME [[Pos 1; Pos 4]; [Pos 2; Pos 2; Pos 4];
+        [Neg 1; Neg 2; Neg 3]; [Neg 4; Neg 5]]
+Proof
+  EVAL_TAC
+QED
+
+(***
+  The compressed LRUP proof format
+ ***)
+
 (* The compressed LRUP format has two proof steps. Both carry the raw
   variable-byte encoded bytes of the record they were read from, so that
   neither the deleted ids nor the RUP hints are ever materialised. *)