test: add regression tests and icnf parser for assumptions

Makefile

@@ -21,8 +21,10 @@ build-dev:
 	@dune build $(OPTS) @install
 
 test:
-	@echo "run API tests…"
+	@echo "run tests…"
 	@dune runtest
+
+test-full: test
 	@echo "run benchmarks…"
 	@/usr/bin/time -f "%e" ./tests/run sat
 

src/core/Internal.ml

@@ -331,10 +331,9 @@ module Make(Plugin : PLUGIN)
   module Clause = struct
     type t = clause
 
-    let make =
+    let make_a =
       let n = ref 0 in
-      fun ?tag ali premise ->
-        let atoms = Array.of_list ali in
+      fun ?tag atoms premise ->
         let name = !n in
         incr n;
         { name;
@@ -345,6 +344,8 @@ module Make(Plugin : PLUGIN)
           activity = 0.;
           cpremise = premise}
 
+    let make ?tag l premise = make_a ?tag (Array.of_list l) premise
+
     let empty = make [] (History [])
     let name = name_of_clause
     let[@inline] equal c1 c2 = c1==c2
@@ -2009,6 +2010,10 @@ module Make(Plugin : PLUGIN)
     cleanup_ st;
     assume st ?tag cls
 
+  let[@inline] add_clause_a st c : unit =
+    let c = Clause.make_a c Hyp in
+    add_clause st c
+
   let[@inline] add_clause st ?tag c : unit =
     cleanup_ st;
     let c = Clause.make ?tag c Hyp in

src/core/Solver_intf.ml

@@ -411,6 +411,9 @@ module type S = sig
   val add_clause : t -> ?tag:int -> atom list -> unit
   (** Lower level addition of clauses *)
 
+  val add_clause_a : t -> atom array -> unit
+  (** Lower level addition of clauses *)
+
   val solve : t -> ?assumptions:atom list -> unit -> res
   (** Try and solves the current set of clauses.
       @param assumptions additional atomic assumptions to be temporarily added.

src/core/Vec.ml

@@ -94,6 +94,7 @@ let exists p t = Sequence.exists p @@ to_seq t
 let for_all p t = Sequence.for_all p @@ to_seq t
 let fold f acc a = Sequence.fold f acc @@ to_seq a
 let to_list a = Sequence.to_list @@ to_seq a
+let to_array a = Array.sub a.data 0 a.sz
 
 let of_list l : _ t =
   match l with

src/core/Vec.mli

@@ -12,6 +12,8 @@ val create : unit -> 'a t
 val to_list : 'a t -> 'a list
 (** Returns the list of elements of the vector *)
 
+val to_array : 'a t -> 'a array
+
 val of_list : 'a list -> 'a t
 
 val to_seq : 'a t -> 'a Sequence.t

src/sat/Expr_sat.ml

@@ -23,6 +23,8 @@ let _make i =
   end else
     raise Bad_atom
 
+let to_int i = i
+
 (** *)
 let neg a = - a
 

src/sat/Expr_sat.mli

@@ -14,6 +14,8 @@ include Solver_intf.FORMULA
 val make : int -> t
 (** Make a proposition from an integer. *)
 
+val to_int : t -> int
+
 val fresh : unit -> t
 (** Make a fresh atom *)
 

tests/Makefile

@@ -0,0 +1,8 @@
+
+test-icnf:
+	@for i in regression/*.icnf ; do \
+		echo "test problem $$i"; \
+		./icnf-solve/icnf_solve.exe $$i > regression/.`basename $$i`.out 2>/dev/null ; \
+		diff regression/.`basename $$i`.out regression/.`basename $$i`.ref \
+		  || ( echo "mismatch for $$i" ; exit 1) ; \
+	 done

tests/dune

@@ -12,4 +12,8 @@
  (deps    test_api.exe)
  (action  (run %{deps})))
 
+(alias
+ (name    runtest)
+ (deps    ./icnf-solve/icnf_solve.exe Makefile (source_tree regression))
+ (action  (run make test-icnf)))
 

tests/icnf-solve/Icnf_solve.ml

@@ -0,0 +1,131 @@
+
+module Vec = Msat.Vec
+
+module Parse : sig
+  type 'a event =
+    | Add_clause of 'a array
+    | Solve of 'a array
+
+  type 'a t
+
+  val make : file:string -> (int -> 'a) -> 'a t
+
+  val next : 'a t -> 'a event (** @raise End_of_file when done *)
+end = struct
+  module L = Lexer
+
+  type 'a event =
+    | Add_clause of 'a array
+    | Solve of 'a array
+
+  type 'a t = {
+    mk: int -> 'a;
+    vec: 'a Vec.t;
+    lex: Lexing.lexbuf;
+  }
+
+  let make ~file mk : _ t =
+    let ic = open_in file in
+    let lex = Lexing.from_channel ic in
+    at_exit (fun () -> close_in_noerr ic);
+    {lex; vec=Vec.create(); mk; }
+
+  let rec next (self:_ t) : _ event =
+    match L.token self.lex with
+    | L.EOF -> raise End_of_file
+    | L.A ->
+      let c = read_ints self in
+      Solve c
+    | L.I 0 ->
+      Add_clause [| |]
+    | L.I x ->
+      let c = read_ints ~first:(self.mk x) self in
+      Add_clause c
+  and read_ints ?first self : _ array =
+    Vec.clear self.vec; (* reuse local vec *)
+    CCOpt.iter (Vec.push self.vec) first;
+    let rec aux() =
+      match L.token self.lex with
+      | L.I 0 -> Vec.to_array self.vec (* done *)
+      | L.I n ->
+        let x = self.mk n in
+        Vec.push self.vec x;
+        aux()
+      | L.A -> failwith "unexpected \"a\""
+      | L.EOF -> failwith "unexpected end of file"
+    in
+    aux()
+end
+
+module Solver = struct
+  module F = Msat_sat.Expr
+  module S = Msat_sat
+  type t = S.t
+
+  let make () = S.create()
+  let mklit s i = S.make_atom s (let v = F.make (abs i) in if i>0 then v else F.neg v)
+  let add_clause s c = S.add_clause_a s c; true
+  let to_int a : int = F.to_int @@ S.Atom.formula a
+  let solve s ass =
+    let ass = Array.to_list ass in
+    match S.solve ~assumptions:ass s () with
+    | S.Sat _ -> true
+    | S.Unsat _ -> false
+end
+
+let solve_with_solver ~debug file : unit =
+  Printf.eprintf "c process %S\n%!" file;
+  let s = Solver.make () in
+  let pp_arr out a =
+    Array.iter (fun lit -> Printf.fprintf out "%d " (Solver.to_int lit)) a;
+  in
+  let p = Parse.make ~file (Solver.mklit s) in
+  let rec process_problem () =
+    match Parse.next p with
+    | Parse.Add_clause c ->
+      if debug then (
+        Printf.printf "add_clause %a\n%!" pp_arr c;
+      );
+      let r = Solver.add_clause s c in
+      if r then process_problem()
+      else (
+        Printf.printf "UNSAT\n%!";
+        skip_problem ()
+      )
+    | Parse.Solve assumptions ->
+      if debug then (
+        Printf.printf "c solve %a\n%!" pp_arr assumptions;
+      );
+      let r = Solver.solve s assumptions in
+      Printf.printf "%s\n%!" (if r then "SAT" else "UNSAT");
+      (* next problem! *)
+      process_problem()
+    | exception End_of_file ->
+      done_ ()
+  and skip_problem() =
+    match Parse.next p with
+    | Parse.Add_clause _ -> skip_problem()
+    | Parse.Solve _ -> process_problem ()
+    | exception End_of_file -> done_ ()
+  and done_ () =
+    Printf.eprintf "c done for %S\n%!" file;
+    ()
+  in
+  process_problem ()
+
+let solve_with_file ~debug file : unit =
+  try solve_with_solver ~debug file
+  with e ->
+    Printf.printf "error while solving %S:\n%s"
+    file (Printexc.to_string e);
+    exit 1
+
+let () =
+  let files = ref [] in
+  let debug = ref false in
+  let opts = [
+    "-d", Arg.Set debug, " debug";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> files := f :: !files) "icnf_solve [options] <file>";
+  List.iter (fun f -> solve_with_file ~debug:!debug f) !files;
+  ()

tests/icnf-solve/dune

@@ -0,0 +1,6 @@
+(executable
+  (name icnf_solve)
+  (modes native)
+  (libraries containers msat msat_sat))
+
+(ocamllex (modules lexer))

tests/icnf-solve/lexer.mll

@@ -0,0 +1,28 @@
+
+{
+  type token = A | I of int | EOF
+}
+
+let space = [' ' '\t']
+let nat = (['0'-'9'])+
+let int = ('-' nat) | nat
+
+rule token = parse
+  | '\n' { Lexing.new_line lexbuf; token lexbuf }
+  | space { token lexbuf }
+  | 'c' { skip_line lexbuf }
+  | 'p' { skip_line lexbuf }
+  | int { let i = int_of_string (Lexing.lexeme lexbuf) in I i }
+  | 'a' { A }
+  | eof { EOF }
+  | _ as c
+    {
+      let msg = Printf.sprintf "lexer fails on char %c\n" c in
+      failwith msg
+    }
+
+and skip_line = parse
+  | '\n' { Lexing.new_line lexbuf; token lexbuf }
+  | eof { EOF }
+  | _ { skip_line lexbuf }
+

tests/regression/.regression1.icnf.ref

@@ -0,0 +1,473 @@
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT

tests/regression/.regression2.icnf.ref

@@ -0,0 +1,249 @@
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT
+SAT
+SAT
+SAT
+SAT
+SAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+UNSAT
+SAT
+SAT