Theory DS_Unsigned_Literal
section ‹Encoding of Literals›
theory DS_Unsigned_Literal
imports SAT_Basic LRAT_Sepref_Base
begin
lemma even_bitwise: "even l ⟷ (l AND 0x1) = 0" for l :: nat by auto
lemma odd_pred_div_eq: "odd l ⟹ (l - Suc 0) div 2 = l div 2" by presburger
subsection ‹Positive Natural Numbers›
text ‹Variables in DIMACs are positive natural numbers›
typedef dimacs_var = "{v::nat. v≠0}" morphisms nat_of_var var_of_nat
by blast
type_synonym dv_lit = "dimacs_var literal"
type_synonym dv_clause = "dimacs_var clause"
type_synonym dv_cnf = "dimacs_var cnf"
lemmas [simp] = nat_of_var_inverse nat_of_var_inject
lemma var_of_nat_inverse'[simp]: "x≠0 ⟹ nat_of_var (var_of_nat x) = x"
using var_of_nat_inverse by auto
lemma var_of_nat_inj[simp]: "⟦x≠0; x'≠0⟧ ⟹ var_of_nat x = var_of_nat x' ⟷ x=x'"
by (metis var_of_nat_inverse')
lemma nat_of_var'[simp]:
"nat_of_var x ≠ 0"
"Suc 0 ≤ nat_of_var x"
"0 < nat_of_var x"
using Suc_le_eq nat_of_var by auto
subsection ‹Unsigned Encoding›
text ‹
The lowest bit is the polarity, 0 for positive, 1 for negated.
The higher bits encode the variable index.
›
definition ulit_α :: "nat ⇒ dimacs_var literal" where
"ulit_α n ≡
if even n then Pos (var_of_nat (n div 2))
else Neg (var_of_nat (n div 2))"
definition ulit_invar :: "nat ⇒ bool" where "ulit_invar n ≡ n≥2"
definition "ulit_rel ≡ br ulit_α ulit_invar"
text ‹
To encode an optional literal, we use the unused value 0. Note that also the value 1 is unused.
›
definition ulito_α :: "nat ⇒ dimacs_var literal option" where
"ulito_α n ≡ if n=0 then None else Some (ulit_α n)"
definition ulito_invar :: "nat ⇒ bool" where "ulito_invar n ≡ n=0 ∨ ulit_invar n"
definition "ulito_rel ≡ br ulito_α ulito_invar"
lemma ulit_α_inj[simp]: "⟦ulit_invar n; ulit_invar n'⟧ ⟹ ulit_α n = ulit_α n' ⟷ n=n'"
unfolding ulit_α_def ulit_invar_def apply auto
using div2_even_ext_nat by presburger
lemma ulito_α_inj[simp]: "⟦ulito_invar n; ulito_invar n'⟧ ⟹ ulito_α n = ulito_α n' ⟷ n=n'"
unfolding ulito_α_def ulito_invar_def by auto
subsection ‹Operations on literals›
subsubsection ‹Constructing from nat›
definition mk_ulito :: "nat ⇒ dv_lit option nres" where "mk_ulito n ≡ do { ASSERT(n≠1); RETURN (ulito_α n) }"
lemmas mk_ulito_correct[refine_vcg] = vcg_of_RETURN[OF mk_ulito_def]
lemma mk_ulito_refine: "(RETURN o id,mk_ulito) ∈ nat_rel → ⟨ulito_rel⟩nres_rel"
unfolding mk_ulito_def
apply refine_vcg
by (auto simp: ulito_rel_def in_br_conv ulito_invar_def ulit_invar_def)
subsubsection ‹Negation›
definition ulit_neg :: "nat ⇒ nat" where "ulit_neg l ≡ (if even l then l+1 else l-1)"
lemma ulit_neg_alt: "ulit_neg l = l XOR 0x1"
unfolding ulit_neg_def
by (auto simp: xor_Suc_0_eq)
lemma ulit_neg_correct[simp]:
"ulit_invar l ⟹ ulit_invar (ulit_neg l)"
"ulit_invar l ⟹ ulit_α (ulit_neg l) = neg_lit (ulit_α l)"
unfolding ulit_invar_def ulit_α_def ulito_α_def ulit_neg_def even_bitwise
apply (auto simp: odd_pred_div_eq bitXOR_1_if_mod_2[simplified] simp flip: even_iff_mod_2_eq_zero)
by presburger
subsubsection ‹Zero›
definition ulito_zero :: "nat" where "ulito_zero ≡ 0"
lemma ulito_zero_correct[simp]:
"ulito_invar ulito_zero"
"ulito_α ulito_zero = None"
unfolding ulito_α_def ulito_invar_def ulito_zero_def by auto
definition ulito_is_zero :: "nat ⇒ bool" where "ulito_is_zero n ≡ n=0"
lemma ulito_is_zero_correct[simp]:
"ulito_invar x ⟹ ulito_is_zero x = is_None (ulito_α x)"
unfolding ulito_α_def ulito_invar_def ulito_is_zero_def by auto
text ‹Tagging operation, to indicate that abstraction changes from ulito to ulit›
definition ulito_the :: "nat ⇒ nat" where
"ulito_the n = n"
lemma ulito_the_correct[simp]:
assumes "ulito_invar n"
assumes "¬is_None (ulito_α n)"
shows
"ulit_invar (ulito_the n)"
"ulit_α (ulito_the n) = the (ulito_α n)"
using assms unfolding ulito_invar_def ulito_α_def ulito_the_def
by (auto split: if_splits)
text ‹Tagging operation, to indicate that abstraction changes from ulit to ulito›
definition ulit_wrapo :: "nat ⇒ nat" where "ulit_wrapo n ≡ n"
lemma ulit_wrapo_correct[simp]:
assumes "ulit_invar l"
shows
"ulito_invar (ulit_wrapo l)"
"ulito_α (ulit_wrapo l) = Some (ulit_α l)"
using assms unfolding ulito_invar_def ulit_wrapo_def ulito_α_def
apply simp_all
unfolding ulit_invar_def by auto
subsection ‹Concretization›
fun ulit_of :: "dimacs_var literal ⇒ nat" where
"ulit_of (Pos v) = 2 * nat_of_var v"
| "ulit_of (Neg v) = 2 * nat_of_var v + 1"
lemma ulit_of_inv[simp]:
"ulit_invar (ulit_of l)"
"ulit_α (ulit_of l) = l"
unfolding ulit_invar_def ulit_α_def
by (cases l; auto; fail)+
lemma ulit_of_gtZ: "0<ulit_of l"
by (cases l; auto)
lemma ulit_of_inv'[simp]: "ulit_invar l ⟹ ulit_of (ulit_α l) = l"
unfolding ulit_α_def ulit_invar_def
by auto
lemma ulit_of_inj[simp]: "ulit_of l = ulit_of l' ⟷ l=l'"
apply (cases l; cases l'; simp)
by presburger+
fun ulito_of :: "dimacs_var literal option ⇒ nat" where
"ulito_of None = 0"
| "ulito_of (Some x) = ulit_of x"
lemma ulito_of_inv[simp]:
"ulito_invar (ulito_of l)"
"ulito_α (ulito_of l) = l"
unfolding ulito_invar_def ulito_α_def
apply (cases l; auto)
by (cases l; auto simp: ulit_of_gtZ)
lemma ulito_of_inv'[simp]: "ulito_invar l ⟹ ulito_of (ulito_α l) = l"
unfolding ulito_invar_def ulito_α_def
apply (cases l)
by auto
lemma ulit_of_α[simp]: "ulit_invar x ⟹ ulit_of (ulit_α x) = x"
using ulit_α_inj ulit_of_inv(1) ulit_of_inv(2) by blast
subsection ‹Range of Variables by Maximum Literal›
text ‹Adjust to next odd number, such that both polarities of any variable are covered›
definition ulit_maxlit_adjust :: "nat ⇒ nat" where "ulit_maxlit_adjust ml ≡ if even ml then ml+1 else ml"
lemma ulit_maxlit_adjust_alt: "ulit_maxlit_adjust ml = ml OR 0x1"
unfolding ulit_maxlit_adjust_def
by (auto simp: or_Suc_0_eq)
text ‹Variables covered by given max-literal›
definition "maxlit_vdom ml ≡ { var_of_lit (ulit_α l) | l. l≤ml ∧ ulit_invar l }"
lemma
ulit_maxlit_adjust_correct[simp]:
"ulit_invar (ulit_maxlit_adjust l) = ulit_invar l"
"var_of_lit (ulit_α (ulit_maxlit_adjust l)) = var_of_lit (ulit_α l)"
"odd (ulit_maxlit_adjust l)"
and
ulit_maxlit_adjust_bounds:
"l ≤ ulit_maxlit_adjust l"
"ulit_neg l ≤ ulit_maxlit_adjust l"
unfolding ulit_maxlit_adjust_def ulit_invar_def ulit_α_def ulit_neg_def
by auto
lemma in_maxlit_vdom_iff: "var_of_lit l ∈ maxlit_vdom ml ⟷ ulit_of l ≤ ulit_maxlit_adjust ml"
unfolding maxlit_vdom_def ulit_maxlit_adjust_def ulit_α_def ulit_invar_def
apply (cases l; simp; intro conjI impI iffI)
apply (auto 0 3 intro:
exI[where x="2 * nat_of_var _"]
)
by presburger
lemma maxlit_adjust_vdom[simp]: "maxlit_vdom (ulit_maxlit_adjust ml) = maxlit_vdom ml"
unfolding maxlit_vdom_def
unfolding ulit_maxlit_adjust_def
apply (auto split: if_splits)
subgoal for l
apply (rule exI[where x="if even l then l else l-1"])
unfolding ulit_α_def ulit_invar_def
apply (auto simp: odd_pred_div_eq)
apply fastforce
by presburger
done
lemma maxlit_vdom_mono: "l≤l' ⟹ maxlit_vdom l ⊆ maxlit_vdom l'"
unfolding maxlit_vdom_def
by auto
subsection ‹Implementation›
sepref_def ulito_zero_impl [llvm_inline] is "uncurry0 (RETURN ulito_zero)" :: "unit_assn⇧k →⇩a lit_assn"
unfolding ulito_zero_def
apply (annot_unat_const "lit_size_T")
by sepref
sepref_def ulito_is_zero_impl [llvm_inline] is "RETURN o ulito_is_zero" :: "lit_assn⇧k →⇩a bool1_assn"
unfolding ulito_is_zero_def
apply (annot_unat_const "lit_size_T")
by sepref
sepref_def ulit_neg_impl [llvm_inline] is "RETURN o ulit_neg" :: "lit_assn⇧k →⇩a lit_assn"
unfolding ulit_neg_alt
apply (annot_unat_const "lit_size_T")
by sepref
sepref_def ulit_maxlit_adjust_impl [llvm_inline] is "RETURN o ulit_maxlit_adjust" :: "lit_assn⇧k →⇩a lit_assn"
unfolding ulit_maxlit_adjust_alt
apply (annot_unat_const "lit_size_T")
by sepref
sepref_register ulito_zero ulito_is_zero ulit_neg ulit_maxlit_adjust
text ‹On this level, we make no distinction between literals and wrapped literals,
so we can simply unfold the coercion tagging constants›
lemmas [sepref_preproc] = ulito_the_def[abs_def] ulit_wrapo_def[abs_def]
definition "dimacs_var_rel ≡ (br var_of_nat ((≠)0))"
definition "dimacs_var_assn_aux ≡ (b_assn (unat_assn' lit_size_T) (λx. x<max_var))"
definition "dimacs_var_assn ≡ hr_comp dimacs_var_assn_aux dimacs_var_rel"
lemma dimacs_var_assn_is_pure[safe_constraint_rules, simp]: "is_pure dimacs_var_assn"
unfolding dimacs_var_assn_def dimacs_var_assn_aux_def
by solve_constraint
lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF dimacs_var_assn_is_pure]
definition "mk_dimacs_var n ≡ doN {
ASSERT (n≠0 ∧ n<max_var);
RETURN (var_of_nat n)
}"
lemmas mk_dimacs_var_correct[refine_vcg] = vcg_of_RETURN[OF mk_dimacs_var_def]
lemma mk_dimacs_var_refine: "(mk_dimacs_var,RETURN o var_of_nat) ∈ [λn. n≠0 ∧ n<max_var]⇩f nat_rel → ⟨Id⟩nres_rel"
apply (rule frefI)
apply refine_vcg
by auto
definition "mk_dimacs_var1 n ≡ doN {
ASSERT (n≠0 ∧ n<max_var);
RETURN (op_snat_unat_downcast lit_size_T n)
}"
lemma mk_dimacs_var1_refine: "(mk_dimacs_var1, mk_dimacs_var) ∈ Id → ⟨dimacs_var_rel⟩nres_rel"
unfolding mk_dimacs_var_def mk_dimacs_var1_def dimacs_var_rel_def
apply refine_vcg
by (auto simp: in_br_conv)
sepref_def mk_dimacs_var_impl [llvm_inline] is "mk_dimacs_var1"
:: "size_assn⇧k →⇩a dimacs_var_assn_aux"
supply [simp] = is_down'
unfolding mk_dimacs_var1_def dimacs_var_assn_aux_def
apply (rule hfref_bassn_resI)
subgoal apply refine_vcg by auto
by sepref
term lit_assn
definition "ulit_assn ≡ hr_comp lit_assn ulit_rel"
lemma fold_ulit_assn: "pure (unat_rel O ulit_rel) = ulit_assn"
unfolding ulit_assn_def
by (simp add: hr_comp_pure)
lemma ulit_assn_is_pure[safe_constraint_rules, simp]: "is_pure ulit_assn"
unfolding ulit_assn_def
by solve_constraint
lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF ulit_assn_is_pure]
definition "ulit_mk_pos n ≡ 2*COPY n"
definition "ulit_mk_neg n ≡ 2*COPY n + 1"
lemma ulit_mk_pos_refine: "(ulit_mk_pos,Pos) ∈ dimacs_var_rel → ulit_rel"
unfolding ulit_mk_pos_def
by (auto simp: dimacs_var_rel_def in_br_conv ulit_rel_def ulit_α_def ulit_invar_def)
lemma ulit_mk_neg_refine: "(ulit_mk_neg,Neg) ∈ dimacs_var_rel → ulit_rel"
unfolding ulit_mk_neg_def
by (auto simp: dimacs_var_rel_def in_br_conv ulit_rel_def ulit_α_def ulit_invar_def)
sepref_def ulit_mk_pos_impl [llvm_inline] is "RETURN o ulit_mk_pos" :: "dimacs_var_assn_aux⇧k →⇩a lit_assn"
unfolding ulit_mk_pos_def dimacs_var_assn_aux_def
apply (annot_unat_const lit_size_T)
by sepref
sepref_def ulit_mk_neg_impl [llvm_inline] is "RETURN o ulit_mk_neg" :: "dimacs_var_assn_aux⇧k →⇩a lit_assn"
unfolding ulit_mk_neg_def dimacs_var_assn_aux_def
apply (annot_unat_const lit_size_T)
by sepref
lemma ulit_neg_refine: "(ulit_neg,neg_lit) ∈ ulit_rel → ulit_rel"
by (auto simp: ulit_rel_def in_br_conv)
definition "ulito_assn ≡ hr_comp lit_assn ulito_rel"
lemma fold_ulito_assn: "pure (unat_rel O ulito_rel) = ulito_assn"
unfolding ulito_assn_def
by (simp add: hr_comp_pure)
lemma ulito_assn_is_pure[safe_constraint_rules, simp]: "is_pure ulito_assn"
unfolding ulito_assn_def
by solve_constraint
lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF ulito_assn_is_pure]
definition ulito_None :: "_ literal option" where [simp]: "ulito_None ≡ None"
lemmas fold_ulito_None = ulito_None_def[symmetric]
sepref_register ulito_None
lemma ulito_zero_refine: "(ulito_zero,ulito_None) ∈ ulito_rel"
by (auto simp: ulito_rel_def in_br_conv)
lemma ulito_is_zero_refine: "(ulito_is_zero,is_None) ∈ ulito_rel → bool_rel"
by (auto simp: ulito_rel_def in_br_conv)
lemma ulito_the_refine: "(ulito_the,the) ∈ [λx. ¬is_None x]⇩f ulito_rel → ulit_rel"
unfolding ulito_the_def ulito_rel_def ulit_rel_def
apply (rule frefI)
apply (clarsimp simp: in_br_conv)
subgoal for x y
using ulito_the_correct[of x]
unfolding ulito_the_def
by auto
done
sepref_def ulito_the_impl [llvm_inline] is "RETURN o ulito_the" :: "lit_assn⇧k →⇩a lit_assn"
unfolding ulito_the_def by sepref
lemma ulit_wrapo_refine: "(ulit_wrapo,Some) ∈ ulit_rel → ulito_rel"
unfolding ulito_rel_def ulit_rel_def
by (auto simp: in_br_conv)
sepref_def ulit_wrapo_impl [llvm_inline] is "RETURN o ulit_wrapo" :: "lit_assn⇧k →⇩a lit_assn"
unfolding ulit_wrapo_def by sepref
sepref_definition lit_id_impl [llvm_inline] is "RETURN o id" :: "lit_assn⇧k →⇩a lit_assn"
by sepref
lemma ulit_of_refine: "(id, ulit_of) ∈ ulit_rel → nat_rel"
by (clarsimp simp: ulit_rel_def in_br_conv)
lemma ulito_of_refine: "(id, ulito_of) ∈ ulito_rel → nat_rel"
by (clarsimp simp: ulito_rel_def in_br_conv)
thm mk_ulito_refine
sepref_register var_of_nat mk_dimacs_var Pos Neg mk_ulito
context
notes [fcomp_norm_unfold] = dimacs_var_assn_def[symmetric] ulit_assn_def[symmetric] ulito_assn_def[symmetric] fold_ulit_assn fold_ulito_assn
begin
lemmas mk_dimacs_var_hnr[sepref_fr_rules] = mk_dimacs_var_impl.refine[FCOMP mk_dimacs_var1_refine]
lemmas mk_dimacs_var_hnr'[sepref_fr_rules] = mk_dimacs_var_hnr[FCOMP mk_dimacs_var_refine]
lemmas ulit_mk_pos_hnr[sepref_fr_rules] = ulit_mk_pos_impl.refine[FCOMP ulit_mk_pos_refine]
lemmas ulit_mk_neg_hnr[sepref_fr_rules] = ulit_mk_neg_impl.refine[FCOMP ulit_mk_neg_refine]
lemmas ulit_neg_hnr[sepref_fr_rules] = ulit_neg_impl.refine[FCOMP ulit_neg_refine]
lemmas ulit_of_hnr[sepref_fr_rules] = lit_id_impl.refine[FCOMP ulit_of_refine]
lemmas ulito_zero_hnr[sepref_fr_rules] = ulito_zero_impl.refine[FCOMP ulito_zero_refine]
lemmas ulito_is_zero_hnr[sepref_fr_rules] = ulito_is_zero_impl.refine[FCOMP ulito_is_zero_refine]
lemmas ulito_the_hnr[sepref_fr_rules] = ulito_the_impl.refine[FCOMP ulito_the_refine]
lemmas ulit_wrapo_hnr[sepref_fr_rules] = ulit_wrapo_impl.refine[FCOMP ulit_wrapo_refine]
lemmas ulito_of_hnr[sepref_fr_rules] = lit_id_impl.refine[FCOMP ulito_of_refine]
lemmas mk_ulito_hnr[sepref_fr_rules] = lit_id_impl.refine[FCOMP mk_ulito_refine]
end
definition "some_var ≡ var_of_nat 1"
definition "some_lit ≡ Pos some_var"
sepref_register some_var some_lit
sepref_def some_var_impl [llvm_inline] is "uncurry0 (RETURN some_var)" :: "unit_assn⇧k →⇩a dimacs_var_assn"
unfolding some_var_def
apply (annot_snat_const size_T)
by sepref
sepref_def some_lit_impl [llvm_inline] is "uncurry0 (RETURN some_lit)" :: "unit_assn⇧k →⇩a ulit_assn"
unfolding some_lit_def
by sepref
end