diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-07 14:29:45 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-07 14:29:45 +0200 |
commit | 917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7 (patch) | |
tree | c4517a0d8785ad601c7272dea0c593380b4ad1e0 | |
parent | ba837ed3edd22a96e9da74b07a2f42058e9c4f9c (diff) | |
download | smtcoq-917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7.tar.gz smtcoq-917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7.zip |
Lia + factorize code
-rw-r--r-- | src/lfsc/lfscLexer.mll | 71 | ||||
-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 |
5 files changed, 97 insertions, 130 deletions
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.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 95f8bd2..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 (lexbuf:Lexing.lexbuf) diff = - lexbuf.lex_curr_p <- - { - lexbuf.lex_curr_p with - pos_lnum = lexbuf.lex_curr_p.pos_lnum + 1; - pos_bol = lexbuf.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 |