SolarLiner/category

.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:

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "lib/minilib"]
+	path = lib/minilib
+	url = git@github.com:SolarLiner/minilib.git

bin/bench.ml

@@ -0,0 +1,30 @@
+open Modulus_lib
+open Strategy
+open Monadsat
+
+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 "  \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_opt solve cnf) in
+    assert (r1.result = r2.result);
+    Printf.printf "  (old) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r1.time;
+    print_result r1.result;
+    Printf.printf "  (new) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r2.time;
+    print_result r2.result;
+  )

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

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 }

src/dune

@@ -2,4 +2,5 @@
 
 (library
  (public_name modulus.modulus_lib)
- (name modulus_lib))
+ (name modulus_lib)
+ (libraries minicat minicat_ext minilib))

src/sat/monadsat.ml

@@ -0,0 +1,37 @@
+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) ^ "}"
+
+let string_of_cnf c =
+  "{" ^ String.concat " " (List.map string_of_clause c) ^ "}"
+
+let remove_lit (l : int) = List.filter ((<>) l)
+
+let propagate l =
+  update @@ List.filter_map (fun c ->
+    if List.mem l c then None
+    else Some (remove_lit (-l) c)
+  )
+
+let add l = fun ls -> l::ls
+
+type 'a solver = 'a t
+
+let solve = ffix @@ fun recall cnf ->
+  match cnf with
+  | [] -> return []
+  | []::_ -> fail "unsat"
+  | (l::_)::_ ->
+    (propagate l <&> recall |> map (add l))
+    <|>
+    (propagate (-l) <&> recall |> map (add (-l)))

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

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) =

src/solver/loop.ml

@@ -108,27 +108,31 @@ 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;
       stack = [];
       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;