Cubicle 1.1.2 documentation and source : Solver.Make.clear

let clear () =
  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.tenv <- Th.empty ();
  env.model <- Vec.make 0 dummy_var;
  env.trail <- Vec.make 601 dummy_atom;
  env.trail_lim <- Vec.make 601 (-105);
  env.tenv_queue <- Vec.make 100 (Th.empty ());
  env.tatoms_queue <- Queue.create ();
  Solver_types.clear ()