diff --git a/Makefile b/Makefile index 942abc33..8b9ca617 100644 --- a/Makefile +++ b/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) diff --git a/_tags b/_tags index 31793d6e..154f72ec 100644 --- a/_tags +++ b/_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 : include : include diff --git a/src/core/internal.ml b/src/core/internal.ml index 5fac1e30..4eec8c1c 100644 --- a/src/core/internal.ml +++ b/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 diff --git a/src/main.ml b/src/main.ml index 2c7abeec..47750217 100644 --- a/src/main.ml +++ b/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 diff --git a/src/util/iheap.ml b/src/util/iheap.ml index 25bbbb18..157bf969 100644 --- a/src/util/iheap.ml +++ b/src/util/iheap.ml @@ -11,6 +11,8 @@ (* *) (**************************************************************************) +[@@@landmark "auto"] + module V = Sparse_vec type t = {heap : int Vec.t; indices : int V.t } diff --git a/src/util/vec.ml b/src/util/vec.ml index b3b248f6..98f2880d 100644 --- a/src/util/vec.ml +++ b/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()=