aboutsummaryrefslogtreecommitdiffstats
path: root/src/Trace.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Trace.v')
-rw-r--r--src/Trace.v289
1 files changed, 207 insertions, 82 deletions
diff --git a/src/Trace.v b/src/Trace.v
index 17338ca..1849c44 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -11,7 +11,6 @@
Require Import Bool Int63 PArray.
-Require Structures.
Require Import Misc State SMT_terms.
Require Import Syntactic Arithmetic Operators Assumptions.
Require Import Cnf Euf Lia BVList Bva_checker Array_checker.
@@ -34,7 +33,7 @@ Section trace.
Variable rho : Valuation.t.
- Definition _trace_ := Structures.trace step.
+ Definition _trace_ := ((list step) * step)%type.
(* A checker for such a trace *)
@@ -42,7 +41,7 @@ Section trace.
Hypothesis is_false_correct : forall c, is_false c -> ~ C.interp rho c.
Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool :=
- let s' := Structures.trace_fold check_step s t in
+ let s' := List.fold_left check_step (fst t) s in
(* let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in *)
is_false (S.get s' confl).
(* Register _checker_ as PrimInline. *)
@@ -78,7 +77,11 @@ Section trace.
intros s t' cid Hf Hv.
apply (is_false_correct Hf).
apply S.valid_get.
- apply Structures.trace_fold_ind; auto.
+ clear Hf.
+ rewrite <- List.fold_left_rev_right in *.
+ induction (List.rev (fst t')); [ apply Hv | ].
+ apply valid_check_step.
+ apply IHl.
(* apply PArray.fold_left_ind; auto. *)
(* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *)
(* intros a0 i0 _ H1;auto. *)
@@ -117,37 +120,37 @@ Module Sat_Checker.
Definition dimacs := PArray.array (PArray.array _lit).
Definition C_interp_or rho c :=
- afold_left _ _ false orb (Lit.interp rho) c.
+ afold_left _ false orb (amap (Lit.interp rho) c).
Lemma C_interp_or_spec : forall rho c,
C_interp_or rho c = C.interp rho (to_list c).
Proof.
intros rho c; unfold C_interp_or; case_eq (C.interp rho (to_list c)).
- unfold C.interp; rewrite List.existsb_exists; intros [x [H1 H2]]; destruct (In_to_list _ _ H1) as [i [H3 H4]]; subst x; apply (afold_left_orb_true _ i); auto.
- unfold C.interp; intro H; apply afold_left_orb_false; intros i H1; case_eq (Lit.interp rho (c .[ i])); auto; intro Heq; assert (H2: exists x, List.In x (to_list c) /\ Lit.interp rho x = true).
+ unfold C.interp; rewrite List.existsb_exists; intros [x [H1 H2]]; destruct (In_to_list _ _ H1) as [i [H3 H4]]; subst x; apply (afold_left_orb_true i); rewrite ?length_amap,?get_amap;auto.
+ unfold C.interp; intro H; apply afold_left_orb_false; rewrite length_amap; intros i H1; rewrite get_amap; case_eq (Lit.interp rho (c .[ i])); auto; intro Heq; assert (H2: exists x, List.In x (to_list c) /\ Lit.interp rho x = true).
exists (c.[i]); split; auto; apply to_list_In; auto.
rewrite <- List.existsb_exists in H2; rewrite H2 in H; auto.
Qed.
Definition valid rho (d:dimacs) :=
- afold_left _ _ true andb (C_interp_or rho) d.
+ afold_left _ true andb (amap (C_interp_or rho) d).
Lemma valid_spec : forall rho d,
valid rho d <->
- (forall i : int, i < length d -> C.interp rho (PArray.to_list (d.[i]))).
+ (forall i : int, i < length d -> C.interp rho (to_list (d.[i]))).
Proof.
unfold valid; intros rho d; split; intro H.
intros i Hi; case_eq (C.interp rho (to_list (d .[ i]))); try reflexivity.
- intro Heq; erewrite afold_left_andb_false in H; try eassumption.
+ intro Heq; erewrite afold_left_andb_false in H; rewrite ?length_amap, ?get_amap; try eassumption.
rewrite C_interp_or_spec; auto.
- apply afold_left_andb_true; try assumption; intros i Hi; rewrite C_interp_or_spec; apply H; auto.
+ apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap, C_interp_or_spec by assumption; apply H; auto.
Qed.
Inductive certif :=
| Certif : int -> _trace_ step -> clause_id -> certif.
Definition add_roots s (d:dimacs) :=
- PArray.foldi_right (fun i c s => S.set_clause s i (PArray.to_list c)) d s.
+ foldi (fun i s => S.set_clause s i (to_list (d.[i]))) 0 (length d) s.
Definition checker (d:dimacs) (c:certif) :=
let (nclauses, t, confl_id) := c in
@@ -157,7 +160,8 @@ Qed.
forall d s, valid rho d -> S.valid rho s ->
S.valid rho (add_roots s d).
Proof.
- intros rho Hwr d s Hd Hs; unfold add_roots; apply (PArray.foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i Hlt Hv; apply S.valid_set_clause; auto; rewrite valid_spec in Hd; apply Hd; auto.
+ intros rho Hwr d s Hd Hs; unfold add_roots.
+apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto; intros i a _ Hle Hv; apply S.valid_set_clause; auto; rewrite valid_spec in Hd; apply Hd; auto.
Qed.
Lemma checker_correct : forall d c,
@@ -230,7 +234,7 @@ Module Cnf_Checker.
Proof.
intros rho rhobv t_form Ht s H; destruct (Form.check_form_correct rho rhobv _ Ht) as [[Ht1 Ht2] Ht3]; intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i]; simpl; try apply S.valid_set_clause; auto.
apply S.valid_set_resolve; auto.
- apply valid_check_flatten; auto; try discriminate; intros a1 a2; unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a1; auto.
+ apply valid_check_flatten; auto; try discriminate; intros a1 a2; unfold is_true; rewrite Int63.eqb_spec; intro; subst a1; auto.
apply valid_check_True; auto.
apply valid_check_False; auto.
apply valid_check_BuildDef; auto.
@@ -280,7 +284,7 @@ Module Cnf_Checker.
checker_b t_form l b c = true ->
Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l = b.
Proof.
- unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto; rewrite Lit.interp_neg, H1; auto.
+ unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto with smtcoq_core; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core.
Qed.
Definition checker_eq t_form l1 l2 l (c:certif) :=
@@ -296,9 +300,9 @@ Module Cnf_Checker.
Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1 =
Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2.
Proof.
- unfold checker_eq; intros t_var t_form l1 l2 l c; rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
- unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto.
- destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
+ unfold checker_eq; intros t_var t_form l1 l2 l c; rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
+ unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core.
+ destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core.
Qed.
End Cnf_Checker.
@@ -433,49 +437,49 @@ Inductive step :=
|pos orig1 orig2 res|pos orig1 orig2 res
|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res
|pos cl |pos orig res |pos orig res |pos orig res | pos orig1 orig2 res | pos orig1 orig2 res |pos res|pos res
- |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto.
- - apply S.valid_set_resolve; auto.
- - apply S.valid_set_weaken; auto.
- - apply valid_check_flatten; auto; intros h1 h2 H.
- + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto.
- + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto.
- - apply valid_check_True; auto.
- - apply valid_check_False; auto.
- - apply valid_check_BuildDef; auto.
- - apply valid_check_BuildDef2; auto.
- - apply valid_check_BuildProj; auto.
- - apply valid_check_ImmBuildDef; auto.
- - apply valid_check_ImmBuildDef2; auto.
- - apply valid_check_ImmBuildProj; auto.
- - apply valid_check_trans; auto.
- - apply valid_check_congr; auto.
- - apply valid_check_congr_pred; auto.
- - apply valid_check_micromega; auto.
- - apply valid_check_diseq; auto.
- - apply valid_check_spl_arith; auto.
- - apply valid_check_distinct_elim; auto.
- - eapply valid_check_bbVar; eauto.
- - apply valid_check_bbConst; auto.
- - apply valid_check_bbOp; auto.
- - apply valid_check_bbNot; auto.
- - apply valid_check_bbNeg; auto.
- - apply valid_check_bbAdd; auto.
- - apply valid_check_bbConcat; auto.
- - apply valid_check_bbMult; auto.
- - apply valid_check_bbUlt; auto.
- - apply valid_check_bbSlt; auto.
- - apply valid_check_bbEq; auto.
- - apply valid_check_bbDiseq; auto.
- - apply valid_check_bbExtract; auto.
- - apply valid_check_bbZextend; auto.
- - apply valid_check_bbSextend; auto.
- - apply valid_check_bbShl; auto.
- - apply valid_check_bbShr; auto.
- - apply valid_check_roweq; auto.
- - apply valid_check_rowneq; auto.
- - apply valid_check_ext; auto.
- - apply valid_check_hole; auto.
- - apply valid_check_forall_inst with lemma; auto.
+ |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto with smtcoq_core.
+ - apply S.valid_set_resolve; auto with smtcoq_core.
+ - apply S.valid_set_weaken; auto with smtcoq_core.
+ - apply valid_check_flatten; auto with smtcoq_core; intros h1 h2 H.
+ + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto with smtcoq_core.
+ + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto with smtcoq_core.
+ - apply valid_check_True; auto with smtcoq_core.
+ - apply valid_check_False; auto with smtcoq_core.
+ - apply valid_check_BuildDef; auto with smtcoq_core.
+ - apply valid_check_BuildDef2; auto with smtcoq_core.
+ - apply valid_check_BuildProj; auto with smtcoq_core.
+ - apply valid_check_ImmBuildDef; auto with smtcoq_core.
+ - apply valid_check_ImmBuildDef2; auto with smtcoq_core.
+ - apply valid_check_ImmBuildProj; auto with smtcoq_core.
+ - apply valid_check_trans; auto with smtcoq_core.
+ - apply valid_check_congr; auto with smtcoq_core.
+ - apply valid_check_congr_pred; auto with smtcoq_core.
+ - apply valid_check_micromega; auto with smtcoq_core.
+ - apply valid_check_diseq; auto with smtcoq_core.
+ - apply valid_check_spl_arith; auto with smtcoq_core.
+ - apply valid_check_distinct_elim; auto with smtcoq_core.
+ - eapply valid_check_bbVar; eauto with smtcoq_core.
+ - apply valid_check_bbConst; auto with smtcoq_core.
+ - apply valid_check_bbOp; auto with smtcoq_core.
+ - apply valid_check_bbNot; auto with smtcoq_core.
+ - apply valid_check_bbNeg; auto with smtcoq_core.
+ - apply valid_check_bbAdd; auto with smtcoq_core.
+ - apply valid_check_bbConcat; auto with smtcoq_core.
+ - apply valid_check_bbMult; auto with smtcoq_core.
+ - apply valid_check_bbUlt; auto with smtcoq_core.
+ - apply valid_check_bbSlt; auto with smtcoq_core.
+ - apply valid_check_bbEq; auto with smtcoq_core.
+ - apply valid_check_bbDiseq; auto with smtcoq_core.
+ - apply valid_check_bbExtract; auto with smtcoq_core.
+ - apply valid_check_bbZextend; auto with smtcoq_core.
+ - apply valid_check_bbSextend; auto with smtcoq_core.
+ - apply valid_check_bbShl; auto with smtcoq_core.
+ - apply valid_check_bbShr; auto with smtcoq_core.
+ - apply valid_check_roweq; auto with smtcoq_core.
+ - apply valid_check_rowneq; auto with smtcoq_core.
+ - apply valid_check_ext; auto with smtcoq_core.
+ - apply valid_check_hole; auto with smtcoq_core.
+ - apply valid_check_forall_inst with lemma; auto with smtcoq_core.
Qed.
Definition euf_checker (* t_atom t_form *) s t :=
@@ -490,8 +494,8 @@ Inductive step :=
~ (S.valid rho s).
Proof.
unfold euf_checker; intros (* t_i t_func t_atom t_form *) rho H1 H2 H10; apply _checker__correct.
- intros c H; apply C.is_false_correct; auto.
- apply step_checker_correct; auto.
+ intros c H; apply C.is_false_correct; auto with smtcoq_core.
+ apply step_checker_correct; auto with smtcoq_core.
Qed.
Inductive certif :=
@@ -499,15 +503,15 @@ Inductive step :=
Definition add_roots s d used_roots :=
match used_roots with
- | Some ur => PArray.foldi_right (fun i c_index s =>
- let c := if c_index < length d then (d.[c_index])::nil else C._true in
- S.set_clause s i c) ur s
- | None => PArray.foldi_right (fun i c s => S.set_clause s i (c::nil)) d s
+ | Some ur => foldi (fun i s =>
+ let c := if (ur.[i]) < length d then (d.[ur.[i]])::nil else C._true in
+ S.set_clause s i c) 0 (length ur) s
+ | None => foldi (fun i s => S.set_clause s i (d.[i]::nil)) 0 (length d) s
end.
Definition valid t_i t_func t_atom t_form d :=
let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form in
- afold_left _ _ true andb (Lit.interp rho) d.
+ afold_left _ true andb (amap (Lit.interp rho) d).
Lemma add_roots_correct : (* forall t_i t_func t_atom t_form, *)
let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form in
@@ -516,11 +520,11 @@ Inductive step :=
forall s d used_roots, S.valid rho s -> valid t_func t_atom t_form d ->
S.valid rho (add_roots s d used_roots).
Proof.
- intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ _ _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto); case used_roots.
- intro ur; apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; case_eq (ur .[ i] < length d).
- intro; unfold C.valid; simpl; rewrite H5; auto.
- intros; apply C.interp_true; auto.
- apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; unfold C.valid; simpl; rewrite H5; auto.
+ intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto with smtcoq_core); case used_roots.
+ intro ur; apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] < length d).
+ intro; unfold C.valid; simpl; specialize (H5 (ur.[i])); rewrite length_amap, get_amap in H5 by assumption; unfold rho; rewrite H5; auto with smtcoq_core.
+ intros; apply C.interp_true; auto with smtcoq_core.
+ apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; unfold C.valid; simpl; specialize (H5 i); rewrite length_amap, get_amap in H5 by assumption; unfold rho; rewrite H5; auto with smtcoq_core.
Qed.
Definition checker (* t_i t_func t_atom t_form *) d used_roots (c:certif) :=
@@ -534,7 +538,7 @@ Inductive step :=
Definition setup_checker_step_debug d used_roots (c:certif) :=
let (nclauses, t, confl) := c in
let s := add_roots (S.make nclauses) d used_roots in
- (s, Structures.trace_to_list t).
+ (s, fst t).
Definition position_of_step (st:step) :=
@@ -686,7 +690,7 @@ Inductive step :=
let (nclauses, t, confl) := c in
let s := add_roots (S.make nclauses) d used_roots in
let '(_, nb, failure) :=
- Structures.trace_fold
+ List.fold_left
(fun acc step =>
match acc with
| (s, nb, None) =>
@@ -698,7 +702,7 @@ Inductive step :=
else (s, nb, None)
| _ => acc
end
- ) (s, O, None) t
+ ) (fst t) (s, O, None)
in
match failure with
| Some st => Some (nb, name_of_step st)
@@ -711,7 +715,7 @@ Inductive step :=
checker (* t_i t_func t_atom t_form *) d used_roots c = true ->
~ (valid t_func t_atom t_form d).
Proof.
- unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H4]; auto.
+ unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core.
Qed.
Definition checker_b (* t_i t_func t_atom t_form *) l (b:bool) (c:certif) :=
@@ -723,7 +727,7 @@ Inductive step :=
checker_b (* t_func t_atom t_form *) l b c = true ->
Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l = b.
Proof.
- unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto.
+ unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto with smtcoq_core; intros H1; elim (checker_correct H2); auto with smtcoq_core; unfold valid; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by assumption; rewrite get_make; auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core.
Qed.
Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) :=
@@ -740,9 +744,9 @@ Inductive step :=
Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1 =
Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2.
Proof.
- unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
- unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto.
- destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
+ unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
+ unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core.
+ destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by assumption; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core.
Qed.
@@ -762,7 +766,7 @@ Inductive step :=
forall t_i t_func, Atom.wt t_i t_func t_atom ->
~ valid t_func t_atom t_form d.
Proof.
- unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto.
+ unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core.
Qed.
*)
@@ -774,6 +778,127 @@ End Euf_Checker.
Unset Implicit Arguments.
+(* Register constants for OCaml access *)
+Register Sat_Checker.valid as SMTCoq.Trace.Sat_Checker.valid.
+Register Sat_Checker.interp_var as SMTCoq.Trace.Sat_Checker.interp_var.
+Register Sat_Checker.Certif as SMTCoq.Trace.Sat_Checker.Certif.
+Register Sat_Checker.step as SMTCoq.Trace.Sat_Checker.step.
+Register Sat_Checker.Res as SMTCoq.Trace.Sat_Checker.Res.
+Register Sat_Checker.dimacs as SMTCoq.Trace.Sat_Checker.dimacs.
+Register Sat_Checker.certif as SMTCoq.Trace.Sat_Checker.certif.
+Register Sat_Checker.theorem_checker as SMTCoq.Trace.Sat_Checker.theorem_checker.
+Register Sat_Checker.checker as SMTCoq.Trace.Sat_Checker.checker.
+
+Register Cnf_Checker.certif as SMTCoq.Trace.Cnf_Checker.certif.
+Register Cnf_Checker.Certif as SMTCoq.Trace.Cnf_Checker.Certif.
+Register Cnf_Checker.checker_b_correct as SMTCoq.Trace.Cnf_Checker.checker_b_correct.
+Register Cnf_Checker.checker_b as SMTCoq.Trace.Cnf_Checker.checker_b.
+Register Cnf_Checker.checker_eq_correct as SMTCoq.Trace.Cnf_Checker.checker_eq_correct.
+Register Cnf_Checker.checker_eq as SMTCoq.Trace.Cnf_Checker.checker_eq.
+Register Cnf_Checker.step as SMTCoq.Trace.Cnf_Checker.step.
+Register Cnf_Checker.Res as SMTCoq.Trace.Cnf_Checker.Res.
+Register Cnf_Checker.ImmFlatten as SMTCoq.Trace.Cnf_Checker.ImmFlatten.
+Register Cnf_Checker.CTrue as SMTCoq.Trace.Cnf_Checker.CTrue.
+Register Cnf_Checker.CFalse as SMTCoq.Trace.Cnf_Checker.CFalse.
+Register Cnf_Checker.BuildDef as SMTCoq.Trace.Cnf_Checker.BuildDef.
+Register Cnf_Checker.BuildDef2 as SMTCoq.Trace.Cnf_Checker.BuildDef2.
+Register Cnf_Checker.BuildProj as SMTCoq.Trace.Cnf_Checker.BuildProj.
+Register Cnf_Checker.ImmBuildDef as SMTCoq.Trace.Cnf_Checker.ImmBuildDef.
+Register Cnf_Checker.ImmBuildDef2 as SMTCoq.Trace.Cnf_Checker.ImmBuildDef2.
+Register Cnf_Checker.ImmBuildProj as SMTCoq.Trace.Cnf_Checker.ImmBuildProj.
+
+Register Euf_Checker.Certif as SMTCoq.Trace.Euf_Checker.Certif.
+Register Euf_Checker.certif as SMTCoq.Trace.Euf_Checker.certif.
+Register Euf_Checker.checker as SMTCoq.Trace.Euf_Checker.checker.
+Register Euf_Checker.checker_correct as SMTCoq.Trace.Euf_Checker.checker_correct.
+Register Euf_Checker.checker_b_correct as SMTCoq.Trace.Euf_Checker.checker_b_correct.
+Register Euf_Checker.checker_b as SMTCoq.Trace.Euf_Checker.checker_b.
+Register Euf_Checker.checker_eq_correct as SMTCoq.Trace.Euf_Checker.checker_eq_correct.
+Register Euf_Checker.checker_eq as SMTCoq.Trace.Euf_Checker.checker_eq.
+Register Euf_Checker.checker_debug as SMTCoq.Trace.Euf_Checker.checker_debug.
+Register Euf_Checker.name_step as SMTCoq.Trace.Euf_Checker.name_step.
+Register Euf_Checker.Name_Res as SMTCoq.Trace.Euf_Checker.Name_Res.
+Register Euf_Checker.Name_Weaken as SMTCoq.Trace.Euf_Checker.Name_Weaken.
+Register Euf_Checker.Name_ImmFlatten as SMTCoq.Trace.Euf_Checker.Name_ImmFlatten.
+Register Euf_Checker.Name_CTrue as SMTCoq.Trace.Euf_Checker.Name_CTrue.
+Register Euf_Checker.Name_CFalse as SMTCoq.Trace.Euf_Checker.Name_CFalse.
+Register Euf_Checker.Name_BuildDef as SMTCoq.Trace.Euf_Checker.Name_BuildDef.
+Register Euf_Checker.Name_BuildDef2 as SMTCoq.Trace.Euf_Checker.Name_BuildDef2.
+Register Euf_Checker.Name_BuildProj as SMTCoq.Trace.Euf_Checker.Name_BuildProj.
+Register Euf_Checker.Name_ImmBuildDef as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef.
+Register Euf_Checker.Name_ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef2.
+Register Euf_Checker.Name_ImmBuildProj as SMTCoq.Trace.Euf_Checker.Name_ImmBuildProj.
+Register Euf_Checker.Name_EqTr as SMTCoq.Trace.Euf_Checker.Name_EqTr.
+Register Euf_Checker.Name_EqCgr as SMTCoq.Trace.Euf_Checker.Name_EqCgr.
+Register Euf_Checker.Name_EqCgrP as SMTCoq.Trace.Euf_Checker.Name_EqCgrP.
+Register Euf_Checker.Name_LiaMicromega as SMTCoq.Trace.Euf_Checker.Name_LiaMicromega.
+Register Euf_Checker.Name_LiaDiseq as SMTCoq.Trace.Euf_Checker.Name_LiaDiseq.
+Register Euf_Checker.Name_SplArith as SMTCoq.Trace.Euf_Checker.Name_SplArith.
+Register Euf_Checker.Name_SplDistinctElim as SMTCoq.Trace.Euf_Checker.Name_SplDistinctElim.
+Register Euf_Checker.Name_BBVar as SMTCoq.Trace.Euf_Checker.Name_BBVar.
+Register Euf_Checker.Name_BBConst as SMTCoq.Trace.Euf_Checker.Name_BBConst.
+Register Euf_Checker.Name_BBOp as SMTCoq.Trace.Euf_Checker.Name_BBOp.
+Register Euf_Checker.Name_BBNot as SMTCoq.Trace.Euf_Checker.Name_BBNot.
+Register Euf_Checker.Name_BBNeg as SMTCoq.Trace.Euf_Checker.Name_BBNeg.
+Register Euf_Checker.Name_BBAdd as SMTCoq.Trace.Euf_Checker.Name_BBAdd.
+Register Euf_Checker.Name_BBConcat as SMTCoq.Trace.Euf_Checker.Name_BBConcat.
+Register Euf_Checker.Name_BBMul as SMTCoq.Trace.Euf_Checker.Name_BBMul.
+Register Euf_Checker.Name_BBUlt as SMTCoq.Trace.Euf_Checker.Name_BBUlt.
+Register Euf_Checker.Name_BBSlt as SMTCoq.Trace.Euf_Checker.Name_BBSlt.
+Register Euf_Checker.Name_BBEq as SMTCoq.Trace.Euf_Checker.Name_BBEq.
+Register Euf_Checker.Name_BBDiseq as SMTCoq.Trace.Euf_Checker.Name_BBDiseq.
+Register Euf_Checker.Name_BBExtract as SMTCoq.Trace.Euf_Checker.Name_BBExtract.
+Register Euf_Checker.Name_BBZextend as SMTCoq.Trace.Euf_Checker.Name_BBZextend.
+Register Euf_Checker.Name_BBSextend as SMTCoq.Trace.Euf_Checker.Name_BBSextend.
+Register Euf_Checker.Name_BBShl as SMTCoq.Trace.Euf_Checker.Name_BBShl.
+Register Euf_Checker.Name_BBShr as SMTCoq.Trace.Euf_Checker.Name_BBShr.
+Register Euf_Checker.Name_RowEq as SMTCoq.Trace.Euf_Checker.Name_RowEq.
+Register Euf_Checker.Name_RowNeq as SMTCoq.Trace.Euf_Checker.Name_RowNeq.
+Register Euf_Checker.Name_Ext as SMTCoq.Trace.Euf_Checker.Name_Ext.
+Register Euf_Checker.Name_Hole as SMTCoq.Trace.Euf_Checker.Name_Hole.
+Register Euf_Checker.step as SMTCoq.Trace.Euf_Checker.step.
+Register Euf_Checker.Res as SMTCoq.Trace.Euf_Checker.Res.
+Register Euf_Checker.Weaken as SMTCoq.Trace.Euf_Checker.Weaken.
+Register Euf_Checker.ImmFlatten as SMTCoq.Trace.Euf_Checker.ImmFlatten.
+Register Euf_Checker.CTrue as SMTCoq.Trace.Euf_Checker.CTrue.
+Register Euf_Checker.CFalse as SMTCoq.Trace.Euf_Checker.CFalse.
+Register Euf_Checker.BuildDef as SMTCoq.Trace.Euf_Checker.BuildDef.
+Register Euf_Checker.BuildDef2 as SMTCoq.Trace.Euf_Checker.BuildDef2.
+Register Euf_Checker.BuildProj as SMTCoq.Trace.Euf_Checker.BuildProj.
+Register Euf_Checker.ImmBuildProj as SMTCoq.Trace.Euf_Checker.ImmBuildProj.
+Register Euf_Checker.ImmBuildDef as SMTCoq.Trace.Euf_Checker.ImmBuildDef.
+Register Euf_Checker.ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.ImmBuildDef2.
+Register Euf_Checker.EqTr as SMTCoq.Trace.Euf_Checker.EqTr.
+Register Euf_Checker.EqCgr as SMTCoq.Trace.Euf_Checker.EqCgr.
+Register Euf_Checker.EqCgrP as SMTCoq.Trace.Euf_Checker.EqCgrP.
+Register Euf_Checker.LiaMicromega as SMTCoq.Trace.Euf_Checker.LiaMicromega.
+Register Euf_Checker.LiaDiseq as SMTCoq.Trace.Euf_Checker.LiaDiseq.
+Register Euf_Checker.SplArith as SMTCoq.Trace.Euf_Checker.SplArith.
+Register Euf_Checker.SplDistinctElim as SMTCoq.Trace.Euf_Checker.SplDistinctElim.
+Register Euf_Checker.BBVar as SMTCoq.Trace.Euf_Checker.BBVar.
+Register Euf_Checker.BBConst as SMTCoq.Trace.Euf_Checker.BBConst.
+Register Euf_Checker.BBOp as SMTCoq.Trace.Euf_Checker.BBOp.
+Register Euf_Checker.BBNot as SMTCoq.Trace.Euf_Checker.BBNot.
+Register Euf_Checker.BBEq as SMTCoq.Trace.Euf_Checker.BBEq.
+Register Euf_Checker.BBDiseq as SMTCoq.Trace.Euf_Checker.BBDiseq.
+Register Euf_Checker.BBNeg as SMTCoq.Trace.Euf_Checker.BBNeg.
+Register Euf_Checker.BBAdd as SMTCoq.Trace.Euf_Checker.BBAdd.
+Register Euf_Checker.BBMul as SMTCoq.Trace.Euf_Checker.BBMul.
+Register Euf_Checker.BBUlt as SMTCoq.Trace.Euf_Checker.BBUlt.
+Register Euf_Checker.BBSlt as SMTCoq.Trace.Euf_Checker.BBSlt.
+Register Euf_Checker.BBConcat as SMTCoq.Trace.Euf_Checker.BBConcat.
+Register Euf_Checker.BBExtract as SMTCoq.Trace.Euf_Checker.BBExtract.
+Register Euf_Checker.BBZextend as SMTCoq.Trace.Euf_Checker.BBZextend.
+Register Euf_Checker.BBSextend as SMTCoq.Trace.Euf_Checker.BBSextend.
+Register Euf_Checker.BBShl as SMTCoq.Trace.Euf_Checker.BBShl.
+Register Euf_Checker.BBShr as SMTCoq.Trace.Euf_Checker.BBShr.
+Register Euf_Checker.RowEq as SMTCoq.Trace.Euf_Checker.RowEq.
+Register Euf_Checker.RowNeq as SMTCoq.Trace.Euf_Checker.RowNeq.
+Register Euf_Checker.Ext as SMTCoq.Trace.Euf_Checker.Ext.
+Register Euf_Checker.Hole as SMTCoq.Trace.Euf_Checker.Hole.
+Register Euf_Checker.ForallInst as SMTCoq.Trace.Euf_Checker.ForallInst.
+
+
(*
Local Variables:
coq-load-path: ((rec "." "SMTCoq"))