aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2
diff options
context:
space:
mode:
Diffstat (limited to 'src/smtlib2')
-rw-r--r--src/smtlib2/sExpr.ml20
-rw-r--r--src/smtlib2/sExpr.mli16
-rw-r--r--src/smtlib2/sExprLexer.mll297
-rw-r--r--src/smtlib2/sExprParser.mly86
-rw-r--r--src/smtlib2/smtlib2_ast.ml66
-rw-r--r--src/smtlib2/smtlib2_ast.mli18
-rw-r--r--src/smtlib2/smtlib2_genConstr.ml296
-rw-r--r--src/smtlib2/smtlib2_genConstr.mli43
-rw-r--r--src/smtlib2/smtlib2_lex.mll1
-rw-r--r--src/smtlib2/smtlib2_parse.mly3
-rw-r--r--src/smtlib2/smtlib2_solver.ml169
-rw-r--r--src/smtlib2/smtlib2_solver.mli39
-rw-r--r--src/smtlib2/smtlib2_util.ml1
-rw-r--r--src/smtlib2/smtlib2_util.mli18
14 files changed, 996 insertions, 77 deletions
diff --git a/src/smtlib2/sExpr.ml b/src/smtlib2/sExpr.ml
new file mode 100644
index 0000000..b130d45
--- /dev/null
+++ b/src/smtlib2/sExpr.ml
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+type t = Atom of string | List of t list
+
+let rec print fmt = function
+ | Atom s -> Format.pp_print_string fmt s
+ | List l ->
+ Format.fprintf fmt "(@[<hov 2>";
+ List.iter (Format.fprintf fmt "%a " print) l;
+ Format.fprintf fmt "@])"
diff --git a/src/smtlib2/sExpr.mli b/src/smtlib2/sExpr.mli
new file mode 100644
index 0000000..26ea9fb
--- /dev/null
+++ b/src/smtlib2/sExpr.mli
@@ -0,0 +1,16 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+(** Type of S-expressions *)
+type t = Atom of string | List of t list
+
+val print : Format.formatter -> t -> unit
diff --git a/src/smtlib2/sExprLexer.mll b/src/smtlib2/sExprLexer.mll
new file mode 100644
index 0000000..6d0cd22
--- /dev/null
+++ b/src/smtlib2/sExprLexer.mll
@@ -0,0 +1,297 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+(* Lexer for S-expressions
+
+ Adapted from the OCaml sexplib, which is part of the ocaml-core
+ alternative standard library for OCaml.
+
+*)
+
+{
+ (** Lexer: Lexer Specification for S-expressions *)
+
+ open Printf
+ 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'
+let lf_cr = ['\010' '\013']
+let dos_newline = "\013\010"
+let blank = [' ' '\009' '\012']
+let unquoted = [^ ';' '(' ')' '"'] # blank # lf_cr
+let digit = ['0'-'9']
+let hexdigit = digit | ['a'-'f' 'A'-'F']
+
+let unquoted_start =
+ unquoted # ['#' '|'] | '#' unquoted # ['|'] | '|' unquoted # ['#']
+
+rule main buf = parse
+ | lf | dos_newline { found_newline lexbuf 0; main buf lexbuf }
+ | blank+ | ';' (_ # lf_cr)* { main buf lexbuf }
+ | '(' { LPAREN }
+ | ')' { RPAREN }
+ | '"'
+ {
+ scan_string buf (lexeme_start_p lexbuf) lexbuf;
+ let str = Buffer.contents buf in
+ Buffer.clear buf;
+ STRING str
+ }
+ | "#;" { HASH_SEMI }
+ | "#|"
+ {
+ scan_block_comment buf [lexeme_start_p lexbuf] lexbuf;
+ main buf lexbuf
+ }
+ | "|#" { main_failure lexbuf "illegal end of comment" }
+ | '|'
+ {
+ scan_quoted buf (lexeme_start_p lexbuf) lexbuf;
+ let str = Buffer.contents buf in
+ Buffer.clear buf;
+ STRING ("|"^ str ^"|")
+ }
+ | unquoted_start unquoted* ("#|" | "|#") unquoted*
+ { main_failure lexbuf "comment tokens in unquoted atom" }
+ | "#" | unquoted_start unquoted* as str { STRING str }
+ | eof { EOF }
+
+and scan_string buf start = parse
+ | '"' { () }
+ | '\\' lf [' ' '\t']*
+ {
+ found_newline lexbuf (lexeme_len lexbuf - 2);
+ scan_string buf start lexbuf
+ }
+ | '\\' dos_newline [' ' '\t']*
+ {
+ found_newline lexbuf (lexeme_len lexbuf - 3);
+ scan_string buf start lexbuf
+ }
+ | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c)
+ {
+ Buffer.add_char buf (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
+ if v > 255 then (
+ let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
+ let msg =
+ sprintf
+ "Sexplib.Lexer.scan_string: \
+ illegal escape at line %d char %d: `\\%c%c%c'"
+ pos_lnum (pos_cnum - pos_bol - 3)
+ c1 c2 c3 in
+ failwith msg);
+ Buffer.add_char buf (Char.chr v);
+ scan_string buf start lexbuf
+ }
+ | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
+ {
+ let v = hex_code c1 c2 in
+ Buffer.add_char buf (Char.chr v);
+ scan_string buf start lexbuf
+ }
+ | '\\' (_ as c)
+ {
+ Buffer.add_char buf '\\';
+ Buffer.add_char buf c;
+ scan_string buf start lexbuf
+ }
+ | lf
+ {
+ found_newline lexbuf 0;
+ Buffer.add_char buf lf;
+ scan_string buf start lexbuf
+ }
+ | ([^ '\\' '"'] # lf)+
+ {
+ Buffer.add_string buf (lexeme lexbuf);
+ scan_string buf start lexbuf
+ }
+ | eof
+ {
+ let msg =
+ sprintf
+ "Sexplib.Lexer.scan_string: unterminated string at line %d char %d"
+ start.pos_lnum (start.pos_cnum - start.pos_bol)
+ in
+ failwith msg
+ }
+
+and scan_quoted buf start = parse
+ | '|' { () }
+ | '\\' lf [' ' '\t']*
+ {
+ found_newline lexbuf (lexeme_len lexbuf - 2);
+ scan_quoted buf start lexbuf
+ }
+ | '\\' dos_newline [' ' '\t']*
+ {
+ found_newline lexbuf (lexeme_len lexbuf - 3);
+ scan_quoted buf start lexbuf
+ }
+ | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' ' '|'] as c)
+ {
+ Buffer.add_char buf (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
+ if v > 255 then (
+ let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
+ let msg =
+ sprintf
+ "Sexplib.Lexer.scan_quoted: \
+ illegal escape at line %d char %d: `\\%c%c%c'"
+ pos_lnum (pos_cnum - pos_bol - 3)
+ c1 c2 c3 in
+ failwith msg);
+ Buffer.add_char buf (Char.chr v);
+ scan_quoted buf start lexbuf
+ }
+ | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
+ {
+ let v = hex_code c1 c2 in
+ Buffer.add_char buf (Char.chr v);
+ scan_quoted buf start lexbuf
+ }
+ | '\\' (_ as c)
+ {
+ Buffer.add_char buf '\\';
+ Buffer.add_char buf c;
+ scan_quoted buf start lexbuf
+ }
+ | lf
+ {
+ found_newline lexbuf 0;
+ Buffer.add_char buf lf;
+ scan_quoted buf start lexbuf
+ }
+ | ([^ '\\' '|'] # lf)+
+ {
+ Buffer.add_string buf (lexeme lexbuf);
+ scan_quoted buf start lexbuf
+ }
+ | eof
+ {
+ let msg =
+ sprintf
+ "Sexplib.Lexer.scan_quoted: unterminated ident at line %d char %d"
+ start.pos_lnum (start.pos_cnum - start.pos_bol)
+ in
+ failwith msg
+ }
+
+and scan_block_comment buf locs = parse
+ | ('#'* | '|'*) lf
+ { found_newline lexbuf 0; scan_block_comment buf locs lexbuf }
+ | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+ { scan_block_comment buf locs lexbuf }
+ | ('#'* | '|'*) '"'
+ {
+ let cur = lexeme_end_p lexbuf in
+ let start = { cur with pos_cnum = cur.pos_cnum - 1 } in
+ scan_string buf start lexbuf;
+ Buffer.clear buf;
+ scan_block_comment buf locs lexbuf
+ }
+ | '#'+ '|'
+ {
+ let cur = lexeme_end_p lexbuf in
+ let start = { cur with pos_cnum = cur.pos_cnum - 2 } in
+ scan_block_comment buf (start :: locs) lexbuf
+ }
+ | '|'+ '#'
+ {
+ match locs with
+ | [_] -> ()
+ | _ :: t -> scan_block_comment buf t lexbuf
+ | [] -> assert false (* impossible *)
+ }
+ | eof
+ {
+ match locs with
+ | [] -> assert false
+ | { pos_lnum; pos_bol; pos_cnum; _ } :: _ ->
+ let msg =
+ sprintf "Sexplib.Lexer.scan_block_comment: \
+ unterminated block comment at line %d char %d"
+ pos_lnum (pos_cnum - pos_bol)
+ in
+ failwith msg
+ }
+
+and ruleTail acc = parse
+ | eof { acc }
+ | _* as str { ruleTail (acc ^ str) lexbuf }
+
+
+{
+ let main ?buf =
+ let buf =
+ match buf with
+ | None -> Buffer.create 64
+ | Some buf -> Buffer.clear buf; buf
+ in
+ main buf
+}
+
diff --git a/src/smtlib2/sExprParser.mly b/src/smtlib2/sExprParser.mly
new file mode 100644
index 0000000..6e3eb77
--- /dev/null
+++ b/src/smtlib2/sExprParser.mly
@@ -0,0 +1,86 @@
+%{
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+(* Parser for S-expressions
+
+ Code lightly adapted from the OCaml sexplib, which is part of the
+ ocaml-core alternative standard library for OCaml.
+
+*)
+
+ (** Parser: Grammar Specification for Parsing S-expressions *)
+
+ open Lexing
+
+ let parse_failure what =
+ let pos = symbol_start_pos () in
+ let msg =
+ Printf.sprintf "SExprParser: failed to parse line %d char %d: %s"
+ pos.pos_lnum (pos.pos_cnum - pos.pos_bol) what in
+ failwith msg
+%}
+
+%token <string> STRING
+%token LPAREN RPAREN HASH_SEMI EOF
+
+%start sexp
+%type <SExpr.t> sexp
+
+%start sexp_opt
+%type <SExpr.t option> sexp_opt
+
+%start sexps
+%type <SExpr.t list> sexps
+
+%start rev_sexps
+%type <SExpr.t list> rev_sexps
+
+%%
+
+sexp:
+| sexp_comments sexp_but_no_comment { $2 }
+| sexp_but_no_comment { $1 }
+
+sexp_but_no_comment
+ : STRING { SExpr.Atom $1 }
+ | LPAREN RPAREN { SExpr.List [] }
+ | LPAREN rev_sexps_aux RPAREN { SExpr.List (List.rev $2) }
+ | error { parse_failure "sexp" }
+
+sexp_comment
+ : HASH_SEMI sexp_but_no_comment { () }
+ | HASH_SEMI sexp_comments sexp_but_no_comment { () }
+
+sexp_comments
+ : sexp_comment { () }
+ | sexp_comments sexp_comment { () }
+
+sexp_opt
+ : sexp_but_no_comment { Some $1 }
+ | sexp_comments sexp_but_no_comment { Some $2 }
+ | EOF { None }
+ | sexp_comments EOF { None }
+
+rev_sexps_aux
+ : sexp_but_no_comment { [$1] }
+ | sexp_comment { [] }
+ | rev_sexps_aux sexp_but_no_comment { $2 :: $1 }
+ | rev_sexps_aux sexp_comment { $1 }
+
+rev_sexps
+ : rev_sexps_aux EOF { $1 }
+ | EOF { [] }
+
+sexps
+ : rev_sexps_aux EOF { List.rev $1 }
+ | EOF { [] }
diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
index cce4625..7317b60 100644
--- a/src/smtlib2/smtlib2_ast.ml
+++ b/src/smtlib2/smtlib2_ast.ml
@@ -15,6 +15,7 @@
(* *)
(**************************************************************************)
+
open Smtlib2_util
type loc = Lexing.position * Lexing.position
@@ -187,3 +188,68 @@ let loc_varbinding = function
let loc_couple = fst
let loc_of e = loc_commands e;;
+
+
+
+let print_specconstant fmt = function
+ | SpecConstsDec (_, s)
+ | SpecConstNum (_, s)
+ | SpecConstString (_, s)
+ | SpecConstsHex (_, s)
+ | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s
+
+
+let print_symbol fmt = function
+ | Symbol (_, s)
+ | SymbolWithOr (_, s) -> Format.pp_print_string fmt s
+
+
+let print_identifier fmt = function
+ | IdSymbol (_, s) -> print_symbol fmt s
+ | IdUnderscoreSymNum (_, s, (_, l)) ->
+ Format.fprintf fmt "(_ %a" print_symbol s;
+ List.iter (Format.fprintf fmt " %s") l;
+ Format.fprintf fmt ")"
+
+let rec print_sort fmt = function
+ | SortIdentifier (_, i) -> print_identifier fmt i
+ | SortIdSortMulti (_, i, (_, ls)) ->
+ Format.fprintf fmt "(%a" print_identifier i;
+ List.iter (Format.fprintf fmt " %a" print_sort) ls;
+ Format.fprintf fmt ")"
+
+let print_qualidentifier fmt = function
+ | QualIdentifierId (_, i) -> print_identifier fmt i
+ | QualIdentifierAs (_, i, s) ->
+ Format.fprintf fmt "(%a as %a)"
+ print_identifier i print_sort s
+
+let print_sortedvar fmt = function
+ | SortedVarSymSort (_, v, s) ->
+ Format.fprintf fmt "(%a %a)" print_symbol v print_sort s
+
+let rec print_varbinding fmt = function
+ | VarBindingSymTerm (_, s, t) ->
+ Format.fprintf fmt "(%a %a)" print_symbol s print_term t
+
+and print_term fmt = function
+ | TermSpecConst (_, c) -> print_specconstant fmt c
+ | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
+ | TermQualIdTerm (_, i, (_, tl)) ->
+ Format.fprintf fmt "(%a" print_qualidentifier i;
+ List.iter (Format.fprintf fmt " %a" print_term) tl;
+ Format.fprintf fmt ")"
+ | TermLetTerm (_, (_, vb), t) ->
+ Format.fprintf fmt "(let (";
+ List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
+ Format.fprintf fmt ") %a)" print_term t
+ | TermForAllTerm (_, (_, sv), t) ->
+ Format.fprintf fmt "(forall (";
+ List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ Format.fprintf fmt ") %a)" print_term t
+ | TermExistsTerm (_, (_, sv), t) ->
+ Format.fprintf fmt "(exists (";
+ List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ Format.fprintf fmt ") %a)" print_term t
+ | TermExclimationPt (_, t, _) -> print_term fmt t
+
diff --git a/src/smtlib2/smtlib2_ast.mli b/src/smtlib2/smtlib2_ast.mli
index 4fb1280..3d3f126 100644
--- a/src/smtlib2/smtlib2_ast.mli
+++ b/src/smtlib2/smtlib2_ast.mli
@@ -1,3 +1,21 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq, originally belong to The Alt-ergo theorem prover *)
+(* Copyright (C) 2006-2010 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* Stephane Lescuyer *)
+(* Mohamed Iguernelala *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type loc = Lexing.position * Lexing.position
type specconstant =
SpecConstsDec of loc * string
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 76dde25..692294d 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -1,13 +1,9 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2016 *)
+(* Copyright (C) 2011 - 2019 *)
(* *)
-(* Michaël Armand *)
-(* Benjamin Grégoire *)
-(* Chantal Keller *)
-(* *)
-(* Inria - École Polytechnique - Université Paris-Sud *)
+(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
@@ -42,45 +38,72 @@ let identifier_of_qualidentifier = function
| QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id
-let string_type s = match s with
- | "Bool" -> Tbool
- | "Int" -> TZ
- | _ -> VeritSyntax.get_btype s
-
+let string_type s =
+ match s with
+ | "Bool" -> fun _ -> Tbool
+ | "Int" -> fun _ -> TZ
+ | "Array" -> (function [ti;te] -> TFArray (ti, te) | _ -> assert false)
+ | _ ->
+ try Scanf.sscanf s "BitVec_%d%!" (fun size -> fun _ -> TBV size)
+ with _ -> fun _ -> VeritSyntax.get_btype s
-let sort_of_string s = (string_type s, [])
+let sort_of_string s = string_type s
let sort_of_symbol s = sort_of_string (string_of_symbol s)
+let rec bigint_binary_size acc i size =
+ let open Big_int in
+ if size = 0 then "#b" ^ String.concat "" acc
+ else
+ if eq_big_int i zero_big_int then
+ bigint_binary_size ("0" :: acc) i (size - 1)
+ else begin
+ assert (gt_big_int i zero_big_int && size > 0);
+ bigint_binary_size (string_of_big_int (and_big_int i unit_big_int) :: acc)
+ (shift_right_big_int i 1) (size - 1)
+ end
+
+let bigint_bv i size = bigint_binary_size [] i size
+
+
+exception DecimalBv of string
+
let string_of_identifier = function
| IdSymbol (_,s) -> (string_of_symbol s)
| IdUnderscoreSymNum (_,s,(_,l)) ->
- List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l
+ let s = string_of_symbol s in
+ let isbvdec =
+ try s.[0] = 'b' && s.[1]= 'v' with Invalid_argument _ -> false in
+ (match isbvdec, l with
+ (* rewrite bitvectors decimal constants *)
+ | true, [size] ->
+ let sbv =
+ Scanf.sscanf s "bv%s" (fun n ->
+ bigint_bv (Big_int.big_int_of_string n) (int_of_string size)) in
+ raise (DecimalBv sbv)
+ | _ -> List.fold_left (fun c c' -> c^"_"^c') s l
+ )
let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id)
let rec sort_of_sort = function
- | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id)
+ | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id) []
| SortIdSortMulti (_,id,(_,l)) ->
- (string_type (string_of_identifier id), List.map sort_of_sort l)
+ sort_of_string (string_of_identifier id) (List.map sort_of_sort l)
let declare_sort rt sym =
let s = string_of_symbol sym in
let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in
- let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in
- let x = mkName "x" in
- let y = mkName "y" in
- let rx = Term.mkRel 2 in
- let ry = Term.mkRel 1 in
- let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
- let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in
- let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in
- let res = declare rt cons_t ce in
+ let compdec_type = mklApp cCompDec [| cons_t |] in
+ let compdec_var =
+ declare_new_variable (Names.id_of_string ("CompDec_"^s)) compdec_type in
+ let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in
+ let res = SmtBtype.declare rt cons_t ce in
VeritSyntax.add_btype s res;
res
@@ -89,15 +112,27 @@ let declare_fun rt ro sym arg cod =
let s = string_of_symbol sym in
let tyl = List.map sort_of_sort arg in
let ty = sort_of_sort cod in
-
- let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in
+ let coqTy = List.fold_right (fun typ c ->
+ Term.mkArrow (interp_to_coq rt typ) c)
+ tyl (interp_to_coq rt ty) in
let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
-
- let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) None in
+ let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
VeritSyntax.add_fun s op;
op
+
+let parse_smt2bv s =
+ let l = ref [] in
+ for i = 2 to String.length s - 1 do
+ match s.[i] with
+ | '0' -> l := false :: !l
+ | '1' -> l := true :: !l
+ | _ -> failwith "Not a bitvector"
+ done;
+ !l
+
+
let make_root_specconstant ra = function
| SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet"
| SpecConstNum (_,s) ->
@@ -110,11 +145,15 @@ let make_root_specconstant ra = function
Atom.hatom_Z_of_bigint ra i)
| SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet"
| SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet"
- | SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet"
+ | SpecConstsBinary (_, s) -> Atom.mk_bvconst ra (parse_smt2bv s)
+
+
type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
+let startwith prefix s =
+ try Scanf.sscanf s (prefix ^^ "%_s") true with _ -> false
let make_root ra rf t =
@@ -122,11 +161,14 @@ let make_root ra rf t =
let rec make_root_term = function
| TermSpecConst (_,c) -> Atom (make_root_specconstant ra c)
- | TermQualIdentifier (_,id) ->
- let v = string_of_qualidentifier id in
- (try Hashtbl.find hlets v with
- | Not_found ->
- make_root_app v [])
+ | TermQualIdentifier (loc,id) ->
+ (try
+ let v = string_of_qualidentifier id in
+ (try Hashtbl.find hlets v with Not_found -> make_root_app v [])
+ with
+ | DecimalBv sbv ->
+ make_root_term (TermSpecConst (loc, SpecConstsBinary (loc, sbv)))
+ )
| TermQualIdTerm (_,id,(_,l)) ->
let v = string_of_qualidentifier id in
make_root_app v l
@@ -144,43 +186,162 @@ let make_root ra rf t =
match (v,l) with
| "=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' ->
- (match Atom.type_of a' with
- | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|])))
- | ty -> Atom (Atom.mk_eq ra true ty a' b'))
- | _, _ -> assert false)
+ | Atom a', Atom b' when Atom.type_of a' <> Tbool ->
+ Atom (Atom.mk_eq ra (Atom.type_of a') a' b')
+ | _ -> Form (Form.get rf (Fapp (Fiff, [|make_root a; make_root b|])))
+ )
| "<", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_lt ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b')
| _, _ -> assert false)
| "<=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_le ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b')
| _, _ -> assert false)
| ">", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_gt ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b')
| _, _ -> assert false)
| ">=", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_ge ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b')
| _, _ -> assert false)
| "+", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_plus ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b')
| _, _ -> assert false)
| "-", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_minus ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b')
| _, _ -> assert false)
| "*", [a;b] ->
(match make_root_term a, make_root_term b with
- | Atom a', Atom b' -> Atom (Atom.mk_mult ra true a' b')
+ | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b')
| _, _ -> assert false)
| "-", [a] ->
(match make_root_term a with
| Atom a' -> Atom (Atom.mk_opp ra a')
| _ -> assert false)
+ | "bvnot", [a] ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvnot ra s a')
+ | _ -> assert false)
+ | _ -> assert false)
+ | "bvneg", [a] ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvneg ra s a')
+ | _ -> assert false)
+ | _ -> assert false)
+ | "bvand", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvand ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvor", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvor ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvxor", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvxor ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvadd", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvadd ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvmul", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvmult ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvult", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvult ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvslt", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvslt ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvule", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom h1, Atom h2 ->
+ (match Atom.type_of h1 with
+ | TBV s ->
+ let a = Atom.mk_bvult ra s h2 h1 in
+ Form (Form.neg (Form.get rf (Fatom a)))
+ | _ -> assert false)
+ | _,_ -> assert false
+ )
+ | "bvsle", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom h1, Atom h2 ->
+ (match Atom.type_of h1 with
+ | TBV s ->
+ let a = Atom.mk_bvslt ra s h2 h1 in
+ Form (Form.neg (Form.get rf (Fatom a)))
+ | _ -> assert false)
+ | _,_ -> assert false
+ )
+ | "bvshl", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvshl ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "bvlshr", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvshr ra s a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "concat", [a;b] ->
+ (match make_root_term a, make_root_term b with
+ | Atom a', Atom b' ->
+ (match Atom.type_of a', Atom.type_of b' with
+ | TBV s1, TBV s2 -> Atom (Atom.mk_bvconcat ra s1 s2 a' b')
+ | _ -> assert false)
+ | _, _ -> assert false)
+ | "select", [a;i] ->
+ (match make_root_term a, make_root_term i with
+ | Atom a', Atom i' ->
+ (match Atom.type_of a' with
+ | TFArray (ti, te) -> Atom (Atom.mk_select ra ti te a' i')
+ | _ -> assert false)
+ | _ -> assert false)
+
+ | "store", [a;i;v] ->
+ (match make_root_term a, make_root_term i, make_root_term v with
+ | Atom a', Atom i', Atom v' ->
+ (match Atom.type_of a' with
+ | TFArray (ti, te) -> Atom (Atom.mk_store ra ti te a' i' v')
+ | _ -> assert false)
+ | _ -> assert false)
+
| "distinct", _ ->
let make_h h =
match make_root_term h with
@@ -205,10 +366,49 @@ let make_root ra rf t =
| "ite", _ ->
Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l))))
| "not", [a] -> Form (Form.neg (make_root a))
+
+ | _, [a] when startwith "extract_" v ->
+ (try
+ Scanf.sscanf v "extract_%s@_%d" (fun s i ->
+ let j = int_of_string s in
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
+ | _, [a] when startwith "zero_extend_" v ->
+ (try
+ Scanf.sscanf v "zero_extend_%d" (fun n ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvzextn ra ~s ~n a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
+ | _, [a] when startwith "sign_extend_" v ->
+ (try
+ Scanf.sscanf v "sign_extend_%d" (fun n ->
+ (match make_root_term a with
+ | Atom a' ->
+ (match Atom.type_of a' with
+ | TBV s -> Atom (Atom.mk_bvsextn ra ~s ~n a')
+ | _ -> assert false)
+ | _ -> assert false)
+ )
+ with _ -> assert false)
+
| _, _ ->
let op = VeritSyntax.get_fun v in
- let l' = List.map (fun t -> match make_root_term t with
- | Atom h -> h | Form _ -> assert false) l in
+ let l' = List.map (fun t ->
+ match make_root_term t with
+ | Atom h -> h | Form _ -> assert false) l in
Atom (Atom.get ra (Aapp (op, Array.of_list l')))
and make_root t =
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
index 1aa992e..40f73c7 100644
--- a/src/smtlib2/smtlib2_genConstr.mli
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -1,32 +1,17 @@
-val pp_symbol : Smtlib2_ast.symbol -> string
-val string_of_symbol : Smtlib2_ast.symbol -> string
-val identifier_of_qualidentifier :
- Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier
-val string_type : string -> SmtBtype.btype
-val sort_of_string : string -> SmtBtype.btype * 'a list
-val sort_of_symbol : Smtlib2_ast.symbol -> SmtBtype.btype * 'a list
-val string_of_identifier : Smtlib2_ast.identifier -> string
-val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string
-val sort_of_sort : Smtlib2_ast.sort -> (SmtBtype.btype * 'a list as 'a)
-val declare_sort :
- SmtBtype.reify_tbl -> Smtlib2_ast.symbol -> SmtBtype.btype
-val declare_fun :
- SmtBtype.reify_tbl ->
- SmtAtom.Op.reify_tbl ->
- Smtlib2_ast.symbol ->
- Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
-val make_root_specconstant :
- SmtAtom.Atom.reify_tbl -> Smtlib2_ast.specconstant -> SmtAtom.hatom
-type atom_form = Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
-val make_root :
- SmtAtom.Atom.reify_tbl ->
- SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t
-val declare_commands :
- SmtBtype.reify_tbl ->
- SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl ->
- SmtAtom.Form.reify ->
- SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+val parse_smt2bv : string -> bool list
+val bigint_bv : Big_int.big_int -> int -> string
val import_smtlib2 :
SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
diff --git a/src/smtlib2/smtlib2_lex.mll b/src/smtlib2/smtlib2_lex.mll
index f235403..2b965af 100644
--- a/src/smtlib2/smtlib2_lex.mll
+++ b/src/smtlib2/smtlib2_lex.mll
@@ -15,6 +15,7 @@
(* *)
(**************************************************************************)
+
{
open Lexing
open Smtlib2_parse
diff --git a/src/smtlib2/smtlib2_parse.mly b/src/smtlib2/smtlib2_parse.mly
index b4e02a7..d618a1a 100644
--- a/src/smtlib2/smtlib2_parse.mly
+++ b/src/smtlib2/smtlib2_parse.mly
@@ -15,6 +15,7 @@
/* */
/**************************************************************************/
+
%{
open Smtlib2_ast
@@ -23,6 +24,8 @@
%}
%start main
+%start term
+%start sort
/* general */
%token EXCLIMATIONPT
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
new file mode 100644
index 0000000..3ee8229
--- /dev/null
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -0,0 +1,169 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+open Format
+
+type result = Sat | Unsat
+
+type t = {
+ cmd : string array;
+ pid : int;
+ stdin : Unix.file_descr;
+ stdout : Unix.file_descr;
+ stderr : Unix.file_descr;
+ lexbuf : Lexing.lexbuf;
+}
+
+
+let create cmd =
+ let executable = cmd.(0) in
+
+ (* Create pipes for input, output and error output *)
+ let stdin_in, stdin_out = Unix.pipe () in
+ let stdout_in, stdout_out = Unix.pipe () in
+ let stderr_in, stderr_out = Unix.pipe () in
+
+ (* Create solver process *)
+ let pid =
+ Unix.create_process
+ executable
+ cmd
+ stdin_in
+ stdout_out
+ stderr_out
+ in
+
+ (* Close our end of the pipe which has been duplicated by the
+ process *)
+ Unix.close stdin_in;
+ Unix.close stdout_out;
+ Unix.close stderr_out;
+
+ (* Get an output channel to read from solver's stdout *)
+ let stdout_ch = Unix.in_channel_of_descr stdout_in in
+
+ let lexbuf = Lexing.from_channel stdout_ch in
+
+ (* Create the solver instance *)
+ { cmd; pid;
+ stdin = stdin_out; stdout = stdout_in; stderr = stderr_in; lexbuf }
+
+
+let kill s =
+ try
+ Unix.close s.stdin;
+ Unix.close s.stdout;
+ Unix.close s.stderr;
+ Unix.kill s.pid Sys.sigkill;
+ with _ -> ()
+
+
+let read_response { lexbuf } =
+ SExprParser.sexp SExprLexer.main lexbuf
+
+
+let error s sexp =
+ kill s;
+ Structures.error (asprintf "Solver error: %a." SExpr.print sexp)
+
+
+let read_success s =
+ match SExprParser.sexp SExprLexer.main s.lexbuf with
+ | SExpr.Atom "success" -> ()
+ | r -> error s r
+
+
+let no_response _ = ()
+
+
+let read_check_result s =
+ match SExprParser.sexp SExprLexer.main s.lexbuf with
+ | SExpr.Atom "sat" -> Sat
+ | SExpr.Atom "unsat" -> Unsat
+ | SExpr.Atom "unknown" -> Structures.error ("Solver returned uknown.")
+ | r -> error s r
+
+
+let send_command s cmd read =
+ eprintf "%s@." cmd;
+ let err_p1 = Unix.((fstat s.stderr).st_size) in
+ try
+ let in_ch = Unix.out_channel_of_descr s.stdin in
+ let fmt = formatter_of_out_channel in_ch in
+ pp_print_string fmt cmd;
+ pp_print_newline fmt ();
+ read s
+ with e ->
+ let err_p2 = Unix.((fstat s.stderr).st_size) in
+ let len = err_p2 - err_p1 in
+ (* Was something written to stderr? *)
+ if len <> 0 then begin
+ let buf = Bytes.create err_p2 in
+ Unix.read s.stderr buf 0 err_p2 |> ignore;
+ let err_msg = Bytes.sub_string buf err_p1 len in
+ Structures.error ("Solver error: "^err_msg);
+ end
+ else (kill s; raise e)
+
+
+let set_option s name b =
+ send_command s
+ (asprintf "(set-option :%s %b)" name b)
+ read_success
+
+
+let set_logic s l =
+ send_command s
+ (sprintf "(set-logic %s)" l)
+ read_success
+
+
+let declare_sort s name arity =
+ send_command s
+ (asprintf "(declare-sort %s %d)" name arity)
+ read_success
+
+
+let declare_fun s name args ret =
+ send_command s
+ (asprintf "(declare-fun %s (%a) %s)"
+ name
+ (fun fmt -> List.iter (fprintf fmt "%s ")) args
+ ret)
+ read_success
+
+
+let assume s f =
+ send_command s
+ (sprintf "(assert %s)" f)
+ read_success
+
+
+let check_sat s =
+ send_command s "(check-sat)" read_check_result
+
+
+let get_proof s process_proof =
+ send_command s "(get-proof)" (fun s -> process_proof s.lexbuf)
+
+
+let get_model s =
+ send_command s "(get-model)" read_response
+
+
+let quit s =
+ try
+ send_command s "(exit)" read_success;
+ with Unix.Unix_error _ -> ();
+ kill s
+
+
diff --git a/src/smtlib2/smtlib2_solver.mli b/src/smtlib2/smtlib2_solver.mli
new file mode 100644
index 0000000..3a7f2fc
--- /dev/null
+++ b/src/smtlib2/smtlib2_solver.mli
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+type t
+
+type result = Sat | Unsat
+
+val create : string array -> t
+
+val send_command : t -> string -> (t -> 'a) -> 'a
+
+val set_option : t -> string -> bool -> unit
+
+val set_logic : t -> string -> unit
+
+val declare_sort : t -> string -> int -> unit
+
+val declare_fun : t -> string -> string list -> string -> unit
+
+val assume : t -> string -> unit
+
+val check_sat : t -> result
+
+val get_proof : t -> (Lexing.lexbuf -> 'a) -> 'a
+
+val get_model : t -> SExpr.t
+
+val quit : t -> unit
+
+
diff --git a/src/smtlib2/smtlib2_util.ml b/src/smtlib2/smtlib2_util.ml
index 1ce5e46..d503145 100644
--- a/src/smtlib2/smtlib2_util.ml
+++ b/src/smtlib2/smtlib2_util.ml
@@ -15,6 +15,7 @@
(* *)
(**************************************************************************)
+
(* auto-generated by gt *)
(* no extra data from grammar file. *)
diff --git a/src/smtlib2/smtlib2_util.mli b/src/smtlib2/smtlib2_util.mli
index 8afbce3..b4e8916 100644
--- a/src/smtlib2/smtlib2_util.mli
+++ b/src/smtlib2/smtlib2_util.mli
@@ -1,3 +1,21 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq, originally belong to The Alt-ergo theorem prover *)
+(* Copyright (C) 2006-2010 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* Stephane Lescuyer *)
+(* Mohamed Iguernelala *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type extradata = unit
val initial_data : unit -> unit
val file : string ref
generated by cgit (git 2.34.1) at 2024-07-01 03:35:15 +0000