aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-06-07 14:29:45 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2021-06-07 14:29:45 +0200
commit917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7 (patch)
treec4517a0d8785ad601c7272dea0c593380b4ad1e0
parentba837ed3edd22a96e9da74b07a2f42058e9c4f9c (diff)
downloadsmtcoq-917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7.tar.gz
smtcoq-917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7.zip
Lia + factorize code
-rw-r--r--src/lfsc/lfscLexer.mll71
-rw-r--r--src/lia/lia.ml20
-rw-r--r--src/smtlib2/sExprLexer.mll80
-rw-r--r--src/trace/smtMisc.ml47
-rw-r--r--src/trace/smtMisc.mli9
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