Use landmarks for profiling

Makefile

@@ -23,6 +23,9 @@ bin:
 	$(COMP) $(FLAGS) $(BIN)
 	cp $(BIN) $(NAME) && rm $(BIN)
 
+bench: bin
+	OCAML_LANDMARKS=on,output=temporary,format=json ./$(NAME) tests/pigeon/hole8.cnf
+
 test_bin:
 	$(COMP) $(FLAGS) $(TEST_BIN)
 

_tags

@@ -4,6 +4,9 @@ true: bin_annot, color(always)
 # optimization options
 true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 
+# landmarks profiling
+<**/*>: package(landmarks), package(landmarks.ppx)
+
 # Include paths
 <src>: include
 <src/core>: include

src/core/internal.ml

@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+[@@@landmark "auto"]
+
 module Make
     (St : Solver_types.S)
     (Plugin : Plugin_intf.S with type term = St.term

src/main.ml

@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+[@@@landmark "auto"]
+
 exception Incorrect_model
 exception Out_of_time
 exception Out_of_space

src/util/iheap.ml

@@ -11,6 +11,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+[@@@landmark "auto"]
+
 module V = Sparse_vec
 
 type t = {heap : int Vec.t; indices : int V.t }

src/util/vec.ml

@@ -11,6 +11,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+[@@@landmark "auto"]
+
 type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
 
 let _size_too_big()=