From d19b798ee928e5bb6cc5fe9923f65270a92b7fb0 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 11 Apr 2018 19:57:51 -0500
Subject: [PATCH] add ability to parse and process dimacs files

---
 src/main/jbuild       |  3 ++-
 src/main/main.ml      | 37 +++++++++++++++---------------
 src/smtlib/Process.ml | 52 +++++++++++++++++++++++++++++++++++++++++++
 src/util/Util.ml      |  1 +
 4 files changed, 74 insertions(+), 19 deletions(-)

diff --git a/src/main/jbuild b/src/main/jbuild
index a621ea0d..1d585f3b 100644
--- a/src/main/jbuild
+++ b/src/main/jbuild
@@ -8,7 +8,8 @@
    (public_name dagon)
    (package dagon)
    (libraries (containers sequence result
-               dagon.sat dagon.smt dagon.smtlib dagon.backend))
+               dagon.sat dagon.smt dagon.smtlib dagon.backend
+               dagon.dimacs))
    (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
diff --git a/src/main/main.ml b/src/main/main.ml
index e3811dd9..1fe66323 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -129,27 +129,28 @@ let main () =
     Dagon_smt.Solver.create ~theories ()
   in
   let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
-  let res = match syn with
+  begin match syn with
     | Smtlib ->
       (* parse pb *)
-      Dagon_smtlib.parse !file >>= fun input ->
-      (* TODO: parse list of plugins on CLI *)
-      (* process statements *)
-      begin
-        try
-          E.fold_l
-            (fun () ->
-               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
-                 solver)
-            () input
-        with Exit ->
-          E.return()
-      end
+      Dagon_smtlib.parse !file
     | Dimacs ->
-      assert false (* TODO *)
+      Dagon_dimacs.parse !file >|= fun cs ->
+      List.map (fun c -> Ast.Assert_bool c) cs
+  end
+  >>= fun input ->
+  (* process statements *)
+  let res =
+    try
+      E.fold_l
+        (fun () ->
+           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
+             solver)
+        () input
+    with Exit ->
+      E.return()
   in
   if !p_stat then (
     Format.printf "%a@." Dagon_smt.Solver.pp_stats solver;
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 027c3f9a..aa05e71d 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -207,6 +207,54 @@ end
 let conv_ty = Conv.conv_ty
 let conv_term = Conv.conv_term
 
+(** {2 Terms for Dimacs atoms} *)
+module I_atom : sig
+  val mk_t : Term.state -> int -> Term.t
+  val mk_atom : Term.state -> int -> Lit.t
+end = struct
+  open Solver_types
+
+  type _ Term.custom +=
+    | Atom of int (* absolute *)
+
+  let pp _ out = function Atom i -> Fmt.int out i | _ -> assert false
+  let eq _ a b = match a, b with Atom a, Atom b -> a = b | _ -> false
+  let hash _ = function Atom i -> CCHash.int i | _ -> 0
+  let get_ty _ _ = Ty.prop
+  let is_semantic _ = false
+  let solve a b = match a, b with
+    | Atom a, Atom b when a=b -> Solve_ok {subst=[]}
+    | _ -> assert false
+  let sub _ _ = ()
+  let abs ~self _ = self, true
+  let relevant _ _ = ()
+  let subst _ _ : _ option = None
+  let explain _ _ _ = []
+
+  let tc : Term_cell.tc = {
+    Term_cell.
+    tc_t_pp = pp;
+    tc_t_equal = eq;
+    tc_t_hash = hash;
+    tc_t_ty = get_ty;
+    tc_t_is_semantic = is_semantic;
+    tc_t_solve = solve;
+    tc_t_sub = sub;
+    tc_t_abs = abs;
+    tc_t_relevant = relevant;
+    tc_t_subst = subst;
+    tc_t_explain = explain
+  }
+
+  let[@inline] mk_t tst i =
+    assert (i>=0);
+    Term.custom tst ~tc (Atom i)
+
+  let[@inline] mk_atom tst i =
+    let a = mk_t tst (Pervasives.abs i) in
+    Lit.atom ~sign:(i>0) a
+end
+
 (* call the solver to check-sat *)
 let solve
     ?gc:_
@@ -312,6 +360,10 @@ let process_stmt
          *)
       Solver.assume solver (IArray.singleton (Lit.atom t));
       E.return()
+    | A.Assert_bool l ->
+      let c = List.rev_map (I_atom.mk_atom tst) l in
+      Solver.assume solver (IArray.of_list c);
+      E.return ()
     | A.Goal (_, _) ->
       Util.errorf "cannot deal with goals yet"
     | A.Data _ ->
diff --git a/src/util/Util.ml b/src/util/Util.ml
index 29d55bdf..39ae1a16 100644
--- a/src/util/Util.ml
+++ b/src/util/Util.ml
@@ -42,3 +42,4 @@ let setup_gc () =
 
 module Int_set = CCSet.Make(CCInt)
 module Int_map = CCMap.Make(CCInt)
+module Int_tbl = CCHashtbl.Make(CCInt)