diff options
-rw-r--r-- | src/Makefile | 38 | ||||
-rw-r--r-- | src/QInst.v | 2 | ||||
-rw-r--r-- | src/SMT_terms.v | 2 | ||||
-rw-r--r-- | src/array/FArray.v | 2 | ||||
-rw-r--r-- | src/bva/BVList.v | 8 | ||||
-rw-r--r-- | src/classes/SMT_classes.v | 4 | ||||
-rw-r--r-- | src/classes/SMT_classes_instances.v | 2 | ||||
-rw-r--r-- | src/lfsc/lfscLexer.mll | 71 | ||||
-rw-r--r-- | src/lia/Lia.v | 206 | ||||
-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 |
13 files changed, 255 insertions, 236 deletions
diff --git a/src/Makefile b/src/Makefile index dfcbd38..95955bb 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.1 +## GNUMakefile for Coq 8.13.1 # 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.1 +COQMAKEFILE_VERSION:=8.13.1 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/QInst.v b/src/QInst.v index b2dd836..41da06b 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -27,7 +27,7 @@ Proof. installed when we compile SMTCoq. *) Qed. -Hint Resolve impl_split : smtcoq_core. +#[global] Hint Resolve impl_split : smtcoq_core. (** verit silently transforms an <implb (a || b) c> into a <or (not a) c> or into a <or (not b) c> when instantiating such a quantified theorem *) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index f88c0c4..b3df896 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 69e56f9..e45abb4 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 91a110d..9e22f98 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 @@ -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. diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index 53d5dcc..be16138 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) : @@ -184,7 +184,7 @@ Proof. intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed. -Hint Resolve +#[export] Hint Resolve ord_of_compdec inh_of_compdec comp_of_compdec diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index a2831cf..ae8f9d6 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -681,4 +681,4 @@ Section list. End list. -Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec : typeclass_instances. +#[export] Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec : typeclass_instances. 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 f3c3ada..145acd3 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -157,44 +157,44 @@ Section certif. Section Build_form. Definition build_not2 i f := - fold (fun f' : BFormula (Formula Z) => N (N f')) 1 i f. + fold (fun f' : BFormula (Formula Z) isProp => NOT (NOT f')) 1 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 => let n := length args in - if n == 0 then Some (vm,TT) + if n == 0 then Some (vm,TT isProp) else - foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,Cj f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in + foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,AND f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.For args => let n := length args in - if n == 0 then Some (vm,FF) + if n == 0 then Some (vm,FF isProp) else - foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,D f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in + foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,OR f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.Fxor a b => @@ -202,26 +202,26 @@ 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 => let n := length args in - if n == 0 then Some (vm,TT) + if n == 0 then Some (vm,TT isProp) else if n <= 1 then let l := args.[0] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end else - foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in + foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else NOT f2 in Some(vm2,IMPL f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in match build_var vm (Lit.blit l) with - | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f) + | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',NOT f) | None => None end) | Form.Fiff a b => @@ -229,9 +229,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 @@ -243,10 +243,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 @@ -271,14 +271,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 @@ -286,7 +286,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 @@ -295,7 +295,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. @@ -477,14 +477,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 := @@ -958,7 +960,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. @@ -1011,7 +1013,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. @@ -1026,14 +1028,14 @@ 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; split; unfold build_not2. apply fold_ind; auto. - apply (fold_ind2 _ _ (fun b f' => b = true <-> eval_f (Zeval_formula (interp_vmap vm)) f')). + apply (fold_ind2 _ _ (fun b (f':GFormula isProp) => b = true <-> eval_f (Zeval_formula (interp_vmap vm)) f')). unfold Lit.interp; rewrite H3; auto. intros b f' H4; rewrite negb_involutive; simpl; split. intros Hb H5; apply H5; rewrite <- H4; auto. @@ -1041,12 +1043,12 @@ 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; split; unfold build_not2. apply fold_ind; auto. - apply (fold_ind2 _ _ (fun b f' => b = true <-> ~ eval_f (Zeval_formula (interp_vmap vm)) f')). + apply (fold_ind2 _ _ (fun b (f':GFormula isProp) => b = true <-> ~ eval_f (Zeval_formula (interp_vmap vm)) f')). unfold Lit.interp; rewrite H3; unfold Var.interp; split. intros H4 H5; rewrite <- H2 in H5; rewrite H5 in H4; discriminate. intro H4; case_eq (rho (Lit.blit l)); auto; intro H5; elim H4; rewrite <- H2; auto. @@ -1059,42 +1061,73 @@ Transparent build_z_atom. 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 -> @@ -1130,7 +1163,7 @@ Transparent build_z_atom. (* Fand *) simpl; unfold afold_left; case (length l == 0). 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; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H4; elim H3; rewrite <- H14; auto. @@ -1142,7 +1175,7 @@ Transparent build_z_atom. (* For *) simpl; unfold afold_left; case (length l == 0). 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); discriminate. - revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. @@ -1152,13 +1185,14 @@ Transparent build_z_atom. 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; 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; case (length l == 0). 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). case (length l <= 1). case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H8 H9; rewrite <- H7 in H9; rewrite H9 in H8; discriminate. intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H9; rewrite H7 in H9; elim H8; auto with smtcoq_core. - revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). + revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' (bf:BFormula (Formula Z) isProp), f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (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)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))). intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate. intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core. @@ -1166,7 +1200,21 @@ Transparent build_z_atom. 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 .[ i])); rewrite H13; auto with smtcoq_core. - simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; 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]))); 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 .[ i])); intro Heq2; simpl. + - unfold Lit.interp. rewrite Heq2. split. + + revert H14. case (Var.interp rho (Lit.blit (l .[ 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 .[ 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 .[ 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 .[ 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. @@ -1293,7 +1341,7 @@ Transparent build_z_atom. ( 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 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 165814b..67c705f 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 5359c15..b153730 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 |