问OCaml回溯链接

EN

CC = ocamlc
LIBES = str.cma
CFLAGS = -g -c
.PHONY : clean 
dpll:   
    -rm -f dpll
    $(CC) $(CFLAGS) dpll.ml 
    $(CC) -o dpll $(LIBES) dpll.cmo
    make clean
test:   
    ./dpll input.cnf
clean: 
    rm -f *.cmi *.cmo

let dpll_SAT  = 
  try 
    let cnf = read_cnf Sys.argv.(1) in
    let state = create_state [] cnf in
    let (result, ass) = dpll state in
    match result with 
|false -> print_string "the cnf clauses are not satisfiable\n"
|_-> print_string "The cnf clauses are satisfiable and a model is as follows:\n"; 
    print_assignment ass;;
with
|x ->   
  print_endline ("Backtrace: "^(Printexc.get_backtrace ()));
  raise x)

 Backtrace: (Program not linked with -g, cannot print stack backtrace)

 Fatal error: exception Not_found
(Program not linked with -g, cannot print stack backtrace)