Fix warnings

src/backend/dedukti.ml

@@ -21,9 +21,9 @@ module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type lemma
   let pp_nl fmt = Format.fprintf fmt "@\n"
   let fprintf fmt format = Format.kfprintf pp_nl fmt format
 
-  let clause_name c = S.St.(c.name)
+  let _clause_name c = S.St.(c.name)
 
-  let pp_clause fmt c =
+  let _pp_clause fmt c =
     let rec aux fmt = function
       | [] -> ()
       | a :: r ->

src/core/external.ml

@@ -48,8 +48,6 @@ module Make
   exception UndecidedLit = S.UndecidedLit
 
   type atom = St.formula
-  type clause = St.clause
-  type proof = Proof.proof
 
   (* Result type *)
   type res =

src/core/internal.ml

@@ -179,7 +179,7 @@ module Make
   let to_int f = int_of_float f
 
   let nb_clauses () = Vec.size env.clauses_hyps
-  let nb_vars    () = St.nb_elt ()
+  (* let nb_vars    () = St.nb_elt () *)
   let decision_level () = Vec.size env.elt_levels
   let base_level () = Vec.size env.user_levels
 
@@ -407,9 +407,6 @@ module Make
     c.attached <- true;
     ()
 
-  (* Is a clause satisfied ? *)
-  let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms
-
   (* Backtracking.
      Used to backtrack, i.e cancel down to [lvl] excluded,
      i.e we want to go back to the state the solver was in
@@ -567,16 +564,6 @@ module Make
         enqueue_semantic atom l;
         Some b
 
-  (* conflict analysis: find the list of atoms of [l] that have the
-     maximal level *)
-  let max_lvl_atoms (l:atom list) : int * atom list =
-    List.fold_left
-      (fun (max_lvl, acc) a ->
-         if a.var.v_level = max_lvl then (max_lvl, a :: acc)
-         else if a.var.v_level > max_lvl then (a.var.v_level, [a])
-         else (max_lvl, acc))
-      (0, []) l
-
   (* find which level to backtrack to, given a conflict clause
      and a boolean stating whether it is
      a UIP ("Unique Implication Point")
@@ -749,7 +736,7 @@ module Make
     record_learnt_clause confl cr
 
   (* Get the correct vector to insert a clause in. *)
-  let rec clause_vector c =
+  let clause_vector c =
     match c.cpremise with
       | Hyp -> env.clauses_hyps
       | Local -> env.clauses_temp
@@ -1114,13 +1101,6 @@ module Make
         pick_branch_lit ()
     done
 
-  (* check that clause is true *)
-  let check_clause (c:clause): unit =
-    let ok = Array_util.exists (fun a -> a.is_true) c.atoms in
-    assert ok
-
-  let check_vec vec = Vec.iter check_clause vec
-
   let eval_level lit =
     let var, negated = make_boolean_var lit in
     if not var.pa.is_true && not var.na.is_true

src/core/res.ml

@@ -14,13 +14,12 @@ module Make(St : Solver_types.S) = struct
   type lemma = St.proof
   type clause = St.clause
   type atom = St.atom
-  type int_cl = clause * St.atom list
 
   exception Insuficient_hyps
   exception Resolution_error of string
 
   (* Log levels *)
-  let error = 1
+  (* let error = 1 *)
   let warn = 3
   let info = 10
   let debug = 80
@@ -34,7 +33,6 @@ module Make(St : Solver_types.S) = struct
   let merge = List.merge compare_atoms
 
   let _c = ref 0
-  let fresh_dpl_name () = incr _c; "D" ^ (string_of_int !_c)
   let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
 
   (* Compute resolution of 2 clauses *)
@@ -84,13 +82,15 @@ module Make(St : Solver_types.S) = struct
       Log.debug warn "Input clause is a tautology";
     cl
 
-  let rec pp_cl fmt l =
+  (*
+  let pp_cl fmt l =
     let rec aux fmt = function
       | [] -> ()
       | a :: r ->
         Format.fprintf fmt "%a@,%a" St.pp_atom a aux r
     in
     Format.fprintf fmt "@[<v>%a@]" aux l
+  *)
 
   (* Comparison of clauses *)
   let cmp_cl c d =
@@ -105,9 +105,6 @@ module Make(St : Solver_types.S) = struct
     in
     aux (c, d)
 
-  let cmp c d =
-    cmp_cl (to_list c) (to_list d)
-
   let prove conclusion =
     assert St.(conclusion.cpremise <> History []);
     conclusion
@@ -134,7 +131,9 @@ module Make(St : Solver_types.S) = struct
           (fun k -> k St.pp_atom a St.pp_clause c');
         c'
       end
-    | _ -> assert false
+    | _ ->
+      raise (Resolution_error
+               (Format.asprintf "Cannot prove atom %a" St.pp_atom a))
 
   let prove_unsat conflict =
     if Array.length conflict.St.atoms = 0 then conflict
@@ -179,11 +178,15 @@ module Make(St : Solver_types.S) = struct
                   l (St.History [c; d]) in
               chain_res (new_clause, l) r
           end
-        | _ -> assert false
+        | _ ->
+          raise (Resolution_error (
+              Format.asprintf "Cannot resolve the clauses: %a && %a"
+                St.pp_clause c St.pp_clause d))
       end
-    | _ -> assert false
+    | _ ->
+      raise (Resolution_error "Bad history")
 
-  let rec expand conclusion =
+  let expand conclusion =
     Log.debugf debug "Expanding : @[%a@]" (fun k -> k St.pp_clause conclusion);
     match conclusion.St.cpremise with
     | St.Lemma l ->
@@ -193,7 +196,8 @@ module Make(St : Solver_types.S) = struct
     | St.Local ->
       { conclusion; step = Assumption; }
     | St.History [] ->
-      assert false
+      raise (Resolution_error (
+          Format.asprintf "Empty history for %a" St.pp_clause conclusion))
     | St.History [ c ] ->
       let duplicates, res = analyze (list c) in
       assert (cmp_cl res (list conclusion) = 0);

src/core/solver_types.ml

@@ -16,8 +16,6 @@ Copyright 2016 Guillaume Bury
 Copyright 2016 Simon Cruanes
 *)
 
-open Printf
-
 module type S = Solver_types_intf.S
 
 (* Solver types for McSat Solving *)

src/sat/sat.mli

@@ -26,6 +26,19 @@ module Expr : sig
   val fresh : unit -> t
   (** Make a fresh atom *)
 
+  val compare : t -> t -> int
+  (** Compare atoms *)
+
+  val sign : t -> bool
+  (** Is the given atom positive ? *)
+
+  val apply_sign : bool -> t -> t
+  (** [apply_sign b] is the identity if [b] is [true], and the negation
+      function if [b] is [false]. *)
+
+  val set_sign : bool -> t -> t
+  (** Return the atom with the sign set. *)
+
 end
 (** The module defining formulas *)
 

src/smt/type_smt.ml

@@ -178,15 +178,6 @@ let find_let env name =
         `Not_found
     end
 
-let pp_expect fmt = function
-  | Nothing -> Format.fprintf fmt "<>"
-  | Type -> Format.fprintf fmt "<tType>"
-  | Typed ty -> Expr.Print.ty fmt ty
-
-let pp_map pp fmt map =
-  M.iter (fun k v ->
-      Format.fprintf fmt "%s->%a;" k.Id.name pp v) map
-
 (* Some helper functions *)
 (* ************************************************************************ *)
 
@@ -288,7 +279,9 @@ let infer env s args =
 
 let rec parse_expr (env : env) t =
   match t with
-  (* Base Type *)
+  (* Base Types *)
+  | { Ast.term = Ast.Builtin Ast.Ttype } ->
+    Ttype
   | { Ast.term = Ast.Symbol { Id.name = "Bool" } } ->
     Ty (Expr_smt.Ty.prop)
 

src/solver/tseitin.ml

@@ -127,7 +127,7 @@ module Make (F : Tseitin_intf.Arg) = struct
       sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
 
   let ( @@ ) l1 l2 = List.rev_append l1 l2
-  let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *)
+  (* let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *) *)
 
   (*
   let distrib l_and l_or =

src/util/iheap.ml

@@ -75,8 +75,10 @@ let in_heap s n = n < V.length s.indices && V.get s.indices n >= 0
 let decrease cmp s n =
   assert (in_heap s n); percolate_up cmp s (V.get s.indices n)
 
+(*
 let increase cmp s n =
   assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
+*)
 
 let filter s filt cmp =
   let j = ref 0 in