proposition: Lemma eval_augment_cnf : forall o l st (HL : has_literal (hconsmap st) l) (WF : wf_state st), (eval_result_state (augment_cnf (is_classic o) l st) -> eval_ohformula o) -> (eval_state st -> eval_ohformula o).
proof: Proof. intros. unfold augment_cnf in H. destruct (cnf_of_literal l (is_classic o) (fst (defs st)) (snd (defs st)) (arrows st) nil (elt (form_of_literal l)) (form_of_literal l)) as (((cp',cm'),ar'),acc') eqn:EQ . assert (EQ':= EQ). apply wf_cnf_of_literal with (m:=hconsmap st) in EQ' ; auto. change acc' with (snd (cp',cm',ar',acc')) in H. rewrite <- EQ in H. generalize (cnf_of_literal_correct (hconsmap st) o (fst (defs st)) (snd (defs st)) (arrows st) l ). rewrite EQ in *. clear EQ. simpl in *. intros W. apply W. apply has_form_of_literal; auto. intro A. apply H. apply eval_fold_update with (EVAL:=eval_watched_clause) (WP:=has_watched_clause); auto. { intros. eapply has_watched_clause_mono; eauto. } { rewrite Forall_forall. intros. split_and. apply hconsmap_insert_fresh_watched_clause. apply wf_insert_fresh_watched_clause; auto. apply eval_insert_fresh_watched_clause; auto. rewrite Forall_forall in * ; auto. } apply wf_insert_defs ; auto. tauto. apply eval_insert_defs ; auto. tauto. apply wf_arrows; auto. apply has_form_of_literal;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause