# Theory Heuristic

```subsection "Heuristic Algorithms"
theory Heuristic
imports VSAlgos Reindex Optimizations
begin
fun IdentityHeuristic :: "nat ⇒ atom list ⇒ atom fm list ⇒ nat" where
"IdentityHeuristic n _ _ = n"

fun step_augment :: "(nat ⇒ atom list ⇒ atom fm list ⇒ atom fm) ⇒ (nat ⇒ atom list ⇒ atom fm list ⇒ nat) ⇒ nat ⇒ nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
"step_augment step heuristic 0 var L F = list_conj (map fm.Atom L @ F)" |
"step_augment step heuristic (Suc 0) 0 L F = step 0 L F" |
"step_augment step heuristic _ 0 L F = list_conj (map fm.Atom L @ F)" |
"step_augment step heuristic (Suc amount) (Suc i) L F =(
let var = heuristic (Suc i) L F in
let swappedL = map (swap_atom (i+1) var) L in
let swappedF = map (swap_fm (i+1) var) F in
list_disj[step_augment step heuristic amount i al fl. (al,fl)<-dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (i+1) swappedL swappedF))])"

fun the_real_step_augment :: "(nat ⇒ atom list ⇒ atom fm list ⇒ atom fm) ⇒ nat ⇒ (atom list * atom fm list * nat) list ⇒ atom fm" where
"the_real_step_augment step 0 F = list_disj (map (λ(L,F,n). ExN n (list_conj (map fm.Atom L @ F))) F)" |
"the_real_step_augment step (Suc amount) F =(
ExQ (the_real_step_augment step amount (dnf_modified ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(list_disj(map (λ(L,F,n). ExN n (step (n+amount) L F)) F))))))"

fun aquireData :: "nat ⇒ atom list ⇒ (nat fset*nat fset*nat fset)"where
"aquireData n L = fold (λA (l,e,g).
case A of
Eq p ⇒
(
funion l (fset_of_list(filter (λv. let (a,b,c) = get_coeffs v p in
((MPoly_Type.degree p v = 1 ∨ MPoly_Type.degree p v = 2) ∧ (check_nonzero_const a ∨ check_nonzero_const b ∨ check_nonzero_const c))) [0..<(n+1)])),
funion e (fset_of_list(filter (λv.(MPoly_Type.degree p v = 1 ∨ MPoly_Type.degree p v = 2)) [0..<(n+1)]))
,ffilter (λv. MPoly_Type.degree p v ≤ 2) g)
| Leq p ⇒ (l,e,ffilter (λv. MPoly_Type.degree p v ≤ 2) g)
| Neq p ⇒ (l,e,ffilter (λv. MPoly_Type.degree p v ≤ 2) g)
| Less p ⇒ (l,e,ffilter (λv. MPoly_Type.degree p v ≤ 2) g)
) L (fempty,fempty,fset_of_list [0..<(n+1)])"

datatype natpair = Pair "nat*nat"

instantiation natpair :: linorder
begin
definition [simp]: "less_eq (A::natpair) B = (case A of Pair(a,b) ⇒ (case B of Pair(c,d) ⇒ if a=c then b≤d else a<c))"
definition [simp]: "less (A::natpair) B = (case A of Pair(a,b) ⇒ (case B of Pair(c,d) ⇒ if a=c then b<d else a<c))"
instance proof
fix x :: natpair
fix y :: natpair
fix z :: natpair
obtain a b where x : "x = Pair (a,b)" apply(cases x) by auto
obtain c d where y : "y = Pair (c,d)" apply(cases y) by auto
obtain e f where z : "z = Pair (e,f)" apply(cases z) by auto
show "(x < y) = strict (≤) x y"
unfolding x y by auto
show "x≤x" unfolding x by auto
show "x≤ y ⟹ y≤ z ⟹ x≤ z" unfolding x y z apply auto
apply (metis dual_order.trans not_less_iff_gr_or_eq)
by (metis less_trans)
show "x ≤ y ⟹ y ≤ x ⟹ x = y" unfolding x y apply auto
apply (metis not_less_iff_gr_or_eq)
by (metis antisym_conv not_less_iff_gr_or_eq)
show "x ≤ y ∨ y ≤ x" unfolding x y by auto
qed
end

fun getBest :: "nat fset ⇒ atom list ⇒ nat option" where
"getBest S L = (let X =  fset_of_list(map (λx. Pair(count_list (map (λl. case l of
Eq p   ⇒ MPoly_Type.degree p x = 0
|  Less p ⇒ MPoly_Type.degree p x = 0
|  Neq p  ⇒ MPoly_Type.degree p x = 0
|  Leq p  ⇒ MPoly_Type.degree p x = 0
) L) False,x)) (sorted_list_of_fset S)) in
(case (sorted_list_of_fset X) of [] ⇒ None | Cons (Pair(x,v)) _ ⇒ Some v))
"

fun heuristicPicker :: "nat ⇒ atom list ⇒ atom fm list ⇒ (nat*(nat ⇒ atom list ⇒ atom fm list ⇒ atom fm)) option"where
"heuristicPicker n L F = (case (let (l,e,g) = aquireData n L in
(case getBest l L of
None ⇒ (case F of
[] ⇒
(case getBest g L of
None ⇒ (case getBest e L of None ⇒ None | Some v ⇒ Some(v,qe_eq_repeat))
| Some v ⇒ Some(v,gen_qe)
)
| _ ⇒ (case getBest e L of None ⇒ None | Some v ⇒ Some(v,qe_eq_repeat))
)
| Some v ⇒ Some(v,luckyFind')
)) of None => None | Some(var,step) => (if var > n then None else Some(var,step)))"

fun superPicker :: "nat ⇒ nat ⇒ atom list ⇒ atom fm list ⇒ atom fm" where
"superPicker 0 var L F = list_conj (map fm.Atom L @ F)"|
"superPicker amount 0 L F = (case heuristicPicker 0 L F of Some(0,step) ⇒ step 0 L F | _ ⇒ list_conj (map fm.Atom L @ F))" |
"superPicker (Suc amount) (Suc i) L F =(
case heuristicPicker (Suc i) L F of
Some(var,step) ⇒
let swappedL = map (swap_atom (i+1) var) L in
let swappedF = map (swap_fm (i+1) var) F in
list_disj[superPicker amount i al fl. (al,fl)<-dnf ((push_forall ∘ nnf ∘ unpower 0 o groupQuantifiers o clearQuantifiers)(step (i+1) swappedL swappedF))]
| None ⇒ list_conj (map fm.Atom L @ F))"

definition [simp]:"A<B =
(if a1=a2 then (
if b1=b2 then (
if c1=c2 then d1<d2 else c1<c2
) else b1<b2
) else a1<a2)))"
definition [simp]:"A≤B =
(if a1=a2 then (
if b1=b2 then (
if c1=c2 then d1≤d2 else c1<c2
) else b1<b2
) else a1<a2)))"
instance proof
fix x y z
obtain a1 b1 c1 d1 where x : "x = Quad(a1,b1,c1,d1)"
obtain a2 b2 c2 d2 where y : "y = Quad(a2,b2,c2,d2)"
obtain a3 b3 c3 d3 where z : "z = Quad(a3,b3,c3,d3)"
show "(x < y) = strict (≤) x y" unfolding x y by auto
show "x ≤ x" unfolding x by auto
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z" unfolding x y z apply auto
apply (metis dual_order.trans not_less_iff_gr_or_eq)
apply (metis less_trans)
apply (metis dual_order.strict_trans not_less_iff_gr_or_eq)
apply (metis less_trans)
apply (metis dual_order.strict_trans not_less_iff_gr_or_eq)
apply (metis less_trans)
apply (metis less_trans not_less_iff_gr_or_eq)
by (metis less_trans)
show "x ≤ y ⟹ y ≤ x ⟹ x = y" unfolding x y apply auto
apply (metis less_imp_not_less)
apply (metis not_less_iff_gr_or_eq)
apply (metis not_less_iff_gr_or_eq)
by (metis antisym_conv not_less_iff_gr_or_eq)
show "x ≤ y ∨ y ≤ x" unfolding x y by auto
qed
end

fun brownsHeuristic :: "nat ⇒ atom list ⇒ atom fm list ⇒ nat" where
"brownsHeuristic n L _ = (case sorted_list_of_fset (fset_of_list (map (λx.
case (foldl (λ(maxdeg,totaldeg,appearancecount) l.
let p = case l of Eq p ⇒ p | Less p ⇒ p | Leq p ⇒ p | Neq p ⇒ p in
let deg = MPoly_Type.degree p x in
(max maxdeg deg,totaldeg+deg,appearancecount+(if deg>0 then 1 else 0))) (0,0,0) L) of (a,b,c) ⇒ Quad(a,b,c,x)
) [0..<n])) of [] ⇒ n | Cons (Quad(_,_,_,x)) _ ⇒ if x>n then n else x)"

end
```