Theory IsaSAT_CDCL_Defs

theory IsaSAT_CDCL_Defs
  imports IsaSAT_Propagate_Conflict_Defs IsaSAT_Other_Defs IsaSAT_Show
begin


paragraph ‹Combining Together: Full Strategy›

definition  cdcl_twl_stgy_prog_wl_D_heur
   :: ‹isasat ⇒ isasat nres›
where
  ‹cdcl_twl_stgy_prog_wl_D_heur S⇩0 =
  do {
    do {
        (brk, T) ← WHILE⇩T
        (λ(brk, _). ¬brk)
        (λ(brk, S).
        do {
          T ← unit_propagation_outer_loop_wl_D_heur S;
          cdcl_twl_o_prog_wl_D_heur T
        })
        (False, S⇩0);
      RETURN T
    }
  }
  ›
definition cdcl_twl_stgy_prog_break_wl_D_heur :: ‹isasat ⇒ isasat nres›
where
  ‹cdcl_twl_stgy_prog_break_wl_D_heur S⇩0 =
  do {
    b ← RETURN (isasat_fast S⇩0);
    (b, brk, T) ← WHILE⇩T⇗λ(b, brk, T). True⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(b, brk, S).
        do {
          ASSERT(isasat_fast S);
          T ← unit_propagation_outer_loop_wl_D_heur S;
          ASSERT(isasat_fast T);
          (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
          b ← RETURN (isasat_fast T);
          RETURN(b, brk, T)
        })
        (b, False, S⇩0);
    if brk then RETURN T
    else cdcl_twl_stgy_prog_wl_D_heur T
  }›


definition cdcl_twl_stgy_prog_bounded_wl_heur :: ‹isasat ⇒ (bool × isasat) nres›
where
  ‹cdcl_twl_stgy_prog_bounded_wl_heur S⇩0 =
  do {
    b ← RETURN (isasat_fast S⇩0);
    (b, brk, T) ← WHILE⇩T⇗λ(b, brk, T). True⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(b, brk, S).
        do {
          ASSERT(isasat_fast S);
          T ← unit_propagation_outer_loop_wl_D_heur S;
          ASSERT(isasat_fast T);
          (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
          b ← RETURN (isasat_fast T);
          RETURN(b, brk, T)
        })
        (b, False, S⇩0);
    RETURN (brk, T)
  }›

end