From 5e0472e4bfd9a5405015b3b89b06225abf30f46a Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Wed, 27 Oct 2021 14:28:07 +0200 Subject: [PATCH 01/18] new SolverMonad --- bin/bench.ml | 29 +++++++++ bin/dune | 6 ++ src/benchmark/runtime.ml | 6 ++ src/sat/monadsat.ml | 130 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 171 insertions(+) create mode 100644 bin/bench.ml create mode 100644 src/benchmark/runtime.ml create mode 100644 src/sat/monadsat.ml diff --git a/bin/bench.ml b/bin/bench.ml new file mode 100644 index 0000000..9e4cfbc --- /dev/null +++ b/bin/bench.ml @@ -0,0 +1,29 @@ +open Modulus_lib +open Monadsat +open SolverMonad + +let () = Random.self_init () + +let random_list () = + let len = Random.int 20 in + List.init len (fun _ -> 20 - Random.int 20) + +let random_cnf () = + let len = Random.int 50 in + List.init len (fun _ -> random_list ()) + +let () = + let print_result = function + | Some m -> Printf.printf " SAT : %s\n" (string_of_clause m) + | None -> Printf.printf " UNSAT\n" + in + List.iteri (fun i cnf -> + Printf.printf "testing unit [%d]\n" i; + let r1 = Runtime.time (fun () -> Sat.solve cnf) in + let r2 = Runtime.time (fun () -> run solve cnf) in + assert (r1.result = r2.result); + Printf.printf " (old) solver result [runtime : %f] : \n" r1.time; + print_result r1.result; + Printf.printf " (new) solver result [runtime : %f] : \n" r2.time; + print_result r2.result; + ) (List.init 1000 (fun _ -> random_cnf ())) \ No newline at end of file diff --git a/bin/dune b/bin/dune index dc39053..ebeacae 100644 --- a/bin/dune +++ b/bin/dune @@ -9,3 +9,9 @@ (public_name test) (libraries modulus_lib) (modules test)) + +(executable + (name bench) + (public_name bench) + (libraries modulus_lib) + (modules bench)) diff --git a/src/benchmark/runtime.ml b/src/benchmark/runtime.ml new file mode 100644 index 0000000..be2c73b --- /dev/null +++ b/src/benchmark/runtime.ml @@ -0,0 +1,6 @@ +type 'a bench = { result : 'a; time : float } + +let time (f : unit -> 'a) : 'a bench = + let t = Sys.time () in + let r = f () in + { result = r; time = Sys.time () -. t } \ No newline at end of file diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml new file mode 100644 index 0000000..408d7c4 --- /dev/null +++ b/src/sat/monadsat.ml @@ -0,0 +1,130 @@ +type clause = int list + +type cnf = clause list + +let string_of_clause c = + "{" ^ String.concat " " (List.map string_of_int c) ^ "}" + +let string_of_cnf c = + "{" ^ String.concat " " (List.map string_of_clause c) ^ "}" + +module SolverMonad : sig + +type ('env, 'res) status + +type ('env, 'res) t + +val return : 'res -> ('env, 'res) t + +val fail : string -> ('env, 'res) t + +val abort : ('env, 'res) t + +val update : ('env -> 'env) -> ('env, 'res) t + +val set : 'env -> ('env, 'res) t + +val bind : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t +val (let*) : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t + +val fast_bind : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t +val (let+) : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t + +val (<|>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t + +val (<&>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t + +val map : ('res -> 'res1) -> ('env, 'res) t -> ('env, 'res1) t +val (=>) : ('env, 'res) t -> ('res -> 'res1) -> ('env, 'res1) t + +val fast_map : ('res -> 'res) -> ('env, 'res) t -> ('env, 'res) t +val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t + +val strategy : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t + +val run : ('env, 'res) t -> 'env -> 'res option + +end = struct + +type ('env, 'res) status = + | Fail of string + | Abort + | Update of 'env + | Value of 'res + +type ('env, 'res) t = 'env -> ('env, 'res) status + +let fail msg = fun _ -> Fail msg + +let return v = fun _ -> Value v + +let update up = fun env -> Update (up env) + +let set env = fun _ -> Update env + +let abort = fun _ -> Abort + +let[@inline] bind m f = fun env -> + match m env with + | Value v -> f v env + | Fail f -> Fail f + | Abort -> Abort + | Update e -> Update e + +let[@inline] (let*) m f = bind m f + +let[@inline] fast_bind m f = fun env -> + match m env with + | Value v -> f v env + | _ as ret -> ret + +let[@inline] (let+) m f = fast_bind m f + +let[@inline] (<|>) (m1 : ('env, 'res) t) (m2 : ('env, 'res) t) = fun (env : 'env) -> + match m1 env with + | Fail _ -> m2 env + | _ as res -> res + +let[@inline] (<&>) (s1 : ('env, 'res) t) (s2 : ('env, 'res) t) : ('env, 'res) t = fun env -> + match s1 env with + | Update e -> s2 e + | _ as ret -> ret + +let map f m = bind m (fun r -> return (f r)) +let[@inline] (=>) = fun m f -> map f m + +let fast_map f m = fast_bind m (fun r -> return (f r)) +let[@inline] (=>>) = fun m f -> fast_map f m + +let strategy (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = + let rec go env = + match step go env env with + | Update env -> go env + | _ as ret -> ret + in go + +let run f e = match f e with Value v -> Some v | _ -> None +end + +let remove_lit (l : int) = List.filter ((<>) l) + +open SolverMonad + +let propagate l = + List.filter_map (fun c -> + if List.mem l c then None + else Some (remove_lit (-l) c) + ) |> SolverMonad.update + +let add l = fun ls -> l::ls + +type ('a, 'b) solver = ('a, 'b) t + +let solve : (cnf, int list) solver = strategy (fun next -> function + | [] -> return [] + | []::_ -> fail "unsat" + | (l::_)::_ -> + (propagate l <&> next =>> add l) + <|> + (propagate (-l) <&> next =>> add (-l)) +) \ No newline at end of file From b5cb00af520227b1d484956e43d3bf379cb264e7 Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Thu, 28 Oct 2021 12:30:00 +0200 Subject: [PATCH 02/18] wip on the rewriting of QfLia with the new monad --- src/sat/monadsat.ml | 8 ++- src/theories/qf_lia/interval.ml | 0 src/theories/qf_lia/qf_lia.ml | 86 ++++++++++++++++++++++++++++++++- 3 files changed, 91 insertions(+), 3 deletions(-) delete mode 100644 src/theories/qf_lia/interval.ml diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml index 408d7c4..98b4d22 100644 --- a/src/sat/monadsat.ml +++ b/src/sat/monadsat.ml @@ -22,6 +22,8 @@ val abort : ('env, 'res) t val update : ('env -> 'env) -> ('env, 'res) t +val step : ('env -> ('env, 'res) t) -> ('env, 'res) t + val set : 'env -> ('env, 'res) t val bind : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t @@ -82,7 +84,7 @@ let[@inline] (let+) m f = fast_bind m f let[@inline] (<|>) (m1 : ('env, 'res) t) (m2 : ('env, 'res) t) = fun (env : 'env) -> match m1 env with - | Fail _ -> m2 env + | Fail _ | Abort -> m2 env | _ as res -> res let[@inline] (<&>) (s1 : ('env, 'res) t) (s2 : ('env, 'res) t) : ('env, 'res) t = fun env -> @@ -103,6 +105,8 @@ let strategy (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t | _ as ret -> ret in go +let step f = fun env -> f env env + let run f e = match f e with Value v -> Some v | _ -> None end @@ -123,7 +127,7 @@ type ('a, 'b) solver = ('a, 'b) t let solve : (cnf, int list) solver = strategy (fun next -> function | [] -> return [] | []::_ -> fail "unsat" - | (l::_)::_ -> + | (l::_)::_ -> (propagate l <&> next =>> add l) <|> (propagate (-l) <&> next =>> add (-l)) diff --git a/src/theories/qf_lia/interval.ml b/src/theories/qf_lia/interval.ml deleted file mode 100644 index e69de29..0000000 diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml index d83f608..eaf9b03 100644 --- a/src/theories/qf_lia/qf_lia.ml +++ b/src/theories/qf_lia/qf_lia.ml @@ -105,5 +105,89 @@ module QfLia = struct match M.solve p with | Model.UNKNOWN -> Last_effort.find_model p - | _ as r -> r + | _ as r -> r +end + +module MiniLia = struct +open Monadsat.SolverMonad + +type env = { n : int; doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } + +type res = Model.t + +type solver = (env, res) t + +let do_setv x d env = { env with doms = (x, d)::env.doms }, d +let do_update x d env = { env with doms = (x, d)::(List.remove_assoc x env.doms) } +let do_updatev x d env = do_update x d env, d + +let rec eval (x : Logic.term) = step (fun env -> + match List.assoc_opt x env.doms with + | Some v -> return v + | None -> + match x with + | Var _ -> + update (do_update x Interval.top) + | Cst v -> + update (do_update x (Interval.singleton v)) + | Add (t1, t2) -> + let* v1 = eval t1 in + let* v2 = eval t2 in + update (do_update x (Interval.add v1 v2)) +) + +let propagate_one (a : Logic.atom) = + match a with + | Logic.Eq (t1, t2) -> + let* d1 = eval t1 in + let* d2 = eval t2 in + let d = Interval.inter d1 d2 in + update (do_update t1 d) <&> update (do_update t2 d) + | Logic.Ne (t1, t2) -> + let* d1 = eval t1 in + let* d2 = eval t2 in + if d1 = d2 then + update (do_update t2 (Interval.inter d1 d2)) + else update (Fun.id) + +let propagate (f : Logic.atom list) = + List.fold_left (<&>) (update (Fun.id)) (List.map propagate_one f) + +let decide v = update (fun env -> + let x = List.hd env.vlist in + let xs = List.tl env.vlist in + let dx = Interval.singleton v in + { env with doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms + ; model = (x, v)::env.model + ; vlist = xs + } +) + +let choice = function + | [] -> assert false + | x::xs -> List.fold_left (<|>) x xs + +let extract_model (f : Logic.atom list) = strategy (fun next ({n; vlist; model; _} as env) -> + if n = 0 then abort + else let next = set {env with n = env.n - 1} <&> next in + match vlist with + | [] -> + if Checker.check_list model f then return model + else fail "extract model" + | x::_ -> + let* dx = eval (Var x) in + match Interval.split dx with + | Single v -> decide v <&> next + | Split (d1, d2) -> + let c1, c2 = Interval.peek d1, Interval.peek d2 in + choice [ + decide c1 <&> next; + decide c2 <&> next; + update (do_update (Var x) d1) <&> propagate f <&> next; + update (do_update (Var x) d2) <&> propagate f <&> next + ]) + +let generic_solver (p : Logic.atom list) = + propagate p <&> extract_model p + end \ No newline at end of file From 9877f1077c25d36425ad5b7448040750b01fbc19 Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Fri, 29 Oct 2021 00:17:47 +0200 Subject: [PATCH 03/18] fix errors in the monadic miniLia --- src/sat/monadsat.ml | 10 ++++++++++ src/theories/qf_lia/qf_lia.ml | 33 +++++++++++++++++++++++++-------- 2 files changed, 35 insertions(+), 8 deletions(-) diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml index 98b4d22..4038153 100644 --- a/src/sat/monadsat.ml +++ b/src/sat/monadsat.ml @@ -44,6 +44,8 @@ val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t val strategy : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t +val bounded_strategy : max_step:int -> (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t + val run : ('env, 'res) t -> 'env -> 'res option end = struct @@ -105,6 +107,14 @@ let strategy (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t | _ as ret -> ret in go +let bounded_strategy ~max_step (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = + let rec go n env = + if n = 0 then Abort + else match step (go n) env env with + | Update env -> go (n - 1) env + | _ as ret -> ret + in go max_step + let step f = fun env -> f env env let run f e = match f e with Value v -> Some v | _ -> None diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml index eaf9b03..733119a 100644 --- a/src/theories/qf_lia/qf_lia.ml +++ b/src/theories/qf_lia/qf_lia.ml @@ -121,19 +121,27 @@ let do_setv x d env = { env with doms = (x, d)::env.doms }, d let do_update x d env = { env with doms = (x, d)::(List.remove_assoc x env.doms) } let do_updatev x d env = do_update x d env, d +let update_dom x d = + if Interval.is_empty d then + fail "unsat" + else + update (do_update x d) + +let update_dom_ret x d = update_dom x d <&> return d + let rec eval (x : Logic.term) = step (fun env -> match List.assoc_opt x env.doms with | Some v -> return v | None -> match x with | Var _ -> - update (do_update x Interval.top) + update_dom_ret x Interval.top | Cst v -> - update (do_update x (Interval.singleton v)) + update_dom_ret x (Interval.singleton v) | Add (t1, t2) -> let* v1 = eval t1 in let* v2 = eval t2 in - update (do_update x (Interval.add v1 v2)) + update_dom_ret x (Interval.add v1 v2) ) let propagate_one (a : Logic.atom) = @@ -142,12 +150,12 @@ let propagate_one (a : Logic.atom) = let* d1 = eval t1 in let* d2 = eval t2 in let d = Interval.inter d1 d2 in - update (do_update t1 d) <&> update (do_update t2 d) + update_dom t1 d <&> update_dom t2 d | Logic.Ne (t1, t2) -> let* d1 = eval t1 in let* d2 = eval t2 in if d1 = d2 then - update (do_update t2 (Interval.inter d1 d2)) + update_dom t2 (Interval.inter d1 d2) else update (Fun.id) let propagate (f : Logic.atom list) = @@ -157,6 +165,7 @@ let decide v = update (fun env -> let x = List.hd env.vlist in let xs = List.tl env.vlist in let dx = Interval.singleton v in + Printf.printf "decide %s := %d\n" x v; { env with doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms ; model = (x, v)::env.model ; vlist = xs @@ -167,9 +176,11 @@ let choice = function | [] -> assert false | x::xs -> List.fold_left (<|>) x xs -let extract_model (f : Logic.atom list) = strategy (fun next ({n; vlist; model; _} as env) -> +let decr = update (fun env -> { env with n = env.n - 1 }) + +let extract_model (f : Logic.atom list) = strategy (fun next {n; vlist; model; _} -> if n = 0 then abort - else let next = set {env with n = env.n - 1} <&> next in + else let next = decr <&> next in match vlist with | [] -> if Checker.check_list model f then return model @@ -186,8 +197,14 @@ let extract_model (f : Logic.atom list) = strategy (fun next ({n; vlist; model; update (do_update (Var x) d1) <&> propagate f <&> next; update (do_update (Var x) d2) <&> propagate f <&> next ]) - let generic_solver (p : Logic.atom list) = propagate p <&> extract_model p +let solve p = + let vlist = Logic.lvars p in + let doms = [] in + let n = 10 in + let model = [] in + run (generic_solver p) {n; doms; model; vlist} + end \ No newline at end of file From 9ab7cb441f775225a5f3a449cfefcceb171ecc21 Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Sun, 31 Oct 2021 12:40:31 +0100 Subject: [PATCH 04/18] redesign qf_lia in a monadic style --- bin/bench.ml | 15 +- src/sat/monadsat.ml | 128 +--------------- src/solver/core.ml | 2 +- src/solver/logic.ml | 9 ++ src/solver/solver.ml | 266 ---------------------------------- src/solver/strategy.ml | 71 +++++++++ src/solver/strategy.mli | 145 ++++++++++++++++++ src/theories/qf_lia/qf_lia.ml | 146 ++++++++++++------- 8 files changed, 332 insertions(+), 450 deletions(-) delete mode 100644 src/solver/solver.ml create mode 100644 src/solver/strategy.ml create mode 100644 src/solver/strategy.mli diff --git a/bin/bench.ml b/bin/bench.ml index 9e4cfbc..a204222 100644 --- a/bin/bench.ml +++ b/bin/bench.ml @@ -1,6 +1,6 @@ open Modulus_lib +open Strategy open Monadsat -open SolverMonad let () = Random.self_init () @@ -14,16 +14,17 @@ let random_cnf () = let () = let print_result = function - | Some m -> Printf.printf " SAT : %s\n" (string_of_clause m) - | None -> Printf.printf " UNSAT\n" + | Some m -> Printf.printf " \x1b[32mSAT\x1b[0m : %s\n" (string_of_clause m) + | None -> Printf.printf " \x1b[31mUNSAT\x1b[0m\n" in + List.init 1000 (fun _ -> random_cnf ()) |> List.iteri (fun i cnf -> Printf.printf "testing unit [%d]\n" i; let r1 = Runtime.time (fun () -> Sat.solve cnf) in - let r2 = Runtime.time (fun () -> run solve cnf) in + let r2 = Runtime.time (fun () -> run_opt solve cnf) in assert (r1.result = r2.result); - Printf.printf " (old) solver result [runtime : %f] : \n" r1.time; + Printf.printf " (old) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r1.time; print_result r1.result; - Printf.printf " (new) solver result [runtime : %f] : \n" r2.time; + Printf.printf " (new) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r2.time; print_result r2.result; - ) (List.init 1000 (fun _ -> random_cnf ())) \ No newline at end of file + ) \ No newline at end of file diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml index 4038153..438e02f 100644 --- a/src/sat/monadsat.ml +++ b/src/sat/monadsat.ml @@ -1,3 +1,5 @@ +open Strategy + type clause = int list type cnf = clause list @@ -8,137 +10,23 @@ let string_of_clause c = let string_of_cnf c = "{" ^ String.concat " " (List.map string_of_clause c) ^ "}" -module SolverMonad : sig - -type ('env, 'res) status - -type ('env, 'res) t - -val return : 'res -> ('env, 'res) t - -val fail : string -> ('env, 'res) t - -val abort : ('env, 'res) t - -val update : ('env -> 'env) -> ('env, 'res) t - -val step : ('env -> ('env, 'res) t) -> ('env, 'res) t - -val set : 'env -> ('env, 'res) t - -val bind : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t -val (let*) : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t - -val fast_bind : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t -val (let+) : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t - -val (<|>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t - -val (<&>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t - -val map : ('res -> 'res1) -> ('env, 'res) t -> ('env, 'res1) t -val (=>) : ('env, 'res) t -> ('res -> 'res1) -> ('env, 'res1) t - -val fast_map : ('res -> 'res) -> ('env, 'res) t -> ('env, 'res) t -val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t - -val strategy : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t - -val bounded_strategy : max_step:int -> (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t - -val run : ('env, 'res) t -> 'env -> 'res option - -end = struct - -type ('env, 'res) status = - | Fail of string - | Abort - | Update of 'env - | Value of 'res - -type ('env, 'res) t = 'env -> ('env, 'res) status - -let fail msg = fun _ -> Fail msg - -let return v = fun _ -> Value v - -let update up = fun env -> Update (up env) - -let set env = fun _ -> Update env - -let abort = fun _ -> Abort - -let[@inline] bind m f = fun env -> - match m env with - | Value v -> f v env - | Fail f -> Fail f - | Abort -> Abort - | Update e -> Update e - -let[@inline] (let*) m f = bind m f - -let[@inline] fast_bind m f = fun env -> - match m env with - | Value v -> f v env - | _ as ret -> ret - -let[@inline] (let+) m f = fast_bind m f - -let[@inline] (<|>) (m1 : ('env, 'res) t) (m2 : ('env, 'res) t) = fun (env : 'env) -> - match m1 env with - | Fail _ | Abort -> m2 env - | _ as res -> res - -let[@inline] (<&>) (s1 : ('env, 'res) t) (s2 : ('env, 'res) t) : ('env, 'res) t = fun env -> - match s1 env with - | Update e -> s2 e - | _ as ret -> ret - -let map f m = bind m (fun r -> return (f r)) -let[@inline] (=>) = fun m f -> map f m - -let fast_map f m = fast_bind m (fun r -> return (f r)) -let[@inline] (=>>) = fun m f -> fast_map f m - -let strategy (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = - let rec go env = - match step go env env with - | Update env -> go env - | _ as ret -> ret - in go - -let bounded_strategy ~max_step (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = - let rec go n env = - if n = 0 then Abort - else match step (go n) env env with - | Update env -> go (n - 1) env - | _ as ret -> ret - in go max_step - -let step f = fun env -> f env env - -let run f e = match f e with Value v -> Some v | _ -> None -end - let remove_lit (l : int) = List.filter ((<>) l) -open SolverMonad - let propagate l = - List.filter_map (fun c -> + update @@ List.filter_map (fun c -> if List.mem l c then None else Some (remove_lit (-l) c) - ) |> SolverMonad.update + ) let add l = fun ls -> l::ls type ('a, 'b) solver = ('a, 'b) t -let solve : (cnf, int list) solver = strategy (fun next -> function +let solve = fix @@ fun recall cnf -> + match cnf with | [] -> return [] | []::_ -> fail "unsat" | (l::_)::_ -> - (propagate l <&> next =>> add l) + (propagate l <&> recall =>> add l) <|> - (propagate (-l) <&> next =>> add (-l)) -) \ No newline at end of file + (propagate (-l) <&> recall =>> add (-l)) \ No newline at end of file diff --git a/src/solver/core.ml b/src/solver/core.ml index 3c7246f..1b30931 100644 --- a/src/solver/core.ml +++ b/src/solver/core.ml @@ -26,7 +26,7 @@ let dpllt f = th atoms in solve_all cnf - |> map (call_theory QfLia.solve) + |> map (call_theory MiniLia.solve) |> find_first_sat |> function | SAT m as res -> assert (check f m = Some true); res diff --git a/src/solver/logic.ml b/src/solver/logic.ml index b45aeb4..9be6948 100644 --- a/src/solver/logic.ml +++ b/src/solver/logic.ml @@ -19,6 +19,15 @@ type formula = | Neg of formula | Atom of atom +let rec pp_term fmt = function + | Var x -> Format.fprintf fmt "%s" x + | Cst v -> Format.fprintf fmt "%d" v + | Add (t1, t2) -> Format.fprintf fmt "(%a + %a)" pp_term t1 pp_term t2 + +let pp_atom fmt = function + | Eq (t1, t2) -> Format.fprintf fmt "%a = %a" pp_term t1 pp_term t2 + | Ne (t1, t2) -> Format.fprintf fmt "%a ≠ %a" pp_term t1 pp_term t2 + module VSet = Set.Make (String) let neg_atom (a : atom) = diff --git a/src/solver/solver.ml b/src/solver/solver.ml deleted file mode 100644 index d76e49c..0000000 --- a/src/solver/solver.ml +++ /dev/null @@ -1,266 +0,0 @@ -(** - This module provides utilities to define new resolution strategies. - We introduce a monad [Solver] to build customized solvers or generate - new ones given a domain (see {!Domain}). -*) - -open Logic -open Checker -open Domain - -(** - !!! THIS MODULE IS A WORK IN PROGRESS !!! - - A generic evaluator for ground terms (see {!Logic.term}). - This module is designed to assist the programmers willing to - extend modulus solver. - - If you want add a solver for a specific theory (see {!Solver}), - this solver will require a custom evaluator. - - An evaluation function [eval] is any function associating a value to - a term for a given model (see {!Model.t}). - If a custom evaluator is not intended to evaluate a specific expression [e], - then [eval e m] should return [None] for any model [m]. -*) -module type Evaluator = sig - val eval : term -> Model.t -> int option -end - -exception Contradiction of string -exception Aborted - -module Make (D : Domain) : sig - type state = (term * D.t) list - (** Internal state of the solver *) - - type 'a status - (** - Status of the solver after an update of the internal state. - The status is either: - {ul - {- A failure (reported if the search space becomes empty)} - {- A simple value (reported if the search space is not updated)} - {- An update notification (reported if the search space has been updated)} - {- An interuption of the resolution} - } - *) - - val get : 'a status -> 'a - (** - Get the a [value] from a status report. - If the reported status is a failure or an interruption - this may raise either a [Contradiction] exception (in case of a failure) - or a [Aborted] exception (in case of an interruption). - *) - - type 'a update - (** A monad to represent functions updating the solver state *) - - val run : 'a update -> state -> 'a status - (** - Execute an update function on a given state - *) - - val return : 'a -> 'a update - (** - [return v] is an update function ignoring the state - of the solver and returning the value [v] - *) - - val update : term -> D.t -> D.t update - (** - [update t v] is an update function - which rebinds the value [v] to the term [t] in - the solver's state and return this new value. - - If [t] is already bound, intersection as defined by [D.inter] is performed - to unify the domains. Such an operation may report a failure if - the intersection results in [D.bot] ! - *) - - val fail : string -> 'a update - (** - [fail msg] is an update function always resulting in a failure - with associated error message [msg]. - *) - - val leak : state update - (** - [leak] is an update functions providing the current state of the solver - as a return value. - *) - - val (>>) : 'a update -> 'b update -> 'b update - (** - if [f] and [g] are 2 update functions, [f >> g] is the update - function performing first [f] and then [g]. - *) - - val (<|>) : 'a update -> 'a update -> 'a update - (** - if [f] and [g] are 2 update functions, [f <|> g] is an update function - trying first to apply [f] and fallbacks to [g] if [f] failed. - *) - - (** TODO : fix operator *) - (* val fix : 'a update -> 'a update *) - - val generic_solver : atom list -> Model.t update - (** - A generic solver generated using the [update] monad. - *) - - val solve : atom list -> Model.answer - (** - Ready to be used version of [generic_solver]. - *) -end = struct - -type state = (term * D.t) list - -type 'a status = - | Value of 'a - | Update of state * 'a - | Fail of string - | Abort - -type 'a update = state -> 'a status - -let[@inline] run f s = f s - -let return (v : 'a) : 'a update = fun _ -> Value v - -let update (t : term) (v : 'a) : 'a update = fun s -> - match List.assoc_opt t s with - | Some v' -> - if v = v' then Value v' else - let d = D.inter v v' in - if D.is_empty d then - Fail (Format.asprintf "update failed %a ∩ %a = %a" - D.pp_print v D.pp_print v' D.pp_print d) - else Update ((t, d)::List.remove_assoc t s, d) - | None -> - Update ((t, v)::s, v) - -let get (s : 'a status) : 'a = - match s with - | Abort -> raise Aborted - | Fail l -> raise (Contradiction l) - | Value v -> v - | Update (_, v) -> v - -let leak : state update = fun s -> Value s - -let fail msg = fun _ -> Fail msg - -let abort = fun _ -> Abort - -let (let*) (m : 'a update) (f : 'a -> 'b update) : 'b update = fun s -> - match m s with - | Abort -> Abort - | Fail _ as err -> err - | Value v -> f v s - | Update (e, v) -> - match f v e with - | Value v -> Update (e, v) - | _ as ret -> ret - -let rec eval (x : term) : D.t update = fun s -> - match List.assoc_opt x s with - | Some v -> Value v - | None -> - match x with - | Var _ -> update x D.top s - | Cst v -> update x (D.singleton v) s - | Add (t1, t2) -> - begin - let* v1 = eval t1 in - let* v2 = eval t2 in - update x (D.add v1 v2) - end s - -let (>>) (f : 'a update) (g : 'b update) : 'b update = - let* _ = f in g - -let (<|>) (u1 : 'a update) (u2 : 'b update) : 'b update = fun s -> - match u1 s with - | Fail _ -> u2 s - | _ as r -> r - -let propagate_one (a : atom) : unit update = - match a with - | Eq (t1, t2) -> - let* d1 = eval t1 in - let* d2 = eval t2 in - let d = D.inter d1 d2 in - update t1 d >> update t2 d >> return () - | Ne (t1, t2) -> - let* d1 = eval t1 in - let* d2 = eval t2 in - if d1 = d2 then - update t1 D.bot >> update t2 D.bot >> return () - else - return () - -let propagate_one_backward (a: atom) : unit update = - let rec step (t : term) (dt : D.t) : unit update = - match t with - | Cst _ | Var _ -> update t dt >> return () - | Add (t1, t2) -> - let* d1 = eval t1 in - let* d2 = eval t2 in - let (d1', d2') = D.add_inv d1 d2 dt in - step t1 d1' >> step t2 d2' >> return () - in - match a with - | Eq (t1, t2) -> - let* d1 = eval t1 in - let* d2 = eval t2 in - step t1 d1 >> step t2 d2 - | Ne _ -> return () - -let sequence (l : 'a list) (p : 'a -> unit update) : unit update = - List.fold_left (>>) (return ()) (List.map p l) - -let propagate l : unit update = - sequence l propagate_one - >> sequence l propagate_one_backward - -let extract_model (p : atom list) = - let rec step depth vlist (model : Model.t) : Model.t update = - if depth <= 0 then abort else - match vlist with - | [] -> - if check_list model p - then return model - else fail "extract model" - | x::xs -> - let* dx = eval (Var x) in - let decide x v = update (Var x) (D.singleton v) >> propagate p in - match D.split dx with - | Split (d1, d2) -> - let c1, c2 = D.peek d1, D.peek d2 in - (decide x c1 >> (step (depth - 1) xs ((x, c1)::model))) - <|> - (decide x c2 >> (step (depth - 1) xs ((x, c2)::model))) - <|> - (update (Var x) d1 >> propagate p >> step (depth - 1) vlist model) - <|> - (update (Var x) d2 >> propagate p >> step (depth - 1) vlist model) - | Single v -> - step (depth - 1) xs ((x, v)::model) - in - step 512 (lvars p) [] - -let generic_solver (p : atom list) = - propagate p >> extract_model p - -let solve (p : atom list) = - let go = propagate p >> extract_model p in - try Model.SAT (get (go [])) - with - | Aborted -> Model.UNKNOWN - | Contradiction _ -> Model.UNSAT - -end \ No newline at end of file diff --git a/src/solver/strategy.ml b/src/solver/strategy.ml new file mode 100644 index 0000000..e60cd58 --- /dev/null +++ b/src/solver/strategy.ml @@ -0,0 +1,71 @@ +type ('env, 'res) status = + | Fail of string + | Abort + | Update of 'env + | UpdateValue of 'env * 'res + | Value of 'res + +type ('env, 'res) t = 'env -> ('env, 'res) status + +let fail msg = fun _ -> Fail msg + +let return v = fun _ -> Value v + +let update up = fun env -> Update (up env) + +let update_ret v f = fun env -> UpdateValue (f env, v) + +let set env = fun _ -> Update env + +let abort = fun _ -> Abort + +let[@inline] bind m f = fun env -> + match m env with + | Value v -> f v env + | Fail f -> Fail f + | Abort -> Abort + | Update e -> Update e + | UpdateValue (e, v) -> f v e + +let[@inline] (let*) m f = bind m f + +let[@inline] fast_bind m f = fun env -> + match m env with + | Value v -> f v env + | _ as ret -> ret + +let[@inline] (let+) m f = fast_bind m f + +let[@inline] (<|>) (m1 : ('env, 'res) t) (m2 : ('env, 'res) t) = fun (env : 'env) -> + match m1 env with + | Fail _ | Abort -> m2 env + | _ as res -> res + +let[@inline] (<&>) (s1 : ('env, 'res) t) (s2 : ('env, 'res) t) : ('env, 'res) t = fun env -> + match s1 env with + | Update e -> s2 e + | _ as ret -> ret + +let map f m = bind m (fun r -> return (f r)) +let[@inline] (=>) = fun m f -> map f m + +let fast_map f m = fast_bind m (fun r -> return (f r)) +let[@inline] (=>>) = fun m f -> fast_map f m + +let fix (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = + let rec go env = + match step go env env with + | Update env -> go env + | _ as ret -> ret + in go + +let step f = fun env -> f env env + +let run f e = f e + +let run_opt f e = + match f e with + | Value v -> Some v + | _ -> None + +let () msg m = fun env -> Printf.printf "%s\n" msg; m env \ No newline at end of file diff --git a/src/solver/strategy.mli b/src/solver/strategy.mli new file mode 100644 index 0000000..604d166 --- /dev/null +++ b/src/solver/strategy.mli @@ -0,0 +1,145 @@ +(** + This module provides utilities to define new resolution strategies. + We introduce a monad [('env, 'res) Strategy.t] to build customized solvers. + + Intuitively, a value of type [('env, 'res) Strategy.t] is a function from ['env -> 'res] + where ['env] is the type of resolution contexts and ['res] is the result of the strategy. + + A strategy may or may not return a valid result. To modelize this situation, the stragegies results are + wrapped in the the [('env, 'res) status] type in order to give additional + information on strategies executions. + + The call [run s e] executes the strategy [s] in context [e] and return a status information. +*) + +type ('env, 'res) status = + | Fail of string + | Abort + | Update of 'env + | UpdateValue of 'env * 'res + | Value of 'res +(** + Status message reported by strategies. + The status is either: + {ul + {- A failure with a message } + {- A value indicating that the strategy successfully computed a result } + {- An update notification indicating that the strategy is not done } + {- An update notification together with an intermediate value. + This indicate that the strategy computed an intermediate value [v] + and updated the environment. It is especially useful to compose intermediate steps. + } + {- A forced interruption of the strategy } + } +*) + +type ('env, 'res) t + +val return : 'res -> ('env, 'res) t +(** [return v] is a trivial strategy always returning [v] *) + +val fail : string -> ('env, 'res) t +(** [fail err] is a trivial strategy always failing with error message [err] *) + +val abort : ('env, 'res) t +(** [abort] is a trivial strategy always returning an interruption notification *) + +val update : ('env -> 'env) -> ('env, 'res) t +(** + [update f] is a strategy applying function [f] to its current environment and + returning the corresponding update notification +*) + +val update_ret : 'res -> ('env -> 'env) -> ('env, 'res) t +(** + [update_ret f v] is similar to [update v] but also returns the + intermediate value [v] +*) + +val step : ('env -> ('env, 'res) t) -> ('env, 'res) t +(** + [step] is used to choose which strategy to apply given a current environment. + If [f] is a function from ['env] to [('env, 'res) t] (that is, a function computing a + strategy given an environment), then [step f] is the strategy which first apply [f] to + its input environnement, and then apply the resulting strategy. +*) + +val set : 'env -> ('env, 'res) t +(** [set env] is a strategy replacing its current environnement with [env] + and returning an update notification. +*) + +val bind : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t +(** + [bind s f] first applies strategy [s]. If the result is a value [v], + then the strategy [f v] is applied, otherwise the + status message of [s] is propagated. +*) + +val (let*) : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t +(** Notation for [bind] *) + +val fast_bind : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t +(** + [fast_bind s f] is exactly like [bind s f] but requires the result types of [s] + and [f] to match. It is usually faster to use [fast_bind] that [fast] in this case. +*) + +val (let+) : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t +(** Notation for [fast_bind] *) + +val (<|>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t +(** + [s1 <|> s2] is the strategy which first tries to apply strategy [s1] + and then apply strategy [s2] is strategy [s1] failed. +*) + +val () : string -> ('env, 'res) t -> ('env, 'res) t +(** + [msg s] is a strategy printing the message [msg] to [stdout] and then applying + strategy [s] +*) + +val (<&>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t +(** + [s1 <&> s2] is a strategy which first applies strategy [s1] and then applies + strategy [s2] if [s1] returned an update notification. [s2] is executed in + the new environnement returned by [s1]. +*) + +val map : ('res -> 'res1) -> ('env, 'res) t -> ('env, 'res1) t +(** [map f s] is the strategy which first executes strategy [s] and then + apply [f] to its result. +*) + +val (=>) : ('env, 'res) t -> ('res -> 'res1) -> ('env, 'res1) t +(** Notation for [map] *) + +val fast_map : ('res -> 'res) -> ('env, 'res) t -> ('env, 'res) t +(** Same as [map f s] but requires [f] to be of type ['a -> 'a]. + [map f s] is usually faster in this case. +*) + +val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t +(** Notation for [fast_map] *) + +val fix : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t +(** + [fix] computes the fixpoint of a strategy. + + If [step] is a function computing a strategy given a strategy [recall] and a context [env], + [fix step] computes a recursive strategy which is similar to [step] but where + every call to the strategy [recall] are recursive calls to the strategy [step] itself. +*) + +val run : ('env, 'res) t -> 'env -> ('env, 'res) status +(** + [run s e] executes strategy [s] in environnement [e] +*) + +val run_opt : ('env, 'res) t -> 'env -> 'res option +(** + [run_opt s e] is similar to [run s e] but convert the resulting [status] + message to an optional value. If [s] returns only a value [v] in context [e], [run_opt s e] is [Some v] + otherwise, [run_opt s e] is [None]. +*) diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml index 733119a..7fc11e7 100644 --- a/src/theories/qf_lia/qf_lia.ml +++ b/src/theories/qf_lia/qf_lia.ml @@ -7,6 +7,7 @@ *) open Domain +open Strategy module Interval : Domain = struct @@ -99,91 +100,121 @@ let peek = function end -module QfLia = struct - module M = Solver.Make (Interval) - let solve p = - match M.solve p with - | Model.UNKNOWN -> - Last_effort.find_model p - | _ as r -> r -end -module MiniLia = struct -open Monadsat.SolverMonad -type env = { n : int; doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } +let asp = Format.asprintf -type res = Model.t +module DomMap = struct +type t = { n : int; doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } -type solver = (env, res) t +let rec pp_print fmt = function + | [] -> () + | (x, d)::next -> + Format.fprintf fmt "%a := %a, %a" + Logic.pp_term x + Interval.pp_print d + pp_print next -let do_setv x d env = { env with doms = (x, d)::env.doms }, d -let do_update x d env = { env with doms = (x, d)::(List.remove_assoc x env.doms) } -let do_updatev x d env = do_update x d env, d +let set_dom_aux x d env = + { env with doms = (x, d)::env.doms } -let update_dom x d = - if Interval.is_empty d then - fail "unsat" - else - update (do_update x d) +let set_dom x d = update (set_dom_aux x d) -let update_dom_ret x d = update_dom x d <&> return d +let set_ret_dom x d = update_ret d (set_dom_aux x d) -let rec eval (x : Logic.term) = step (fun env -> +let rec eval (x : Logic.term) = step @@ fun env -> + (* asp "evaluating %a in ctx [%a...]" Logic.pp_term x pp_print env.doms *) match List.assoc_opt x env.doms with - | Some v -> return v + | Some v -> + (* asp "find %a := %a" Logic.pp_term x Interval.pp_print v *) + return v | None -> match x with | Var _ -> - update_dom_ret x Interval.top - | Cst v -> - update_dom_ret x (Interval.singleton v) + (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.top) *) + set_ret_dom x Interval.top + | Cst v -> + (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.singleton v) *) + set_ret_dom x (Interval.singleton v) | Add (t1, t2) -> let* v1 = eval t1 in let* v2 = eval t2 in - update_dom_ret x (Interval.add v1 v2) -) + (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.add v1 v2) *) + set_ret_dom x (Interval.add v1 v2) + +let update_dom x d = + (* asp "update %a := %a" Logic.pp_term x Interval.pp_print d *) + let* dx = eval x in + let dx' = Interval.inter dx d in + if Interval.is_empty dx' then + fail "unsat" + else update @@ fun env -> + { env with doms = (x, d)::(List.remove_assoc x env.doms) } + +let update_ret_dom x d = update_dom x d <&> return d +end + +module MiniLia = struct + +type solver = (DomMap.t, Model.t) t +open DomMap + +let no_update = update (Fun.id) + +let debug = step @@ fun env -> + asp "In ctx [%a...]" pp_print env.doms no_update + +let rec propagate_one_back t d = + let open Logic in + (* asp "propagating backward %a := %a" Logic.pp_term t Interval.pp_print d *) + match t with + | Cst _ | Var _ -> update_dom t d + | Add (t1, t2) -> + let* d1 = eval t1 in + let* d2 = eval t2 in + let (d1', d2') = Interval.add_inv d1 d2 d in + propagate_one_back t1 d1' <&> propagate_one_back t2 d2' let propagate_one (a : Logic.atom) = + (* asp "propagating %a" Logic.pp_atom a *) match a with | Logic.Eq (t1, t2) -> let* d1 = eval t1 in let* d2 = eval t2 in let d = Interval.inter d1 d2 in - update_dom t1 d <&> update_dom t2 d + propagate_one_back t1 d <&> propagate_one_back t2 d | Logic.Ne (t1, t2) -> let* d1 = eval t1 in let* d2 = eval t2 in - if d1 = d2 then - update_dom t2 (Interval.inter d1 d2) - else update (Fun.id) - + if d1 = d2 then fail "unsat" + else no_update + let propagate (f : Logic.atom list) = - List.fold_left (<&>) (update (Fun.id)) (List.map propagate_one f) + (* asp "propagate" *) + List.fold_left (<&>) no_update (List.map propagate_one f) -let decide v = update (fun env -> +let decide v = step (fun env -> let x = List.hd env.vlist in let xs = List.tl env.vlist in let dx = Interval.singleton v in - Printf.printf "decide %s := %d\n" x v; - { env with doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms - ; model = (x, v)::env.model - ; vlist = xs - } + (* asp "decide %s := %d" x v *) + set { env with doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms + ; model = (x, v)::env.model + ; vlist = xs + } ) let choice = function - | [] -> assert false + | [] -> fail "no choice" | x::xs -> List.fold_left (<|>) x xs -let decr = update (fun env -> { env with n = env.n - 1 }) - -let extract_model (f : Logic.atom list) = strategy (fun next {n; vlist; model; _} -> +let rec extract_model (n : int) (f : Logic.atom list) = step @@ fun {vlist; model; _} -> + let next = extract_model (n/2) f in + let next_decision = extract_model (n - 1) f in if n = 0 then abort - else let next = decr <&> next in - match vlist with + else match vlist with | [] -> - if Checker.check_list model f then return model + if Checker.check_list model f then "found model !" return model else fail "extract model" | x::_ -> let* dx = eval (Var x) in @@ -192,19 +223,22 @@ let extract_model (f : Logic.atom list) = strategy (fun next {n; vlist; model; _ | Split (d1, d2) -> let c1, c2 = Interval.peek d1, Interval.peek d2 in choice [ - decide c1 <&> next; - decide c2 <&> next; - update (do_update (Var x) d1) <&> propagate f <&> next; - update (do_update (Var x) d2) <&> propagate f <&> next - ]) + decide c1 <&> next_decision; + decide c2 <&> next_decision; + update_dom (Var x) d1 <&> propagate f <&> next; + update_dom (Var x) d2 <&> propagate f <&> next + ] + let generic_solver (p : Logic.atom list) = - propagate p <&> extract_model p + propagate p <&> debug <&> extract_model 64 p let solve p = let vlist = Logic.lvars p in let doms = [] in let n = 10 in let model = [] in - run (generic_solver p) {n; doms; model; vlist} - + match run (generic_solver p) {n; doms; model; vlist} with + | Fail _ -> Model.UNSAT + | Value m -> Model.SAT m + | _ -> Last_effort.find_model p end \ No newline at end of file From a4a17895a992ed6f56e7fae2711a278272e5d3ce Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Sun, 31 Oct 2021 13:35:21 +0100 Subject: [PATCH 05/18] cleaning and documentation of the new monad --- src/sat/monadsat.ml | 2 +- src/solver/strategy.ml | 7 ++- src/solver/strategy.mli | 12 +++-- src/theories/qf_lia/qf_lia.ml | 95 +++++++++++++++++++++++------------ 4 files changed, 76 insertions(+), 40 deletions(-) diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml index 438e02f..4fa544a 100644 --- a/src/sat/monadsat.ml +++ b/src/sat/monadsat.ml @@ -22,7 +22,7 @@ let add l = fun ls -> l::ls type ('a, 'b) solver = ('a, 'b) t -let solve = fix @@ fun recall cnf -> +let solve = ffix @@ fun recall cnf -> match cnf with | [] -> return [] | []::_ -> fail "unsat" diff --git a/src/solver/strategy.ml b/src/solver/strategy.ml index e60cd58..64cf364 100644 --- a/src/solver/strategy.ml +++ b/src/solver/strategy.ml @@ -52,13 +52,18 @@ let[@inline] (=>) = fun m f -> map f m let fast_map f m = fast_bind m (fun r -> return (f r)) let[@inline] (=>>) = fun m f -> fast_map f m -let fix (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = +let ffix (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = let rec go env = match step go env env with | Update env -> go env | _ as ret -> ret in go +(* let rec fix s env = + match s env with + | Update env -> fix s env + | _ as ret -> ret *) + let step f = fun env -> f env env let run f e = f e diff --git a/src/solver/strategy.mli b/src/solver/strategy.mli index 604d166..057b18f 100644 --- a/src/solver/strategy.mli +++ b/src/solver/strategy.mli @@ -61,11 +61,11 @@ val step : ('env -> ('env, 'res) t) -> ('env, 'res) t [step] is used to choose which strategy to apply given a current environment. If [f] is a function from ['env] to [('env, 'res) t] (that is, a function computing a strategy given an environment), then [step f] is the strategy which first apply [f] to - its input environnement, and then apply the resulting strategy. + its input environment, and then apply the resulting strategy. *) val set : 'env -> ('env, 'res) t -(** [set env] is a strategy replacing its current environnement with [env] +(** [set env] is a strategy replacing its current environment with [env] and returning an update notification. *) @@ -104,7 +104,7 @@ val (<&>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t (** [s1 <&> s2] is a strategy which first applies strategy [s1] and then applies strategy [s2] if [s1] returned an update notification. [s2] is executed in - the new environnement returned by [s1]. + the new environment returned by [s1]. *) val map : ('res -> 'res1) -> ('env, 'res) t -> ('env, 'res1) t @@ -123,13 +123,15 @@ val fast_map : ('res -> 'res) -> ('env, 'res) t -> ('env, 'res) t val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t (** Notation for [fast_map] *) -val fix : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t +val ffix : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t (** - [fix] computes the fixpoint of a strategy. + [ffix] computes the fixpoint of a parametrized strategy. If [step] is a function computing a strategy given a strategy [recall] and a context [env], [fix step] computes a recursive strategy which is similar to [step] but where every call to the strategy [recall] are recursive calls to the strategy [step] itself. + The recursion continues while [step] returns an update notification. + It may not terminates ! *) val run : ('env, 'res) t -> 'env -> ('env, 'res) status diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml index 7fc11e7..bc2c022 100644 --- a/src/theories/qf_lia/qf_lia.ml +++ b/src/theories/qf_lia/qf_lia.ml @@ -1,9 +1,7 @@ (** {1 Lia} - The Modulus internal solver for LIA - - Disclaimer : this module is a "work in progress" + Modulus internal solver for QF_LIA *) open Domain @@ -101,11 +99,18 @@ let peek = function end +(** Alias for {!Format.asprintf} *) +let info = Format.asprintf -let asp = Format.asprintf - +(** + A module describing the resolution environments +*) module DomMap = struct -type t = { n : int; doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } + +(** A context is a record including a mapping from terms to intervals, + a list of unbounded variables and a partial model. +*) +type t = { doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } let rec pp_print fmt = function | [] -> () @@ -115,58 +120,76 @@ let rec pp_print fmt = function Interval.pp_print d pp_print next -let set_dom_aux x d env = - { env with doms = (x, d)::env.doms } - -let set_dom x d = update (set_dom_aux x d) - -let set_ret_dom x d = update_ret d (set_dom_aux x d) +(** [set_dom_aux x d] is a strategy which binds domain [d] to the term [x] + assuming [x] was unbound. This strategy returns [d] as return value. +*) +let set_dom x d = + let set_dom_aux x d env = + { env with doms = (x, d)::env.doms } + in update_ret d (set_dom_aux x d) +(** [eval x] is a strategy which evaluates the term [x] in the current environment. + If [x] is not bound to a domain, [eval x] binds [x] to {!Interval.top} first. +*) let rec eval (x : Logic.term) = step @@ fun env -> - (* asp "evaluating %a in ctx [%a...]" Logic.pp_term x pp_print env.doms *) + (* info "evaluating %a in ctx [%a...]" Logic.pp_term x pp_print env.doms *) match List.assoc_opt x env.doms with | Some v -> - (* asp "find %a := %a" Logic.pp_term x Interval.pp_print v *) + (* info "find %a := %a" Logic.pp_term x Interval.pp_print v *) return v | None -> match x with | Var _ -> - (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.top) *) - set_ret_dom x Interval.top + (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.top) *) + set_dom x Interval.top | Cst v -> - (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.singleton v) *) - set_ret_dom x (Interval.singleton v) + (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.singleton v) *) + set_dom x (Interval.singleton v) | Add (t1, t2) -> let* v1 = eval t1 in let* v2 = eval t2 in - (* asp "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.add v1 v2) *) - set_ret_dom x (Interval.add v1 v2) + (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.add v1 v2) *) + set_dom x (Interval.add v1 v2) +(** [update_dom x d] is a strategy which update the domain of [x] with domain [d]. + If [x] is already bound to a domain [d'], the domain of [x] is set to be the intersection + [Interval.inter d d']. If the intersection is {!Interval.bot}, the strategy fails. +*) let update_dom x d = - (* asp "update %a := %a" Logic.pp_term x Interval.pp_print d *) + (* info "update %a := %a" Logic.pp_term x Interval.pp_print d *) let* dx = eval x in let dx' = Interval.inter dx d in if Interval.is_empty dx' then fail "unsat" else update @@ fun env -> { env with doms = (x, d)::(List.remove_assoc x env.doms) } - -let update_ret_dom x d = update_dom x d <&> return d end +(** + A mini monadic solver for QF_LIA +*) module MiniLia = struct +(** A solver is a strategy which operates on environments of type {!DomMap.t} and + returns a {!Model.t}. +*) type solver = (DomMap.t, Model.t) t open DomMap +(** A strategy doing nothing *) let no_update = update (Fun.id) +(** A strategy printing its current environment *) let debug = step @@ fun env -> - asp "In ctx [%a...]" pp_print env.doms no_update + info "In ctx [%a...]" pp_print env.doms no_update +(** A strategy performing backward propagation. + [propagate_one_back t d] assumes that term [t] should evaluates to domain [d] + and consequently propagates this information to all subterms of [t]. +*) let rec propagate_one_back t d = let open Logic in - (* asp "propagating backward %a := %a" Logic.pp_term t Interval.pp_print d *) + (* info "propagating backward %a := %a" Logic.pp_term t Interval.pp_print d *) match t with | Cst _ | Var _ -> update_dom t d | Add (t1, t2) -> @@ -175,8 +198,13 @@ let rec propagate_one_back t d = let (d1', d2') = Interval.add_inv d1 d2 d in propagate_one_back t1 d1' <&> propagate_one_back t2 d2' +(** A strategy performing constraint propagation. + [propagate_one c] propagate the constraint [c] in the current + environment, thus restraining the domains. + It may fails if the constraints [c] is insatisfiable in the context. +*) let propagate_one (a : Logic.atom) = - (* asp "propagating %a" Logic.pp_atom a *) + (* info "propagating %a" Logic.pp_atom a *) match a with | Logic.Eq (t1, t2) -> let* d1 = eval t1 in @@ -189,16 +217,18 @@ let propagate_one (a : Logic.atom) = if d1 = d2 then fail "unsat" else no_update +(** [propagate f] is a strategy +*) let propagate (f : Logic.atom list) = - (* asp "propagate" *) + (* info "propagate" *) List.fold_left (<&>) no_update (List.map propagate_one f) let decide v = step (fun env -> let x = List.hd env.vlist in let xs = List.tl env.vlist in let dx = Interval.singleton v in - (* asp "decide %s := %d" x v *) - set { env with doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms + (* info "decide %s := %d" x v *) + set { doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms ; model = (x, v)::env.model ; vlist = xs } @@ -214,7 +244,7 @@ let rec extract_model (n : int) (f : Logic.atom list) = step @@ fun {vlist; mode if n = 0 then abort else match vlist with | [] -> - if Checker.check_list model f then "found model !" return model + if Checker.check_list model f then return model else fail "extract model" | x::_ -> let* dx = eval (Var x) in @@ -230,14 +260,13 @@ let rec extract_model (n : int) (f : Logic.atom list) = step @@ fun {vlist; mode ] let generic_solver (p : Logic.atom list) = - propagate p <&> debug <&> extract_model 64 p + propagate p <&> extract_model 16 p let solve p = let vlist = Logic.lvars p in let doms = [] in - let n = 10 in let model = [] in - match run (generic_solver p) {n; doms; model; vlist} with + match run (generic_solver p) { doms; model; vlist } with | Fail _ -> Model.UNSAT | Value m -> Model.SAT m | _ -> Last_effort.find_model p From a3078e439c1156d5fbb7862fe8f02ad8a99ef49c Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Wed, 27 Oct 2021 21:37:14 +0200 Subject: [PATCH 06/18] chore: add minilib dependency --- .gitmodules | 3 +++ lib/minilib | 1 + 2 files changed, 4 insertions(+) create mode 100644 .gitmodules create mode 160000 lib/minilib diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..9c975c9 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "lib/minilib"] + path = lib/minilib + url = git@github.com:SolarLiner/minilib.git diff --git a/lib/minilib b/lib/minilib new file mode 160000 index 0000000..dd1ab2b --- /dev/null +++ b/lib/minilib @@ -0,0 +1 @@ +Subproject commit dd1ab2bfea11dea60c15809d63768dd6103ca667 From ecbd1a7507d7f34f303b19daf08c0a6733e8dcb9 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Wed, 27 Oct 2021 22:02:37 +0200 Subject: [PATCH 07/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index dd1ab2b..3d274f8 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit dd1ab2bfea11dea60c15809d63768dd6103ca667 +Subproject commit 3d274f8fa1b068a3b977cca380fe5da5192b92cb From d7c609aa306339a1dd7a1b3187b01484947ee309 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Wed, 27 Oct 2021 23:49:20 +0200 Subject: [PATCH 08/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index 3d274f8..65f989c 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit 3d274f8fa1b068a3b977cca380fe5da5192b92cb +Subproject commit 65f989c80fb82fb6a109485ddae019e6971c9c6b From e9140f7d95c35352a3eb95779085171e575d009b Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Thu, 28 Oct 2021 11:33:37 +0200 Subject: [PATCH 09/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index 65f989c..35d61d3 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit 65f989c80fb82fb6a109485ddae019e6971c9c6b +Subproject commit 35d61d3a8321e7c5820ead49418d998310ef968b From 122815a7c74ca991a2d8b48ef3f441629da908e8 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Thu, 28 Oct 2021 11:33:51 +0200 Subject: [PATCH 10/18] wip: use minilib --- src/dune | 3 ++- src/utils/parsing.ml | 61 -------------------------------------------- src/utils/sexp.ml | 50 ++++++++++++++---------------------- 3 files changed, 21 insertions(+), 93 deletions(-) delete mode 100644 src/utils/parsing.ml diff --git a/src/dune b/src/dune index 1856b71..36da497 100644 --- a/src/dune +++ b/src/dune @@ -2,4 +2,5 @@ (library (public_name modulus.modulus_lib) - (name modulus_lib)) + (name modulus_lib) + (libraries minicat minicat_ext minilib)) diff --git a/src/utils/parsing.ml b/src/utils/parsing.ml deleted file mode 100644 index ab5001f..0000000 --- a/src/utils/parsing.ml +++ /dev/null @@ -1,61 +0,0 @@ -open Lstream - -type ('i, 'o) presult = ('o * 'i t) option - -type ('i, 'o) parser = 'i t -> ('i, 'o) presult - -let zero _ = None - -let return x = fun i -> Some (x, i) - -let (>>=) p fp = fun i -> - match p i with - | None -> None - | Some (o, i') -> fp o i' - -let any : ('a, 'a) parser = fun inp -> - match Lazy.force inp with - | Nil -> None - | Cons (x, i) -> Some (x, i) - -let satisfy test = - any >>= (fun res -> if test res then return res else zero) - -let eof x = function - | Nil -> Some (x, Nil) - | Cons _ -> None - -let (=>) x f = x >>= fun r -> return (f r) - -let (>>) x y = x >>= fun _ -> y - -let (<<) x y = x >>= fun r -> y >>= fun _ -> return r - -let (<~>) x xs = x >>= fun r -> xs >>= fun rs -> return (r :: rs) - -let (<|>) p p' = fun i -> - match p i with - | None -> p' i - | Some _ as r -> r - -let option default x = x <|> return default - -let rec many p = option [] (p >>= fun r -> many p >>= fun rs -> return (r :: rs)) - -let many1 p = p <~> many p - -let char (c : char) = satisfy ((=) c) - -let digit = satisfy (function '0'..'9' -> true | _ -> false) - -let implode x = String.concat "" @@ List.map (String.make 1) x - -let number = many1 digit => implode => int_of_string - -let alpha = - satisfy (function 'a'..'z' | 'A'..'Z' -> true | _ -> false) - -let spaces = - many (satisfy (function '\n' | '\t' | ' ' -> true | _ -> false)) - -let (let*) = (>>=) \ No newline at end of file diff --git a/src/utils/sexp.ml b/src/utils/sexp.ml index 2238227..9d4a083 100644 --- a/src/utils/sexp.ml +++ b/src/utils/sexp.ml @@ -1,5 +1,6 @@ -open Lstream -open Parsing +open Minilib.Parsing +open Minicat.Monad.Make(Minilib.Parsing) +open Minicat.Alternative.Make(Minilib.Parsing) type sexp = | Sym of string @@ -7,41 +8,28 @@ type sexp = | Cons of sexp list let ident = - spaces >> - many1 (alpha <|> char '-') => (fun x -> Sym (implode x)) - << spaces + let open Fold(Minicat_ext.Seq_ext) in (* < provides [many1] over [Seq.t] *) + let+ sym = token (many1 (alpha <|> char '-')) in + Sym (String.of_seq sym) let operator = - spaces >> ( - char '+' - <|> char '-' - <|> char '/' - <|> char '*' - <|> char '=' - <|> char '%' - ) << spaces => (fun x -> Sym (String.make 1 x)) - + let op' = ['+';'-';'/';'*';'=';'%'] |> List.map char |> choice in + let+ op = token op' in + Sym (String.make 1 op) let num = - spaces >> - number => (fun x -> Int x) - << spaces + let open Fold(Minicat_ext.Seq_ext) in + let+ chars = many1 digit in + let num = String.of_seq chars |> int_of_string in + Int num let atom = ident <|> num <|> operator -let parens p = - spaces >> char '(' >> p << char ')' << spaces +let parens p = surround (token (char '(')) (token (char ')')) p -let rec parse_sexp i = - begin - atom - <|> - parens (many parse_sexp => (fun r -> Cons r)) - end i +let sexp = + let call sexp = let+ vals = many sexp in Cons vals in + fix (fun sexp -> parens (call sexp) <|> atom) -let of_string s = - Lstream.of_string s |> many1 parse_sexp +let of_string s = parse_string sexp s -let of_file f = - open_in f - |> of_channel - |> many1 parse_sexp \ No newline at end of file +let of_file f = parse_file sexp f \ No newline at end of file From 0e0921dcbc86d7f123552e6a54f37ccd186105f9 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 30 Oct 2021 11:35:58 +0200 Subject: [PATCH 11/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index 35d61d3..495864a 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit 35d61d3a8321e7c5820ead49418d998310ef968b +Subproject commit 495864a1eac9ad233a99a1bd794b5beb13028676 From 64e5e47fae2be58d13e144224a147d03840d17bf Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 30 Oct 2021 11:37:07 +0200 Subject: [PATCH 12/18] fix: update sexp module to use minilib parsing --- src/utils/sexp.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/utils/sexp.ml b/src/utils/sexp.ml index 9d4a083..ce01048 100644 --- a/src/utils/sexp.ml +++ b/src/utils/sexp.ml @@ -22,14 +22,16 @@ let num = let num = String.of_seq chars |> int_of_string in Int num -let atom = ident <|> num <|> operator +let atom = ident <|> num <|> operator "atom" -let parens p = surround (token (char '(')) (token (char ')')) p +let parens p = surround (token (char '(')) (token (char ')')) p "parentheses" let sexp = let call sexp = let+ vals = many sexp in Cons vals in - fix (fun sexp -> parens (call sexp) <|> atom) + fix (fun sexp -> parens (call sexp) <|> atom "fix") "sexp" -let of_string s = parse_string sexp s +let parser = many sexp <* eof -let of_file f = parse_file sexp f \ No newline at end of file +let of_string s = parse_string parser s + +let of_file f = parse_file parser f From c6c4079e26cf553e32badbf5547a0b871d44d542 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 30 Oct 2021 11:40:30 +0200 Subject: [PATCH 13/18] fix: update solver loop from sexp module --- src/solver/loop.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/solver/loop.ml b/src/solver/loop.ml index 983d476..1e541cf 100644 --- a/src/solver/loop.ml +++ b/src/solver/loop.ml @@ -108,7 +108,7 @@ let exec_one ctx sxp = let batch f = match Sexp.of_file f with - | Some (sxp, rem) when (Lazy.force rem = Nil) -> + | Ok sxp -> List.fold_left exec_one { tenv = Hashtbl.create 50; state = Start_mode; @@ -116,19 +116,23 @@ let batch f = logic = ALL; model = UNKNOWN; } sxp - | _ -> Printf.eprintf "parse error\n"; exit 1 + | Error (err, off) -> Printf.eprintf "%d: parse error: %s\n" off err; exit 1 let repl () = let rec step ctx = flush stderr; Printf.printf "> "; match Sexp.of_string (read_line ()) with - | None | Some ([], _) | Some (_::_::_, _) -> - Printf.eprintf "(error \"this command is incorrect\")\n"; - step ctx - | Some ([s], _) -> + | Ok [s] -> begin try step (exec_one ctx s) with Exit -> exit 0 + end + | Ok _ -> + Printf.eprintf "(error \"This command is incorrect\")"; + step ctx + | Error (err, off) -> + Printf.eprintf "(error %S)\n" (Printf.sprintf "Parse error: %d: %s" off err); + step ctx in step { tenv = Hashtbl.create 50; From a4201d7ad87d1f2d08b39db4488e17d0e0663547 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 30 Oct 2021 23:31:01 +0200 Subject: [PATCH 14/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index 495864a..d1b7987 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit 495864a1eac9ad233a99a1bd794b5beb13028676 +Subproject commit d1b7987f8e5bd921f4544aa3d6beef7406c1fd02 From e59af69242d75a4e1e45a1be2e2fd8af3a3c058e Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 30 Oct 2021 23:31:40 +0200 Subject: [PATCH 15/18] fix: sexp parser --- src/utils/sexp.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/utils/sexp.ml b/src/utils/sexp.ml index ce01048..b33fd02 100644 --- a/src/utils/sexp.ml +++ b/src/utils/sexp.ml @@ -22,15 +22,15 @@ let num = let num = String.of_seq chars |> int_of_string in Int num -let atom = ident <|> num <|> operator "atom" +let atom = token (ident <|> num <|> operator) "atom" let parens p = surround (token (char '(')) (token (char ')')) p "parentheses" let sexp = let call sexp = let+ vals = many sexp in Cons vals in - fix (fun sexp -> parens (call sexp) <|> atom "fix") "sexp" + fix (fun sexp -> (parens (call sexp) <|> atom) "fix") "sexp" -let parser = many sexp <* eof +let parser = many sexp let of_string s = parse_string parser s From f426ab21820bcb53aef7a299d5f460e29678125c Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sun, 31 Oct 2021 15:36:33 +0100 Subject: [PATCH 16/18] ci: recurse through submodules on checkout --- .github/workflows/ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 66d4fe0..6d9d93c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,6 +10,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v2 + with: + submodules: recursive - name: Set up OCaml uses: ocaml/setup-ocaml@v1.1.11 with: From f5975041df0588ca3ed8a210ef7da18381567af0 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 6 Nov 2021 13:15:39 +0100 Subject: [PATCH 17/18] chore: use minicat to explicit all monads --- src/sat/monadsat.ml | 15 ++-- src/solver/strategy.ml | 100 +++++++++++++----------- src/solver/strategy.mli | 138 ++++++++++------------------------ src/theories/qf_lia/qf_lia.ml | 29 ++++--- 4 files changed, 124 insertions(+), 158 deletions(-) diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml index 4fa544a..61dcf89 100644 --- a/src/sat/monadsat.ml +++ b/src/sat/monadsat.ml @@ -1,9 +1,14 @@ -open Strategy - type clause = int list type cnf = clause list +module S = Strategy.Make(struct type t = cnf end) + +open Strategy +open S +open Minicat.Monad.Make(S) +open Minicat.Alternative.Make(S) + let string_of_clause c = "{" ^ String.concat " " (List.map string_of_int c) ^ "}" @@ -20,13 +25,13 @@ let propagate l = let add l = fun ls -> l::ls -type ('a, 'b) solver = ('a, 'b) t +type 'a solver = 'a t let solve = ffix @@ fun recall cnf -> match cnf with | [] -> return [] | []::_ -> fail "unsat" | (l::_)::_ -> - (propagate l <&> recall =>> add l) + (propagate l <&> recall |> map (add l)) <|> - (propagate (-l) <&> recall =>> add (-l)) \ No newline at end of file + (propagate (-l) <&> recall |> map (add (-l))) \ No newline at end of file diff --git a/src/solver/strategy.ml b/src/solver/strategy.ml index 64cf364..d8d5620 100644 --- a/src/solver/strategy.ml +++ b/src/solver/strategy.ml @@ -7,9 +7,12 @@ type ('env, 'res) status = type ('env, 'res) t = 'env -> ('env, 'res) status -let fail msg = fun _ -> Fail msg - -let return v = fun _ -> Value v +let[@inline] coerce_status : (('env, 'a) status -> ('env, 'b) status) = + function + | Value _ | UpdateValue _ -> assert false + | Fail _ as x -> x + | Abort as x -> x + | Update _ as x -> x let update up = fun env -> Update (up env) @@ -19,58 +22,67 @@ let set env = fun _ -> Update env let abort = fun _ -> Abort -let[@inline] bind m f = fun env -> - match m env with - | Value v -> f v env - | Fail f -> Fail f - | Abort -> Abort - | Update e -> Update e - | UpdateValue (e, v) -> f v e +let run f e = f e + +let run_opt f e = + match f e with + | Value v -> Some v + | _ -> None + +module Make(Env: sig type t end) : sig + include Minicat.Monad.MONAD with type 'a t = (Env.t -> (Env.t, 'a) status) + include Minicat.Alternative.ALTERNATIVE with type 'a t := 'a t + + val ffix : ('a t -> Env.t -> 'a t) -> 'a t -let[@inline] (let*) m f = bind m f + val step : (Env.t -> 'a t) -> 'a t -let[@inline] fast_bind m f = fun env -> - match m env with - | Value v -> f v env - | _ as ret -> ret + val (<&>) : 'a t -> 'a t -> 'a t -let[@inline] (let+) m f = fast_bind m f + val () : string -> 'a t -> 'a t +end = struct -let[@inline] (<|>) (m1 : ('env, 'res) t) (m2 : ('env, 'res) t) = fun (env : 'env) -> - match m1 env with - | Fail _ | Abort -> m2 env - | _ as res -> res + type 'res t = Env.t -> (Env.t, 'res) status -let[@inline] (<&>) (s1 : ('env, 'res) t) (s2 : ('env, 'res) t) : ('env, 'res) t = fun env -> - match s1 env with - | Update e -> s2 e - | _ as ret -> ret + let empty = fun _ -> Abort -let map f m = bind m (fun r -> return (f r)) -let[@inline] (=>) = fun m f -> map f m + let fail msg = fun _ -> Fail msg -let fast_map f m = fast_bind m (fun r -> return (f r)) -let[@inline] (=>>) = fun m f -> fast_map f m + let pure v = fun _ -> Value v -let ffix (step : ('env, 'res) t -> 'env -> ('env, 'res) t) : ('env, 'res) t = - let rec go env = - match step go env env with - | Update env -> go env + let[@inline] bind m f = fun env -> + match m env with + | Value v -> f v env + | UpdateValue (e, v) -> f v e + | x -> coerce_status x + + let[@inline] alt m1 m2 = fun (env : Env.t) -> + match m1 env with + | Fail _ | Abort -> m2 env + | _ as res -> res + + let[@inline] (<&>) s1 s2 = fun env -> + match s1 env with + | Update e -> s2 e | _ as ret -> ret - in go -(* let rec fix s env = - match s env with - | Update env -> fix s env - | _ as ret -> ret *) + let map f m = bind m (fun r -> pure (f r)) -let step f = fun env -> f env env + let app fm xm = bind fm (fun f -> map f xm) -let run f e = f e + let ffix (step : 'a t -> Env.t -> 'a t) : 'a t = + let rec go env = + match step go env env with + | Update env -> go env + | _ as ret -> ret + in go -let run_opt f e = - match f e with - | Value v -> Some v - | _ -> None + (* let rec fix s env = + match s env with + | Update env -> fix s env + | _ as ret -> ret *) + + let step f = fun env -> f env env -let () msg m = fun env -> Printf.printf "%s\n" msg; m env \ No newline at end of file + let () msg m = fun env -> Printf.printf "%s\n" msg; m env +end \ No newline at end of file diff --git a/src/solver/strategy.mli b/src/solver/strategy.mli index 057b18f..96cb8aa 100644 --- a/src/solver/strategy.mli +++ b/src/solver/strategy.mli @@ -13,7 +13,7 @@ *) type ('env, 'res) status = - | Fail of string + Fail of string | Abort | Update of 'env | UpdateValue of 'env * 'res @@ -33,108 +33,22 @@ type ('env, 'res) status = } *) -type ('env, 'res) t +type ('env, 'a) t -val return : 'res -> ('env, 'res) t -(** [return v] is a trivial strategy always returning [v] *) +val update : ('env -> 'env) -> ('env, 'a) t +(** [update f] updates the environment of the strategy monad by applying [f] on it, and saving the result. *) -val fail : string -> ('env, 'res) t -(** [fail err] is a trivial strategy always failing with error message [err] *) +val update_ret : 'a -> ('env -> 'env) -> ('env, 'a) t +(** [update_ret v f] updates the environment like [update f], but also combines it wdith a [pure v] as the return value. *) -val abort : ('env, 'res) t -(** [abort] is a trivial strategy always returning an interruption notification *) +val set : 'env -> ('env, 'a) t +(** [set env] replaces the current environment by the one provided in [env]. It is the equivalent of [update (Fun.const env)]. *) -val update : ('env -> 'env) -> ('env, 'res) t -(** - [update f] is a strategy applying function [f] to its current environment and - returning the corresponding update notification -*) - -val update_ret : 'res -> ('env -> 'env) -> ('env, 'res) t -(** - [update_ret f v] is similar to [update v] but also returns the - intermediate value [v] -*) +val abort : ('env, 'a) t +(** Aborts computation immediately. *) -val step : ('env -> ('env, 'res) t) -> ('env, 'res) t -(** - [step] is used to choose which strategy to apply given a current environment. - If [f] is a function from ['env] to [('env, 'res) t] (that is, a function computing a - strategy given an environment), then [step f] is the strategy which first apply [f] to - its input environment, and then apply the resulting strategy. -*) -val set : 'env -> ('env, 'res) t -(** [set env] is a strategy replacing its current environment with [env] - and returning an update notification. -*) - -val bind : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t -(** - [bind s f] first applies strategy [s]. If the result is a value [v], - then the strategy [f v] is applied, otherwise the - status message of [s] is propagated. -*) - -val (let*) : ('env, 'res) t -> ('res -> ('env, 'res2) t) -> ('env, 'res2) t -(** Notation for [bind] *) - -val fast_bind : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t -(** - [fast_bind s f] is exactly like [bind s f] but requires the result types of [s] - and [f] to match. It is usually faster to use [fast_bind] that [fast] in this case. -*) - -val (let+) : ('env, 'res) t -> ('res -> ('env, 'res) t) -> ('env, 'res) t -(** Notation for [fast_bind] *) - -val (<|>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t -(** - [s1 <|> s2] is the strategy which first tries to apply strategy [s1] - and then apply strategy [s2] is strategy [s1] failed. -*) - -val () : string -> ('env, 'res) t -> ('env, 'res) t -(** - [msg s] is a strategy printing the message [msg] to [stdout] and then applying - strategy [s] -*) - -val (<&>) : ('env, 'res) t -> ('env, 'res) t -> ('env, 'res) t -(** - [s1 <&> s2] is a strategy which first applies strategy [s1] and then applies - strategy [s2] if [s1] returned an update notification. [s2] is executed in - the new environment returned by [s1]. -*) - -val map : ('res -> 'res1) -> ('env, 'res) t -> ('env, 'res1) t -(** [map f s] is the strategy which first executes strategy [s] and then - apply [f] to its result. -*) - -val (=>) : ('env, 'res) t -> ('res -> 'res1) -> ('env, 'res1) t -(** Notation for [map] *) - -val fast_map : ('res -> 'res) -> ('env, 'res) t -> ('env, 'res) t -(** Same as [map f s] but requires [f] to be of type ['a -> 'a]. - [map f s] is usually faster in this case. -*) - -val (=>>) : ('env, 'res) t -> ('res -> 'res) -> ('env, 'res) t -(** Notation for [fast_map] *) - -val ffix : (('env, 'res) t -> 'env -> ('env, 'res) t) -> ('env, 'res) t -(** - [ffix] computes the fixpoint of a parametrized strategy. - - If [step] is a function computing a strategy given a strategy [recall] and a context [env], - [fix step] computes a recursive strategy which is similar to [step] but where - every call to the strategy [recall] are recursive calls to the strategy [step] itself. - The recursion continues while [step] returns an update notification. - It may not terminates ! -*) - -val run : ('env, 'res) t -> 'env -> ('env, 'res) status +val run : ('env, 'a) t -> 'env -> ('env, 'a) status (** [run s e] executes strategy [s] in environnement [e] *) @@ -145,3 +59,33 @@ val run_opt : ('env, 'res) t -> 'env -> 'res option message to an optional value. If [s] returns only a value [v] in context [e], [run_opt s e] is [Some v] otherwise, [run_opt s e] is [None]. *) + +(** Creates the strategy monad, passing in an instance of the environment type. *) +module Make : + functor (Env : sig type t end) -> + sig + include Minicat.Monad.MONAD with type 'a t = (Env.t, 'a) t + include Minicat.Alternative.ALTERNATIVE with type 'a t := 'a t + + val ffix : ('a t -> Env.t -> 'a t) -> 'a t + (** + [ffix] computes the fixpoint of a parametrized strategy. + If [step] is a function computing a strategy given a strategy [recall] and a context [env], + [fix step] computes a recursive strategy which is similar to [step] but where + every call to the strategy [recall] are recursive calls to the strategy [step] itself. + The recursion continues while [step] returns an update notification. + It may not terminates ! + *) + + val step : (Env.t -> 'a t) -> 'a t + (** + [step] is used to choose which strategy to apply given a current environment. + If [f] is a function from ['env] to [('env, 'res) t] (that is, a function computing a + strategy given an environment), then [step f] is the strategy which first apply [f] to + its input environment, and then apply the resulting strategy. + *) + + val (<&>) : 'a t -> 'a t -> 'a t + + val () : string -> 'a t -> 'a t + end diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml index bc2c022..fc016e3 100644 --- a/src/theories/qf_lia/qf_lia.ml +++ b/src/theories/qf_lia/qf_lia.ml @@ -106,11 +106,16 @@ let info = Format.asprintf A module describing the resolution environments *) module DomMap = struct +module Typedef = struct + (** A context is a record including a mapping from terms to intervals, + a list of unbounded variables and a partial model. + *) + type t = { doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } +end -(** A context is a record including a mapping from terms to intervals, - a list of unbounded variables and a partial model. -*) -type t = { doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t } +include Typedef +module S = Strategy.Make(Typedef) +open Minicat.Monad.Make(S) let rec pp_print fmt = function | [] -> () @@ -131,7 +136,7 @@ let set_dom x d = (** [eval x] is a strategy which evaluates the term [x] in the current environment. If [x] is not bound to a domain, [eval x] binds [x] to {!Interval.top} first. *) -let rec eval (x : Logic.term) = step @@ fun env -> +let rec eval (x : Logic.term) = S.step @@ fun env -> (* info "evaluating %a in ctx [%a...]" Logic.pp_term x pp_print env.doms *) match List.assoc_opt x env.doms with | Some v -> @@ -160,7 +165,7 @@ let update_dom x d = let* dx = eval x in let dx' = Interval.inter dx d in if Interval.is_empty dx' then - fail "unsat" + S.fail "unsat" else update @@ fun env -> { env with doms = (x, d)::(List.remove_assoc x env.doms) } end @@ -170,11 +175,15 @@ end *) module MiniLia = struct +open DomMap +open DomMap.S +open Minicat.Monad.Make(DomMap.S) +open Minicat.Alternative.Make(DomMap.S) + (** A solver is a strategy which operates on environments of type {!DomMap.t} and returns a {!Model.t}. *) -type solver = (DomMap.t, Model.t) t -open DomMap +type solver = Model.t t (** A strategy doing nothing *) let no_update = update (Fun.id) @@ -234,10 +243,6 @@ let decide v = step (fun env -> } ) -let choice = function - | [] -> fail "no choice" - | x::xs -> List.fold_left (<|>) x xs - let rec extract_model (n : int) (f : Logic.atom list) = step @@ fun {vlist; model; _} -> let next = extract_model (n/2) f in let next_decision = extract_model (n - 1) f in From f27e14fe51ac00f308e808af96683a2f9fb3c566 Mon Sep 17 00:00:00 2001 From: Nathan Graule Date: Sat, 6 Nov 2021 18:15:04 +0100 Subject: [PATCH 18/18] chore: sync minilib --- lib/minilib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/minilib b/lib/minilib index d1b7987..f439454 160000 --- a/lib/minilib +++ b/lib/minilib @@ -1 +1 @@ -Subproject commit d1b7987f8e5bd921f4544aa3d6beef7406c1fd02 +Subproject commit f4394545ade8ea0a705e05087697b3d488f884b5