From 2fcef323b358e1ab79ab72ab01f5296b60dd2686 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 11 Feb 2018 10:43:38 -0600 Subject: [PATCH] move back process to dagon_smtlib --- src/main/main.ml | 3 +- src/smt/th_bool/Dagon_th_bool.ml | 54 +++++++++++++++---------------- src/smt/th_bool/Dagon_th_bool.mli | 22 ++++++------- src/smt/th_bool/jbuild | 2 +- src/smtlib/Dagon_smtlib.ml | 1 + src/smtlib/Dagon_smtlib.mli | 1 + src/{smt => smtlib}/Process.ml | 33 ++++++++++++------- src/{smt => smtlib}/Process.mli | 2 ++ src/smtlib/jbuild | 2 +- 9 files changed, 66 insertions(+), 54 deletions(-) rename src/{smt => smtlib}/Process.ml (96%) rename src/{smt => smtlib}/Process.mli (96%) diff --git a/src/main/main.ml b/src/main/main.ml index ad3b08e1..5fe5bc10 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -11,6 +11,7 @@ module Fmt = CCFormat module Term = Dagon_smt.Term module Ast = Dagon_smt.Ast module Solver = Dagon_smt.Solver +module Process = Dagon_smtlib.Process type 'a or_error = ('a, string) E.t @@ -137,7 +138,7 @@ let main () = try E.fold_l (fun () -> - Dagon_smt.Process.process_stmt + Process.process_stmt ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ~time:!time_limit ~memory:!size_limit ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress diff --git a/src/smt/th_bool/Dagon_th_bool.ml b/src/smt/th_bool/Dagon_th_bool.ml index 75a7aed2..8c6ac39c 100644 --- a/src/smt/th_bool/Dagon_th_bool.ml +++ b/src/smt/th_bool/Dagon_th_bool.ml @@ -103,11 +103,11 @@ module TC = struct let pp sub_pp out = function | Builtin {view=b;_} -> begin match b with - | B_not t -> Fmt.fprintf out "(@[not@ %a@])" sub_pp t + | B_not t -> Fmt.fprintf out "(@[not@ %a@])" sub_pp t | B_and l -> - Fmt.fprintf out "(@[and@ %a])" (Util.pp_list sub_pp) l + Fmt.fprintf out "(@[and@ %a])" (Util.pp_list sub_pp) l | B_or l -> - Fmt.fprintf out "(@[or@ %a@])" (Util.pp_list sub_pp) l + Fmt.fprintf out "(@[or@ %a@])" (Util.pp_list sub_pp) l | B_imply (a,b) -> Fmt.fprintf out "(@[=>@ %a@ %a@])" (Util.pp_list sub_pp) a sub_pp b | B_eq (a,b) -> @@ -190,38 +190,36 @@ module T_cell = struct let neq a b = distinct [a;b] end -module T = struct - let make = Term.make +let make = Term.make - let not_ st t = make st (T_cell.not_ t) +let not_ st t = make st (T_cell.not_ t) - let and_l st = function - | [] -> Term.true_ st - | [t] -> t - | l -> make st (T_cell.and_ l) +let and_l st = function + | [] -> Term.true_ st + | [t] -> t + | l -> make st (T_cell.and_ l) - let or_l st = function - | [] -> Term.false_ st - | [t] -> t - | l -> make st (T_cell.or_ l) +let or_l st = function + | [] -> Term.false_ st + | [t] -> t + | l -> make st (T_cell.or_ l) - let and_ st a b = and_l st [a;b] - let or_ st a b = or_l st [a;b] - let imply st a b = match a, Term.cell b with - | [], _ -> b - | _::_, Term_cell.Custom {view=Builtin {view=B_imply (a',b')}; _} -> - make st (T_cell.imply (CCList.append a a') b') - | _ -> make st (T_cell.imply a b) - let eq st a b = make st (T_cell.eq a b) - let distinct st l = make st (T_cell.distinct l) - let neq st a b = make st (T_cell.neq a b) - let builtin st b = make st (T_cell.builtin b) -end +let and_ st a b = and_l st [a;b] +let or_ st a b = or_l st [a;b] +let imply st a b = match a, Term.cell b with + | [], _ -> b + | _::_, Term_cell.Custom {view=Builtin {view=B_imply (a',b')}; _} -> + make st (T_cell.imply (CCList.append a a') b') + | _ -> make st (T_cell.imply a b) +let eq st a b = make st (T_cell.eq a b) +let distinct st l = make st (T_cell.distinct l) +let neq st a b = make st (T_cell.neq a b) +let builtin st b = make st (T_cell.builtin b) module Lit = struct type t = Lit.t - let eq tst a b = Lit.atom ~sign:true (T.eq tst a b) - let neq tst a b = Lit.atom ~sign:false (T.eq tst a b) + let eq tst a b = Lit.atom ~sign:true (eq tst a b) + let neq tst a b = Lit.atom ~sign:false (neq tst a b) end type t = { diff --git a/src/smt/th_bool/Dagon_th_bool.mli b/src/smt/th_bool/Dagon_th_bool.mli index 7f40a4a8..51e58086 100644 --- a/src/smt/th_bool/Dagon_th_bool.mli +++ b/src/smt/th_bool/Dagon_th_bool.mli @@ -28,18 +28,16 @@ module T_cell : sig val distinct : term list -> t end -module T : sig - val builtin : Term.state -> term builtin -> term - val and_ : Term.state -> term -> term -> term - val or_ : Term.state -> term -> term -> term - val not_ : Term.state -> term -> term - val imply : Term.state -> term list -> term -> term - val eq : Term.state -> term -> term -> term - val neq : Term.state -> term -> term -> term - val distinct : Term.state -> term list -> term - val and_l : Term.state -> term list -> term - val or_l : Term.state -> term list -> term -end +val builtin : Term.state -> term builtin -> term +val and_ : Term.state -> term -> term -> term +val or_ : Term.state -> term -> term -> term +val not_ : Term.state -> term -> term +val imply : Term.state -> term list -> term -> term +val eq : Term.state -> term -> term -> term +val neq : Term.state -> term -> term -> term +val distinct : Term.state -> term list -> term +val and_l : Term.state -> term list -> term +val or_l : Term.state -> term list -> term module Lit : sig type t = Lit.t diff --git a/src/smt/th_bool/jbuild b/src/smt/th_bool/jbuild index b5303589..976ae248 100644 --- a/src/smt/th_bool/jbuild +++ b/src/smt/th_bool/jbuild @@ -1,7 +1,7 @@ ; vim:ft=lisp: (library ((name Dagon_th_bool) - (public_name dagon.th_bool) + (public_name dagon.smt.th_bool) (libraries (containers dagon.smt)) (flags (:standard -w +a-4-44-48-58-60@8 -color always -safe-string -short-paths -open Dagon_util)) diff --git a/src/smtlib/Dagon_smtlib.ml b/src/smtlib/Dagon_smtlib.ml index 888a84c5..a5fa6fe8 100644 --- a/src/smtlib/Dagon_smtlib.ml +++ b/src/smtlib/Dagon_smtlib.ml @@ -5,6 +5,7 @@ module Fmt = CCFormat module Ast = Dagon_smt.Ast module E = CCResult module Loc = Locations +module Process = Process type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Dagon_smtlib.mli b/src/smtlib/Dagon_smtlib.mli index dac3fea8..f2e027ea 100644 --- a/src/smtlib/Dagon_smtlib.mli +++ b/src/smtlib/Dagon_smtlib.mli @@ -8,6 +8,7 @@ type 'a or_error = ('a, string) CCResult.t module Ast = Dagon_smt.Ast +module Process = Process val parse : string -> Ast.statement list or_error diff --git a/src/smt/Process.ml b/src/smtlib/Process.ml similarity index 96% rename from src/smt/Process.ml rename to src/smtlib/Process.ml index 256073fb..f57dc829 100644 --- a/src/smt/Process.ml +++ b/src/smtlib/Process.ml @@ -1,10 +1,13 @@ (** {2 Conversion into {!Term.t}} *) +open Dagon_smt + type 'a or_error = ('a, string) CCResult.t module E = CCResult module A = Ast +module Form = Dagon_th_bool module Fmt = CCFormat module Subst = struct @@ -25,7 +28,7 @@ module Conv = struct let conv_ty (ty:A.Ty.t) : Ty.t = let mk_ty id = Ty.atomic id Ty.Uninterpreted ~card:(lazy Ty_card.infinite) in (* convert a type *) - let rec aux_ty (ty:A.Ty.t) : Ty.t = match ty with + let aux_ty (ty:A.Ty.t) : Ty.t = match ty with | A.Ty.Prop -> Ty.prop (* | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat *) | A.Ty.App (id, []) -> mk_ty id @@ -38,7 +41,7 @@ module Conv = struct let conv_term (tst:Term.state) (t:A.term): Term.t = (* polymorphic equality *) - let mk_eq t u = Term.eq tst t u in (* TODO: use theory of booleans *) + let mk_eq t u = Form.eq tst t u in (* TODO: use theory of booleans *) let mk_app f l = Term.app_cst tst f (IArray.of_list l) in let mk_const = Term.const tst in (* @@ -105,14 +108,14 @@ module Conv = struct subst vbs in aux subst u - | A.Op (A.And, l) -> Term.and_l tst (List.map (aux subst) l) - | A.Op (A.Or, l) -> Term.or_l tst (List.map (aux subst) l) + | 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 -> - Term.imply tst hyps ret + Form.imply tst hyps ret end | A.Op (A.Eq, l) -> let l = List.map (aux subst) l in @@ -122,10 +125,10 @@ module Conv = struct | a :: b :: tail -> mk_eq a b :: curry_eq (b::tail) in - Term.and_l tst (curry_eq l) + Form.and_l tst (curry_eq l) | A.Op (A.Distinct, l) -> - Term.distinct tst @@ List.map (aux subst) l - | A.Not f -> Term.not_ tst (aux subst f) + Form.distinct 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 *) @@ -264,8 +267,16 @@ let process_stmt Log.debugf 5 (fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt); let tst = Solver.tst solver in - let decl_sort _ _ : unit = assert false in (* TODO *) - let decl _id _args _ret : unit = assert false in (* TODO *) + let decl_sort c n : unit = + Log.debugf 1 (fun k->k "(@[declare-sort %a@ :arity %d@])" ID.pp c n); + (* TODO: more? *) + in + let decl_fun id args ret : unit = + Log.debugf 1 + (fun k->k "(@[declare-fun %a@ :args (@[%a@])@ :ret %a@])" + ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret); + (* TODO: more? *) + in begin match stmt with | A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return () | A.SetLogic s -> @@ -289,7 +300,7 @@ let process_stmt 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 - 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 diff --git a/src/smt/Process.mli b/src/smtlib/Process.mli similarity index 96% rename from src/smt/Process.mli rename to src/smtlib/Process.mli index e234369b..9c5bc346 100644 --- a/src/smt/Process.mli +++ b/src/smtlib/Process.mli @@ -1,6 +1,8 @@ (** {1 Process Statements} *) +open Dagon_smt + type 'a or_error = ('a, string) CCResult.t (* TODO: record type for config *) diff --git a/src/smtlib/jbuild b/src/smtlib/jbuild index eb430fb0..0797cd0e 100644 --- a/src/smtlib/jbuild +++ b/src/smtlib/jbuild @@ -7,7 +7,7 @@ ((name dagon_smtlib) (public_name dagon.smtlib) (optional) ; only if deps present - (libraries (containers dagon.smt dagon.util zarith)) + (libraries (containers dagon.smt dagon.util dagon.smt.th_bool zarith)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always -open Dagon_util)) (ocamlopt_flags (:standard -O3 -color always -bin-annot