Cubicle 1.1.2 documentation and source : Enumsolver.Make.clear

let clear () =
  (* let empty_theory = Th.empty () in *)
  env.is_unsat <- false;
  env.unsat_core <- [];
  env.clauses <- Vec.make 0 dummy_clause; 
  env.learnts <- Vec.make 0 dummy_clause; 
  env.clause_inc <- 1.;
  env.var_inc <- 1.;
  env.vars <- Vec.make 0 dummy_var; 
  env.qhead <- 0;
  env.simpDB_assigns <- -1;
  env.simpDB_props <- 0;
  env.order <- Iheap.init 0; (* sera mis a jour dans solve *)
  env.progress_estimate <- 0.;
  env.restart_first <- 100;
  env.starts <- 0;
  env.decisions <- 0;
  env.propagations <- 0;
  env.conflicts <- 0;
  env.clauses_literals <- 0;
  env.learnts_literals <- 0;
  env.max_literals <- 0;
  env.tot_literals <- 0;
  env.nb_init_vars <- 0;
  env.nb_init_clauses <- 0;
  env.model <- Vec.make 0 dummy_var;
  env.trail <- Vec.make 601 dummy_atom;
  env.trail_lim <- Vec.make 601 (-105);
  (* env.tenv <- empty_theory; *)
  (* env.tenv_queue <- Vec.make 100 (empty_theory); *)
  (* env.tatoms_queue <- Queue.create (); *)
  Enumsolver_types.clear ()