Cubicle 1.1.2 documentation and source : Enumsolver.Make.solve

let solve () = 
  (* printf "------------SMT---------------@."; *)
  (* for i = 0 to Vec.size env.vars - 1 do *)
  (*   let v = Vec.get env.vars i in *)
  (*   if v.level = 0 then *)
  (*     printf "%a@." Debug.atom (if v.pa.is_true then v.pa else v.na); *)
  (* done; *)
  (* for i = 0 to Vec.size env.clauses - 1 do *)
  (*   printf "%a@." Debug.clause (Vec.get env.clauses i); *)
  (* done; *)
  (* printf "------------smt---------------@."; *)
  if env.is_unsat then raise (Unsat env.unsat_core);
  let n_of_conflicts = ref (to_float env.restart_first) in
  let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
  try
    while true do
      (try search (to_int !n_of_conflicts) (to_int !n_of_learnts);
       with Restart -> ());
      n_of_conflicts := !n_of_conflicts *. env.restart_inc;
      n_of_learnts   := !n_of_learnts *. env.learntsize_inc;
    done;
  with 
    | Sat -> 
        (*check_model ();*)
        raise Sat
    | (Unsat cl) as e -> 
        (* check_unsat_core cl; *)
        raise e