diff options
Diffstat (limited to 'src/Trace.v')
| -rw-r--r-- | src/Trace.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/Trace.v b/src/Trace.v index 9566c47..0446dae 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -15,6 +15,7 @@ Require Import Bool Int63 PArray. +Require Structures. Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators Assumptions. Local Open Scope array_scope. @@ -35,8 +36,7 @@ Section trace. Variable rho : Valuation.t. - (* We use [array array step] to allow bigger trace *) - Definition _trace_ := array (array step). + Definition _trace_ := Structures.trace step. (* A checker for such a trace *) @@ -44,7 +44,8 @@ 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' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in + let s' := Structures.trace_fold check_step s t 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. *) @@ -82,9 +83,10 @@ Section trace. intros s t' cid Hf Hv. apply (is_false_correct Hf). apply S.valid_get. - apply PArray.fold_left_ind; auto. - intros a i _ Ha;apply PArray.fold_left_ind;trivial. - intros a0 i0 _ H1;auto. + apply Structures.trace_fold_ind; auto. + (* apply PArray.fold_left_ind; auto. *) + (* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *) + (* intros a0 i0 _ H1;auto. *) Qed. End trace. |