Merge pull request #828 from CakeML/sat_encodings

New example: verified SAT encoding functions

developers/build-sequence

@@ -97,6 +97,10 @@ examples/opentheory/compilation
 examples/opentheory/compilation/proofs
 examples/opentheory/compilation/ag32
 examples/opentheory/compilation/ag32/proofs
+examples/sat_encodings
+examples/sat_encodings/case_studies
+examples/sat_encodings/translation
+examples/sat_encodings/translation/compilation
 
 translator/okasaki-examples
 translator/other-examples

examples/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = $(HOLDIR)/examples/formal-languages/regular\
+INCLUDES = $(HOLDIR)/examples/formal-languages/regular $(HOLDIR)/examples/bootstrap \
 					 $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
 					 $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis/pure $(CAKEMLDIR)/basis\
 					 $(CAKEMLDIR)/translator $(CAKEMLDIR)/characteristic

examples/README.md

@@ -54,6 +54,9 @@ Faster cat: process 2048 chars at a time.
 [lcsScript.sml](lcsScript.sml):
 Verification of longest common subsequence algorithms.
 
+[lispProgScript.sml](lispProgScript.sml):
+Parsing and pretty printing of s-expressions
+
 [lpr_checker](lpr_checker):
 An LPR checker built on CakeML
 
@@ -73,6 +76,9 @@ In-place quick sort on a polymorphic array.
 [replProgScript.sml](replProgScript.sml):
 The CakeML REPL
 
+[sat_encodings](sat_encodings):
+Encodings of puzzles to CNF, to use as SAT-solver input.
+
 [sortProgScript.sml](sortProgScript.sml):
 Program to sort the lines in a file, built on top of the quick sort example.
 

examples/lispProgScript.sml

@@ -0,0 +1,92 @@
+(*
+  Parsing and pretty printing of s-expressions
+*)
+open preamble basis miscTheory set_sepTheory listTheory mlstringTheory;
+open (* lisp: *) parsingTheory source_valuesTheory printingTheory;
+
+val _ = new_theory "lispProg";
+
+val _ = translation_extends "basisProg";
+
+val _ = show_assums := true;
+
+(* --- functions from source_valuesTheory --- *)
+
+val res = translate name_def;
+val res = translate head_def;
+val res = translate tail_def;
+val res = translate isNum_def;
+val res = translate v2list_def;
+val res = translate list_def;
+
+(* --- functions from parsingTheory --- *)
+
+val res = translate quote_def;
+val res = translate parse_def;
+val res = translate end_line_def;
+val res = translate read_num_def;
+val res = translate (REWRITE_RULE [MEMBER_INTRO] lex_def);
+
+val ind_lemma = Q.prove(
+  `^(first is_forall (hyp res))`,
+  rpt gen_tac
+  \\ rpt (disch_then strip_assume_tac)
+  \\ match_mp_tac (latest_ind ())
+  \\ rpt strip_tac
+  \\ last_x_assum match_mp_tac
+  \\ rpt strip_tac
+  \\ fs [FORALL_PROD]
+  \\ gvs[MEMBER_def])
+  |> update_precondition;
+
+val res = translate lexer_def;
+
+Definition from_str_def:
+  from_str s = head (parse (lexer s) (Num 0) [])
+End
+
+val res = translate from_str_def;
+
+(* --- functions from printingTheory --- *)
+
+val res = translate num2str_def;
+
+Triviality num2str_side:
+  ∀n. num2str_side n
+Proof
+  ho_match_mp_tac num2str_ind \\ rpt strip_tac
+  \\ once_rewrite_tac [fetch "-" "num2str_side_def"] \\ rw []
+  \\ ‘n MOD 10 < 10’ by fs [MOD_LESS, SF SFY_ss] \\ simp []
+QED
+
+val _ = update_precondition num2str_side;
+
+val res = translate num2ascii_def;
+val res = translate ascii_name_def;
+
+Triviality ascii_name_side:
+  ∀n. ascii_name_side n
+Proof
+  rw [fetch "-" "ascii_name_side_def"]
+  \\ fs [Once num2ascii_def,AllCaseEqs()]
+QED
+
+val _ = update_precondition ascii_name_side;
+
+val res = translate name2str_def;
+val res = translate dest_quote_def;
+val res = translate dest_list_def;
+val res = translate newlines_def;
+val res = translate v2pretty_def;
+val res = translate get_size_def;
+val res = translate get_next_size_def;
+val res = translate annotate_def;
+val res = translate remove_all_def;
+val res = translate smart_remove_def;
+val res = translate flatten_def;
+val res = translate dropWhile_def;
+val res = translate is_comment_def;
+val res = translate v2str_def;
+val res = translate vs2str_def;
+
+val _ = export_theory();

examples/sat_encodings/Holmakefile

@@ -0,0 +1,11 @@
+INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
+
+
+

examples/sat_encodings/README.md

@@ -0,0 +1,38 @@
+Encodings of puzzles to CNF, to use as SAT-solver input.
+
+[boolExpToCnfScript.sml](boolExpToCnfScript.sml):
+Encoding from boolExp to cnf using Tseytin transformation
+
+[case_studies](case_studies):
+Different puzzles and problems encoded to suitable versatile datatypes.
+
+[cnfScript.sml](cnfScript.sml):
+Definition of CNF
+
+[demo](demo):
+Scripts and example problems for the encoders.
+
+[numBoolExpScript.sml](numBoolExpScript.sml):
+Encode natural numbers to Booleans using order encoding
+
+[numBoolExtendedScript.sml](numBoolExtendedScript.sml):
+Extend numBoolExp with more functionality
+
+[numBoolRangeScript.sml](numBoolRangeScript.sml):
+Add individual upper and lower bounds for each number variable
+
+[old_boolExpToCnfScript.sml](old_boolExpToCnfScript.sml):
+Encoding from Boolean expressions to CNF.
+
+[orderEncodingBoolScript.sml](orderEncodingBoolScript.sml):
+Extend pseudoBoolExp with OrderAxiom, to prepare for order encoding
+of natural numbers.
+
+[quantifierExpScript.sml](quantifierExpScript.sml):
+Quantifiers over Boolean expressions and pseudo-Boolean constraints
+
+[translation](translation):
+Translation scripts for puzzle encodings.
+
+[unorderedSetsScript.sml](unorderedSetsScript.sml):
+Encode unordered sets to natural numbers