Theory IsaSAT_Print_LLVM

theory IsaSAT_Print_LLVM
  imports IsaSAT_Literals_LLVM
begin

definition print_propa :: ‹64 word ⇒ unit› where
  ‹print_propa _ = ()›

definition print_confl :: ‹64 word ⇒ unit› where
  ‹print_confl _ = ()›

definition print_dec :: ‹64 word ⇒ unit› where
  ‹print_dec _ = ()›

definition print_res :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_res _ _ = ()›

definition print_lres :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_lres _ _ = ()›

definition print_uset :: ‹64 word ⇒ unit› where
  ‹print_uset _ = ()›

definition print_gcs :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_gcs _ _ = ()›

definition print_binary_unit :: ‹64 word ⇒ unit› where
  ‹print_binary_unit _ = ()›

definition print_binary_red_removed :: ‹64 word ⇒ unit› where
  ‹print_binary_red_removed _ = ()›

definition print_purelit_elim :: ‹64 word ⇒ unit› where
  ‹print_purelit_elim _ = ()›

definition print_purelit_rounds :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_purelit_rounds _ _ = ()›

definition print_lbds :: ‹64 word ⇒ unit› where
  ‹print_lbds _ = ()›

definition print_forward_rounds :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_forward_rounds _ _ = ()›

definition print_forward_subsumed :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_forward_subsumed _ _ = ()›

definition print_forward_tried :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_forward_tried _ _ = ()›

definition print_forward_strengthened :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_forward_strengthened _ _ = ()›

definition print_rephased :: ‹64 word ⇒ 64 word ⇒ unit› where
  ‹print_rephased _ _ = ()›

sepref_def print_propa_impl
  is ‹RETURN o print_propa›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_propa_def
  by sepref

sepref_def print_confl_impl
  is ‹RETURN o print_confl›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_confl_def
  by sepref

sepref_def print_dec_impl
  is ‹RETURN o print_dec›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_dec_def
  by sepref

sepref_def print_res_impl
  is ‹uncurry (RETURN oo print_res)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_res_def
  by sepref

sepref_def print_lres_impl
  is ‹uncurry (RETURN oo print_lres)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_lres_def
  by sepref

sepref_def print_uset_impl
  is ‹RETURN o print_uset›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_uset_def
  by sepref

definition print_irred_clss :: ‹64 word ⇒ unit› where
  ‹print_irred_clss _ = ()›

sepref_def print_gc_impl
  is ‹uncurry (RETURN oo print_gcs)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_gcs_def
  by sepref

sepref_def print_irred_clss_impl
  is ‹RETURN o print_irred_clss›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_irred_clss_def
  by sepref

sepref_def print_binary_unit_impl
  is ‹RETURN o print_binary_unit›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_binary_unit_def
  by sepref

sepref_def print_purelit_rounds_impl
  is ‹uncurry (RETURN oo print_purelit_rounds)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_purelit_rounds_def
  by sepref

sepref_def print_purelit_elim_impl
  is ‹RETURN o print_purelit_elim›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_purelit_elim_def
  by sepref

sepref_def print_binary_red_removed_impl
  is ‹RETURN o print_binary_red_removed›
  :: ‹word_assn⇧k →⇩a unit_assn›
  unfolding print_binary_red_removed_def
  by sepref

sepref_def print_forward_rounds_impl
  is ‹uncurry (RETURN oo print_forward_rounds)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_forward_rounds_def
  by sepref

sepref_def print_forward_subsumed_impl
  is ‹uncurry (RETURN oo print_forward_subsumed)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_forward_subsumed_def
  by sepref

sepref_def print_forward_tried_impl
  is ‹uncurry (RETURN oo print_forward_tried)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_forward_tried_def
  by sepref

sepref_def print_forward_strengthened_impl
  is ‹uncurry (RETURN oo print_forward_strengthened)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_forward_strengthened_def
  by sepref

sepref_def print_rephased_impl
  is ‹uncurry (RETURN oo print_rephased)›
  :: ‹word_assn⇧k *⇩a word_assn⇧k →⇩a unit_assn›
  unfolding print_rephased_def
  by sepref

end