diff options
Diffstat (limited to 'src/cnf/Cnf.v')
| -rw-r--r-- | src/cnf/Cnf.v | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index b5ecfb0..73f9f97 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -1,22 +1,17 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) (**************************************************************************) -(* Add LoadPath ".." as SMTCoq. *) Require Import PArray List Bool. -Require Import Misc State SMT_terms. +Require Import Misc State SMT_terms BVList. Import Form. @@ -255,14 +250,15 @@ Section CHECKER. (** The correctness proofs *) Variable interp_atom : atom -> bool. + Variable interp_bvatom : atom -> forall s, BITVECTOR_LIST.bitvector s. Hypothesis Hch_f : check_form t_form. - Local Notation rho := (Form.interp_state_var interp_atom t_form). + Local Notation rho := (Form.interp_state_var interp_atom interp_bvatom t_form). Let Hwfrho : Valuation.wf rho. Proof. - destruct (check_form_correct interp_atom _ Hch_f) as (_, H);exact H. + destruct (check_form_correct interp_atom interp_bvatom _ Hch_f) as (_, H);exact H. Qed. Lemma valid_check_True : C.valid rho check_True. @@ -279,9 +275,9 @@ Section CHECKER. Qed. Let rho_interp : forall x : int, - rho x = interp interp_atom t_form (t_form.[ x]). + rho x = interp interp_atom interp_bvatom t_form (t_form.[ x]). Proof. - destruct (check_form_correct interp_atom _ Hch_f) as ((H,H0), _). + destruct (check_form_correct interp_atom interp_bvatom _ Hch_f) as ((H,H0), _). intros x;apply wf_interp_form;trivial. Qed. |