diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 42b285a5..b6e06d4c 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -65,6 +65,7 @@ and ty_view = and ty_def = | Ty_uninterpreted of ID.t + | Ty_data of data | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; @@ -72,6 +73,18 @@ and ty_def = card: ty list -> ty_card; } +and data = { + data_id: ID.t; + data_cstors: (ty * select list) ID.Map.t; +} + +and select = { + select_name: ID.t lazy_t; + select_cstor: ID.t; + select_ty: ty lazy_t; + select_i: int; +} + and ty_card = | Finite | Infinite @@ -92,6 +105,20 @@ and value = and value_custom_view = .. +type definition = ID.t * ty * term + +type statement = + | Stmt_set_logic of string + | Stmt_set_option of string list + | Stmt_set_info of string * string + | Stmt_data of data list + | Stmt_ty_decl of ID.t * int (* new atomic cstor *) + | Stmt_decl of ID.t * ty list * ty + | Stmt_define of definition list + | Stmt_assert of term + | Stmt_check_sat + | Stmt_exit + let[@inline] term_equal_ (a:term) b = a==b let[@inline] term_hash_ a = a.term_id let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id @@ -130,6 +157,9 @@ let rec pp_ty out t = match t.ty_view with | Ty_atomic {def=Ty_uninterpreted id; args; _} -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args | Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args + | Ty_atomic {def=Ty_data d; args=[];_} -> ID.pp out d.data_id + | Ty_atomic {def=Ty_data d; args;_} -> + Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data_id (Util.pp_list pp_ty) args let pp_term_view_gen ~pp_id ~pp_t out = function | Bool true -> Fmt.string out "true" @@ -155,44 +185,58 @@ let pp_term = pp_term_top ~ids:false let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term module Ty_card : sig -type t = ty_card = Finite | Infinite + type t = ty_card = Finite | Infinite -val (+) : t -> t -> t -val ( * ) : t -> t -> t -val ( ^ ) : t -> t -> t -val finite : t -val infinite : t + val (+) : t -> t -> t + val ( * ) : t -> t -> t + val ( ^ ) : t -> t -> t + val finite : t + val infinite : t -val sum : t list -> t -val product : t list -> t + val sum : t list -> t + val product : t list -> t -val equal : t -> t -> bool -val compare : t -> t -> int -val pp : t CCFormat.printer - end = struct -type t = ty_card = Finite | Infinite + val equal : t -> t -> bool + val compare : t -> t -> int + val pp : t CCFormat.printer +end = struct + type t = ty_card = Finite | Infinite -let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite -let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite -let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite -let finite = Finite -let infinite = Infinite + let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let finite = Finite + let infinite = Infinite -let sum = List.fold_left (+) Finite -let product = List.fold_left ( * ) Finite + let sum = List.fold_left (+) Finite + let product = List.fold_left ( * ) Finite -let equal = (=) -let compare = Pervasives.compare -let pp out = function - | Finite -> CCFormat.string out "finite" - | Infinite -> CCFormat.string out "infinite" - - end + let equal = (=) + let compare = Pervasives.compare + let pp out = function + | Finite -> CCFormat.string out "finite" + | Infinite -> CCFormat.string out "infinite" +end module Ty : sig type t = ty - type view = ty_view - type def = ty_def + type view = ty_view = + | Ty_bool + | Ty_atomic of { + def: ty_def; + args: ty list; + card: ty_card lazy_t; + } + + type def = ty_def = + | Ty_uninterpreted of ID.t + | Ty_data of data + | Ty_def of { + id: ID.t; + pp: ty Fmt.printer -> ty list Fmt.printer; + default_val: value list -> value; (* default value of this type *) + card: ty list -> ty_card; + } val id : t -> int val view : t -> view @@ -228,8 +272,22 @@ module Ty : sig end end = struct type t = ty - type view = ty_view - type def = ty_def + type view = ty_view = + | Ty_bool + | Ty_atomic of { + def: ty_def; + args: ty list; + card: ty_card lazy_t; + } + type def = ty_def = + | Ty_uninterpreted of ID.t + | Ty_data of data + | Ty_def of { + id: ID.t; + pp: ty Fmt.printer -> ty list Fmt.printer; + default_val: value list -> value; (* default value of this type *) + card: ty list -> ty_card; + } let[@inline] id t = t.ty_id let[@inline] view t = t.ty_view @@ -241,7 +299,8 @@ end = struct let equal_def d1 d2 = match d1, d2 with | Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2 | Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id - | Ty_uninterpreted _, _ | Ty_def _, _ + | Ty_data d1, Ty_data d2 -> ID.equal d1.data_id d2.data_id + | (Ty_uninterpreted _ | Ty_def _ | Ty_data _), _ -> false module H = Hashcons.Make(struct @@ -259,6 +318,8 @@ end = struct Hash.combine3 10 (ID.hash id) (Hash.list hash args) | Ty_atomic {def=Ty_def d; args; _} -> Hash.combine3 20 (ID.hash d.id) (Hash.list hash args) + | Ty_atomic {def=Ty_data d; args; _} -> + Hash.combine3 30 (ID.hash d.data_id) (Hash.list hash args) let set_id ty id = assert (ty.ty_id < 0); @@ -284,6 +345,7 @@ end = struct | Ty_uninterpreted _ -> if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite | Ty_def d -> d.card args + | Ty_data _ -> assert false (* TODO *) ) in make_ (Ty_atomic {def; args; card}) @@ -335,6 +397,7 @@ module Fun : sig val do_cc : t -> bool val mk_undef : ID.t -> Ty.Fun.t -> t + val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t val mk_undef_const : ID.t -> Ty.t -> t val pp : t CCFormat.printer @@ -360,6 +423,7 @@ end = struct let[@inline] mk_undef id ty = make id (Fun_undef ty) let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty) + let[@inline] mk_undef' id args ret = mk_undef id {fun_ty_args=args; fun_ty_ret=ret} let[@inline] do_cc (c:t) : bool = match view c with | Fun_undef _ -> true @@ -809,7 +873,51 @@ end = struct mk_elt (ID.makef "v_%d" t.term_id) t.term_ty end +module Data = struct + type t = data = { + data_id: ID.t; + data_cstors: (ty * select list) ID.Map.t; + } +end + +module Select = struct + type t = select = { + select_name: ID.t lazy_t; + select_cstor: ID.t; + select_ty: ty lazy_t; + select_i: int; + } +end + module Proof = struct type t = Default let default = Default end + +module Statement = struct + type t = statement = + | Stmt_set_logic of string + | Stmt_set_option of string list + | Stmt_set_info of string * string + | Stmt_data of data list + | Stmt_ty_decl of ID.t * int (* new atomic cstor *) + | Stmt_decl of ID.t * ty list * ty + | Stmt_define of definition list + | Stmt_assert of term + | Stmt_check_sat + | Stmt_exit + + let pp out = function + | Stmt_set_logic s -> Fmt.fprintf out "(set-logic %s)" s + | Stmt_set_option l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l + | Stmt_set_info (a,b) -> Fmt.fprintf out "(@[set-info@ %s@ %s@])" a b + | Stmt_check_sat -> Fmt.string out "(check-sat)" + | Stmt_ty_decl (s,n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n + | Stmt_decl (id,args,ret) -> + Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])" + ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret + | Stmt_assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t + | Stmt_exit -> Fmt.string out "(exit)" + | Stmt_data _ -> assert false (* TODO *) + | Stmt_define _ -> assert false (* TODO *) +end diff --git a/src/base-term/Sidekick_base_term.ml b/src/base-term/Sidekick_base_term.ml index 256b8a59..cc936713 100644 --- a/src/base-term/Sidekick_base_term.ml +++ b/src/base-term/Sidekick_base_term.ml @@ -8,6 +8,9 @@ module Term = Base_types.Term module Value = Base_types.Value module Term_cell = Base_types.Term_cell module Ty = Base_types.Ty +module Statement = Base_types.Statement +module Data = Base_types.Data +module Select = Base_types.Select module Arg : Sidekick_core.TERM diff --git a/src/main/main.ml b/src/main/main.ml index de413e02..dca6875e 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -9,7 +9,6 @@ open CCResult.Infix module E = CCResult module Fmt = CCFormat module Term = Sidekick_base_term.Term -module Ast = Sidekick_smtlib.Ast module Solver = Sidekick_smtlib.Solver module Process = Sidekick_smtlib.Process module Vec = Msat.Vec @@ -33,7 +32,7 @@ let p_stat = ref false let p_gc_stat = ref false let p_progress = ref false -let hyps : Ast.term list ref = ref [] +let hyps : Term.t list ref = ref [] (* Arguments parsing *) let int_arg r arg = @@ -79,8 +78,9 @@ let argspec = Arg.align [ "--no-p", Arg.Clear p_progress, " no progress bar"; "--size", Arg.String (int_arg size_limit), " [kMGT] sets the size limit for the sat solver"; "--time", Arg.String (int_arg time_limit), " [smhd] sets the time limit for the sat solver"; - "-v", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; - ] + "-d", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; + "--debug", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; + ] |> List.sort compare (* Limits alarm *) let check_limits () = @@ -116,7 +116,7 @@ let main () = (* might have to check conflicts *) Solver.add_theory solver Process.Check_cc.theory; ); - Sidekick_smtlib.parse !file >>= fun input -> + Sidekick_smtlib.parse tst !file >>= fun input -> (* process statements *) let res = try diff --git a/src/smtlib/Ast.ml b/src/smtlib/Ast.ml deleted file mode 100644 index 46f44c56..00000000 --- a/src/smtlib/Ast.ml +++ /dev/null @@ -1,493 +0,0 @@ -(* This file is free software. See file "license" for more details. *) - -(** {1 Preprocessing AST} *) - -open Sidekick_base_term - -type 'a or_error = ('a, string) CCResult.t - -(** {2 Types} *) - -module Var = struct - type 'ty t = { - id: ID.t; - ty: 'ty; - } - - let make id ty = {id;ty} - let makef ~ty fmt = - CCFormat.ksprintf fmt ~f:(fun s -> make (ID.make s) ty) - let copy {id;ty} = {ty; id=ID.copy id} - let id v = v.id - let ty v = v.ty - - let equal a b = ID.equal a.id b.id - let compare a b = ID.compare a.id b.id - let pp out v = ID.pp out v.id -end - -module Ty = struct - type t = - | Prop - | App of ID.t * t list - | Arrow of t * t - - let prop = Prop - let app id l = App (id,l) - let const id = app id [] - let arrow a b = Arrow (a,b) - let arrow_l = List.fold_right arrow - - let int = const ID.B.int - let rat = const ID.B.rat - - let to_int_ = function - | Prop -> 0 - | App _ -> 1 - | Arrow _ -> 2 - - let () = CCOrd.() - - let rec compare a b = match a, b with - | Prop, Prop -> 0 - | App (a,la), App (b,lb) -> - CCOrd.(ID.compare a b (list compare, la, lb)) - | Arrow (a1,a2), Arrow (b1,b2) -> - compare a1 b1 (compare, a2,b2) - | Prop, _ - | App _, _ - | Arrow _, _ -> CCInt.compare (to_int_ a) (to_int_ b) - - let equal a b = compare a b = 0 - - let hash _ = 0 (* TODO *) - - let unfold ty = - let rec aux acc ty = match ty with - | Arrow (a,b) -> aux (a::acc) b - | _ -> List.rev acc, ty - in - aux [] ty - - let rec pp out = function - | Prop -> Fmt.string out "prop" - | App (id,[]) -> ID.pp out id - | App (id,l) -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp) l - | Arrow _ as ty -> - let args, ret = unfold ty in - Fmt.fprintf out "(@[-> %a@ %a@])" - (Util.pp_list ~sep:" " pp) args pp ret - - (** {2 Datatypes} *) - - type data = { - data_id: ID.t; - data_cstors: t ID.Map.t; - } - - module Map = CCMap.Make(struct - type _t = t - type t = _t - let compare = compare - end) - - let ill_typed fmt = - Error.errorf ("ill-typed: " ^^ fmt) -end - -type var = Ty.t Var.t - -type op = - | And - | Or - | Imply - | Eq - | Distinct - -type arith_op = - | Leq - | Lt - | Geq - | Gt - | Add - | Minus - | Mult - | Div - -type binder = - | Fun - | Forall - | Exists - | Mu - -type term = { - term: term_cell; - ty: Ty.t; -} -and term_cell = - | Var of var - | Const of ID.t - | Num_z of Z.t - | Num_q of Q.t - | App of term * term list - | If of term * term * term - | Match of term * (var list * term) ID.Map.t - | Select of select * term - | Bind of binder * var * term - | Arith of arith_op * term list - | Let of (var * term) list * term - | Not of term - | Op of op * term list - | Asserting of {t: term; guard: term} - | Undefined_value - | Bool of bool - -and select = { - select_name: ID.t lazy_t; - select_cstor: ID.t; - select_i: int; -} - - -type definition = ID.t * Ty.t * term - -type statement = - | SetLogic of string - | SetOption of string list - | SetInfo of string list - | Data of Ty.data list - | TyDecl of ID.t * int (* new atomic cstor *) - | Decl of ID.t * Ty.t - | Define of definition list - | Assert of term - | Goal of var list * term - | CheckSat - | Exit - -(** {2 Helpers} *) - -let is_true = function {term=Bool true;_} -> true | _ -> false -let is_false = function {term=Bool false;_} -> true | _ -> false - -let unfold_binder b t = - let rec aux acc t = match t.term with - | Bind (b', v, t') when b=b' -> aux (v::acc) t' - | _ -> List.rev acc, t - in - aux [] t - -let unfold_fun = unfold_binder Fun - -let pp_binder out = function - | Forall -> Fmt.string out "forall" - | Exists -> Fmt.string out "exists" - | Fun -> Fmt.string out "lambda" - | Mu -> Fmt.string out "mu" - -let pp_op out = function - | And -> Fmt.string out "and" - | Or -> Fmt.string out "or" - | Imply -> Fmt.string out "=>" - | Eq -> Fmt.string out "=" - | Distinct -> Fmt.string out "distinct" - -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 pp_term = - let rec pp out t = match t.term with - | Var v -> Var.pp out v - | Const id -> ID.pp out id - | App (f, l) -> Fmt.fprintf out "(@[%a@ %a@])" pp f (Util.pp_list pp) l - | If (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" pp a pp b pp c - | Match (u, m) -> - let pp_case out (id,(vars,rhs)) = - if vars=[] then Fmt.fprintf out "(@[<2>case %a@ %a@])" ID.pp id pp rhs - else Fmt.fprintf out "(@[<2>case (@[%a@ %a@])@ %a@])" - ID.pp id (Util.pp_list Var.pp) vars pp rhs - in - Fmt.fprintf out "(@[match %a@ %a@])" - pp u (Util.pp_list pp_case) (ID.Map.to_list m) - | Select (s, t) -> - Fmt.fprintf out "(@[select_%a_%d@ %a@])" - ID.pp s.select_cstor s.select_i pp t - | Bool b -> Fmt.fprintf out "%B" b - | Not t -> Fmt.fprintf out "(@[<1>not@ %a@])" pp t - | Op (o,l) -> Fmt.fprintf out "(@[%a@ %a@])" pp_op o (Util.pp_list pp) l - | Bind (b,v,u) -> - Fmt.fprintf out "(@[<1>%a ((@[%a@ %a@]))@ %a@])" - pp_binder b Var.pp v Ty.pp (Var.ty v) pp u - | Let (vbs,u) -> - Fmt.fprintf out "(@[<1>let (@[%a@])@ %a@])" pp_vbs vbs pp u - | Num_z z -> Z.pp_print out z - | Num_q z -> Q.pp_print out z - | Arith (op, l) -> - Fmt.fprintf out "(@[%a@ %a@])" pp_arith op (Util.pp_list pp) l - | Undefined_value -> Fmt.string out "" - | Asserting {t;guard} -> - Fmt.fprintf out "(@[asserting@ %a@ %a@])" pp t pp guard - - and pp_vbs out l = - let pp_vb out (v,t) = Fmt.fprintf out "(@[%a@ %a@])" Var.pp v pp t in - Util.pp_list pp_vb out l - in pp - -let pp_ty = Ty.pp - -(** {2 Constructors} *) - -let term_view t = t.term - -let rec app_ty_ ty l : Ty.t = match ty, l with - | _, [] -> ty - | Ty.Arrow (ty_a,ty_rest), a::tail -> - if Ty.equal ty_a a.ty - then app_ty_ ty_rest tail - else Ty.ill_typed "expected `@[%a@]`,@ got `@[%a : %a@]`" - Ty.pp ty_a pp_term a Ty.pp a.ty - | (Ty.Prop | Ty.App _), a::_ -> - Ty.ill_typed "cannot apply ty `@[%a@]`@ to `@[%a@]`" Ty.pp ty pp_term a - -let mk_ term ty = {term; ty} -let ty t = t.ty - -let true_ = mk_ (Bool true) Ty.prop -let false_ = mk_ (Bool false) Ty.prop -let undefined_value ty = mk_ Undefined_value ty - -let asserting t g = - if not (Ty.equal Ty.prop g.ty) then ( - Ty.ill_typed "asserting: test must have type prop, not `@[%a@]`" Ty.pp g.ty; - ); - mk_ (Asserting {t;guard=g}) t.ty - -let var v = mk_ (Var v) (Var.ty v) -let const id ty = mk_ (Const id) ty - -let app f l = match f.term, l with - | _, [] -> f - | App (f1, l1), _ -> - let ty = app_ty_ f.ty l in - mk_ (App (f1, l1 @ l)) ty - | _ -> - let ty = app_ty_ f.ty l in - mk_ (App (f, l)) ty - -let app_a f a = app f (Array.to_list a) - -let if_ a b c = - if a.ty <> Ty.Prop - then Ty.ill_typed "if: test must have type prop, not `@[%a@]`" Ty.pp a.ty; - if not (Ty.equal b.ty c.ty) - then Ty.ill_typed - "if: both branches must have same type,@ not `@[%a@]` and `@[%a@]`" - Ty.pp b.ty Ty.pp c.ty; - mk_ (If (a,b,c)) b.ty - -let match_ t m = - let c1, (_, rhs1) = ID.Map.choose m in - ID.Map.iter - (fun c (_, rhs) -> - if not (Ty.equal rhs1.ty rhs.ty) - then Ty.ill_typed - "match: cases %a and %a disagree on return type,@ \ - between %a and %a" - ID.pp c1 ID.pp c Ty.pp rhs1.ty Ty.pp rhs.ty) - m; - mk_ (Match (t,m)) rhs1.ty - -let let_l vbs t = match vbs with - | [] -> t - | _::_ -> - List.iter - (fun (v,t) -> - if not (Ty.equal (Var.ty v) t.ty) then ( - Ty.ill_typed - "let: variable %a : @[%a@]@ and bounded term : %a@ should have same type" - Var.pp v Ty.pp (Var.ty v) Ty.pp t.ty; - );) - vbs; - mk_ (Let (vbs,t)) t.ty - -let let_ v t u = let_l [v,t] u - -let bind ~ty b v t = mk_ (Bind(b,v,t)) ty - -let select ~ty (s:select) (t:term) = mk_ (Select (s,t)) ty - -let fun_ v t = - let ty = Ty.arrow (Var.ty v) t.ty in - mk_ (Bind (Fun,v,t)) ty - -let quant_ q v t = - if not (Ty.equal t.ty Ty.prop) then ( - Ty.ill_typed - "quantifier: bounded term : %a@ should have type prop" - Ty.pp t.ty; - ); - let ty = Ty.prop in - mk_ (q v t) ty - -let forall = quant_ (fun v t -> Bind (Forall,v,t)) -let exists = quant_ (fun v t -> Bind (Exists,v,t)) - -let mu v t = - if not (Ty.equal (Var.ty v) t.ty) - then Ty.ill_typed "mu-term: var has type %a,@ body %a" - Ty.pp (Var.ty v) Ty.pp t.ty; - let ty = Ty.arrow (Var.ty v) t.ty in - mk_ (Bind (Fun,v,t)) ty - -let fun_l = List.fold_right fun_ -let fun_a = Array.fold_right fun_ -let forall_l = List.fold_right forall -let exists_l = List.fold_right exists - -let eq a b = - if not (Ty.equal a.ty b.ty) - then Ty.ill_typed "eq: `@[%a@]` and `@[%a@]` do not have the same type" - pp_term a pp_term b; - mk_ (Op (Eq,[a;b])) Ty.prop - -let check_prop_ t = - if not (Ty.equal t.ty Ty.prop) then ( - Ty.ill_typed "expected prop, got `@[%a : %a@]`" pp_term t Ty.pp t.ty - ) - -let op op l = mk_ (Op (op, l)) Ty.prop -let binop_prop o a b = - check_prop_ a; check_prop_ b; - op o [a;b] - -let and_ = binop_prop And -let or_ = binop_prop Or -let imply = binop_prop Imply - -let and_l = function - | [] -> true_ - | [f] -> f - | l -> op And l - -let or_l = function - | [] -> false_ - | [f] -> f - | l -> op Or l - -let not_ t = - check_prop_ t; - mk_ (Not t) Ty.prop - -let arith ty op l = mk_ (Arith (op,l)) ty - -let num_q ty z = mk_ (Num_q z) ty -let num_z ty z = mk_ (Num_z z) ty - -let parse_num ~where (s:string) : [`Q of Q.t | `Z of Z.t] = - let fail() = - Error.errorf "%sexpected number, got `%s`" (Lazy.force where) s - in - begin match Z.of_string s with - | n -> `Z n - | exception _ -> - begin match Q.of_string s with - | n -> `Q n - | exception _ -> - if String.contains s '.' then ( - let p1, p2 = CCString.Split.left_exn ~by:"." s in - let n1, n2 = - try Z.of_string p1, Z.of_string p2 - with _ -> fail() - in - let factor_10 = Z.pow (Z.of_int 10) (String.length p2) in - (* [(p1·10^{length p2}+p2) / 10^{length p2}] *) - let n = - Q.div - (Q.of_bigint (Z.add n2 (Z.mul n1 factor_10))) - (Q.of_bigint factor_10) - in - `Q n - ) else fail() - end - end - -let num_str ty s = - begin match parse_num ~where:(Lazy.from_val "") s with - | `Q x -> num_q ty x - | `Z x -> num_z ty x - end - -(** {2 More IO} *) - -let pp_statement out = function - | SetLogic s -> Fmt.fprintf out "(set-logic %s)" s - | SetOption l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l - | SetInfo l -> Fmt.fprintf out "(@[set-info@ %a@])" (Util.pp_list Fmt.string) l - | CheckSat -> Fmt.string out "(check-sat)" - | TyDecl (s,n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n - | Decl (id,ty) -> - let args, ret = Ty.unfold ty in - Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])" - ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret - | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t - | Goal (vars,g) -> - Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g)) - | Exit -> Fmt.string out "(exit)" - | Data _ -> assert false (* TODO *) - | Define _ -> assert false (* TODO *) - -(** {2 Environment} *) - -type env_entry = - | E_uninterpreted_ty - | E_uninterpreted_cst (* domain element *) - | E_const of Ty.t - | E_data of Ty.t ID.Map.t (* list of cstors *) - | E_cstor of Ty.t (* datatype it belongs to *) - | E_defined of Ty.t * term (* if defined *) - -type env = { - defs: env_entry ID.Map.t; -} -(** Environment with definitions and goals *) - -let env_empty = { - defs=ID.Map.empty; -} - -let add_def id def env = { defs=ID.Map.add id def env.defs} - -let env_add_statement env st = - match st with - | Data l -> - List.fold_left - (fun env {Ty.data_id; data_cstors} -> - let map = add_def data_id (E_data data_cstors) env in - ID.Map.fold - (fun c_id c_ty map -> add_def c_id (E_cstor c_ty) map) - data_cstors map) - env l - | TyDecl (id,_) -> add_def id E_uninterpreted_ty env - | Decl (id,ty) -> add_def id (E_const ty) env - | Define l -> - List.fold_left - (fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map) - env l - | Goal _ | Assert _ | CheckSat | Exit - | SetLogic _ | SetOption _ | SetInfo _ - -> env - -let env_of_statements seq = - Iter.fold env_add_statement env_empty seq - -let env_find_def env id = - try Some (ID.Map.find id env.defs) - with Not_found -> None - -let env_add_def env id def = add_def id def env diff --git a/src/smtlib/Ast.mli b/src/smtlib/Ast.mli deleted file mode 100644 index e2574826..00000000 --- a/src/smtlib/Ast.mli +++ /dev/null @@ -1,216 +0,0 @@ -(* This file is free software. See file "license" for more details. *) - -(** {1 Preprocessing AST} *) - -open Sidekick_base_term - -type 'a or_error = ('a, string) CCResult.t - -(** {2 Types} *) - -module Var : sig - type 'ty t = private { - id: ID.t; - ty: 'ty; - } - - val make : ID.t -> 'ty -> 'ty t - val makef : ty:'a -> ('b, Format.formatter, unit, 'a t) format4 -> 'b - val copy : 'a t -> 'a t - val id : _ t -> ID.t - val ty : 'a t -> 'a - - val equal : 'a t -> 'a t -> bool - val compare : 'a t -> 'a t -> int - val pp : _ t CCFormat.printer -end - -module Ty : sig - type t = - | Prop - | App of ID.t * t list - | Arrow of t * t - - val prop : t - val const : ID.t -> t - val app : ID.t -> t list -> t - val arrow : t -> t -> t - val arrow_l : t list -> t -> t - - val rat : t - val int : t - - include Intf.EQ with type t := t - include Intf.ORD with type t := t - include Intf.HASH with type t := t - include Intf.PRINT with type t := t - - val unfold : t -> t list * t - (** [unfold ty] will get the list of arguments, and the return type - of any function. An atomic type is just a function with no arguments *) - - (** {2 Datatypes} *) - - (** Mutually recursive datatypes *) - type data = { - data_id: ID.t; - data_cstors: t ID.Map.t; - } - - module Map : CCMap.S with type key = t - - (** {2 Error Handling} *) - - val ill_typed : ('a, Format.formatter, unit, 'b) format4 -> 'a -end - -type var = Ty.t Var.t - -type op = - | And - | Or - | Imply - | Eq - | Distinct - -type arith_op = - | Leq - | Lt - | Geq - | Gt - | Add - | Minus - | Mult - | Div - -type binder = - | Fun - | Forall - | Exists - | Mu - -type term = private { - term: term_cell; - ty: Ty.t; -} -and term_cell = - | Var of var - | Const of ID.t - | Num_z of Z.t - | Num_q of Q.t - | App of term * term list - | If of term * term * term - | Match of term * (var list * term) ID.Map.t - | Select of select * term - | Bind of binder * var * term - | Arith of arith_op * term list - | Let of (var * term) list * term - | Not of term - | Op of op * term list - | Asserting of {t: term; guard: term} - | Undefined_value - | Bool of bool - -and select = { - select_name: ID.t lazy_t; - select_cstor: ID.t; - select_i: int; -} - -(* TODO: records? *) - -type definition = ID.t * Ty.t * term - -type statement = - | SetLogic of string - | SetOption of string list - | SetInfo of string list - | Data of Ty.data list - | TyDecl of ID.t * int (* new atomic cstor *) - | Decl of ID.t * Ty.t - | Define of definition list - | Assert of term - | Goal of var list * term - | CheckSat - | Exit - -(** {2 Constructors} *) - -val term_view : term -> term_cell -val ty : term -> Ty.t - -val var : var -> term -val const : ID.t -> Ty.t -> term -val app : term -> term list -> term -val app_a : term -> term array -> term -val if_ : term -> term -> term -> term -val match_ : term -> (var list * term) ID.Map.t -> term -val let_ : var -> term -> term -> term -val let_l : (var * term) list -> term -> term -val bind : ty:Ty.t -> binder -> var -> term -> term -val select : ty:Ty.t -> select -> term -> term -val fun_ : var -> term -> term -val fun_l : var list -> term -> term -val fun_a : var array -> term -> term -val forall : var -> term -> term -val forall_l : var list -> term -> term -val exists : var -> term -> term -val exists_l : var list -> term -> term -val mu : var -> term -> term -val eq : term -> term -> term -val not_ : term -> term -val op : op -> term list -> term -val and_ : term -> term -> term -val and_l : term list -> term -val or_ : term -> term -> term -val or_l : term list -> term -val imply : term -> term -> term -val true_ : term -val false_ : term -val undefined_value : Ty.t -> term -val asserting : term -> term -> term -val num_z : Ty.t -> Z.t -> term -val num_q : Ty.t -> Q.t -> term -val num_str : Ty.t -> string -> term (** parses int + {!num} *) - -val arith : Ty.t -> arith_op -> term list -> term - -(** {2 helpers} *) - -val is_true : term -> bool -val is_false : term -> bool - -val unfold_binder : binder -> term -> var list * term -val unfold_fun : term -> var list * term - -(** {2 Printing} *) - -val pp_ty : Ty.t CCFormat.printer -val pp_term : term CCFormat.printer -val pp_statement : statement CCFormat.printer - -(** {2 Environment} *) - -type env_entry = - | E_uninterpreted_ty - | E_uninterpreted_cst (* domain element *) - | E_const of Ty.t - | E_data of Ty.t ID.Map.t (* list of cstors *) - | E_cstor of Ty.t - | E_defined of Ty.t * term (* if defined *) - -type env = { - defs: env_entry ID.Map.t; -} -(** Environment with definitions and goals *) - -val env_empty : env - -val env_add_statement : env -> statement -> env - -val env_of_statements: statement Iter.t -> env - -val env_find_def : env -> ID.t -> env_entry option - -val env_add_def : env -> ID.t -> env_entry -> env - diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml new file mode 100644 index 00000000..e819171d --- /dev/null +++ b/src/smtlib/Form.ml @@ -0,0 +1,180 @@ +open Sidekick_base_term + +module T = Term +open Sidekick_th_bool_static +exception Not_a_th_term + +let id_and = ID.make "and" +let id_or = ID.make "or" +let id_imply = ID.make "=>" +let id_ite = ID.make "ite" + +let view_id fid args = + if ID.equal fid id_and then ( + B_and args + ) else if ID.equal fid id_or then ( + B_or args + ) else if ID.equal fid id_imply && IArray.length args >= 2 then ( + (* conclusion is stored first *) + let len = IArray.length args in + B_imply (IArray.sub args 1 (len-1), IArray.get args 0) + ) else if ID.equal fid id_ite && IArray.length args = 3 then ( + B_ite (IArray.get args 0, IArray.get args 1, IArray.get args 2) + ) else ( + raise_notrace Not_a_th_term + ) + +let view_as_bool (t:T.t) : T.t bool_view = + match T.view t with + | Bool b -> B_bool b + | Not u -> B_not u + | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b) + | App_fun ({fun_id; _}, args) -> + (try view_id fun_id args with Not_a_th_term -> B_atom t) + | _ -> B_atom t + +module Funs = struct + let get_ty id args = + if ID.equal id id_ite then T.ty (IArray.get args 1) + else Ty.bool + + let abs ~self _a = + match T.view self with + | Not u -> u, false + | _ -> self, true + + (* no congruence closure for boolean terms *) + let relevant _id _ _ = false + + let eval id args = + let open Value in + match view_id id args with + | B_bool b -> Value.bool b + | B_not (V_bool b) -> Value.bool (not b) + | B_and a when IArray.for_all Value.is_true a -> Value.true_ + | B_and a when IArray.exists Value.is_false a -> Value.false_ + | B_or a when IArray.exists Value.is_true a -> Value.true_ + | B_or a when IArray.for_all Value.is_false a -> Value.false_ + | B_imply (_, V_bool true) -> Value.true_ + | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ + | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ + | B_ite(a,b,c) -> + if Value.is_true a then b + else if Value.is_false a then c + else Error.errorf "non boolean value %a in ite" Value.pp a + | B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b) + | B_atom v -> v + | B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t + | B_not _ | B_and _ | B_or _ | B_imply _ + -> Error.errorf "non boolean value in boolean connective" + + let mk_fun ?(do_cc=false) id : Fun.t = + {fun_id=id; + fun_view=Fun_def { + pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; } + + let and_ = mk_fun id_and + let or_ = mk_fun id_or + let imply = mk_fun id_imply + let ite = mk_fun id_ite +end + +let as_id id (t:T.t) : T.t IArray.t option = + match T.view t with + | App_fun ({fun_id; _}, args) when ID.equal id fun_id -> Some args + | _ -> None + +(* flatten terms of the given ID *) +let flatten_id op sign (l:T.t list) : T.t list = + CCList.flat_map + (fun t -> match as_id op t with + | Some args -> IArray.to_list args + | None when (sign && T.is_true t) || (not sign && T.is_false t) -> + [] (* idempotent *) + | None -> [t]) + l + +let and_l st l = + match flatten_id id_and true l with + | [] -> T.true_ st + | l when List.exists T.is_false l -> T.false_ st + | [x] -> x + | args -> T.app_fun st Funs.and_ (IArray.of_list args) + +let or_l st l = + match flatten_id id_or false l with + | [] -> T.false_ st + | l when List.exists T.is_true l -> T.true_ st + | [x] -> x + | args -> T.app_fun st Funs.or_ (IArray.of_list args) + +let and_ st a b = and_l st [a;b] +let or_ st a b = or_l st [a;b] +let and_a st a = and_l st (IArray.to_list a) +let or_a st a = or_l st (IArray.to_list a) +let eq = T.eq +let not_ = T.not_ + +let ite st a b c = match T.view a with + | T.Bool ba -> if ba then b else c + | _ -> T.app_fun st Funs.ite (IArray.of_array_unsafe [| a;b;c |]) + +let equiv st a b = + if T.equal a b then T.true_ st + else if T.is_true a then b + else if T.is_true b then a + else if T.is_false a then not_ st b + else if T.is_false b then not_ st a + else T.eq st a b + +let neq st a b = not_ st @@ eq st a b + +let imply_a st xs y = + if IArray.is_empty xs then y + else T.app_fun st Funs.imply (IArray.append (IArray.singleton y) xs) + +let imply_l st xs y = match xs with + | [] -> y + | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs) + +let imply st a b = imply_a st (IArray.singleton a) b + +let distinct_l tst l = + match l with + | [] | [_] -> T.true_ tst + | l -> + (* turn into [and_{i List.map (fun (a,b) -> neq tst a b) + in + and_l tst cs + +let mk_bool st = function + | B_bool b -> T.bool st b + | B_atom t -> t + | B_and l -> and_a st l + | B_or l -> or_a st l + | B_imply (a,b) -> imply_a st a b + | B_ite (a,b,c) -> ite st a b c + | B_equiv (a,b) -> equiv st a b + | B_eq (a,b) -> T.eq st a b + | B_not t -> not_ st t + | B_opaque_bool t -> t + +module Gensym = struct + type t = { + tst: T.state; + mutable fresh: int; + } + + let create tst : t = {tst; fresh=0} + + let fresh_term (self:t) ~pre (ty:Ty.t) : T.t = + let name = Printf.sprintf "_tseitin_%s%d" pre self.fresh in + self.fresh <- 1 + self.fresh; + let id = ID.make name in + T.const self.tst @@ Fun.mk_undef_const id ty +end + +(* NOTE: no plugin produces new boolean formulas *) +let check_congruence_classes = false diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index b38e3a6a..da8fe397 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -7,396 +7,8 @@ open Sidekick_base_term type 'a or_error = ('a, string) CCResult.t module E = CCResult -module A = Ast module Fmt = CCFormat -module Form = struct - module T = Term - open Sidekick_th_bool_static - exception Not_a_th_term - - let id_and = ID.make "and" - let id_or = ID.make "or" - let id_imply = ID.make "=>" - let id_ite = ID.make "ite" - - let view_id fid args = - if ID.equal fid id_and then ( - B_and args - ) else if ID.equal fid id_or then ( - B_or args - ) else if ID.equal fid id_imply && IArray.length args >= 2 then ( - (* conclusion is stored first *) - let len = IArray.length args in - B_imply (IArray.sub args 1 (len-1), IArray.get args 0) - ) else if ID.equal fid id_ite && IArray.length args = 3 then ( - B_ite (IArray.get args 0, IArray.get args 1, IArray.get args 2) - ) else ( - raise_notrace Not_a_th_term - ) - - let view_as_bool (t:T.t) : T.t bool_view = - match T.view t with - | Bool b -> B_bool b - | Not u -> B_not u - | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b) - | App_fun ({fun_id; _}, args) -> - (try view_id fun_id args with Not_a_th_term -> B_atom t) - | _ -> B_atom t - - module Funs = struct - let get_ty id args = - if ID.equal id id_ite then T.ty (IArray.get args 1) - else Ty.bool - - let abs ~self _a = - match T.view self with - | Not u -> u, false - | _ -> self, true - - (* no congruence closure for boolean terms *) - let relevant _id _ _ = false - - let eval id args = - let open Value in - match view_id id args with - | B_bool b -> Value.bool b - | B_not (V_bool b) -> Value.bool (not b) - | B_and a when IArray.for_all Value.is_true a -> Value.true_ - | B_and a when IArray.exists Value.is_false a -> Value.false_ - | B_or a when IArray.exists Value.is_true a -> Value.true_ - | B_or a when IArray.for_all Value.is_false a -> Value.false_ - | B_imply (_, V_bool true) -> Value.true_ - | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ - | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ - | B_ite(a,b,c) -> - if Value.is_true a then b - else if Value.is_false a then c - else Error.errorf "non boolean value %a in ite" Value.pp a - | B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b) - | B_atom v -> v - | B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t - | B_not _ | B_and _ | B_or _ | B_imply _ - -> Error.errorf "non boolean value in boolean connective" - - let mk_fun ?(do_cc=false) id : Fun.t = - {fun_id=id; - fun_view=Fun_def { - pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; } - - let and_ = mk_fun id_and - let or_ = mk_fun id_or - let imply = mk_fun id_imply - let ite = mk_fun id_ite - end - - let as_id id (t:T.t) : T.t IArray.t option = - match T.view t with - | App_fun ({fun_id; _}, args) when ID.equal id fun_id -> Some args - | _ -> None - - (* flatten terms of the given ID *) - let flatten_id op sign (l:T.t list) : T.t list = - CCList.flat_map - (fun t -> match as_id op t with - | Some args -> IArray.to_list args - | None when (sign && T.is_true t) || (not sign && T.is_false t) -> - [] (* idempotent *) - | None -> [t]) - l - - let and_l st l = - match flatten_id id_and true l with - | [] -> T.true_ st - | l when List.exists T.is_false l -> T.false_ st - | [x] -> x - | args -> T.app_fun st Funs.and_ (IArray.of_list args) - - let or_l st l = - match flatten_id id_or false l with - | [] -> T.false_ st - | l when List.exists T.is_true l -> T.true_ st - | [x] -> x - | args -> T.app_fun st Funs.or_ (IArray.of_list args) - - let and_ st a b = and_l st [a;b] - let or_ st a b = or_l st [a;b] - let and_a st a = and_l st (IArray.to_list a) - let or_a st a = or_l st (IArray.to_list a) - let eq = T.eq - let not_ = T.not_ - - let ite st a b c = match T.view a with - | T.Bool ba -> if ba then b else c - | _ -> T.app_fun st Funs.ite (IArray.of_array_unsafe [| a;b;c |]) - - let equiv st a b = - if T.equal a b then T.true_ st - else if T.is_true a then b - else if T.is_true b then a - else if T.is_false a then not_ st b - else if T.is_false b then not_ st a - else T.eq st a b - - let neq st a b = not_ st @@ eq st a b - - let imply_a st xs y = - if IArray.is_empty xs then y - else T.app_fun st Funs.imply (IArray.append (IArray.singleton y) xs) - - let imply_l st xs y = match xs with - | [] -> y - | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs) - - let imply st a b = imply_a st (IArray.singleton a) b - - let distinct_l tst l = - match l with - | [] | [_] -> T.true_ tst - | l -> - (* turn into [and_{i List.map (fun (a,b) -> neq tst a b) - in - and_l tst cs - - let mk_bool st = function - | B_bool b -> T.bool st b - | B_atom t -> t - | B_and l -> and_a st l - | B_or l -> or_a st l - | B_imply (a,b) -> imply_a st a b - | B_ite (a,b,c) -> ite st a b c - | B_equiv (a,b) -> equiv st a b - | B_eq (a,b) -> T.eq st a b - | B_not t -> not_ st t - | B_opaque_bool t -> t - - module Gensym = struct - type t = { - tst: T.state; - mutable fresh: int; - } - - let create tst : t = {tst; fresh=0} - - let fresh_term (self:t) ~pre (ty:Ty.t) : T.t = - let name = Printf.sprintf "_tseitin_%s%d" pre self.fresh in - self.fresh <- 1 + self.fresh; - let id = ID.make name in - T.const self.tst @@ Fun.mk_undef_const id ty - end - - (* NOTE: no plugin produces new boolean formulas *) - let check_congruence_classes = false -end - -module Subst = struct - type 'a t = 'a ID.Map.t - let empty = ID.Map.empty - let mem subst v = ID.Map.mem (A.Var.id v) subst - let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out - let add subst v t = - if mem subst v then ( - Error.errorf "%a already bound" A.Var.pp v; - ); - ID.Map.add (A.Var.id v) t subst - let find subst v = ID.Map.get (A.Var.id v) subst - let find_exn subst v = ID.Map.find (A.Var.id v) subst -end - -module Conv = struct - let conv_ty (ty:A.Ty.t) : Ty.t = - let mk_ty id = Ty.atomic_uninterpreted id in - (* convert a type *) - let aux_ty (ty:A.Ty.t) : Ty.t = match ty with - | A.Ty.Prop -> Ty.bool - (* | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat *) - | A.Ty.App (id, []) -> mk_ty id - | A.Ty.App (_, _) -> - Error.errorf "cannot convert parametrized type %a" A.Ty.pp ty - | A.Ty.Arrow _ -> - Error.errorf "cannot convert arrow type `%a`" A.Ty.pp ty - in - aux_ty ty - - let conv_fun_ty (ty:A.Ty.t) : Ty.Fun.t = - let rec aux args ty = - match ty with - | A.Ty.Arrow (a,b) -> - aux (conv_ty a :: args) b - | _ -> Ty.Fun.mk (List.rev args) (conv_ty ty) - in - aux [] ty - - let conv_term (tst:Term.state) (t:A.term): Term.t = - (* polymorphic equality *) - let mk_eq t u = Term.eq tst t u in - let mk_app f l = Term.app_fun tst f (IArray.of_list l) in - let mk_const = Term.const tst in - (* - let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in - let mk_lra_eq t u = mk_lra_pred Mc2_lra.Eq0 (RLE.diff t u) |> Term.Bool.pa in - let side_clauses : atom list list ref = ref [] in - (* introduce intermediate variable for LRA sub-expression *) - let mk_lra_expr (e:RLE.t): term = match RLE.as_const e, RLE.as_singleton e with - | Some n, _ -> Reg.find_exn reg Mc2_lra.k_make_const n - | None, Some (n,t) when Q.equal n Q.one -> t - | _ -> - let id = mk_lra_id() in - Log.debugf 30 - (fun k->k"(@[smtlib.name_lra@ %a@ :as %a@])" RLE.pp e ID.pp id); - decl id [] (Reg.find_exn reg Mc2_lra.k_rat); - let t = mk_const id in - side_clauses := [mk_lra_eq (RLE.singleton1 t) e] :: !side_clauses; - t - in - (* adaptative equality *) - let mk_eq_t_tf (t:term) (u:term_or_form) : F.t = match u with - | F u -> F.equiv (F.atom (Term.Bool.pa t)) u - | T u when Term.is_bool u -> - F.equiv (F.atom (Term.Bool.pa t)) (F.atom (Term.Bool.pa u)) - | T u -> mk_eq t u |> F.atom - | Rat u -> mk_lra_eq (RLE.singleton1 t) u |> F.atom - and mk_eq_tf_tf (t:term_or_form) (u:term_or_form) = match t, u with - | T t, T u -> mk_eq t u |> F.atom - | T t, Rat u | Rat u, T t -> mk_lra_eq (RLE.singleton1 t) u |> F.atom - | Rat t, Rat u -> mk_lra_eq t u |> F.atom - | F t, F u -> F.equiv t u - | _ -> assert false - in - *) - (* convert term. - @param subst used to expand let-bindings on the fly *) - let rec aux (subst:Term.t Subst.t) (t:A.term) : Term.t = - begin match A.term_view t with - | A.Var v -> - begin match Subst.find subst v with - | None -> Error.errorf "variable %a not bound" A.Var.pp v - | Some t -> t - end - | A.Const id -> - let ty = conv_fun_ty @@ A.ty t in - mk_const (Fun.mk_undef id ty) - | A.App (f, l) -> - let l = List.map (aux subst) l in - begin match A.term_view f with - | A.Const id -> - (* TODO: lookup definition of [f] *) - mk_app (Fun.mk_undef id (conv_fun_ty @@ A.ty f)) l - | _ -> Error.errorf "cannot process HO application %a" A.pp_term t - end - | A.If (a,b,c) -> - let a = aux subst a in - let b = aux subst b in - let c = aux subst c in - Form.ite tst a b c - | A.Let (vbs,u) -> - let subst = - List.fold_left - (fun s (v,t) -> Subst.add s v (aux subst t)) - subst vbs - in - aux subst u - | A.Op (A.And, l) -> Form.and_l tst (List.map (aux subst) l) - | A.Op (A.Or, l) -> Form.or_l tst (List.map (aux subst) l) - | A.Op (A.Imply, l) -> - let l = List.map (aux subst) l in - begin match List.rev l with - | [] -> Term.true_ tst - | ret :: hyps -> - Form.imply_l tst hyps ret - end - | A.Op (A.Eq, l) -> - let l = List.map (aux subst) l in - let rec curry_eq = function - | [] | [_] -> assert false - | [a;b] -> [mk_eq a b] - | a :: b :: tail -> - mk_eq a b :: curry_eq (b::tail) - in - Form.and_l tst (curry_eq l) - | A.Op (A.Distinct, l) -> - Form.distinct_l tst @@ List.map (aux subst) l - | A.Not f -> Form.not_ tst (aux subst f) - | A.Bool true -> Term.true_ tst - | A.Bool false -> Term.false_ tst - | A.Num_q _n -> assert false (* TODO Mc2_lra.LE.const n |> ret_rat *) - | A.Num_z _n -> assert false (* TODO Mc2_lra.LE.const (Q.of_bigint n) |> ret_rat *) - | A.Arith (_op, _l) -> - assert false - (* TODO - let l = List.map (aux_rat subst) l in - begin match op, l with - | A.Minus, [a] -> RLE.neg a |> ret_rat - | _, [] | _, [_] -> - Error.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t - | A.Leq, [a;b] -> - let e = RLE.diff a b in - mk_lra_pred Mc2_lra.Leq0 e |> ret_any - | A.Geq, [a;b] -> - let e = RLE.diff b a in - mk_lra_pred Mc2_lra.Leq0 e |> ret_any - | A.Lt, [a;b] -> - let e = RLE.diff a b in - mk_lra_pred Mc2_lra.Lt0 e |> ret_any - | A.Gt, [a;b] -> - let e = RLE.diff b a in - mk_lra_pred Mc2_lra.Lt0 e |> ret_any - | (A.Leq | A.Lt | A.Geq | A.Gt), _ -> - Error.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t - | A.Add, _ -> - let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in - mk_lra_expr e |> ret_t - | A.Minus, a::tail -> - let e = - List.fold_left - (fun n t -> RLE.diff n t) - a tail - in - mk_lra_expr e |> ret_t - | A.Mult, _::_::_ -> - let coeffs, terms = - CCList.partition_map - (fun t -> match RLE.as_const t with - | None -> `Right t - | Some c -> `Left c) - l - in - begin match coeffs, terms with - | c::c_tail, [] -> - List.fold_right RLE.mult c_tail (RLE.const c) |> ret_rat - | _, [t] -> - List.fold_right RLE.mult coeffs t |> ret_rat - | _ -> - Error.errorf "non-linear expr:@ `%a`" A.pp_term t - end - | A.Div, (first::l) -> - (* support t/a/b/c where only [t] is a rational *) - let coeffs = - List.map - (fun c -> match RLE.as_const c with - | None -> - Error.errorf "non-linear expr:@ `%a`" A.pp_term t - | Some c -> Q.inv c) - l - in - List.fold_right RLE.mult coeffs first |> ret_rat - end - *) - | A.Select _ -> assert false (* TODO *) - | A.Match _ -> assert false (* TODO *) - | A.Bind _ -> assert false (* TODO *) - | A.Undefined_value -> assert false (* TODO *) - | A.Asserting _ -> assert false (* TODO *) - end - in - aux Subst.empty t -end - -let conv_ty = Conv.conv_ty -let conv_term = Conv.conv_term - (* instantiate solver here *) module Solver_arg = struct module T = Sidekick_base_term @@ -587,10 +199,9 @@ let process_stmt ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?(check=false) ?time ?memory ?progress (solver:Solver.t) - (stmt:Ast.statement) : unit or_error = + (stmt:Statement.t) : unit or_error = Log.debugf 5 - (fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt); - let tst = Solver.tst solver in + (fun k->k "(@[<2>process statement@ %a@])" Statement.pp stmt); let decl_sort c n : unit = Log.debugf 1 (fun k->k "(@[declare-sort %a@ :arity %d@])" ID.pp c n); (* TODO: more? *) @@ -602,34 +213,31 @@ let process_stmt (* TODO: more? *) in begin match stmt with - | A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return () - | A.SetLogic s -> + | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> + E.return () (* TODO: QF_DT *) + | Statement.Stmt_set_logic s -> Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s); E.return () - | A.SetOption l -> + | Statement.Stmt_set_option l -> Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l); E.return () - | A.SetInfo _ -> E.return () - | A.Exit -> + | Statement.Stmt_set_info _ -> E.return () + | Statement.Stmt_exit -> Log.debug 1 "exit"; raise Exit - | A.CheckSat -> + | Statement.Stmt_check_sat -> solve ?gc ?restarts ?dot_proof ~check ?pp_model ?time ?memory ?progress ~assumptions:[] ?hyps solver; E.return() - | A.TyDecl (id,n) -> + | Statement.Stmt_ty_decl (id,n) -> decl_sort id n; E.return () - | A.Decl (f,ty) -> - let ty_args, ty_ret = A.Ty.unfold ty in - let ty_args = List.map conv_ty ty_args in - let ty_ret = conv_ty ty_ret in + | Statement.Stmt_decl (f,ty_args,ty_ret) -> decl_fun f ty_args ty_ret; E.return () - | A.Assert t -> - let t = conv_term tst t in + | Statement.Stmt_assert t -> if pp_cnf then ( Format.printf "(@[assert@ %a@])@." Term.pp t ); @@ -637,14 +245,27 @@ let process_stmt CCOpt.iter (fun h -> Vec.push h [atom]) hyps; Solver.add_clause solver (IArray.singleton atom); E.return() - | A.Goal (_, _) -> - Error.errorf "cannot deal with goals yet" - | A.Data _ -> + | Statement.Stmt_data _ -> Error.errorf "cannot deal with datatypes yet" - | A.Define _ -> + | Statement.Stmt_define _ -> Error.errorf "cannot deal with definitions yet" end +(* TODO: this + datatypes +module Th_cstor = Sidekick_th_cstor.Make(struct + module Solver = Solver + module T = Solver.A.Term + + let[@inline] view_as_cstor t = match view t with + | App_cst (c, args) when Fun.do_cc + | If (a,b,c) -> T_ite (a,b,c) + | Bool b -> T_bool b + | _ -> T_other t + end + + end) + *) + module Th_bool = Sidekick_th_bool_static.Make(struct module S = Solver type term = S.T.Term.t diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index abc4dbed..fcdb0b84 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -11,12 +11,6 @@ val th_bool : Solver.theory type 'a or_error = ('a, string) CCResult.t -(* TODO: record type for config *) - -val conv_ty : Ast.Ty.t -> Ty.t - -val conv_term : Term.state -> Ast.term -> Term.t - module Check_cc : sig (** theory that check validity of conflicts *) val theory : Solver.theory @@ -34,5 +28,5 @@ val process_stmt : ?memory:float -> ?progress:bool -> Solver.t -> - Ast.statement -> + Statement.t -> unit or_error diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 0f50de59..370d98ee 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -2,12 +2,13 @@ module ID = Sidekick_base_term.ID module Fmt = CCFormat -module Ast = Ast module E = CCResult module Loc = Smtlib_utils.V_2_6.Loc module Parse_ast = Smtlib_utils.V_2_6.Ast module Process = Process module Solver = Process.Solver +module Term = Sidekick_base_term.Term +module Stmt = Sidekick_base_term.Statement module Proof = struct type t = Proof_default @@ -29,18 +30,18 @@ module Parse = struct try Result.Ok (parse_file_exn file) with e -> Result.Error (Printexc.to_string e) - let parse_file_exn ctx file : Ast.statement list = + let parse_file_exn ctx file : Stmt.t list = (* delegate parsing to [Tip_parser] *) parse_file_exn file |> CCList.flat_map (Typecheck.conv_statement ctx) - let parse file = - let ctx = Typecheck.Ctx.create () in + let parse tst file = + let ctx = Typecheck.Ctx.create tst in try Result.Ok (parse_file_exn ctx file) with e -> Result.Error (Printexc.to_string e) - let parse_stdin () = - let ctx = Typecheck.Ctx.create () in + let parse_stdin tst = + let ctx = Typecheck.Ctx.create tst in try parse_chan_exn ~filename:"" stdin |> CCList.flat_map (Typecheck.conv_statement ctx) @@ -48,183 +49,5 @@ module Parse = struct with e -> Result.Error (Printexc.to_string e) end -(* TODO: remove -module Term_bool : sig - open Sidekick_th_bool_dyn - type 'a view = 'a Bool_intf.view - - type term = Sidekick_smt.Term.t - - include Bool_intf.BOOL_TERM - with type t = term - and type state = Sidekick_smt.Term.state - - val and_ : state -> term -> term -> term - val or_ : state -> term -> term -> term - val not_ : state -> term -> term - val imply : state -> term -> term -> term - val imply_a : state -> term IArray.t -> term -> term - val imply_l : state -> term list -> term -> term - val eq : state -> term -> term -> term - val neq : state -> term -> term -> term - val and_a : state -> term IArray.t -> term - val and_l : state -> term list -> term - val or_a : state -> term IArray.t -> term - val or_l : state -> term list -> term -end = struct - module ID = Sidekick_smt.ID - module T = Sidekick_smt.Term - module Ty = Sidekick_smt.Ty - open Sidekick_smt.Solver_types - - open Bool_intf - - type term = T.t - type t = T.t - type state = T.state - - type 'a view = 'a Bool_intf.view - - exception Not_a_th_term - - let id_and = ID.make "and" - let id_or = ID.make "or" - let id_imply = ID.make "=>" - - let equal = T.equal - let hash = T.hash - - let view_id cst_id args = - if ID.equal cst_id id_and then ( - B_and args - ) else if ID.equal cst_id id_or then ( - B_or args - ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then ( - (* conclusion is stored first *) - let len = IArray.length args in - B_imply (IArray.sub args 1 (len-1), IArray.get args 0) - ) else ( - raise_notrace Not_a_th_term - ) - - let view_as_bool (t:T.t) : T.t view = - match T.view t with - | Not u -> B_not u - | App_cst ({cst_id; _}, args) -> - (try view_id cst_id args with Not_a_th_term -> B_atom t) - | _ -> B_atom t - - module C = struct - - let get_ty _ _ = Ty.prop - - let abs ~self _a = - match T.view self with - | Not u -> u, false - | _ -> self, true - - let eval id args = - let module Value = Sidekick_smt.Value in - match view_id id args with - | B_not (V_bool b) -> Value.bool (not b) - | B_and a when IArray.for_all Value.is_true a -> Value.true_ - | B_and a when IArray.exists Value.is_false a -> Value.false_ - | B_or a when IArray.exists Value.is_true a -> Value.true_ - | B_or a when IArray.for_all Value.is_false a -> Value.false_ - | B_imply (_, V_bool true) -> Value.true_ - | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ - | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ - | B_atom v -> v - | B_not _ | B_and _ | B_or _ | B_imply _ - -> Error.errorf "non boolean value in boolean connective" - - (* no congruence closure for boolean terms *) - let relevant _id _ _ = false - - let mk_cst ?(do_cc=false) id : cst = - {cst_id=id; - cst_view=Cst_def { - pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; } - - let not = T.not_ - let and_ = mk_cst id_and - let or_ = mk_cst id_or - let imply = mk_cst id_imply - end - - let as_id id (t:T.t) : T.t IArray.t option = - match T.view t with - | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args - | _ -> None - - (* flatten terms of the given ID *) - let flatten_id op sign (l:T.t list) : T.t list = - CCList.flat_map - (fun t -> match as_id op t with - | Some args -> IArray.to_list args - | None when (sign && T.is_true t) || (not sign && T.is_false t) -> - [] (* idempotent *) - | None -> [t]) - l - - let and_l st l = - match flatten_id id_and true l with - | [] -> T.true_ st - | l when List.exists T.is_false l -> T.false_ st - | [x] -> x - | args -> T.app_cst st C.and_ (IArray.of_list args) - - let or_l st l = - match flatten_id id_or false l with - | [] -> T.false_ st - | l when List.exists T.is_true l -> T.true_ st - | [x] -> x - | args -> T.app_cst st C.or_ (IArray.of_list args) - - let and_ st a b = and_l st [a;b] - let or_ st a b = or_l st [a;b] - let and_a st a = and_l st (IArray.to_list a) - let or_a st a = or_l st (IArray.to_list a) - let eq = T.eq - let not_ = T.not_ - - let neq st a b = not_ st @@ eq st a b - - let imply_a st xs y = - if IArray.is_empty xs then y - else T.app_cst st C.imply (IArray.append (IArray.singleton y) xs) - - let imply_l st xs y = match xs with - | [] -> y - | _ -> T.app_cst st C.imply (IArray.of_list @@ y :: xs) - - let imply st a b = imply_a st (IArray.singleton a) b - - let make st = function - | B_atom t -> t - | B_and l -> and_a st l - | B_or l -> or_a st l - | B_imply (a,b) -> imply_a st a b - | B_not t -> not_ st t -end - *) - -module Theories = struct - (* TODO - module Th_cstor = Sidekick_th_cstor.Make(struct - module Solver = Solver - module T = Solver.A.Term - - let[@inline] view_as_cstor t = match view t with - | App_cst (c, args) when Fun.do_cc - | If (a,b,c) -> T_ite (a,b,c) - | Bool b -> T_bool b - | _ -> T_other t - end - - end) - *) -end - let parse = Parse.parse let parse_stdin = Parse.parse_stdin diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index eddef0a6..6c9a3c6b 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -6,10 +6,11 @@ type 'a or_error = ('a, string) CCResult.t -module Ast = Ast +module Term = Sidekick_base_term.Term +module Stmt = Sidekick_base_term.Statement module Process = Process module Solver = Process.Solver -val parse : string -> Ast.statement list or_error +val parse : Term.state -> string -> Stmt.t list or_error -val parse_stdin : unit -> Ast.statement list or_error +val parse_stdin : Term.state -> Stmt.t list or_error diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 705db130..11cb10c2 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -7,8 +7,12 @@ module Loc = Smtlib_utils.V_2_6.Loc module Fmt = CCFormat module Log = Msat.Log -module A = Ast module PA = Smtlib_utils.V_2_6.Ast +module BT = Sidekick_base_term +module Ty = BT.Ty +module T = BT.Term +module Fun = BT.Fun +module Stmt = BT.Statement type 'a or_error = ('a, string) CCResult.t @@ -21,27 +25,28 @@ module StrTbl = CCHashtbl.Make(CCString) module Ctx = struct type kind = | K_ty of ty_kind - | K_fun of A.Ty.t - | K_var of A.var (* local *) - | K_cstor of A.Ty.t - | K_select of A.Ty.t * A.select + | K_fun of Fun.t + | K_cstor of Fun.t * Ty.t + | K_select of Fun.t * Ty.t * BT.Select.t and ty_kind = - | K_uninterpreted (* uninterpreted type *) - | K_other + | K_atomic of Ty.def | K_bool - | K_data (* data type *) type t = { + tst: T.state; names: ID.t StrTbl.t; kinds: kind ID.Tbl.t; - data: (ID.t * A.Ty.t) list ID.Tbl.t; (* data -> cstors *) + lets: T.t StrTbl.t; + data: (ID.t * Ty.t) list ID.Tbl.t; (* data -> cstors *) mutable loc: Loc.t option; (* current loc *) } - let create () : t = { + let create (tst:T.state) : t = { + tst; names=StrTbl.create 64; kinds=ID.Tbl.create 64; + lets=StrTbl.create 16; data=ID.Tbl.create 64; loc=None; } @@ -49,53 +54,46 @@ module Ctx = struct let loc t = t.loc let set_loc ?loc t = t.loc <- loc - let add_id t (s:string) (k:kind): ID.t = + let add_id_ self (s:string) (k:ID.t -> kind): ID.t = let id = ID.make s in - StrTbl.add t.names s id; - ID.Tbl.add t.kinds id k; + StrTbl.add self.names s id; + ID.Tbl.add self.kinds id (k id); id - let add_data t (id:ID.t) cstors: unit = - ID.Tbl.add t.data id cstors + let add_id self (s:string) (k:kind): ID.t = add_id_ self s (fun _ ->k) - let with_var t (s:string) (ty:A.Ty.t) (f:A.var -> 'a): 'a = - let id = ID.make s in - StrTbl.add t.names s id; - let v = A.Var.make id ty in - ID.Tbl.add t.kinds id (K_var v); - CCFun.finally1 f v - ~h:(fun () -> StrTbl.remove t.names s) + let add_data self (id:ID.t) cstors: unit = + ID.Tbl.add self.data id cstors - let with_vars t (l:(string*A.Ty.t) list) (f:A.var list -> 'a): 'a = - let rec aux ids l f = match l with - | [] -> f (List.rev ids) - | (s,ty) :: l' -> with_var t s ty (fun id -> aux (id::ids) l' f) - in - aux [] l f + (* locally bind [bs] and call [f], then remove bindings *) + let with_lets (self:t) (bs:(string*T.t) list) (f:unit -> 'a): 'a = + List.iter (fun (v,u) -> StrTbl.add self.lets v u) bs; + CCFun.finally ~f + ~h:(fun () -> + List.iter (fun (v,_) -> StrTbl.remove self.lets v) bs) - let find_kind t (id:ID.t) : kind = - try ID.Tbl.find t.kinds id + let find_kind self (id:ID.t) : kind = + try ID.Tbl.find self.kinds id with Not_found -> Error.errorf "did not find kind of ID `%a`" ID.pp id - let as_data t (ty:A.Ty.t) : (ID.t * A.Ty.t) list = match ty with - | A.Ty.App (id,_) -> - begin match ID.Tbl.get t.data id with - | Some l -> l - | None -> Error.errorf "expected %a to be a datatype" A.Ty.pp ty - end - | _ -> Error.errorf "expected %a to be a constant type" A.Ty.pp ty + let find_ty_def self (id:ID.t) : Ty.def = + match find_kind self id with + | K_ty (K_atomic def) -> def + | _ -> Error.errorf "expected %a to be an atomic type" ID.pp id + + let as_data _self (ty:Ty.t) : BT.Data.t = + match Ty.view ty with + | Ty.Ty_atomic {def=Ty.Ty_data d;_} -> d + | _ -> Error.errorf "expected %a to be a constant type" Ty.pp ty let pp_kind out = function | K_ty _ -> Format.fprintf out "type" - | K_cstor ty -> - Format.fprintf out "(@[cstor : %a@])" A.Ty.pp ty - | K_select (ty,s) -> + | K_cstor (_,ty) -> + Format.fprintf out "(@[cstor : %a@])" Ty.pp ty + | K_select (_,ty,s) -> Format.fprintf out "(@[select-%a-%d : %a@])" - ID.pp s.A.select_cstor s.A.select_i A.Ty.pp ty - | K_fun ty -> - Format.fprintf out "(@[fun : %a@])" A.Ty.pp ty - | K_var v -> - Format.fprintf out "(@[var : %a@])" A.Ty.pp (A.Var.ty v) + ID.pp s.Select.select_cstor s.Select.select_i Ty.pp ty + | K_fun f -> Fun.pp out f let pp out t = Format.fprintf out "ctx {@[%a@]}" @@ -106,9 +104,12 @@ let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx) let errorf_ctx ctx msg = Error.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx) -let check_bool_ t = - if not (A.Ty.equal (A.ty t) A.Ty.prop) then ( - A.Ty.ill_typed "expected bool, got `@[%a : %a@]`" A.pp_term t A.Ty.pp (A.ty t) +let ill_typed ctx fmt = + errorf_ctx ctx ("ill-typed: " ^^ fmt) + +let check_bool_ ctx t = + if not (Ty.equal (T.ty t) Ty.bool) then ( + ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t) ) let find_id_ ctx (s:string): ID.t = @@ -116,24 +117,25 @@ let find_id_ ctx (s:string): ID.t = with Not_found -> errorf_ctx ctx "name `%s` not in scope" s (* 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 +let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with + | PA.Ty_bool -> Ty.bool + | PA.Ty_real -> + ill_typed ctx "cannot handle reals for now" + (* FIXME + Ty.rat, Ctx.K_ty Ctx.K_other + *) + | PA.Ty_app ("Rat",[]) -> + ill_typed ctx "cannot handle reals for now" + (* TODO A.Ty.rat, Ctx.K_ty Ctx.K_other *) + | PA.Ty_app ("Int",[]) -> + ill_typed ctx "cannot handle ints for now" + (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *) | PA.Ty_app (f, l) -> - let id = find_id_ ctx f in - let l = List.map (conv_ty_fst ctx) l in - A.Ty.app id l, Ctx.find_kind ctx id - | PA.Ty_arrow (args, ret) -> - let args = List.map (conv_ty_fst ctx) args in - let ret, _ = conv_ty ctx ret in - A.Ty.arrow_l args ret, Ctx.K_ty Ctx.K_other - -and conv_ty_fst ctx t = fst (conv_ty ctx t) - -let conv_var ctx (v,ty) = v, conv_ty_fst ctx ty -let conv_vars ctx l = List.map (fun (v,ty) -> v, conv_ty_fst ctx ty) l + let def = Ctx.find_ty_def ctx @@ find_id_ ctx f in + let l = List.map (conv_ty ctx) l in + Ty.atomic def l + | PA.Ty_arrow _ -> + ill_typed ctx "cannot handle arrow types" let is_num s = let is_digit_or_dot = function '0' .. '9' | '.' -> true | _ -> false in @@ -141,26 +143,37 @@ let is_num s = then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1)) else CCString.for_all is_digit_or_dot s -let rec conv_term ctx (t:PA.term) : A.term = match t with - | PA.True -> A.true_ - | PA.False -> A.false_ - | PA.Const s when is_num s -> A.num_str A.Ty.rat s (* numeral *) +(* conversion of terms *) +let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = + let tst = ctx.Ctx.tst in + match t with + | PA.True -> T.true_ tst + | PA.False -> T.false_ tst + | PA.Const s when is_num s -> + errorf_ctx ctx "cannot handle numbers for now" + (* FIXME A.num_str Ty.rat s (* numeral *) *) | PA.Const f | PA.App (f, []) -> - let id = find_id_ ctx f in - begin match Ctx.find_kind ctx id with - | Ctx.K_var v -> A.var v - | Ctx.K_fun ty -> A.const id ty - | Ctx.K_ty _ -> - errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id - | Ctx.K_cstor ty -> A.const id ty - | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported" + (* lookup in `let` table, then in type defs *) + begin match StrTbl.find ctx.Ctx.lets f with + | u -> u + | exception Not_found -> + let id = find_id_ ctx f in + begin match Ctx.find_kind ctx id with + | Ctx.K_fun f -> T.const tst f + | Ctx.K_ty _ -> + errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id + | Ctx.K_cstor _ -> + errorf_ctx ctx "cannot handle constructors for now" + (* FIXME: A.const id ty *) + | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported" + end end | PA.App (f, args) -> let id = find_id_ ctx f in let args = List.map (conv_term ctx) args in begin match Ctx.find_kind ctx id with - | Ctx.K_fun ty -> A.app (A.const id ty) args + | Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args) | _ -> (* TODO: constructor + selector *) errorf_ctx ctx "expected constant application; got `%a`" ID.pp id @@ -169,60 +182,47 @@ 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 let c = conv_term ctx c in - A.if_ a b c - | PA.Fun (v, body) -> - let v = conv_var ctx v in - Ctx.with_var ctx (fst v)(snd v) - (fun v -> - let body = conv_term ctx body in - A.fun_ v body) - | PA.Forall _ | PA.Exists _ -> - errorf_ctx ctx "cannot process quantifiers in %a" PA.pp_term t - | PA.Let (vbs, u) -> - let vars, terms = + T.ite tst a b c + | PA.Fun _ | PA.Forall _ | PA.Exists _ -> + errorf_ctx ctx "cannot process lambda/quantifiers in %a" PA.pp_term t + | PA.Let (vbs, body) -> + let bs = List.map - (fun (v,t) -> - let t = conv_term ctx t in - (v,A.ty t), t) + (fun (v,u) -> + let u = conv_term ctx u in + v, u) vbs - |> List.split in - Ctx.with_vars ctx vars - (fun vars -> - let vbs = List.combine vars terms in - let u = conv_term ctx u in - A.let_l vbs u) + Ctx.with_lets ctx bs (fun () -> conv_term ctx body) | PA.Distinct l -> let l = List.map (conv_term ctx) l in - A.op A.Distinct l + Form.distinct_l tst l | PA.And l -> let l = List.map (conv_term ctx) l in - A.and_l l + Form.and_l tst l | PA.Or l -> let l = List.map (conv_term ctx) l in - A.or_l l + Form.or_l tst l | PA.Not a -> let a = conv_term ctx a in - A.not_ a + Form.not_ tst a | PA.Eq (a,b) -> let a = conv_term ctx a in let b = conv_term ctx b in - A.eq a b + Form.eq tst a b | PA.Imply (a,b) -> let a = conv_term ctx a in let b = conv_term ctx b in - A.imply a b - | PA.Match (lhs, l) -> - (* + Form.imply tst a b + | PA.Match (_lhs, _l) -> errorf_ctx ctx "TODO: support match in %a" PA.pp_term t - assert false - *) + (* FIXME: do that properly, using [with_lets] with selectors (* convert a regular case *) let conv_case c vars rhs = let c_id = find_id_ ctx c in (* obtain the type *) let ty_args, _ty_ret = match Ctx.find_kind ctx c_id with - | Ctx.K_cstor ty -> A.Ty.unfold ty + | Ctx.K_cstor ty -> Ty.unfold ty | _ -> errorf_ctx ctx "expected `@[%a@]`@ to be a constructor" ID.pp c_id in @@ -281,59 +281,63 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with (fun cases (cstor,ty_cstor) -> if ID.Map.mem cstor cases then cases else ( - let args, _ = A.Ty.unfold ty_cstor in + let args, _ = Ty.unfold ty_cstor in let vars = List.mapi (fun i ty -> A.Var.makef ~ty "_%d" i) args in ID.Map.add cstor (vars, def_rhs) cases )) cases all_cstors in A.match_ lhs cases - | PA.Arith (op, l) -> + *) + | PA.Arith (_op, _l) -> + errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t + (* FIXME: arith let l = List.map (conv_term ctx) l in List.iter (fun t -> - if not (A.Ty.equal A.Ty.rat (A.ty t)) then ( + if not (Ty.equal Ty.rat (A.ty t)) then ( errorf_ctx ctx "expected rational term,@ got `%a`" A.pp_term t )) l; let ty, op = match op with - | PA.Leq -> A.Ty.prop, A.Leq - | PA.Lt -> A.Ty.prop,A. Lt - | PA.Geq -> A.Ty.prop, A.Geq - | PA.Gt -> A.Ty.prop, A.Gt - | PA.Add -> A.Ty.rat, A.Add - | PA.Minus -> A.Ty.rat, A.Minus - | PA.Mult -> A.Ty.rat, A.Mult - | PA.Div -> A.Ty.rat, A.Div + | PA.Leq -> Ty.prop, A.Leq + | PA.Lt -> Ty.prop,A. Lt + | PA.Geq -> Ty.prop, A.Geq + | PA.Gt -> Ty.prop, A.Gt + | PA.Add -> Ty.rat, A.Add + | PA.Minus -> Ty.rat, A.Minus + | PA.Mult -> Ty.rat, A.Mult + | PA.Div -> Ty.rat, A.Div in A.arith ty op l + *) | PA.Cast (t, ty_expect) -> let t = conv_term ctx t in - let ty_expect = conv_ty_fst ctx ty_expect in - if not (A.Ty.equal (A.ty t) ty_expect) then ( - A.Ty.ill_typed "term `%a`@ should have type `%a`" A.pp_term t A.Ty.pp ty_expect + let ty_expect = conv_ty ctx ty_expect in + if not (Ty.equal (T.ty t) ty_expect) then ( + ill_typed ctx "term `%a`@ should have type `%a`" T.pp t Ty.pp ty_expect ); t | _ -> errorf_ctx ctx "unsupported term %a" PA.pp_term t -let conv_fun_decl ctx f : string * A.Ty.t = +let conv_fun_decl ctx f : string * Ty.t list * Ty.t = if f.PA.fun_ty_vars <> [] then ( errorf_ctx ctx "cannot convert polymorphic function@ %a" (PA.pp_fun_decl PA.pp_ty) f ); - let args = List.map (conv_ty_fst ctx) f.PA.fun_args in - let ty = A.Ty.arrow_l args (conv_ty_fst ctx f.PA.fun_ret) in - f.PA.fun_name, ty + let args = List.map (conv_ty ctx) f.PA.fun_args in + let ret = conv_ty ctx f.PA.fun_ret in + f.PA.fun_name, args, ret -let conv_fun_def ctx f_decl body : string * A.Ty.t * (unit -> A.term) = +(* FIXME: fun defs +let conv_fun_def ctx f_decl body : string * Ty.t * (unit -> T.t) = if f_decl.PA.fun_ty_vars <> [] then ( errorf_ctx ctx "cannot convert polymorphic function@ %a" (PA.pp_fun_decl PA.pp_typed_var) f_decl; ); let args = conv_vars ctx f_decl.PA.fun_args in let ty = - A.Ty.arrow_l (List.map snd args) (conv_ty_fst ctx f_decl.PA.fun_ret) in @@ -351,27 +355,34 @@ let conv_fun_defs ctx decls bodies : A.definition list = let defs = List.map2 (fun id (_,ty,body) -> id, ty, body()) ids l in (* parse id,ty and declare them before parsing the function bodies *) defs + *) -let rec conv_statement ctx (s:PA.statement): A.statement list = +let rec conv_statement ctx (s:PA.statement): Stmt.t list = Log.debugf 4 (fun k->k "(@[<1>statement_of_ast@ %a@])" PA.pp_stmt s); Ctx.set_loc ctx ?loc:(PA.loc s); conv_statement_aux ctx s -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 (a,b) -> [A.SetInfo [a;b]] - | PA.Stmt_exit -> [A.Exit] +and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = + let tst = ctx.Ctx.tst in + match PA.view stmt with + | PA.Stmt_set_logic s -> [Stmt.Stmt_set_logic s] + | PA.Stmt_set_option l -> [Stmt.Stmt_set_option l] + | PA.Stmt_set_info (a,b) -> [Stmt.Stmt_set_info (a,b)] + | PA.Stmt_exit -> [Stmt.Stmt_exit] | PA.Stmt_decl_sort (s,n) -> - let id = Ctx.add_id ctx s (Ctx.K_ty Ctx.K_uninterpreted) in - [A.TyDecl (id,n)] + let id = Ctx.add_id_ ctx s + (fun id -> Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id))) in + [Stmt.Stmt_ty_decl (id, n)] | PA.Stmt_decl fr -> - let f, ty = conv_fun_decl ctx fr in - let id = Ctx.add_id ctx f (Ctx.K_fun ty) in - [A.Decl (id, ty)] + let f, args, ret = conv_fun_decl ctx fr in + let id = Ctx.add_id_ ctx f + (fun id -> Ctx.K_fun (Fun.mk_undef' id args ret)) in + [Stmt.Stmt_decl (id, args,ret)] | PA.Stmt_data l when List.for_all (fun ((_,n),_) -> n=0) l -> + errorf_ctx ctx "cannot typecheck datatypes" + (* FIXME (* first, read and declare each datatype (it can occur in the other - datatypes' construtors) *) + datatypes' constructors) *) let pre_parse ((data_name,arity),cases) = if arity <> 0 then ( errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name; @@ -384,7 +395,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie let l = List.map (fun (data_id, (cstors:PA.cstor list)) -> - let data_ty = A.Ty.const data_id in + let data_ty = Ty.const data_id in let parse_case {PA.cstor_name=c; cstor_args; cstor_ty_vars} = if cstor_ty_vars <> [] then ( errorf_ctx ctx "cannot handle polymorphic constructor %s" c; @@ -394,7 +405,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie in let ty_args = List.map snd selectors in (* declare cstor *) - let ty_c = A.Ty.arrow_l ty_args data_ty in + let ty_c = Ty.arrow_l ty_args data_ty in let id_c = Ctx.add_id ctx c (Ctx.K_cstor ty_c) in (* now declare selectors *) List.iteri @@ -415,37 +426,42 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie let cstors = List.map parse_case cstors in (* update info on [data] *) Ctx.add_data ctx data_id cstors; - {A.Ty.data_id; data_cstors=ID.Map.of_list cstors}) + {Ty.data_id; data_cstors=ID.Map.of_list cstors}) l in [A.Data l] + *) | PA.Stmt_data _ -> errorf_ctx ctx "not implemented: parametric datatypes" PA.pp_stmt stmt - | PA.Stmt_funs_rec defs -> - (* errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt *) + | PA.Stmt_funs_rec _defs -> + errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt + (* TODO let {PA.fsr_decls=decls; fsr_bodies=bodies} = defs in if List.length decls <> List.length bodies then ( errorf_ctx ctx "declarations and bodies should have same length"; ); let defs = conv_fun_defs ctx decls bodies in [A.Define defs] + *) | PA.Stmt_fun_def {PA.fr_decl={PA.fun_ty_vars=[]; fun_args=[]; fun_name; fun_ret}; fr_body} -> (* turn [def f : ret := body] into [decl f : ret; assert f=body] *) - let ret = conv_ty_fst ctx fun_ret in - let id = Ctx.add_id ctx fun_name (Ctx.K_fun ret) in + let ret = conv_ty ctx fun_ret in + let id = Ctx.add_id_ ctx fun_name + (fun id -> Ctx.K_fun (Fun.mk_undef_const id ret)) in + let f = match Ctx.find_kind ctx id with Ctx.K_fun f->f | _ -> assert false in let rhs = conv_term ctx fr_body in - [ A.Decl (id,ret); - A.Assert (A.eq (A.const id ret) rhs); + [ Stmt.Stmt_decl (id,[],ret); + Stmt.Stmt_assert (Form.eq tst (T.const tst f) rhs); ] | PA.Stmt_fun_rec _ | PA.Stmt_fun_def _ -> errorf_ctx ctx "unsupported definition: %a" PA.pp_stmt stmt | PA.Stmt_assert t -> let t = conv_term ctx t in - check_bool_ t; - [A.Assert t] - | PA.Stmt_check_sat -> [A.CheckSat] + check_bool_ ctx t; + [Stmt.Stmt_assert t] + | PA.Stmt_check_sat -> [Stmt.Stmt_check_sat] | PA.Stmt_check_sat_assuming _ | PA.Stmt_get_assertions | PA.Stmt_get_option _ @@ -460,5 +476,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie | PA.Stmt_push _ | PA.Stmt_pop _ | PA.Stmt_get_value _ - -> errorf_ctx ctx "cannot handle statement %a" PA.pp_stmt stmt + -> + (* TODO: handle more of these *) + errorf_ctx ctx "cannot handle statement %a" PA.pp_stmt stmt diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index 23d1dac8..d5dbfafa 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -3,6 +3,9 @@ (** {1 Preprocessing AST} *) module Loc = Smtlib_utils.V_2_6.Loc +module PA = Smtlib_utils.V_2_6.Ast +module T = Sidekick_base_term.Term +module Stmt = Sidekick_base_term.Statement type 'a or_error = ('a, string) CCResult.t @@ -10,14 +13,11 @@ type 'a or_error = ('a, string) CCResult.t module Ctx : sig type t - val create: unit -> t + val create: T.state -> t val pp : t CCFormat.printer end -module PA = Smtlib_utils.V_2_6.Ast -module A = Ast +val conv_term : Ctx.t -> PA.term -> T.t -val conv_term : Ctx.t -> PA.term -> A.term - -val conv_statement : Ctx.t -> PA.statement -> A.statement list +val conv_statement : Ctx.t -> PA.statement -> Stmt.t list diff --git a/src/smtlib/dune b/src/smtlib/dune index 8666bf3c..9913fdde 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -4,4 +4,6 @@ (libraries containers zarith msat sidekick.core sidekick.util sidekick.msat-solver sidekick.base-term sidekick.th-bool-static sidekick.mini-cc msat.backend smtlib-utils) - (flags :standard -open Sidekick_util)) + (flags :standard -warn-error -27-37 -open Sidekick_util)) + +; TODO: enable warn-error again