Theory IsaSAT_Other_Defs

theory IsaSAT_Other_Defs
imports IsaSAT_Conflict_Analysis_Defs IsaSAT_Backtrack_Defs IsaSAT_Decide_Defs
begin
chapter ‹Combining Together: the Other Rules›

definition cdcl_twl_o_prog_wl_D_heur
 :: ‹isasat ⇒ (bool × isasat) nres›
where
  ‹cdcl_twl_o_prog_wl_D_heur S =
    do {
      if get_conflict_wl_is_None_heur S
      then decide_wl_or_skip_D_heur S
      else do {
        if count_decided_st_heur S > 0
        then do {
          T ← skip_and_resolve_loop_wl_D_heur S;
          ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur T));
          ASSERT(get_learned_count S = get_learned_count T);
          U ← backtrack_wl_D_nlit_heur T;
          U ← isasat_current_status U; ― ‹Print some information every once in a while›
          RETURN (False, U)
        }
        else RETURN (True, S)
      }
    }
  ›

end