mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
refactor: depend on smtlib-utils instead of having custom parser
This commit is contained in:
Simon Cruanes
parent
721b1874b7
commit
8162a841fe
9 changed files with 14 additions and 863 deletions
|
|
@ -15,11 +15,15 @@ depends: [
|
|||
"containers"
|
||||
"iter"
|
||||
"zarith"
|
||||
"smtlib-utils" { >= "0.1" & < "0.2" }
|
||||
"sidekick" { = version }
|
||||
"menhir"
|
||||
"msat" { >= "0.8" < "0.9" }
|
||||
"ocaml" { >= "4.03" }
|
||||
]
|
||||
pin-depends: [
|
||||
["smtlib-utils.0.1" "git+https://github.com/c-cube/smtlib-utils.git"]
|
||||
]
|
||||
tags: [ "sat" "smt" ]
|
||||
homepage: "https://github.com/c-cube/sidekick"
|
||||
dev-repo: "git+https://github.com/c-cube/sidekick.git"
|
||||
|
|
|
|||
|
|
@ -1,95 +0,0 @@
|
|||
|
||||
(* This file is free software. See file "license" for more details. *)
|
||||
|
||||
(** {1 Lexer for TIP} *)
|
||||
|
||||
{
|
||||
module A = Parse_ast
|
||||
module Loc = Locations
|
||||
open Parser (* for tokens *)
|
||||
|
||||
}
|
||||
|
||||
let printable_char = [^ '\n']
|
||||
let comment_line = ';' printable_char*
|
||||
|
||||
let sym = [^ '"' '(' ')' '\\' ' ' '\t' '\r' '\n']
|
||||
|
||||
let ident = sym+
|
||||
|
||||
let quoted = '"' ([^ '"'] | '\\' '"')* '"'
|
||||
let escaped = '|' [^ '|']* '|'
|
||||
|
||||
rule token = parse
|
||||
| eof { EOI }
|
||||
| '\n' { Lexing.new_line lexbuf; token lexbuf }
|
||||
| [' ' '\t' '\r'] { token lexbuf }
|
||||
| comment_line { token lexbuf }
|
||||
| '(' { LEFT_PAREN }
|
||||
| ')' { RIGHT_PAREN }
|
||||
| "true" { TRUE }
|
||||
| "false" { FALSE }
|
||||
| "or" { OR }
|
||||
| "and" { AND }
|
||||
| "not" { NOT }
|
||||
| "xor" { XOR }
|
||||
| "distinct" { DISTINCT }
|
||||
| "ite" { IF }
|
||||
| "as" { AS }
|
||||
| "match" { MATCH }
|
||||
| "case" { CASE }
|
||||
| "default" { DEFAULT }
|
||||
| "lambda" { FUN }
|
||||
| "let" { LET }
|
||||
| "par" { PAR }
|
||||
| "=>" { ARROW }
|
||||
| "=" { EQ }
|
||||
| "@" { AT }
|
||||
| "+" { ADD }
|
||||
| "-" { MINUS }
|
||||
| "*" { PROD }
|
||||
| "/" { DIV }
|
||||
| "<=" { LEQ }
|
||||
| "<" { LT }
|
||||
| ">=" { GEQ }
|
||||
| ">" { GT }
|
||||
| "declare-datatypes" { DATA }
|
||||
| "assert" { ASSERT }
|
||||
| "lemma" { LEMMA }
|
||||
| "assert-not" { ASSERT_NOT }
|
||||
| "declare-sort" { DECLARE_SORT }
|
||||
| "declare-fun" { DECLARE_FUN }
|
||||
| "declare-const" { DECLARE_CONST }
|
||||
| "define-fun" { DEFINE_FUN }
|
||||
| "define-fun-rec" { DEFINE_FUN_REC }
|
||||
| "define-funs-rec" { DEFINE_FUNS_REC }
|
||||
| "forall" { FORALL }
|
||||
| "exists" { EXISTS }
|
||||
| "check-sat" { CHECK_SAT }
|
||||
| "set-logic" { SET_LOGIC }
|
||||
| "set-option" { SET_OPTION }
|
||||
| "set-info" { SET_INFO }
|
||||
| "exit" { EXIT }
|
||||
| ident {
|
||||
let s = Lexing.lexeme lexbuf in
|
||||
IDENT(s)
|
||||
}
|
||||
| quoted {
|
||||
(* TODO: unescape *)
|
||||
let s = Lexing.lexeme lexbuf in
|
||||
let s = String.sub s 1 (String.length s -2) in (* remove " " *)
|
||||
QUOTED s }
|
||||
| escaped {
|
||||
let s = Lexing.lexeme lexbuf in
|
||||
CCString.iter (function '\n' -> Lexing.new_line lexbuf | _ -> ()) s;
|
||||
let s = String.sub s 1 (String.length s -2) in (* remove "|" *)
|
||||
ESCAPED s }
|
||||
| _ as c
|
||||
{
|
||||
let loc = Loc.of_lexbuf lexbuf in
|
||||
A.parse_errorf ~loc "unexpected char '%c'" c
|
||||
}
|
||||
|
||||
{
|
||||
|
||||
}
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *)
|
||||
|
||||
(** {1 Locations} *)
|
||||
|
||||
type t = {
|
||||
file : string;
|
||||
start_line : int;
|
||||
start_column : int;
|
||||
stop_line : int;
|
||||
stop_column : int;
|
||||
}
|
||||
|
||||
let mk file start_line start_column stop_line stop_column =
|
||||
{ file; start_line; start_column; stop_line; stop_column; }
|
||||
|
||||
let mk_pair file (a,b)(c,d) = mk file a b c d
|
||||
|
||||
let mk_pos start stop =
|
||||
let open Lexing in
|
||||
mk
|
||||
start.pos_fname
|
||||
start.pos_lnum (start.pos_cnum - start.pos_bol)
|
||||
stop.pos_lnum (stop.pos_cnum - stop.pos_bol)
|
||||
|
||||
let equal = (=)
|
||||
|
||||
let pp out pos =
|
||||
if pos.start_line = pos.stop_line
|
||||
then
|
||||
Format.fprintf out "file '%s': line %d, col %d to %d"
|
||||
pos.file pos.start_line pos.start_column pos.stop_column
|
||||
else
|
||||
Format.fprintf out "file '%s': line %d, col %d to line %d, col %d"
|
||||
pos.file
|
||||
pos.start_line pos.start_column
|
||||
pos.stop_line pos.stop_column
|
||||
|
||||
let pp_opt out = function
|
||||
| None -> Format.fprintf out "<no location>"
|
||||
| Some pos -> pp out pos
|
||||
|
||||
let pp_to_string pp x =
|
||||
let buf = Buffer.create 64 in
|
||||
let fmt = Format.formatter_of_buffer buf in
|
||||
pp fmt x;
|
||||
Format.pp_print_flush fmt ();
|
||||
Buffer.contents buf
|
||||
|
||||
let to_string_opt = pp_to_string pp_opt
|
||||
|
||||
(** {2 Lexbuf} *)
|
||||
|
||||
let set_file buf filename =
|
||||
let open Lexing in
|
||||
buf.lex_curr_p <- {buf.lex_curr_p with pos_fname=filename;};
|
||||
()
|
||||
|
||||
let get_file buf =
|
||||
let open Lexing in
|
||||
buf.lex_curr_p.pos_fname
|
||||
|
||||
let of_lexbuf lexbuf =
|
||||
let start = Lexing.lexeme_start_p lexbuf in
|
||||
let end_ = Lexing.lexeme_end_p lexbuf in
|
||||
let s_l = start.Lexing.pos_lnum in
|
||||
let s_c = start.Lexing.pos_cnum - start.Lexing.pos_bol in
|
||||
let e_l = end_.Lexing.pos_lnum in
|
||||
let e_c = end_.Lexing.pos_cnum - end_.Lexing.pos_bol in
|
||||
let file = get_file lexbuf in
|
||||
mk file s_l s_c e_l e_c
|
||||
|
|
@ -1,294 +0,0 @@
|
|||
|
||||
(* This file is free software. See file "license" for more details. *)
|
||||
|
||||
(** {1 Simple AST for parsing} *)
|
||||
|
||||
module Loc = Locations
|
||||
module Fmt = CCFormat
|
||||
|
||||
let pp_str = Format.pp_print_string
|
||||
|
||||
let pp_to_string pp x =
|
||||
let buf = Buffer.create 64 in
|
||||
let fmt = Format.formatter_of_buffer buf in
|
||||
pp fmt x;
|
||||
Format.pp_print_flush fmt ();
|
||||
Buffer.contents buf
|
||||
|
||||
type var = string
|
||||
type ty_var = string
|
||||
|
||||
(** Polymorphic types *)
|
||||
type ty =
|
||||
| Ty_bool
|
||||
| Ty_app of ty_var * ty list
|
||||
| Ty_arrow of ty list * ty
|
||||
|
||||
type typed_var = var * ty
|
||||
|
||||
type arith_op =
|
||||
| Leq
|
||||
| Lt
|
||||
| Geq
|
||||
| Gt
|
||||
| Add
|
||||
| Minus
|
||||
| Mult
|
||||
| Div
|
||||
|
||||
(** {2 AST: S-expressions with locations} *)
|
||||
type term =
|
||||
| True
|
||||
| False
|
||||
| Const of string
|
||||
| Arith of arith_op * term list
|
||||
| App of string * term list
|
||||
| HO_app of term * term (* higher-order application *)
|
||||
| Match of term * match_branch list
|
||||
| If of term * term * term
|
||||
| Let of (var * term) list * term
|
||||
| Fun of typed_var * term
|
||||
| Eq of term * term
|
||||
| Imply of term * term
|
||||
| And of term list
|
||||
| Or of term list
|
||||
| Not of term
|
||||
| Xor of term * term
|
||||
| Distinct of term list
|
||||
| Cast of term * ty (* type cast *)
|
||||
| Forall of (var * ty) list * term
|
||||
| Exists of (var * ty) list * term
|
||||
|
||||
and match_branch =
|
||||
| Match_default of term
|
||||
| Match_case of string * var list * term
|
||||
|
||||
type cstor = {
|
||||
cstor_name: string;
|
||||
cstor_args: (string * ty) list; (* selector+type *)
|
||||
}
|
||||
|
||||
type 'arg fun_decl = {
|
||||
fun_ty_vars: ty_var list;
|
||||
fun_name: string;
|
||||
fun_args: 'arg list;
|
||||
fun_ret: ty;
|
||||
}
|
||||
|
||||
type fun_def = {
|
||||
fr_decl: typed_var fun_decl;
|
||||
fr_body: term;
|
||||
}
|
||||
|
||||
type funs_rec_def = {
|
||||
fsr_decls: typed_var fun_decl list;
|
||||
fsr_bodies: term list;
|
||||
}
|
||||
|
||||
type statement = {
|
||||
stmt: stmt;
|
||||
loc: Loc.t option;
|
||||
}
|
||||
|
||||
and stmt =
|
||||
| Stmt_decl_sort of string * int (* arity *)
|
||||
| Stmt_decl of ty fun_decl
|
||||
| Stmt_fun_def of fun_def
|
||||
| Stmt_fun_rec of fun_def
|
||||
| Stmt_funs_rec of funs_rec_def
|
||||
| Stmt_data of ty_var list * (string * cstor list) list
|
||||
| Stmt_assert of term
|
||||
| Stmt_lemma of term
|
||||
| Stmt_assert_not of ty_var list * term
|
||||
| Stmt_set_logic of string
|
||||
| Stmt_set_option of string list
|
||||
| Stmt_set_info of string list
|
||||
| Stmt_check_sat
|
||||
| Stmt_exit
|
||||
|
||||
let ty_bool = Ty_bool
|
||||
let ty_app s l = Ty_app (s,l)
|
||||
let ty_const s = ty_app s []
|
||||
let ty_arrow_l args ret = if args=[] then ret else Ty_arrow (args, ret)
|
||||
let ty_arrow a b = ty_arrow_l [a] b
|
||||
|
||||
let true_ = True
|
||||
let false_ = False
|
||||
let const s = Const s
|
||||
let app f l = App (f,l)
|
||||
let ho_app a b = HO_app (a,b)
|
||||
let ho_app_l a l = List.fold_left ho_app a l
|
||||
let match_ u l = Match (u,l)
|
||||
let if_ a b c = If(a,b,c)
|
||||
let fun_ v t = Fun (v,t)
|
||||
let fun_l = List.fold_right fun_
|
||||
let let_ l t = Let (l,t)
|
||||
let eq a b = Eq (a,b)
|
||||
let imply a b = Imply(a,b)
|
||||
let xor a b = Xor (a,b)
|
||||
let and_ l = And l
|
||||
let or_ l = Or l
|
||||
let distinct l = Distinct l
|
||||
let cast t ~ty = Cast (t, ty)
|
||||
let forall vars f = match vars with [] -> f | _ -> Forall (vars, f)
|
||||
let exists vars f = match vars with [] -> f | _ -> Exists (vars, f)
|
||||
let rec not_ t = match t with
|
||||
| Forall (vars,u) -> exists vars (not_ u)
|
||||
| Exists (vars,u) -> forall vars (not_ u)
|
||||
| _ -> Not t
|
||||
|
||||
let arith op l = Arith (op,l)
|
||||
|
||||
let _mk ?loc stmt = { loc; stmt }
|
||||
|
||||
let mk_cstor name l : cstor = { cstor_name=name; cstor_args=l }
|
||||
let mk_fun_decl ~ty_vars f args ret =
|
||||
{ fun_ty_vars=ty_vars; fun_name=f;
|
||||
fun_args=args; fun_ret=ret; }
|
||||
let mk_fun_rec ~ty_vars f args ret body =
|
||||
{ fr_decl=mk_fun_decl ~ty_vars f args ret; fr_body=body; }
|
||||
|
||||
let decl_sort ?loc s ~arity = _mk ?loc (Stmt_decl_sort (s, arity))
|
||||
let decl_fun ?loc ~tyvars f ty_args ty_ret =
|
||||
let d = {fun_ty_vars=tyvars; fun_name=f; fun_args=ty_args; fun_ret=ty_ret} in
|
||||
_mk ?loc (Stmt_decl d)
|
||||
let fun_def ?loc fr = _mk ?loc (Stmt_fun_def fr)
|
||||
let fun_rec ?loc fr = _mk ?loc (Stmt_fun_rec fr)
|
||||
let funs_rec ?loc decls bodies = _mk ?loc (Stmt_funs_rec {fsr_decls=decls; fsr_bodies=bodies})
|
||||
let data ?loc tyvars l = _mk ?loc (Stmt_data (tyvars,l))
|
||||
let assert_ ?loc t = _mk ?loc (Stmt_assert t)
|
||||
let lemma ?loc t = _mk ?loc (Stmt_lemma t)
|
||||
let assert_not ?loc ~ty_vars t = _mk ?loc (Stmt_assert_not (ty_vars, t))
|
||||
let set_logic ?loc s = _mk ?loc (Stmt_set_logic s)
|
||||
let set_option ?loc l = _mk ?loc (Stmt_set_option l)
|
||||
let set_info ?loc l = _mk ?loc (Stmt_set_info l)
|
||||
let check_sat ?loc () = _mk ?loc Stmt_check_sat
|
||||
let exit ?loc () = _mk ?loc Stmt_exit
|
||||
|
||||
let loc t = t.loc
|
||||
let view t = t.stmt
|
||||
|
||||
let fpf = Format.fprintf
|
||||
|
||||
|
||||
let pp_tyvar = pp_str
|
||||
|
||||
let rec pp_ty out (ty:ty) = match ty with
|
||||
| Ty_bool -> pp_str out "Bool"
|
||||
| Ty_app (s,[]) -> pp_str out s
|
||||
| Ty_app (s,l) -> Format.fprintf out "(@[<hv1>%s@ %a@])" s (Util.pp_list pp_ty) l
|
||||
| Ty_arrow (args,ret) ->
|
||||
fpf out "(@[=>@ %a@ %a@])" (Util.pp_list pp_ty) args pp_ty ret
|
||||
|
||||
let pp_arith out = function
|
||||
| Leq -> Fmt.string out "<="
|
||||
| Lt -> Fmt.string out "<"
|
||||
| Geq -> Fmt.string out ">="
|
||||
| Gt -> Fmt.string out ">"
|
||||
| Add -> Fmt.string out "+"
|
||||
| Minus -> Fmt.string out "-"
|
||||
| Mult -> Fmt.string out "*"
|
||||
| Div -> Fmt.string out "/"
|
||||
|
||||
let rec pp_term out (t:term) = match t with
|
||||
| True -> pp_str out "true"
|
||||
| False -> pp_str out "false"
|
||||
| Arith (op,l) ->
|
||||
Fmt.fprintf out "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp_term) l
|
||||
| Const s -> pp_str out s
|
||||
| App (f,l) -> fpf out "(@[<1>%s@ %a@])" f (Util.pp_list pp_term) l
|
||||
| HO_app (a,b) -> fpf out "(@[<1>@@@ %a@ %a@])" pp_term a pp_term b
|
||||
| Match (lhs,cases) ->
|
||||
let pp_case out = function
|
||||
| Match_default rhs -> fpf out "(@[<1>case default@ %a@])" pp_term rhs
|
||||
| Match_case (c,[],rhs) ->
|
||||
fpf out "(@[<1>case %s@ %a@])" c pp_term rhs
|
||||
| Match_case (c,vars,rhs) ->
|
||||
fpf out "(@[<1>case@ (@[%s@ %a@])@ %a@])" c (Util.pp_list pp_str) vars pp_term rhs
|
||||
in
|
||||
fpf out "(@[<1>match@ %a@ @[<v>%a@]@])" pp_term lhs
|
||||
(Util.pp_list pp_case) cases
|
||||
| If (a,b,c) -> fpf out "(@[<hv1>ite %a@ %a@ %a@])" pp_term a pp_term b pp_term c
|
||||
| Fun (v,body) -> fpf out "(@[<1>lambda @ (%a)@ %a@])" pp_typed_var v pp_term body
|
||||
| Let (l,t) ->
|
||||
let pp_binding out (v,t) = fpf out "(@[%s@ %a@])" v pp_term t in
|
||||
fpf out "(@[let@ (@[%a@])@ %a@])" (Util.pp_list pp_binding) l pp_term t
|
||||
| Eq (a,b) -> fpf out "(@[=@ %a@ %a@])" pp_term a pp_term b
|
||||
| Imply (a,b) -> fpf out "(@[=>@ %a@ %a@])" pp_term a pp_term b
|
||||
| Xor(a,b) -> fpf out "(@[xor@ %a@ %a@])" pp_term a pp_term b
|
||||
| And l -> fpf out "(@[<hv>and@ %a@])" (Util.pp_list pp_term) l
|
||||
| Or l -> fpf out "(@[<hv>or@ %a@])" (Util.pp_list pp_term) l
|
||||
| Not t -> fpf out "(not %a)" pp_term t
|
||||
| Distinct l -> fpf out "(@[distinct@ %a@])" (Util.pp_list pp_term) l
|
||||
| Cast (t, ty) -> fpf out "(@[<hv1>as@ @[%a@]@ @[%a@]@])" pp_term t pp_ty ty
|
||||
| Forall (vars,f) ->
|
||||
fpf out "(@[<hv1>forall@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
|
||||
| Exists (vars,f) ->
|
||||
fpf out "(@[<hv1>exists@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
|
||||
and pp_typed_var out (v,ty) =
|
||||
fpf out "(@[%s@ %a@])" v pp_ty ty
|
||||
|
||||
let pp_par pp_x out (ty_vars,x) = match ty_vars with
|
||||
| [] -> pp_x out x
|
||||
| _ ->
|
||||
fpf out "(@[<1>par (@[%a@])@ (%a)@])" (Util.pp_list pp_tyvar) ty_vars pp_x x
|
||||
|
||||
let pp_fun_decl pp_arg out fd =
|
||||
fpf out "%s@ (@[%a@])@ %a"
|
||||
fd.fun_name (Util.pp_list pp_arg) fd.fun_args pp_ty fd.fun_ret
|
||||
|
||||
let pp_fr out fr =
|
||||
fpf out "@[<1>%a@ %a@]" (pp_fun_decl pp_typed_var) fr.fr_decl pp_term fr.fr_body
|
||||
|
||||
let pp_stmt out (st:statement) = match view st with
|
||||
| Stmt_set_logic s -> fpf out "(@[declare-logic@ %s@])" s
|
||||
| Stmt_set_option l -> fpf out "(@[set-option@ %a@])" (Util.pp_list CCFormat.string) l
|
||||
| Stmt_set_info l -> fpf out "(@[set-info@ %a@])" (Util.pp_list CCFormat.string) l
|
||||
| Stmt_decl_sort (s,n) -> fpf out "(@[declare-sort@ %s %d@])" s n
|
||||
| Stmt_assert t -> fpf out "(@[assert@ %a@])" pp_term t
|
||||
| Stmt_lemma t -> fpf out "(@[lemma@ %a@])" pp_term t
|
||||
| Stmt_assert_not (ty_vars,t) ->
|
||||
fpf out "(@[assert-not@ %a@])" (pp_par pp_term) (ty_vars,t)
|
||||
| Stmt_decl d ->
|
||||
fpf out "(@[declare-fun@ %a@])"
|
||||
(pp_par (pp_fun_decl pp_ty)) (d.fun_ty_vars,d)
|
||||
| Stmt_fun_def fr ->
|
||||
fpf out "(@[<1>define-fun@ %a@])"
|
||||
(pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
|
||||
| Stmt_fun_rec fr ->
|
||||
fpf out "(@[<1>define-fun-rec@ %a@])"
|
||||
(pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
|
||||
| Stmt_funs_rec fsr ->
|
||||
let pp_decl' out d = fpf out "(@[<1>%a@])" (pp_fun_decl pp_typed_var) d in
|
||||
fpf out "(@[<hv1>define-funs-rec@ (@[<v>%a@])@ (@[<v>%a@])@])"
|
||||
(Util.pp_list pp_decl') fsr.fsr_decls (Util.pp_list pp_term) fsr.fsr_bodies
|
||||
| Stmt_data (tyvars,l) ->
|
||||
let pp_cstor_arg out (sel,ty) = fpf out "(@[%s %a@])" sel pp_ty ty in
|
||||
let pp_cstor out c =
|
||||
if c.cstor_args = []
|
||||
then fpf out "(%s)" c.cstor_name
|
||||
else fpf out "(@[<1>%s@ %a@])" c.cstor_name (Util.pp_list pp_cstor_arg) c.cstor_args
|
||||
in
|
||||
let pp_data out (s,cstors) =
|
||||
fpf out "(@[<1>%s@ @[<v>%a@]@])" s (Util.pp_list pp_cstor) cstors
|
||||
in
|
||||
fpf out "(@[<hv1>declare-datatypes@ (@[%a@])@ (@[<v>%a@])@])"
|
||||
(Util.pp_list pp_tyvar) tyvars (Util.pp_list pp_data) l
|
||||
| Stmt_check_sat -> pp_str out "(check-sat)"
|
||||
| Stmt_exit -> pp_str out "(exit)"
|
||||
|
||||
(** {2 Errors} *)
|
||||
|
||||
exception Parse_error of Loc.t option * string
|
||||
|
||||
let () = Printexc.register_printer
|
||||
(function
|
||||
| Parse_error (loc, msg) ->
|
||||
let pp out () =
|
||||
Format.fprintf out "parse error at %a:@ %s" Loc.pp_opt loc msg
|
||||
in
|
||||
Some (pp_to_string pp ())
|
||||
| _ -> None)
|
||||
|
||||
let parse_error ?loc msg = raise (Parse_error (loc, msg))
|
||||
let parse_errorf ?loc msg = Format.ksprintf (parse_error ?loc) msg
|
||||
|
|
@ -1,377 +0,0 @@
|
|||
|
||||
|
||||
(* This file is free software, part of tip-parser. See file "license" for more details. *)
|
||||
|
||||
(** {1 Parser for TIP} *)
|
||||
|
||||
(* vim:SyntasticToggleMode:
|
||||
vim:set ft=yacc: *)
|
||||
|
||||
%{
|
||||
module A = Parse_ast
|
||||
module Loc = Locations
|
||||
|
||||
%}
|
||||
|
||||
%token EOI
|
||||
|
||||
%token LEFT_PAREN
|
||||
%token RIGHT_PAREN
|
||||
|
||||
%token PAR
|
||||
%token ARROW
|
||||
|
||||
%token TRUE
|
||||
%token FALSE
|
||||
%token OR
|
||||
%token AND
|
||||
%token XOR
|
||||
%token DISTINCT
|
||||
%token NOT
|
||||
%token EQ
|
||||
%token IF
|
||||
%token MATCH
|
||||
%token CASE
|
||||
%token DEFAULT
|
||||
%token FUN
|
||||
%token LET
|
||||
%token AS
|
||||
%token AT
|
||||
|
||||
%token LEQ
|
||||
%token LT
|
||||
%token GEQ
|
||||
%token GT
|
||||
%token ADD
|
||||
%token MINUS
|
||||
%token PROD
|
||||
%token DIV
|
||||
|
||||
%token SET_LOGIC
|
||||
%token SET_OPTION
|
||||
%token SET_INFO
|
||||
%token DATA
|
||||
%token ASSERT
|
||||
%token LEMMA
|
||||
%token ASSERT_NOT
|
||||
%token FORALL
|
||||
%token EXISTS
|
||||
%token DECLARE_SORT
|
||||
%token DECLARE_CONST
|
||||
%token DECLARE_FUN
|
||||
%token DEFINE_FUN
|
||||
%token DEFINE_FUN_REC
|
||||
%token DEFINE_FUNS_REC
|
||||
%token CHECK_SAT
|
||||
%token EXIT
|
||||
|
||||
%token <string>IDENT
|
||||
%token <string>QUOTED
|
||||
%token <string>ESCAPED
|
||||
|
||||
%start <Parse_ast.term> parse_term
|
||||
%start <Parse_ast.ty> parse_ty
|
||||
%start <Parse_ast.statement> parse
|
||||
%start <Parse_ast.statement list> parse_list
|
||||
|
||||
%%
|
||||
|
||||
parse_list: l=stmt* EOI {l}
|
||||
parse: t=stmt EOI { t }
|
||||
parse_term: t=term EOI { t }
|
||||
parse_ty: t=ty EOI { t }
|
||||
|
||||
cstor_arg:
|
||||
| LEFT_PAREN name=id ty=ty RIGHT_PAREN { name, ty }
|
||||
|
||||
cstor:
|
||||
| LEFT_PAREN c=id RIGHT_PAREN { A.mk_cstor c [] }
|
||||
| LEFT_PAREN c=id l=cstor_arg+ RIGHT_PAREN
|
||||
{ A.mk_cstor c l }
|
||||
|
||||
data:
|
||||
| LEFT_PAREN s=id l=cstor+ RIGHT_PAREN { s,l }
|
||||
|
||||
fun_def_mono:
|
||||
| f=id
|
||||
LEFT_PAREN args=typed_var* RIGHT_PAREN
|
||||
ret=ty
|
||||
{ f, args, ret }
|
||||
|
||||
fun_decl_mono:
|
||||
| f=id
|
||||
LEFT_PAREN args=ty* RIGHT_PAREN
|
||||
ret=ty
|
||||
{ f, args, ret }
|
||||
|
||||
fun_decl:
|
||||
| tup=fun_decl_mono { let f, args, ret = tup in [], f, args, ret }
|
||||
| LEFT_PAREN
|
||||
PAR
|
||||
LEFT_PAREN tyvars=tyvar* RIGHT_PAREN
|
||||
LEFT_PAREN tup=fun_decl_mono RIGHT_PAREN
|
||||
RIGHT_PAREN
|
||||
{ let f, args, ret = tup in tyvars, f, args, ret }
|
||||
|
||||
fun_rec:
|
||||
| tup=fun_def_mono body=term
|
||||
{
|
||||
let f, args, ret = tup in
|
||||
A.mk_fun_rec ~ty_vars:[] f args ret body
|
||||
}
|
||||
| LEFT_PAREN
|
||||
PAR
|
||||
LEFT_PAREN l=tyvar* RIGHT_PAREN
|
||||
LEFT_PAREN tup=fun_def_mono body=term RIGHT_PAREN
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let f, args, ret = tup in
|
||||
A.mk_fun_rec ~ty_vars:l f args ret body
|
||||
}
|
||||
|
||||
funs_rec_decl:
|
||||
| LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
|
||||
{
|
||||
let f, args, ret = tup in
|
||||
A.mk_fun_decl ~ty_vars:[] f args ret
|
||||
}
|
||||
| LEFT_PAREN
|
||||
PAR
|
||||
LEFT_PAREN l=tyvar* RIGHT_PAREN
|
||||
LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let f, args, ret = tup in
|
||||
A.mk_fun_decl ~ty_vars:l f args ret
|
||||
}
|
||||
|
||||
assert_not:
|
||||
| LEFT_PAREN
|
||||
PAR LEFT_PAREN tyvars=tyvar+ RIGHT_PAREN t=term
|
||||
RIGHT_PAREN
|
||||
{ tyvars, t }
|
||||
| t=term
|
||||
{ [], t }
|
||||
|
||||
id:
|
||||
| s=IDENT { s }
|
||||
| s=QUOTED { s }
|
||||
| s=ESCAPED { s }
|
||||
|
||||
stmt:
|
||||
| LEFT_PAREN SET_LOGIC s=id RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.set_logic ~loc s
|
||||
}
|
||||
| LEFT_PAREN SET_OPTION l=id+ RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.set_option ~loc l
|
||||
}
|
||||
| LEFT_PAREN SET_INFO l=id+ RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.set_info ~loc l
|
||||
}
|
||||
| LEFT_PAREN ASSERT t=term RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.assert_ ~loc t
|
||||
}
|
||||
| LEFT_PAREN LEMMA t=term RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.lemma ~loc t
|
||||
}
|
||||
| LEFT_PAREN DECLARE_SORT s=id n=id RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
try
|
||||
let n = int_of_string n in
|
||||
A.decl_sort ~loc s ~arity:n
|
||||
with Failure _ ->
|
||||
A.parse_errorf ~loc "expected arity to be an integer, not `%s`" n
|
||||
}
|
||||
| LEFT_PAREN DATA
|
||||
LEFT_PAREN vars=tyvar* RIGHT_PAREN
|
||||
LEFT_PAREN l=data+ RIGHT_PAREN
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.data ~loc vars l
|
||||
}
|
||||
| LEFT_PAREN DECLARE_FUN tup=fun_decl RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
let tyvars, f, args, ret = tup in
|
||||
A.decl_fun ~loc ~tyvars f args ret
|
||||
}
|
||||
| LEFT_PAREN DECLARE_CONST f=id ty=ty RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.decl_fun ~loc ~tyvars:[] f [] ty
|
||||
}
|
||||
| LEFT_PAREN DEFINE_FUN f=fun_rec RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.fun_def ~loc f
|
||||
}
|
||||
| LEFT_PAREN
|
||||
DEFINE_FUN_REC
|
||||
f=fun_rec
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.fun_rec ~loc f
|
||||
}
|
||||
| LEFT_PAREN
|
||||
DEFINE_FUNS_REC
|
||||
LEFT_PAREN decls=funs_rec_decl+ RIGHT_PAREN
|
||||
LEFT_PAREN bodies=term+ RIGHT_PAREN
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.funs_rec ~loc decls bodies
|
||||
}
|
||||
| LEFT_PAREN
|
||||
ASSERT_NOT
|
||||
tup=assert_not
|
||||
RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
let ty_vars, f = tup in
|
||||
A.assert_not ~loc ~ty_vars f
|
||||
}
|
||||
| LEFT_PAREN CHECK_SAT RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.check_sat ~loc ()
|
||||
}
|
||||
| LEFT_PAREN EXIT RIGHT_PAREN
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.exit ~loc ()
|
||||
}
|
||||
| error
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.parse_errorf ~loc "expected statement"
|
||||
}
|
||||
|
||||
var:
|
||||
| s=id { s }
|
||||
tyvar:
|
||||
| s=id { s }
|
||||
|
||||
ty:
|
||||
| s=id {
|
||||
begin match s with
|
||||
| "Bool" -> A.ty_bool
|
||||
| _ -> A.ty_const s
|
||||
end
|
||||
}
|
||||
| LEFT_PAREN s=id args=ty+ RIGHT_PAREN
|
||||
{ A.ty_app s args }
|
||||
| LEFT_PAREN ARROW tup=ty_arrow_args RIGHT_PAREN
|
||||
{
|
||||
let args, ret = tup in
|
||||
A.ty_arrow_l args ret }
|
||||
| error
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.parse_errorf ~loc "expected type"
|
||||
}
|
||||
|
||||
ty_arrow_args:
|
||||
| a=ty ret=ty { [a], ret }
|
||||
| a=ty tup=ty_arrow_args { a :: fst tup, snd tup }
|
||||
|
||||
typed_var:
|
||||
| LEFT_PAREN s=id ty=ty RIGHT_PAREN { s, ty }
|
||||
|
||||
case:
|
||||
| LEFT_PAREN
|
||||
CASE
|
||||
c=id
|
||||
rhs=term
|
||||
RIGHT_PAREN
|
||||
{ A.Match_case (c, [], rhs) }
|
||||
| LEFT_PAREN
|
||||
CASE
|
||||
LEFT_PAREN c=id vars=var+ RIGHT_PAREN
|
||||
rhs=term
|
||||
RIGHT_PAREN
|
||||
{ A.Match_case (c, vars, rhs) }
|
||||
| LEFT_PAREN
|
||||
CASE DEFAULT rhs=term
|
||||
RIGHT_PAREN
|
||||
{ A.Match_default rhs }
|
||||
|
||||
binding:
|
||||
| LEFT_PAREN v=var t=term RIGHT_PAREN { v, t }
|
||||
|
||||
term:
|
||||
| TRUE { A.true_ }
|
||||
| FALSE { A.false_ }
|
||||
| s=id { A.const s }
|
||||
| t=composite_term { t }
|
||||
| error
|
||||
{
|
||||
let loc = Loc.mk_pos $startpos $endpos in
|
||||
A.parse_errorf ~loc "expected term"
|
||||
}
|
||||
|
||||
%inline arith_op:
|
||||
| ADD { A.Add }
|
||||
| MINUS { A.Minus }
|
||||
| PROD { A.Mult }
|
||||
| DIV { A.Div }
|
||||
| LEQ { A.Leq }
|
||||
| LT { A.Lt }
|
||||
| GEQ { A.Geq }
|
||||
| GT { A.Gt }
|
||||
|
||||
composite_term:
|
||||
| LEFT_PAREN IF a=term b=term c=term RIGHT_PAREN { A.if_ a b c }
|
||||
| LEFT_PAREN OR l=term+ RIGHT_PAREN { A.or_ l }
|
||||
| LEFT_PAREN AND l=term+ RIGHT_PAREN { A.and_ l }
|
||||
| LEFT_PAREN NOT t=term RIGHT_PAREN { A.not_ t }
|
||||
| LEFT_PAREN DISTINCT l=term+ RIGHT_PAREN { A.distinct l }
|
||||
| LEFT_PAREN EQ a=term b=term RIGHT_PAREN { A.eq a b }
|
||||
| LEFT_PAREN ARROW a=term b=term RIGHT_PAREN { A.imply a b }
|
||||
| LEFT_PAREN XOR a=term b=term RIGHT_PAREN { A.xor a b }
|
||||
| LEFT_PAREN f=id args=term+ RIGHT_PAREN { A.app f args }
|
||||
| LEFT_PAREN o=arith_op args=term+ RIGHT_PAREN { A.arith o args }
|
||||
| LEFT_PAREN f=composite_term args=term+ RIGHT_PAREN { A.ho_app_l f args }
|
||||
| LEFT_PAREN AT f=term arg=term RIGHT_PAREN { A.ho_app f arg }
|
||||
| LEFT_PAREN
|
||||
MATCH
|
||||
lhs=term
|
||||
l=case+
|
||||
RIGHT_PAREN
|
||||
{ A.match_ lhs l }
|
||||
| LEFT_PAREN
|
||||
FUN
|
||||
LEFT_PAREN vars=typed_var+ RIGHT_PAREN
|
||||
body=term
|
||||
RIGHT_PAREN
|
||||
{ A.fun_l vars body }
|
||||
| LEFT_PAREN
|
||||
LET
|
||||
LEFT_PAREN l=binding+ RIGHT_PAREN
|
||||
r=term
|
||||
RIGHT_PAREN
|
||||
{ A.let_ l r }
|
||||
| LEFT_PAREN AS t=term ty=ty RIGHT_PAREN
|
||||
{ A.cast t ~ty }
|
||||
| LEFT_PAREN FORALL LEFT_PAREN vars=typed_var+ RIGHT_PAREN
|
||||
f=term
|
||||
RIGHT_PAREN
|
||||
{ A.forall vars f }
|
||||
| LEFT_PAREN EXISTS LEFT_PAREN vars=typed_var+ RIGHT_PAREN
|
||||
f=term
|
||||
RIGHT_PAREN
|
||||
{ A.exists vars f }
|
||||
|
||||
%%
|
||||
|
|
@ -4,7 +4,8 @@ module ID = Sidekick_base_term.ID
|
|||
module Fmt = CCFormat
|
||||
module Ast = Ast
|
||||
module E = CCResult
|
||||
module Loc = Locations
|
||||
module Loc = Smtlib_utils.Loc
|
||||
module Parse_ast = Smtlib_utils.Ast
|
||||
module Process = Process
|
||||
module Solver = Process.Solver
|
||||
|
||||
|
|
@ -19,7 +20,7 @@ module Parse = struct
|
|||
let parse_chan_exn ?(filename="<no name>") ic =
|
||||
let lexbuf = Lexing.from_channel ic in
|
||||
Loc.set_file lexbuf filename;
|
||||
Parser.parse_list Lexer.token lexbuf
|
||||
Smtlib_utils.Parser.parse_list Smtlib_utils.Lexer.token lexbuf
|
||||
|
||||
let parse_file_exn file : Parse_ast.statement list =
|
||||
CCIO.with_in file (parse_chan_exn ~filename:file)
|
||||
|
|
|
|||
|
|
@ -3,12 +3,12 @@
|
|||
(** {1 Preprocessing AST} *)
|
||||
|
||||
open Sidekick_base_term
|
||||
module Loc = Locations
|
||||
module Loc = Smtlib_utils.Loc
|
||||
module Fmt = CCFormat
|
||||
module Log = Msat.Log
|
||||
|
||||
module A = Ast
|
||||
module PA = Parse_ast
|
||||
module PA = Smtlib_utils.Ast
|
||||
|
||||
type 'a or_error = ('a, string) CCResult.t
|
||||
|
||||
|
|
@ -118,6 +118,7 @@ let find_id_ ctx (s:string): ID.t =
|
|||
(* parse a type *)
|
||||
let rec conv_ty ctx (t:PA.ty) : A.Ty.t * _ = match t with
|
||||
| PA.Ty_bool -> A.Ty.prop, Ctx.K_ty Ctx.K_bool
|
||||
| PA.Ty_real -> A.Ty.rat, Ctx.K_ty Ctx.K_other
|
||||
| PA.Ty_app ("Rat",[]) -> A.Ty.rat, Ctx.K_ty Ctx.K_other
|
||||
| PA.Ty_app ("Int",[]) -> A.Ty.int , Ctx.K_ty Ctx.K_other
|
||||
| PA.Ty_app (f, l) ->
|
||||
|
|
@ -211,10 +212,6 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
|
|||
let a = conv_term ctx a in
|
||||
let b = conv_term ctx b in
|
||||
A.imply a b
|
||||
| PA.Xor (a,b) ->
|
||||
let a = conv_term ctx a in
|
||||
let b = conv_term ctx b in
|
||||
A.or_ (A.and_ a (A.not_ b)) (A.and_ (A.not_ a) b)
|
||||
| PA.Match (lhs, l) ->
|
||||
(*
|
||||
errorf_ctx ctx "TODO: support match in %a" PA.pp_term t
|
||||
|
|
@ -363,7 +360,7 @@ let rec conv_statement ctx (s:PA.statement): A.statement list =
|
|||
and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.view stmt with
|
||||
| PA.Stmt_set_logic s -> [A.SetLogic s]
|
||||
| PA.Stmt_set_option l -> [A.SetOption l]
|
||||
| PA.Stmt_set_info l -> [A.SetInfo l]
|
||||
| PA.Stmt_set_info (a,b) -> [A.SetInfo [a;b]]
|
||||
| PA.Stmt_exit -> [A.Exit]
|
||||
| PA.Stmt_decl_sort (s,n) ->
|
||||
let id = Ctx.add_id ctx s (Ctx.K_ty Ctx.K_uninterpreted) in
|
||||
|
|
@ -442,14 +439,5 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie
|
|||
let t = conv_term ctx t in
|
||||
check_bool_ t;
|
||||
[A.Assert t]
|
||||
| PA.Stmt_assert_not ([], t) ->
|
||||
let vars, t = A.unfold_binder A.Forall (conv_term ctx t) in
|
||||
let g = A.not_ t in (* negate *)
|
||||
[A.Goal (vars, g)]
|
||||
| PA.Stmt_assert_not (_::_, _) ->
|
||||
errorf_ctx ctx "cannot convert polymorphic goal@ `@[%a@]`"
|
||||
PA.pp_stmt stmt
|
||||
| PA.Stmt_lemma _ ->
|
||||
errorf_ctx ctx "smbc does not know how to handle `lemma` statements"
|
||||
| PA.Stmt_check_sat -> [A.CheckSat]
|
||||
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
(** {1 Preprocessing AST} *)
|
||||
|
||||
module Loc = Locations
|
||||
module Loc = Smtlib_utils.Loc
|
||||
|
||||
type 'a or_error = ('a, string) CCResult.t
|
||||
|
||||
|
|
@ -14,7 +14,7 @@ module Ctx : sig
|
|||
val pp : t CCFormat.printer
|
||||
end
|
||||
|
||||
module PA = Parse_ast
|
||||
module PA = Smtlib_utils.Ast
|
||||
module A = Ast
|
||||
|
||||
val conv_term : Ctx.t -> PA.term -> A.term
|
||||
|
|
|
|||
|
|
@ -3,11 +3,5 @@
|
|||
(public_name sidekick-bin.smtlib)
|
||||
(libraries containers zarith msat sidekick.core sidekick.util
|
||||
sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
|
||||
sidekick.mini-cc msat.backend)
|
||||
sidekick.mini-cc msat.backend smtlib-utils)
|
||||
(flags :standard -open Sidekick_util))
|
||||
|
||||
(menhir
|
||||
(modules Parser))
|
||||
|
||||
(ocamllex
|
||||
(modules Lexer))
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue