diff options
| -rw-r--r-- | INSTALL.md | 8 | ||||
| -rw-r--r-- | src/Makefile | 38 | ||||
| -rw-r--r-- | src/SMT_terms.v | 2 | ||||
| -rw-r--r-- | src/array/FArray.v | 2 | ||||
| -rw-r--r-- | src/bva/BVList.v | 38 | ||||
| -rw-r--r-- | src/classes/SMT_classes.v | 2 | ||||
| -rw-r--r-- | src/lfsc/lfscLexer.mll | 71 | ||||
| -rw-r--r-- | src/lia/Lia.v | 200 | ||||
| -rw-r--r-- | src/lia/lia.ml | 20 | ||||
| -rw-r--r-- | src/smtlib2/sExprLexer.mll | 80 | ||||
| -rw-r--r-- | src/trace/smtMisc.ml | 47 | ||||
| -rw-r--r-- | src/trace/smtMisc.mli | 9 | ||||
| -rw-r--r-- | unit-tests/Tests_lfsc_tactics.v | 14 |
13 files changed, 275 insertions, 256 deletions
@@ -73,7 +73,7 @@ Then follow the instructions of the previous section. ### Requirements -You need to have OCaml version >= 4.11.1 and Coq version 8.12.*. +You need to have OCaml version >= 4.11.1 and Coq version 8.13.*. > **Warning**: The version of Coq that you plan to use must have been compiled > with the same version of OCaml that you are going to use to compile @@ -111,16 +111,16 @@ opam switch create ocaml-base-compiler.4.11.1 ### Install Coq -After OCaml is installed, you can install Coq-8.12.1 through opam. +After OCaml is installed, you can install Coq-8.13.2 through opam. ```bash -opam install coq.8.12.1 +opam install coq.8.13.2 ``` If you also want to install CoqIDE at the same time you can do ```bash -opam install coq.8.12.1 coqide.8.12.1 +opam install coq.8.13.2 coqide.8.13.2 ``` but you might need to install some extra packages and libraries for your system diff --git a/src/Makefile b/src/Makefile index 5653389..3efcfc3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -7,7 +7,7 @@ ## # GNU Lesser General Public License Version 2.1 ## ## # (see LICENSE file for the text of the license) ## ########################################################################## -## GNUMakefile for Coq 8.12.2 +## GNUMakefile for Coq 8.13.2 # For debugging purposes (must stay here, don't move below) INITIAL_VARS := $(.VARIABLES) @@ -104,7 +104,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=num,str,unix,dynlink,threads +CAMLDONTLINK=str,unix,dynlink,threads,zarith # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line TGTS ?= +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -203,7 +218,7 @@ COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.12.2 +COQMAKEFILE_VERSION:=8.13.2 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") @@ -227,17 +242,6 @@ else TIMING_ARG= endif -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) - -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) - # Files ####################################################################### # # We here define a bunch of variables about the files being part of the @@ -463,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok) .PHONY: vok validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ .PHONY: validate only: $(TGTS) @@ -577,7 +581,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ done .PHONY: uninstall @@ -797,7 +801,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack # projects. Note that extra options might be on the command line. VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) -$(VDFILE): $(VFILES) +$(VDFILE): _CoqProject $(VFILES) $(SHOW)'COQDEP VFILES' $(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index d03d23d..c0d109f 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -18,7 +18,7 @@ Local Open Scope list_scope. Local Open Scope array_scope. Local Open Scope int63_scope. -Hint Unfold is_true : smtcoq_core. +#[export] Hint Unfold is_true : smtcoq_core. (* Remark: I use Notation instead of Definition du eliminate conversion check during the type checking *) diff --git a/src/array/FArray.v b/src/array/FArray.v index dfff5e8..f46dcb7 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -130,7 +130,7 @@ Module Raw. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. unfold ltk; eauto. Qed. + Proof. unfold ltk; eauto with typeclass_ordtype. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed. diff --git a/src/bva/BVList.v b/src/bva/BVList.v index d8632bb..b5a44e3 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) := (ult_list_big_endian (List.rev x) (List.rev y)). -Fixpoint slt_list_big_endian (x y: list bool) := +Definition slt_list_big_endian (x y: list bool) := match x, y with | nil, _ => false | _ , nil => false @@ -696,7 +696,7 @@ Definition bvmult_bool (a b: list bool) (n: nat) : list bool := Definition mult_list a b := bvmult_bool a b (length a). Definition bv_mult (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then mult_list a b else zeros (@size a). @@ -710,11 +710,11 @@ Proof. intro n. Qed. Definition _of_bits (a:list bool) (s: N) := -if (N.of_nat (length a) =? s) then a else zeros s. +if (N.of_nat (length a) =? s)%N then a else zeros s. Lemma _of_bits_size l s: (size (_of_bits l s)) = s. Proof. unfold of_bits, size. unfold _of_bits. - case_eq ( N.of_nat (length l) =? s). + case_eq ( N.of_nat (length l) =? s)%N. intros. now rewrite N.eqb_eq in H. intros. unfold zeros. rewrite length_mk_list_false. now rewrite N2Nat.id. @@ -800,7 +800,7 @@ Qed. Lemma bv_eq_reflect a b : bv_eq a b = true <-> a = b. Proof. - unfold bv_eq. case_eq (size a =? size b); intro Heq; simpl. + unfold bv_eq. case_eq (size a =? size b)%N; intro Heq; simpl. - apply List_eq. - split; try discriminate. intro H. rewrite H, N.eqb_refl in Heq. discriminate. @@ -1880,11 +1880,11 @@ Qed. Lemma bv_ult_B2P: forall x y, bv_ult x y = true <-> bv_ultP x y. Proof. intros. split; intros; unfold bv_ult, bv_ultP in *. - case_eq (size x =? size y); intros; + case_eq (size x =? size y)%N; intros; rewrite H0 in H; unfold ult_listP. now rewrite H. now contradict H. unfold ult_listP in *. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. rewrite H0 in H. case_eq (ult_list x y); intros. easy. rewrite H1 in H. now contradict H. @@ -1893,11 +1893,11 @@ Qed. Lemma bv_slt_B2P: forall x y, bv_slt x y = true <-> bv_sltP x y. Proof. intros. split; intros; unfold bv_slt, bv_sltP in *. - case_eq (size x =? size y); intros; + case_eq (size x =? size y)%N; intros; rewrite H0 in H; unfold slt_listP. now rewrite H. now contradict H. unfold slt_listP in *. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. rewrite H0 in H. case_eq (slt_list x y); intros. easy. rewrite H1 in H. now contradict H. @@ -1962,28 +1962,28 @@ Qed. Lemma bv_ult_not_eqP : forall x y, bv_ultP x y -> x <> y. Proof. intros x y. unfold bv_ultP. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply ult_list_not_eqP in H0. - now contradict H0. Qed. Lemma bv_slt_not_eqP : forall x y, bv_sltP x y -> x <> y. Proof. intros x y. unfold bv_sltP. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply slt_list_not_eqP in H0. - now contradict H0. Qed. Lemma bv_ult_not_eq : forall x y, bv_ult x y = true -> x <> y. Proof. intros x y. unfold bv_ult. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply ult_list_not_eq in H0. - now contradict H0. Qed. Lemma bv_slt_not_eq : forall x y, bv_slt x y = true -> x <> y. Proof. intros x y. unfold bv_slt. - case_eq (size x =? size y); intros. + case_eq (size x =? size y)%N; intros. - now apply slt_list_not_eq in H0. - now contradict H0. Qed. @@ -2103,7 +2103,7 @@ Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. - case b in *. simpl. rewrite IHa. simpl. omega. + case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa. Qed. @@ -2117,8 +2117,8 @@ Lemma prop_mult_bool_step: forall k' a b res k, length (mult_bool_step a b res k k') = (length res)%nat. Proof. intro k'. induction k'. - - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega. - - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega. + - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. lia. + - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; lia. Qed. Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a. @@ -2258,7 +2258,7 @@ Qed. size a = n1 -> size (@bv_extr i n0 n1 a) = n0%N. Proof. intros. unfold bv_extr, size in *. - case_eq (n1 <? n0 + i). + case_eq (n1 <? n0 + i)%N. intros. now rewrite length_mk_list_false, N2Nat.id. intros. specialize (@length_extract a i (n0 + i)). intros. @@ -2455,7 +2455,7 @@ Qed. (** bit-vector extension *) Definition bv_shl (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then shl_be a b else zeros (@size a). @@ -2510,7 +2510,7 @@ Qed. (** bit-vector extension *) Definition bv_shr (a b : bitvector) : bitvector := - if ((@size a) =? (@size b)) + if ((@size a) =? (@size b))%N then shr_be a b else zeros (@size a). diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index e1fd8e9..9a33271 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -98,7 +98,7 @@ Class OrdType T := { lt_not_eq : forall x y : T, lt x y -> x <> y }. -Hint Resolve lt_not_eq lt_trans. +#[export] Hint Resolve lt_not_eq lt_trans : typeclass_ordtype. Global Instance StrictOrder_OrdType T `(OrdType T) : diff --git a/src/lfsc/lfscLexer.mll b/src/lfsc/lfscLexer.mll index 3428b72..0aaf839 100644 --- a/src/lfsc/lfscLexer.mll +++ b/src/lfsc/lfscLexer.mll @@ -17,51 +17,6 @@ open Lexing open LfscParser - let char_for_backslash = function - | 'n' -> '\010' - | 'r' -> '\013' - | 'b' -> '\008' - | 't' -> '\009' - | c -> c - - let lf = '\010' - - let dec_code c1 c2 c3 = - 100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48) - - let hex_code c1 c2 = - let d1 = Char.code c1 in - let val1 = - if d1 >= 97 then d1 - 87 - else if d1 >= 65 then d1 - 55 - else d1 - 48 in - let d2 = Char.code c2 in - let val2 = - if d2 >= 97 then d2 - 87 - else if d2 >= 65 then d2 - 55 - else d2 - 48 in - val1 * 16 + val2 - - let found_newline ({ lex_curr_p; _ } as lexbuf) diff = - lexbuf.lex_curr_p <- - { - lex_curr_p with - pos_lnum = lex_curr_p.pos_lnum + 1; - pos_bol = lex_curr_p.pos_cnum - diff; - } - - (* same length computation as in [Lexing.lexeme] *) - let lexeme_len { lex_start_pos; lex_curr_pos; _ } = lex_curr_pos - lex_start_pos - - let main_failure lexbuf msg = - let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_start_p lexbuf in - let msg = - sprintf - "Sexplib.Lexer.main: %s at line %d char %d" - msg pos_lnum (pos_cnum - pos_bol) - in - failwith msg - module type T = sig module Quoted_string_buffer : sig type t @@ -138,7 +93,7 @@ let ident = ('_')* ['a'-'z' 'A'-'Z' '\'' ]['a'-'z' 'A'-'Z' '0'-'9' '\\' '_']* rule main buf = parse - | lf | dos_newline { found_newline lexbuf 0; + | lf | dos_newline { SmtMisc.found_newline lexbuf 0; main buf lexbuf } | blank+ { main buf lexbuf } | (';' (_ # lf_cr)*) as text { Token.comment text ~main buf lexbuf } @@ -172,13 +127,13 @@ rule main buf = parse Quoted_string_buffer.clear buf; tok } - | "|#" { main_failure lexbuf "illegal end of comment" } + | "|#" { SmtMisc.main_failure lexbuf "illegal end of comment" } | "#" "#"+ "|" unquoted* (* unquoted_start can match ##, so ##| (which should be refused) would not not be parsed by this case if the regexp on the left was not there *) | "|" "|"+ "#" unquoted* | unquoted_start unquoted* ("#|" | "|#") unquoted* - { main_failure lexbuf "comment tokens in unquoted atom" } + { SmtMisc.main_failure lexbuf "comment tokens in unquoted atom" } | "#" | "|" | unquoted_start unquoted* as str { Token.simple_string str } | eof { Token.eof } @@ -186,27 +141,27 @@ and scan_string buf start = parse | '"' { Quoted_string_buffer.add_lexeme buf lexbuf; () } | '\\' lf [' ' '\t']* { - let len = lexeme_len lexbuf - 2 in - found_newline lexbuf len; + let len = SmtMisc.lexeme_len lexbuf - 2 in + SmtMisc.found_newline lexbuf len; Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf } | '\\' dos_newline [' ' '\t']* { - let len = lexeme_len lexbuf - 3 in - found_newline lexbuf len; + let len = SmtMisc.lexeme_len lexbuf - 3 in + SmtMisc.found_newline lexbuf len; Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf } | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c) { - Quoted_string_buffer.add_char buf (char_for_backslash c); + Quoted_string_buffer.add_char buf (SmtMisc.char_for_backslash c); Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf } | '\\' (digit as c1) (digit as c2) (digit as c3) { - let v = dec_code c1 c2 c3 in + let v = SmtMisc.dec_code c1 c2 c3 in if v > 255 then ( let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_end_p lexbuf in let msg = @@ -222,7 +177,7 @@ and scan_string buf start = parse } | '\\' 'x' (hexdigit as c1) (hexdigit as c2) { - let v = hex_code c1 c2 in + let v = SmtMisc.hex_code c1 c2 in Quoted_string_buffer.add_char buf (Char.chr v); Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf @@ -236,8 +191,8 @@ and scan_string buf start = parse } | lf { - found_newline lexbuf 0; - Quoted_string_buffer.add_char buf lf; + SmtMisc.found_newline lexbuf 0; + Quoted_string_buffer.add_char buf SmtMisc.lf; Quoted_string_buffer.add_lexeme buf lexbuf; scan_string buf start lexbuf } @@ -262,7 +217,7 @@ and scan_string buf start = parse and scan_block_comment buf locs = parse | ('#'* | '|'*) lf { Quoted_string_buffer.add_lexeme buf lexbuf; - found_newline lexbuf 0; scan_block_comment buf locs lexbuf } + SmtMisc.found_newline lexbuf 0; scan_block_comment buf locs lexbuf } | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+ { Quoted_string_buffer.add_lexeme buf lexbuf; scan_block_comment buf locs lexbuf } diff --git a/src/lia/Lia.v b/src/lia/Lia.v index 4f5d9ef..71c4020 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -157,62 +157,62 @@ Section certif. Section Build_form. Definition build_not2 i f := - foldi (fun _ (f' : BFormula (Formula Z)) => N (N f')) 0 i f. + foldi (fun _ (f' : BFormula (Formula Z) isProp) => NOT (NOT f')) 0 i f. - Variable build_var : vmap -> var -> option (vmap*BFormula (Formula Z)). + Variable build_var : vmap -> var -> option (vmap*(BFormula (Formula Z) isProp)). - Definition build_hform vm f : option (vmap*BFormula (Formula Z)) := + Definition build_hform vm f : option (vmap*(BFormula (Formula Z) isProp)) := match f with | Form.Fatom h => match build_formula vm h with - | Some (vm,f) => Some (vm, A f tt) + | Some (vm,f) => Some (vm, A isProp f tt) | None => None end - | Form.Ftrue => Some (vm, TT) - | Form.Ffalse => Some (vm, FF) + | Form.Ftrue => Some (vm, TT isProp) + | Form.Ffalse => Some (vm, FF isProp) | Form.Fnot2 i l => match build_var vm (Lit.blit l) with | Some (vm, f) => let f' := build_not2 i f in - let f'' := if Lit.is_pos l then f' else N f' in + let f'' := if Lit.is_pos l then f' else NOT f' in Some (vm,f'') | None => None end | Form.Fand args => afold_left _ - (fun vm => Some (vm, TT)) + (fun vm => Some (vm, TT isProp)) (fun a b vm => match a vm with | Some (vm1, f1) => match b vm1 with - | Some (vm2, f2) => Some (vm2, Cj f1 f2) + | Some (vm2, f2) => Some (vm2, AND f1 f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with - | Some (vm', f) => Some (vm', if Lit.is_pos l then f else N f) + | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) vm | Form.For args => afold_left _ - (fun vm => Some (vm, FF)) + (fun vm => Some (vm, FF isProp)) (fun a b vm => match a vm with | Some (vm1, f1) => match b vm1 with - | Some (vm2, f2) => Some (vm2, D f1 f2) + | Some (vm2, f2) => Some (vm2, OR f1 f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with - | Some (vm', f) => Some (vm', if Lit.is_pos l then f else N f) + | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) @@ -222,28 +222,28 @@ Section certif. | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - Some (vm2, Cj (D f1' f2') (D (N f1') (N f2'))) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + Some (vm2, AND (OR f1' f2') (OR (NOT f1') (NOT f2'))) | None => None end | None => None end | Form.Fimp args => afold_right _ - (fun vm => Some (vm, TT)) + (fun vm => Some (vm, TT isProp)) (fun a b vm => match b vm with | Some (vm2, f2) => match a vm2 with - | Some (vm1, f1) => Some (vm1, I f1 None f2) + | Some (vm1, f1) => Some (vm1, IMPL f1 None f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with - | Some (vm', f) => Some (vm', if Lit.is_pos l then f else N f) + | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) @@ -253,9 +253,9 @@ Section certif. | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - Some (vm2, Cj (D f1' (N f2')) (D (N f1') f2')) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + Some (vm2, AND (OR f1' (NOT f2')) (OR (NOT f1') f2')) | None => None end | None => None @@ -267,10 +267,10 @@ Section certif. | Some (vm2, f2) => match build_var vm2 (Lit.blit c) with | Some (vm3, f3) => - let f1' := if Lit.is_pos a then f1 else N f1 in - let f2' := if Lit.is_pos b then f2 else N f2 in - let f3' := if Lit.is_pos c then f3 else N f3 in - Some (vm3, D (Cj f1' f2') (Cj (N f1') f3')) + let f1' := if Lit.is_pos a then f1 else NOT f1 in + let f2' := if Lit.is_pos b then f2 else NOT f2 in + let f3' := if Lit.is_pos c then f3 else NOT f3 in + Some (vm3, OR (AND f1' f2') (AND (NOT f1') f3')) | None => None end | None => None @@ -295,14 +295,14 @@ Section certif. let l := Lit.neg l in match build_form vm (get_form (Lit.blit l)) with | Some (vm,f) => - let f := if Lit.is_pos l then f else N f in + let f := if Lit.is_pos l then f else NOT f in Some (vm,f) | None => None end. Fixpoint build_clause_aux vm (cl:list _lit) {struct cl} : - option (vmap * BFormula (Formula Z)) := + option (vmap * BFormula (Formula Z) isProp) := match cl with | nil => None | l::nil => build_nlit vm l @@ -310,7 +310,7 @@ Section certif. match build_nlit vm l with | Some (vm,bf1) => match build_clause_aux vm cl with - | Some (vm,bf2) => Some (vm, Cj bf1 bf2) + | Some (vm,bf2) => Some (vm, AND bf1 bf2) | _ => None end | None => None @@ -319,7 +319,7 @@ Section certif. Definition build_clause vm cl := match build_clause_aux vm cl with - | Some (vm, bf) => Some (vm, I bf None FF) + | Some (vm, bf) => Some (vm, IMPL bf None (FF isProp)) | None => None end. @@ -502,14 +502,16 @@ Section certif. Definition bounded_formula (p:positive) (f:Formula Z) := bounded_pexpr p (f.(Flhs)) && bounded_pexpr p (f.(Frhs)). - Fixpoint bounded_bformula (p:positive) (bf:BFormula (Formula Z)) := + Fixpoint bounded_bformula (p:positive) {k:kind} (bf:BFormula (Formula Z) k) : bool := match bf with - | @TT _ | @FF _ | @X _ _ _ _ _ => true - | A f _ => bounded_formula p f - | Cj bf1 bf2 - | D bf1 bf2 - | I bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 - | N bf => bounded_bformula p bf + | @TT _ _ _ _ _ | @FF _ _ _ _ _ | @X _ _ _ _ _ _ => true + | A _ f _ => bounded_formula p f + | AND bf1 bf2 + | OR bf1 bf2 + | IMPL bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 + | NOT bf => bounded_bformula p bf + | IFF bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 + | EQ bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2 end. Definition interp_vmap (vm:vmap) p := @@ -981,7 +983,7 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ - (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') f). + (interp_bool t_i (interp_atom a) <->Zeval_formula (interp_vmap vm') isProp f). Proof. intros a vm vm' f t. destruct a;simpl;try discriminate. @@ -1034,7 +1036,7 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_formula (fst vm') f /\ - (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') f). + (interp_form_hatom h' <-> Zeval_formula (interp_vmap vm') isProp f). Proof. unfold build_formula;intros h. unfold Atom.interp_form_hatom, Atom.interp_hatom. @@ -1049,9 +1051,9 @@ Transparent build_z_atom. Qed. - Local Notation eval_f := (eval_f (fun x => x)). + Local Notation eval_f := (eval_f (fun k x => x)). - Lemma build_not2_pos_correct : forall vm f l i, + Lemma build_not2_pos_correct : forall vm (f:GFormula isProp) l i, bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)). Proof. simpl; intros vm f l i H1 H2 H3; unfold build_not2. @@ -1067,8 +1069,8 @@ Transparent build_z_atom. Qed. - Lemma build_not2_neg_correct : forall vm f l i, - bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (N (build_not2 i f)) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (N (build_not2 i f))). + Lemma build_not2_neg_correct : forall vm (f:GFormula isProp) l i, + bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (NOT (build_not2 i f)) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (NOT (build_not2 i f))). Proof. simpl; intros vm f l i H1 H2 H3; unfold build_not2. case (Z.le_gt_cases 1 [|i|]); [ intro Hle | intro Hlt ]. @@ -1080,48 +1082,79 @@ Transparent build_z_atom. unfold is_true; rewrite not_true_iff_false, not_false_iff_true; tauto. rewrite 2!foldi_ge by (rewrite leb_spec, to_Z_0; lia). unfold Lit.interp; rewrite H3, <- H2; unfold is_true; rewrite negb_true_iff, not_true_iff_false; tauto. -Qed. + Qed. Lemma bounded_bformula_le : forall p p', (nat_of_P p <= nat_of_P p')%nat -> - forall bf, + forall (bf:BFormula (Formula Z) isProp), bounded_bformula p bf -> bounded_bformula p' bf. Proof. unfold is_true;induction bf;simpl;trivial. - destruct a;unfold bounded_formula;simpl. - rewrite andb_true_iff;intros (H1, H2). - rewrite (bounded_pexpr_le _ _ H _ H1), (bounded_pexpr_le _ _ H _ H2);trivial. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. + - destruct a;unfold bounded_formula;simpl. + rewrite andb_true_iff;intros (H1, H2). + rewrite (bounded_pexpr_le _ _ H _ H1), (bounded_pexpr_le _ _ H _ H2);trivial. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. + - rewrite !andb_true_iff;intros (H1, H2);auto. Qed. - Lemma interp_bformula_le : - forall vm vm', - (forall (p : positive), - (nat_of_P p < nat_of_P (fst vm))%nat -> - nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = - nth_error (snd vm') (nat_of_P (fst vm' - p) - 1)) -> - forall bf, - bounded_bformula (fst vm) bf -> - (eval_f (Zeval_formula (interp_vmap vm)) bf <-> - eval_f (Zeval_formula (interp_vmap vm')) bf). - Proof. - intros vm vm' Hnth. - unfold is_true;induction bf;simpl;try tauto. - destruct t;unfold bounded_formula;simpl. - rewrite andb_true_iff;intros (H1, H2). - rewrite !(interp_pexpr_le _ _ Hnth);tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto. - Qed. + Section Interp_bformula. + + Variables vm vm' : positive * list atom. + Variable Hnth : forall p : positive, + (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> + nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = + nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1). + + Definition P k : GFormula k -> Prop := + match k as k return GFormula k -> Prop with + | isProp => fun (bf:BFormula (Formula Z) isProp) => + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf <-> + eval_f (Zeval_formula (interp_vmap vm')) bf) + | isBool => fun (bf:BFormula (Formula Z) isBool) => + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf = + eval_f (Zeval_formula (interp_vmap vm')) bf) + end. + + Lemma interp_bformula_le_gen : forall k f, P k f. + Proof. + intro k. induction f as [k|k|k t|k t a|k f1 IHf1 f2 IHf2|k f1 IHf1 f2 IHf2|k f1 IHf1|k f1 IHf1 o f2 IHf2|k f1 IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; unfold P in *; + try (destruct k; simpl; tauto); + try (destruct k; simpl; unfold is_true;rewrite andb_true_iff;intros (H1,H2);rewrite IHf1, IHf2;tauto). + - destruct k; simpl; + destruct t;unfold bounded_formula;simpl; + unfold is_true;rewrite andb_true_iff;intros (H1, H2); + rewrite !(interp_pexpr_le _ _ Hnth);tauto. + - destruct k; simpl; intro H; now rewrite IHf1. + - destruct k; simpl. + + unfold is_true;rewrite andb_true_iff;intros (H1, H2). + split. + * intros H3 H4. rewrite <- IHf2; auto. apply H3. now rewrite IHf1. + * intros H3 H4. rewrite IHf2; auto. apply H3. now rewrite <- IHf1. + + unfold is_true;rewrite andb_true_iff;intros (H1, H2). + now rewrite IHf1, IHf2. + - simpl. unfold is_true;rewrite andb_true_iff;intros (H1, H2). + now rewrite IHf1, IHf2. + Qed. + + Lemma interp_bformula_le : + forall (bf:BFormula (Formula Z) isProp), + bounded_bformula (fst vm) bf -> + (eval_f (Zeval_formula (interp_vmap vm)) bf <-> + eval_f (Zeval_formula (interp_vmap vm')) bf). + Proof. exact (interp_bformula_le_gen isProp). Qed. + + End Interp_bformula. Lemma build_hform_correct : - forall (build_var : vmap -> var -> option (vmap*BFormula (Formula Z))), + forall (build_var : vmap -> var -> option (vmap*BFormula (Formula Z) isProp)), (forall v vm vm' bf, build_var vm v = Some (vm', bf) -> wf_vmap vm -> @@ -1181,6 +1214,7 @@ Qed. simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core. simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; rewrite get_amap by exact H1; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate. (* Fimp *) + { simpl; unfold afold_right; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl. intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core). revert vm' bf; rewrite !get_amap by (apply minus_1_lt; rewrite eqb_false_spec, not_0_ltb; exact Hl); set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2. @@ -1195,7 +1229,21 @@ Qed. intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith. split. simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[length l - 1 - i])); rewrite H13; auto with smtcoq_core. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[length l - 1 - i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[length l - 1 - i]))); auto with smtcoq_core; try discriminate; simpl; intro H; apply H; discriminate. + simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9. + case_eq (Lit.is_pos (l .[length l - 1 - i])); intro Heq2; simpl. + - unfold Lit.interp. rewrite Heq2. split. + + revert H14. case (Var.interp rho (Lit.blit (l .[ length l - 1 - i]))); simpl. + * intros H101 H102 H103. now rewrite <- H9. + * intros H101 H102 H103. rewrite <- H101 in H103. discriminate. + + revert H14. case (Var.interp rho (Lit.blit (l .[ length l - 1 - i]))); simpl; auto. + intros H101 H102. rewrite H9. apply H102. now rewrite <- H101. + - unfold Lit.interp. rewrite Heq2. split. + + revert H14. case (Var.interp rho (Lit.blit (l .[ length l - 1 - i]))); simpl. + * intros H101 H102 H103. elim H103. now rewrite <- H101. + * intros H101 H102 H103. now rewrite <- H9. + + revert H14. case (Var.interp rho (Lit.blit (l .[ length l - 1 - i]))); simpl; auto. + intros H101 H102. rewrite H9. apply H102. now rewrite <- H101. + } (* Fxor *) simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split. intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith. @@ -1323,7 +1371,7 @@ Qed. ( match build_nlit vm a with | Some (vm0, bf1) => match build_clause_aux vm0 (i::l) with - | Some (vm1, bf2) => Some (vm1, Cj bf1 bf2) + | Some (vm1, bf2) => Some (vm1, AND bf1 bf2) | None => None end | None => None @@ -1465,8 +1513,8 @@ Qed. unfold Atom.interp, Atom.interp_hatom. rewrite HHa, HHb; simpl. intros. - case_eq (va <=? vb); intros; subst. - case_eq (vb <=? va); intros; subst. + case_eq (va <=? vb)%Z; intros; subst. + case_eq (vb <=? va)%Z; intros; subst. apply Zle_bool_imp_le in H2. apply Zle_bool_imp_le in H3. apply Z.eqb_neq in H. diff --git a/src/lia/lia.ml b/src/lia/lia.ml index e00092e..5dc5620 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -123,13 +123,13 @@ let binop_array g tbl op def t = let rec smt_Form_to_coq_micromega_formula tbl l = let v = match Form.pform l with - | Fatom ha -> A (smt_Atom_to_micromega_formula tbl ha, Tt) - | Fapp (Ftrue, _) -> TT - | Fapp (Ffalse, _) -> FF - | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Cj (x,y)) TT l - | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> D (x,y)) FF l + | Fatom ha -> A (IsProp, smt_Atom_to_micromega_formula tbl ha, Tt) + | Fapp (Ftrue, _) -> TT IsProp + | Fapp (Ffalse, _) -> FF IsProp + | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> AND (IsProp, x,y)) (TT IsProp) l + | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> OR (IsProp, x,y)) (FF IsProp) l | Fapp (Fxor, l) -> failwith "todo:Fxor" - | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> I (x,None,y)) TT l + | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> IMPL (IsProp, x,None,y)) (TT IsProp) l | Fapp (Fiff, l) -> failwith "todo:Fiff" | Fapp (Fite, l) -> failwith "todo:Fite" | Fapp (Fnot2 _, l) -> @@ -141,7 +141,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = | Fapp (Fforall _, _) -> assert false in if Form.is_pos l then v - else N(v) + else NOT(IsProp, v) let binop_list tbl op def l = match l with @@ -149,10 +149,10 @@ let binop_list tbl op def l = | f::l -> List.fold_left (fun x y -> op x (smt_Form_to_coq_micromega_formula tbl y)) (smt_Form_to_coq_micromega_formula tbl f) l let smt_clause_to_coq_micromega_formula tbl cl = - binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) + binop_list tbl (fun x y -> AND (IsProp, x,y)) (TT IsProp) (List.map Form.neg cl) let tauto_lia ff = - let cnf_ff,_ = CoqInterface.Micromega_plugin_Micromega.cnfZ ff in + let cnf_ff,_ = CoqInterface.Micromega_plugin_Micromega.cnfZ IsProp ff in let rec xwitness_list l = match l with | [] -> Some [] @@ -168,5 +168,5 @@ let tauto_lia ff = (* call to micromega solver *) let build_lia_certif cl = let tbl = create_tbl 13 in - let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in + let f = IMPL(IsProp, smt_clause_to_coq_micromega_formula tbl cl, None, (FF IsProp)) in tauto_lia f diff --git a/src/smtlib2/sExprLexer.mll b/src/smtlib2/sExprLexer.mll index 1c7983f..ec85b5f 100644 --- a/src/smtlib2/sExprLexer.mll +++ b/src/smtlib2/sExprLexer.mll @@ -24,50 +24,6 @@ open Lexing open SExprParser - let char_for_backslash = function - | 'n' -> '\010' - | 'r' -> '\013' - | 'b' -> '\008' - | 't' -> '\009' - | c -> c - - let lf = '\010' - - let dec_code c1 c2 c3 = - 100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48) - - let hex_code c1 c2 = - let d1 = Char.code c1 in - let val1 = - if d1 >= 97 then d1 - 87 - else if d1 >= 65 then d1 - 55 - else d1 - 48 in - let d2 = Char.code c2 in - let val2 = - if d2 >= 97 then d2 - 87 - else if d2 >= 65 then d2 - 55 - else d2 - 48 in - val1 * 16 + val2 - - let found_newline ({ lex_curr_p; _ } as lexbuf) diff = - lexbuf.lex_curr_p <- - { - lex_curr_p with - pos_lnum = lex_curr_p.pos_lnum + 1; - pos_bol = lex_curr_p.pos_cnum - diff; - } - - (* same length computation as in [Lexing.lexeme] *) - let lexeme_len { lex_start_pos; lex_curr_pos; _ } = lex_curr_pos - lex_start_pos - - let main_failure lexbuf msg = - let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_start_p lexbuf in - let msg = - sprintf - "Sexplib.Lexer.main: %s at line %d char %d" - msg pos_lnum (pos_cnum - pos_bol) - in - failwith msg } let lf = '\010' @@ -82,7 +38,7 @@ let unquoted_start = unquoted # ['#' '|'] | '#' unquoted # ['|'] | '|' unquoted # ['#'] rule main buf = parse - | lf | dos_newline { found_newline lexbuf 0; main buf lexbuf } + | lf | dos_newline { SmtMisc.found_newline lexbuf 0; main buf lexbuf } | blank+ | ';' (_ # lf_cr)* { main buf lexbuf } | '(' { LPAREN } | ')' { RPAREN } @@ -99,7 +55,7 @@ rule main buf = parse scan_block_comment buf [lexeme_start_p lexbuf] lexbuf; main buf lexbuf } - | "|#" { main_failure lexbuf "illegal end of comment" } + | "|#" { SmtMisc.main_failure lexbuf "illegal end of comment" } | '|' { scan_quoted buf (lexeme_start_p lexbuf) lexbuf; @@ -108,7 +64,7 @@ rule main buf = parse STRING ("|"^ str ^"|") } | unquoted_start unquoted* ("#|" | "|#") unquoted* - { main_failure lexbuf "comment tokens in unquoted atom" } + { SmtMisc.main_failure lexbuf "comment tokens in unquoted atom" } | "#" | unquoted_start unquoted* as str { STRING str } | eof { EOF } @@ -116,22 +72,22 @@ and scan_string buf start = parse | '"' { () } | '\\' lf [' ' '\t']* { - found_newline lexbuf (lexeme_len lexbuf - 2); + SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 2); scan_string buf start lexbuf } | '\\' dos_newline [' ' '\t']* { - found_newline lexbuf (lexeme_len lexbuf - 3); + SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 3); scan_string buf start lexbuf } | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c) { - Buffer.add_char buf (char_for_backslash c); + Buffer.add_char buf (SmtMisc.char_for_backslash c); scan_string buf start lexbuf } | '\\' (digit as c1) (digit as c2) (digit as c3) { - let v = dec_code c1 c2 c3 in + let v = SmtMisc.dec_code c1 c2 c3 in if v > 255 then ( let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in let msg = @@ -146,7 +102,7 @@ and scan_string buf start = parse } | '\\' 'x' (hexdigit as c1) (hexdigit as c2) { - let v = hex_code c1 c2 in + let v = SmtMisc.hex_code c1 c2 in Buffer.add_char buf (Char.chr v); scan_string buf start lexbuf } @@ -158,8 +114,8 @@ and scan_string buf start = parse } | lf { - found_newline lexbuf 0; - Buffer.add_char buf lf; + SmtMisc.found_newline lexbuf 0; + Buffer.add_char buf SmtMisc.lf; scan_string buf start lexbuf } | ([^ '\\' '"'] # lf)+ @@ -181,22 +137,22 @@ and scan_quoted buf start = parse | '|' { () } | '\\' lf [' ' '\t']* { - found_newline lexbuf (lexeme_len lexbuf - 2); + SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 2); scan_quoted buf start lexbuf } | '\\' dos_newline [' ' '\t']* { - found_newline lexbuf (lexeme_len lexbuf - 3); + SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 3); scan_quoted buf start lexbuf } | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' ' '|'] as c) { - Buffer.add_char buf (char_for_backslash c); + Buffer.add_char buf (SmtMisc.char_for_backslash c); scan_quoted buf start lexbuf } | '\\' (digit as c1) (digit as c2) (digit as c3) { - let v = dec_code c1 c2 c3 in + let v = SmtMisc.dec_code c1 c2 c3 in if v > 255 then ( let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in let msg = @@ -211,7 +167,7 @@ and scan_quoted buf start = parse } | '\\' 'x' (hexdigit as c1) (hexdigit as c2) { - let v = hex_code c1 c2 in + let v = SmtMisc.hex_code c1 c2 in Buffer.add_char buf (Char.chr v); scan_quoted buf start lexbuf } @@ -223,8 +179,8 @@ and scan_quoted buf start = parse } | lf { - found_newline lexbuf 0; - Buffer.add_char buf lf; + SmtMisc.found_newline lexbuf 0; + Buffer.add_char buf SmtMisc.lf; scan_quoted buf start lexbuf } | ([^ '\\' '|'] # lf)+ @@ -244,7 +200,7 @@ and scan_quoted buf start = parse and scan_block_comment buf locs = parse | ('#'* | '|'*) lf - { found_newline lexbuf 0; scan_block_comment buf locs lexbuf } + { SmtMisc.found_newline lexbuf 0; scan_block_comment buf locs lexbuf } | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+ { scan_block_comment buf locs lexbuf } | ('#'* | '|'*) '"' { diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 11eee8a..f08ea41 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -56,3 +56,50 @@ type logic = SL.t let rec filter_map f = function | [] -> [] | x::xs -> match f x with Some x -> x::(filter_map f xs) | None -> filter_map f xs + + +(** Lexing *) +let char_for_backslash = function + | 'n' -> '\010' + | 'r' -> '\013' + | 'b' -> '\008' + | 't' -> '\009' + | c -> c + +let lf = '\010' + +let dec_code c1 c2 c3 = + 100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48) + +let hex_code c1 c2 = + let d1 = Char.code c1 in + let val1 = + if d1 >= 97 then d1 - 87 + else if d1 >= 65 then d1 - 55 + else d1 - 48 in + let d2 = Char.code c2 in + let val2 = + if d2 >= 97 then d2 - 87 + else if d2 >= 65 then d2 - 55 + else d2 - 48 in + val1 * 16 + val2 + +let found_newline (lexbuf:Lexing.lexbuf) diff = + lexbuf.Lexing.lex_curr_p <- + { + lexbuf.Lexing.lex_curr_p with + Lexing.pos_lnum = lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum + 1; + Lexing.pos_bol = lexbuf.Lexing.lex_curr_p.Lexing.pos_cnum - diff; + } + +(* same length computation as in [Lexing.lexeme] *) +let lexeme_len { Lexing.lex_start_pos; Lexing.lex_curr_pos; _ } = lex_curr_pos - lex_start_pos + +let main_failure lexbuf msg = + let { Lexing.pos_lnum; Lexing.pos_bol; Lexing.pos_cnum; Lexing.pos_fname = _ } = Lexing.lexeme_start_p lexbuf in + let msg = + Printf.sprintf + "Sexplib.Lexer.main: %s at line %d char %d" + msg pos_lnum (pos_cnum - pos_bol) + in + failwith msg diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index 632ac79..6b1ca90 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -22,3 +22,12 @@ type logic = SL.t (** Utils *) val filter_map : ('a -> 'b option) -> 'a list -> 'b list + +(** Lexing *) +val char_for_backslash : char -> char +val lf : char +val dec_code : char -> char -> char -> int +val hex_code : char -> char -> int +val found_newline : Lexing.lexbuf -> int -> unit +val lexeme_len : Lexing.lexbuf -> int +val main_failure : Lexing.lexbuf -> string -> 'a diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index cb9d7ba..4cef5f1 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -503,8 +503,8 @@ Qed. -Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) --> - ((x + y <=? 10) || (x + z <=? 12)) = true. +Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9)))%Z --> + ((x + y <=? 10) || (x + z <=? 12))%Z = true. Proof using. smt. Qed. @@ -515,29 +515,29 @@ Proof using. Qed. -Goal forall x y, (x >? y) --> (y + 1 <=? x) = true. +Goal forall x y, (x >? y)%Z --> (y + 1 <=? x)%Z = true. Proof using. smt. Qed. -Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true. +Goal forall x y, Bool.eqb (x <? y)%Z (x <=? y - 1)%Z = true. Proof using. smt. Qed. Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) - || (x <=? - (3))) && (x >=? 0) = false. + || (x <=? - (3)))%Z && (x >=? 0) = false. Proof using. smt. Qed. -Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true. +Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3)))%Z --> (x >=? 10) = true. Proof using. smt. Qed. -Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true. +Goal forall x, (Z.eqb (x - 3) 7)%Z --> (10 <=? x)%Z = true. Proof using. smt. Qed. |