simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(smtlib): remove intermediate typed AST, type directly into terms

Browse source
This commit is contained in:
Simon Cruanes 2019-11-19 17:30:30 -06:00
parent 1a71535178
commit 3327c86841
13 changed files with 550 additions and 1509 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

168
src/base-term/Base_types.ml
View file

@ -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
let equal = (=)
let compare = Pervasives.compare
let pp out = function
| Finite -> CCFormat.string out "finite"
| Infinite -> CCFormat.string out "infinite"
end
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

3
src/base-term/Sidekick_base_term.ml
View file

@ -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

10
src/main/main.ml
View file

@ -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), " <s>[kMGT] sets the size limit for the sat solver";
"--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
"-v", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
]
"-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
"--debug", Arg.Int Msat.Log.set_debug, "<lvl> 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

493
src/smtlib/Ast.ml
View file

@ -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 "(@[<hv1>%a@ %a@])" pp f (Util.pp_list pp) l
| If (a,b,c) -> Fmt.fprintf out "(@[<hv>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 "(@[<hv2>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 "(@[<hv1>%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 "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp) l
| Undefined_value -> Fmt.string out "<undefined>"
| 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

216
src/smtlib/Ast.mli
View file

@ -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

180
src/smtlib/Form.ml Normal file
View file

@ -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<j} t_i != t_j] *)
let cs =
CCList.diagonal l |> 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

437
src/smtlib/Process.ml
View file

@ -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<j} t_i != t_j] *)
let cs =
CCList.diagonal l |> 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 "(@[<hv1>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

8
src/smtlib/Process.mli
View file

@ -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

191
src/smtlib/Sidekick_smtlib.ml
View file

@ -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>" 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

7
src/smtlib/Sidekick_smtlib.mli
View file

@ -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

318
src/smtlib/Typecheck.ml
View file

@ -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, []) ->
(* 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_var v -> A.var v
| Ctx.K_fun ty -> A.const id ty
| 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 ty -> A.const id ty
| 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)
vbs
|> List.split
in
Ctx.with_vars ctx vars
(fun vars ->
let vbs = List.combine vars terms in
(fun (v,u) ->
let u = conv_term ctx u in
A.let_l vbs u)
v, u)
vbs
in
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

12
src/smtlib/Typecheck.mli
View file

@ -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

4
src/smtlib/dune
View file

@ -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