-
Notifications
You must be signed in to change notification settings - Fork 87
/
Copy pathsat_encodersProgScript.sml
187 lines (163 loc) · 6.33 KB
/
sat_encodersProgScript.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
(*
Translate of all to-CNF encoding functions
*)
open preamble basis miscTheory set_sepTheory listTheory lispProgTheory;
open boolExpToCnfTheory quantifierExpTheory orderEncodingBoolTheory;
open numBoolExpTheory numBoolExtendedTheory numBoolRangeTheory;
open unorderedSetsTheory toCnfHelperTheory cnfTheory;
open (* for parsing: *) parsingTheory source_valuesTheory;
val _ = new_theory "sat_encodersProg";
val _ = translation_extends "lispProg";
val _ = show_assums := true;
(* boolExp *)
val res = translate bind_def;
val res = translate get_fresh_name_constFree_def;
val res = translate boolExp_to_constFree_def;
val res = translate constFree_to_cnf_inner_def;
val res = translate negate_literal_def;
val res = translate replace_not_def;
val res = translate replace_or_def;
val res = translate replace_and_def;
val res = translate replace_impl_def;
val res = translate replace_iff_def;
val res = translate rhs_to_cnf_def;
val res = translate append_aux_def;
val res = translate append_def;
val res = translate map_to_cnf_def;
val res = translate constFree_to_cnf_def;
val res = translate boolExp_to_cnf_def;
(* quantifierExp *)
val res = translate bool_to_quant_def;
val res = translate quant_size';
val res = translate pseudoBool_size';
val res = translate replace_name_quant_def;
val res = translate quant_to_boolExp_def;
val res = translate none_of_list_to_quant_def;
val res = translate most_one_to_quant_def;
val res = translate pseudoBool_to_quant_def;
(* orderEncodingBool *)
val res = translate orderBool_size';
val res = translate encode_orderAxiom_def;
val res = translate orderBool_to_pseudoBool_def;
(* numBoolExp *)
val res = translate (REWRITE_RULE [MEMBER_INTRO] add_numVar_to_list_def);
val res = translate (REWRITE_RULE [MEMBER_INTRO] nub_def);
val res = translate create_numVarList_inner_def;
val res = translate create_numVarList_def;
val res = translate get_fresh_boolVar_def;
val res = translate create_numVarMap_inner_def;
val res = translate create_numVarMap_def;
val res = translate vMap_to_orderBool_def;
val res = translate encode_combinations_def;
val res = translate encode_add_def;
val res = translate encode_leq_def;
val res = translate EL;
val el_side_def = fetch "-" "el_side_def";
Theorem el_side:
∀ n l.
n < LENGTH l ⇒
el_side n l
Proof
gs[Once el_side_def]
>> Induct
>- (rw[]
>> Cases_on ‘l = []’ >> gs[])
>> rw[]
>> rw[Once el_side_def]
>- (Cases_on ‘l’ >> gs[]
>> Cases_on ‘t’ >> gs[])
>> first_x_assum (qspecl_then [‘TL l’] assume_tac)
>> first_x_assum irule
>> gs[ADD1]
>> Cases_on ‘l’ >> gs[]
QED
val res = translate encode_eqConst_def; (* side *)
val encode_eqconst_side_def = fetch "-" "encode_eqconst_side_def";
Theorem encode_eqconst_side:
∀ n bvs.
encode_eqconst_side n bvs
Proof
gs[Once encode_eqconst_side_def]
>> rw[]
>- gs[]
>- (irule el_side
>> gs[])
>> irule el_side
>> gs[]
QED
val _ = update_precondition encode_eqconst_side;
val res = translate encode_leqConst_def; (* side *)
val encode_leqconst_side_def = fetch "-" "encode_leqconst_side_def";
Theorem encode_leqconst_side:
∀ n bvs.
encode_leqconst_side n bvs
Proof
rw[Once encode_leqconst_side_def]
>> irule el_side >> gs[]
QED
val _ = update_precondition encode_leqconst_side;
val res = translate numBoolExp_to_orderBool_def;
val res = translate encode_axioms_def;
val res = translate numBool_to_orderBool_def;
val res = translate invert_numVarMap_def;
val res = translate encode_assignment_def;
val res = translate minimal_encode_assignment_def;
val res = translate find_value_def;
val res = translate assignment_to_numVarAssignment_def;
val res = translate minimal_assignment_to_numVarAssignment_def;
(* numBoolExtended *)
val res = translate create_numVarList_numBoolExtended_inner_def;
val res = translate create_numVarList_numBoolExtended_def;
val res = translate numBoolExtended_to_numBoolExp_def;
val res = translate encode_assignment_numBoolExtended_def;
val res = translate assignment_to_numVarAssignment_numBoolExtended_def;
(* numBoolRange *)
val res = translate equation_to_numBoolExtended_def;
val res = translate ranges_to_numBoolExtended_def;
val res = translate numBoolRange_to_numBoolExtended_def;
val res = translate get_highest_max_def;
val res = translate rangeList_to_numVarList_def;
val res = translate encode_assignment_numBoolRange_def;
val res = translate assignment_to_numVarAssignment_numBoolRange_def;
(* unorderedSet *)
val res = translate get_varList_inner_def;
val res = translate get_varList_def;
val res = translate indexedListsTheory.findi_def;
val res = translate encode_constant_def;
val res = translate equation_to_numBoolRange_def;
val res = translate get_setName_def;
val res = translate elementVarAssignment_to_numVarAssignment_inner_def;
val res = translate elementVarAssignment_to_numVarAssignment_def;
val res = translate get_max_def;
val res = translate equation_to_rangeList_inner_def;
val res = translate equation_to_rangeList_def;
val res = translate eval_literal_def;
val res = translate eval_rhs_def;
val res = translate make_assignments_def;
val res = translate constFree_to_assignment_def;
val res = translate boolExp_to_assignment_def;
val res = translate pseudoBool_to_assignment_def;
val res = translate orderBool_to_assignment_def;
val res = translate numBoolExp_to_assignment_def;
val res = translate numBoolExtended_to_assignment_def;
val res = translate numBoolRange_to_assignment_def;
val res = translate encode_assignment_unorderedSet_def;
val res = translate oEL_def;
val res = translate numVarAssignment_to_elementVarAssignment_inner_def;
val res = translate numVarAssignment_to_elementVarAssignment_def;
val res = translate assignment_to_elementVarAssignment_def;
val res = translate constFree_to_cnf_inner_def;
val res = translate constFree_to_cnf_def;
val res = translate boolExp_to_cnf_def;
val res = translate pseudoBool_to_cnf_def;
val res = translate orderBool_to_cnf_def;
val res = translate numBool_to_cnf_def;
val res = translate numBoolExtended_to_cnf_def;
val res = translate numBoolRange_to_cnf_def;
val res = translate equation_to_cnf_def;
val res = translate rangeList_ok_def;
val res = translate (exp_rangeList_ok_def |> PURE_REWRITE_RULE [MEMBER_INTRO]);
val res = translate (numVarAssignment_range_ok_def |> PURE_REWRITE_RULE [MEMBER_INTRO]);
val res = translate get_first_non_boolVar_num_def
val res = translate get_boolVar_list_def
val _ = export_theory();