From e7e8873295f3d94c9949e7a48ed59ef365a4708b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 27 Aug 2021 09:28:59 -0400 Subject: [PATCH] fix more warnings --- src/base-solver/sidekick_base_solver.ml | 9 ++--- src/base/Base_types.ml | 6 ---- src/base/Model.ml | 2 +- src/base/Solver_arg.ml | 2 +- src/checker/drup_check.ml | 4 +-- src/core/Sidekick_core.ml | 2 +- src/drup/sidekick_drup.ml | 3 +- src/dune | 4 ++- src/lit/Sidekick_lit.ml | 2 +- src/lra/sidekick_arith_lra.ml | 1 - src/main/main.ml | 3 +- src/main/pure_sat_solver.ml | 2 +- src/mini-cc/tests/sidekick_test_minicc.ml | 2 +- src/smt-solver/Sidekick_smt_solver.ml | 12 +++---- src/smtlib/Process.ml | 9 ++--- src/smtlib/Process.mli | 1 - src/smtlib/Sidekick_smtlib.ml | 2 -- src/smtlib/Typecheck.ml | 44 +++++++++++------------ 18 files changed, 49 insertions(+), 61 deletions(-) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 2ce8c468..090da86f 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -5,7 +5,7 @@ from {!Sidekick_core}, using data structures from {!Sidekick_base}. *) -open Sidekick_base +open! Sidekick_base (** Argument to the SMT solver *) module Solver_arg = struct @@ -24,8 +24,8 @@ module Solver = Sidekick_smt_solver.Make(Solver_arg) (** Theory of datatypes *) module Th_data = Sidekick_th_data.Make(struct module S = Solver - open Base_types - open Sidekick_th_data + open! Base_types + open! Sidekick_th_data module Proof = Proof_stub module Cstor = Cstor @@ -89,7 +89,8 @@ module Th_lra = Sidekick_arith_lra.Make(struct let mk_bool = T.bool let view_as_lra t = match T.view t with | T.LRA l -> l - | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b) + | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> + LRA_pred (Eq, a, b) | _ -> LRA_other t let ty_lra _st = Ty.real() diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index c788cf97..53acd5ff 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -769,12 +769,6 @@ end = struct | Eq (a,b) -> Eq (f a, f b) | Ite (a,b,c) -> Ite (f a, f b, f c) | LRA l -> LRA (Sidekick_arith_lra.map_view f l) - - module Tbl = CCHashtbl.Make(struct - type t = term view - let equal = equal - let hash = hash - end) end (** Term creation and manipulation *) diff --git a/src/base/Model.ml b/src/base/Model.ml index c4a8f6a4..2c7665fc 100644 --- a/src/base/Model.ml +++ b/src/base/Model.ml @@ -1,6 +1,6 @@ (* This file is free software. See file "license" for more details. *) -open Base_types +open! Base_types module Val_map = struct module M = CCMap.Make(CCInt) diff --git a/src/base/Solver_arg.ml b/src/base/Solver_arg.ml index aa4b120f..0ede83e0 100644 --- a/src/base/Solver_arg.ml +++ b/src/base/Solver_arg.ml @@ -1,5 +1,5 @@ -open Base_types +open! Base_types module Term = Term module Fun = Fun diff --git a/src/checker/drup_check.ml b/src/checker/drup_check.ml index dde952d8..8771b768 100644 --- a/src/checker/drup_check.ml +++ b/src/checker/drup_check.ml @@ -56,7 +56,7 @@ end = struct let dump oc self : unit = let fpf = Printf.fprintf in - let pp_c out c = Clause.iter c ~f:(fun a -> fpf oc "%d " (a:atom:>int)); in + let pp_c out c = Clause.iter c ~f:(fun a -> fpf out "%d " (a:atom:>int)); in Vec.iter (function | Input c -> fpf oc "i %a0\n" pp_c c; @@ -82,8 +82,6 @@ module Fwd_check : sig indexes in the trace of the steps that failed. *) val check : Trace.t -> (unit, error) result end = struct - module ISet = CCSet.Make(CCInt) - type t = { checker: Checker.t; errors: VecI32.t; diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index ffcc279d..4fe3fcb5 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -259,7 +259,7 @@ module type LIT = sig val signed_term : t -> T.Term.t * bool (** Return the atom and the sign *) - val atom : T.Term.store -> ?sign:bool -> T.Term.t -> t + val atom : ?sign:bool -> T.Term.store -> T.Term.t -> t (** [atom store t] makes a literal out of a term, possibly normalizing its sign in the process. @param sign if provided, and [sign=false], negate the resulting lit. *) diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml index 995472d2..cbe0d992 100644 --- a/src/drup/sidekick_drup.ml +++ b/src/drup/sidekick_drup.ml @@ -228,7 +228,7 @@ module Make() : S = struct exception Conflict - let raise_conflict_ self a = + let raise_conflict_ _self a = Log.debugf 5 (fun k->k"conflict on atom %a" Atom.pp a); raise Conflict @@ -245,7 +245,6 @@ module Make() : S = struct let pp_trail_ out self = Fmt.fprintf out "(@[%a@])" (Fmt.iter Atom.pp) (Atom.Stack.to_iter self.trail) - exception Found_watch of atom exception Is_sat exception Is_undecided diff --git a/src/dune b/src/dune index 955acfd9..78060e9f 100644 --- a/src/dune +++ b/src/dune @@ -1,5 +1,7 @@ (env (_ - (flags :standard -warn-error -3-32 -color always -safe-string -short-paths) + (flags :standard -warn-error + -a+8+9 -w +a-4-32-40-41-42-44-48 + -color always -safe-string -short-paths) (ocamlopt_flags :standard -O3 -color always -unbox-closures -unbox-closures-factor 20))) diff --git a/src/lit/Sidekick_lit.ml b/src/lit/Sidekick_lit.ml index 29fd8fb9..669e45fd 100644 --- a/src/lit/Sidekick_lit.ml +++ b/src/lit/Sidekick_lit.ml @@ -19,7 +19,7 @@ module Make(T : Sidekick_core.TERM) let make ~sign t = {lit_sign=sign; lit_term=t} - let atom tst ?(sign=true) (t:term) : t = + let atom ?(sign=true) tst (t:term) : t = let t, sign' = T.Term.abs tst t in let sign = if not sign' then not sign else sign in make ~sign t diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 9dc60761..844f0be6 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -133,7 +133,6 @@ module Make(A : ARG) : S with module A = A = struct module LE_ = Linear_expr.Make(A.Q)(SimpVar) module LE = LE_.Expr module SimpSolver = Simplex2.Make(A.Q)(SimpVar) - module LConstr = SimpSolver.Constraint module Subst = SimpSolver.Subst module Comb_map = CCMap.Make(LE_.Comb) diff --git a/src/main/main.ml b/src/main/main.ml index 4d63a4ea..483bc4f0 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -111,6 +111,7 @@ let main_smt () : _ result = in Process.Solver.create ~proof ~theories tst () () in + (* FIXME: emit an actual proof *) let proof_file = if !proof_file ="" then None else Some !proof_file in if !check then ( (* might have to check conflicts *) @@ -126,7 +127,7 @@ let main_smt () : _ result = E.fold_l (fun () -> Process.process_stmt - ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file + ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ~time:!time_limit ~memory:!size_limit ~pp_model:!p_model ~check:!check ~progress:!p_progress diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index d7337114..a1f14109 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -192,7 +192,7 @@ let solve ?(check=false) ?in_memory_proof (solver:SAT.t) : (unit, string) result | SAT.Sat _ -> let t3 = Sys.time () -. t2 in Format.printf "Sat (%.3f/%.3f)@." t2 t3; - | SAT.Unsat (module US) -> + | SAT.Unsat _ -> if check then ( match in_memory_proof with diff --git a/src/mini-cc/tests/sidekick_test_minicc.ml b/src/mini-cc/tests/sidekick_test_minicc.ml index f8bff6b9..1aa46511 100644 --- a/src/mini-cc/tests/sidekick_test_minicc.ml +++ b/src/mini-cc/tests/sidekick_test_minicc.ml @@ -1,4 +1,4 @@ -open Sidekick_base +open! Sidekick_base module A = Alcotest module CC = Sidekick_mini_cc.Make(struct diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 1eface44..a9029d00 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -75,7 +75,6 @@ module Make(A : ARG) end module CC = Sidekick_cc.Make(CC_actions) - module Expl = CC.Expl module N = CC.N (** Internal solver, given to theories and to Msat *) @@ -85,7 +84,6 @@ module Make(A : ARG) module Lit = Lit module CC = CC module N = CC.N - type formula = Lit.t type nonrec proof = proof type dproof = proof -> unit type term = Term.t @@ -199,8 +197,6 @@ module Make(A : ARG) type solver = t - module Eq_class = CC.N - module Expl = CC.Expl module Proof = P let[@inline] cc (t:t) = Lazy.force t.cc @@ -244,7 +240,7 @@ module Make(A : ARG) Stat.incr self.count_axiom; A.add_clause ~keep lits proof - let add_sat_lit self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit = + let add_sat_lit _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit = let (module A) = acts in A.add_lit ?default_pol lit @@ -337,7 +333,7 @@ module Make(A : ARG) (module struct let add_lit ?default_pol lit = let lit = preprocess_lit lit in - A0.add_lit lit + A0.add_lit ?default_pol lit let add_clause c pr = Stat.incr self.count_preprocess_clause; let c = CCList.map preprocess_lit c in @@ -772,8 +768,12 @@ module Make(A : ARG) let _lits f = SAT.iter_trail f in (* TODO: theory combination *) let m = mk_model self _lits in + (* TODO: check model *) + let _ = check in + do_on_exit (); Sat m + | Sat_solver.Unsat (module UNSAT) -> let unsat_core () = UNSAT.unsat_assumptions () in do_on_exit (); diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index fbef278e..ea534db3 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -1,8 +1,7 @@ (** {2 Conversion into {!Term.t}} *) -module BT = Sidekick_base module Profile = Sidekick_util.Profile -open Sidekick_base +open! Sidekick_base module SBS = Sidekick_base_solver [@@@ocaml.warning "-32"] @@ -17,7 +16,6 @@ module Solver = SBS.Solver module Check_cc = struct module Lit = Solver.Solver_internal.Lit module SI = Solver.Solver_internal - module CC = Solver.Solver_internal.CC module MCC = Sidekick_mini_cc.Make(SBS.Solver_arg) let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c @@ -136,7 +134,6 @@ let solve ?gc:_ ?restarts:_ ?(pp_model=false) - ?proof_file ?(check=false) ?time:_ ?memory:_ ?(progress=false) ~assumptions @@ -199,7 +196,7 @@ let solve (* process a single statement *) let process_stmt ?gc ?restarts ?(pp_cnf=false) - ?proof_file ?pp_model ?(check=false) + ?pp_model ?(check=false) ?time ?memory ?progress (solver:Solver.t) (stmt:Statement.t) : unit or_error = @@ -237,7 +234,7 @@ let process_stmt l in solve - ?gc ?restarts ~check ?proof_file ?pp_model + ?gc ?restarts ~check ?pp_model ?time ?memory ?progress ~assumptions solver; diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 57990c89..eba0bed4 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -24,7 +24,6 @@ val process_stmt : ?gc:bool -> ?restarts:bool -> ?pp_cnf:bool -> - ?proof_file:string -> ?pp_model:bool -> ?check:bool -> ?time:float -> diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 6b0b4607..9c60a1ec 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -1,7 +1,5 @@ (** {1 Process Statements} *) -module ID = Sidekick_base.ID -module E = CCResult module Loc = Smtlib_utils.V_2_6.Loc module Parse_ast = Smtlib_utils.V_2_6.Ast module Process = Process diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 1faed13b..dcd4b60a 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -2,9 +2,8 @@ (** {1 Preprocessing AST} *) -open Sidekick_base +open! Sidekick_base module Loc = Smtlib_utils.V_2_6.Loc -module Fmt = CCFormat module PA = Smtlib_utils.V_2_6.Ast module BT = Sidekick_base @@ -111,7 +110,7 @@ let string_as_q (s:string) : Q.t option = with _ -> None let t_as_q t = match Term.view t with - | T.LRA (LRA_const n) -> Some n + | T.LRA (Base_types.LRA_const n) -> Some n | _ -> None (* conversion of terms *) @@ -141,7 +140,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = | PA.App ("xor", [a;b]) -> let a = conv_term ctx a in let b = conv_term ctx b in - Form.xor ctx.tst a b + Form.xor ctx.Ctx.tst a b | PA.App (f, args) -> let args = List.map (conv_term ctx) args in begin match find_id_ ctx f with @@ -188,7 +187,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = | PA.Is_a (s, u) -> let u = conv_term ctx u in begin match find_id_ ctx s with - | _, Ctx.K_fun {Fun.fun_view=Fun_cstor c; _} -> + | _, Ctx.K_fun {Fun.fun_view=Base_types.Fun_cstor c; _} -> Term.is_a tst c u | _ -> errorf_ctx ctx "expected `%s` to be a constructor" s end @@ -270,35 +269,36 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = | PA.Arith (op, l) -> let l = List.map (conv_term ctx) l in let open Base_types in + let tst = ctx.Ctx.tst in begin match op, l with - | PA.Leq, [a;b] -> T.lra ctx.tst (LRA_pred (Leq, a, b)) - | PA.Lt, [a;b] -> T.lra ctx.tst (LRA_pred (Lt, a, b)) - | PA.Geq, [a;b] -> T.lra ctx.tst (LRA_pred (Geq, a, b)) - | PA.Gt, [a;b] -> T.lra ctx.tst (LRA_pred (Gt, a, b)) - | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b)) + | PA.Leq, [a;b] -> T.lra tst (LRA_pred (Leq, a, b)) + | PA.Lt, [a;b] -> T.lra tst (LRA_pred (Lt, a, b)) + | PA.Geq, [a;b] -> T.lra tst (LRA_pred (Geq, a, b)) + | PA.Gt, [a;b] -> T.lra tst (LRA_pred (Gt, a, b)) + | PA.Add, [a;b] -> T.lra tst (LRA_op (Plus, a, b)) | PA.Add, (a::l) -> - List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l + List.fold_left (fun a b -> T.lra tst (LRA_op (Plus,a,b))) a l | PA.Minus, [a] -> begin match t_as_q a with - | Some a -> T.lra ctx.tst (LRA_const (Q.neg a)) + | Some a -> T.lra tst (LRA_const (Q.neg a)) | None -> - T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a)) + T.lra tst (LRA_op (Minus, T.lra tst (LRA_const Q.zero), a)) end - | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b)) + | PA.Minus, [a;b] -> T.lra tst (LRA_op (Minus, a, b)) | PA.Minus, (a::l) -> - List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l + List.fold_left (fun a b -> T.lra tst (LRA_op (Minus,a,b))) a l | PA.Mult, [a;b] -> begin match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra ctx.tst (LRA_const (Q.mul a b)) - | Some a, _ -> T.lra ctx.tst (LRA_mult (a, b)) - | _, Some b -> T.lra ctx.tst (LRA_mult (b, a)) + | Some a, Some b -> T.lra tst (LRA_const (Q.mul a b)) + | Some a, _ -> T.lra tst (LRA_mult (a, b)) + | _, Some b -> T.lra tst (LRA_mult (b, a)) | None, None -> errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t end | PA.Div, [a;b] -> begin match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra ctx.tst (LRA_const (Q.div a b)) - | _, Some b -> T.lra ctx.tst (LRA_mult (Q.inv b, a)) + | Some a, Some b -> T.lra tst (LRA_const (Q.div a b)) + | _, Some b -> T.lra tst (LRA_mult (Q.inv b, a)) | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t end @@ -440,7 +440,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = cstor_args=lazy (mk_selectors cstor); cstor_arity=0; cstor_ty_as_data=data; - cstor_ty=data.data_as_ty; + cstor_ty=data.Base_types.data_as_ty; } in (* declare cstor *) Ctx.add_id_ ctx cstor_name cstor_id (Ctx.K_fun (Fun.cstor cstor)); @@ -475,7 +475,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = (* now force definitions *) List.iter (fun {Data.data_cstors=lazy m;data_as_ty=lazy _;_} -> - ID.Map.iter (fun _ ({Cstor.cstor_args=lazy l;_} as r) -> r.cstor_arity <- List.length l) m; + ID.Map.iter (fun _ ({Cstor.cstor_args=lazy l;_} as r) -> r.Base_types.cstor_arity <- List.length l) m; ()) l; [Stmt.Stmt_data l]