From fade033458b17244cee7df631603a90250cc7b2a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 20 May 2018 14:30:13 -0500 Subject: [PATCH] refactor: get SAT properly again on some problems --- src/backend/Dot.ml | 39 +----------------- src/backend/Dot.mli | 5 +-- src/dimacs/Lexer.mll | 2 +- src/dimacs/Parser.mly | 4 +- src/main/main.ml | 22 +--------- src/sat/Internal.ml | 62 +++++++++++++++++++---------- src/sat/Solver.ml | 2 + src/sat/Solver_intf.ml | 4 +- src/smt/Ast.ml | 4 +- src/smt/Model.ml | 4 +- src/smt/Model.mli | 4 ++ src/smt/Solver.ml | 12 ++++-- src/smt/Solver.mli | 3 ++ src/smt/th_bool/Sidekick_th_bool.ml | 2 +- src/smtlib/Process.ml | 41 ++++++++----------- src/smtlib/Typecheck.ml | 8 ++-- src/smtlib/jbuild | 3 +- src/util/Error.ml | 12 ++++++ src/util/Error.mli | 6 +++ src/util/Util.ml | 9 ----- src/util/Util.mli | 5 --- 21 files changed, 114 insertions(+), 139 deletions(-) create mode 100644 src/util/Error.ml create mode 100644 src/util/Error.mli diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 2796fa64..c33bc9ec 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -147,41 +147,4 @@ module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom end -module Simple(S : Sidekick_sat.S) - (A : Arg with type atom := S.atom - and type hyp = S.atom list - and type lemma := S.lemma - and type assumption = S.atom) = - Make(S)(struct - module Atom = S.Atom - module Clause = S.Clause - module P = S.Proof - - (* Some helpers *) - let get_form = Atom.get_formula - - let get_assumption c = - match Clause.atoms_l c with - | [ x ] -> x - | _ -> assert false - - let get_lemma c = - match P.expand (P.prove c) with - | {P.step=P.Lemma p;_} -> p - | _ -> assert false - - (* Actual functions *) - let print_atom fmt a = - A.print_atom fmt a - - let hyp_info c = - A.hyp_info (Clause.atoms_l c) - - let lemma_info c = - A.lemma_info (get_lemma c) - - let assumption_info c = - A.assumption_info (get_assumption c) - - end) - +module Simple(S : Sidekick_sat.S) = Make(S)(Default(S)) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index 85313dba..1fb85eed 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -60,10 +60,7 @@ module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom and type assumption := S.clause) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. *) -module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.atom - and type hyp = S.atom list - and type lemma := S.lemma - and type assumption = S.atom) : S with type t := S.proof +module Simple(S : Sidekick_sat.S) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml. *) diff --git a/src/dimacs/Lexer.mll b/src/dimacs/Lexer.mll index 09b9c420..f1b2ce31 100644 --- a/src/dimacs/Lexer.mll +++ b/src/dimacs/Lexer.mll @@ -15,7 +15,7 @@ rule token = parse | '\n' { Lexing.new_line lexbuf; token lexbuf } | '0' { ZERO } | '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) } - | _ { Util.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) } + | _ { Error.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) } and comment = parse | '\n' { Lexing.new_line lexbuf; token lexbuf } diff --git a/src/dimacs/Parser.mly b/src/dimacs/Parser.mly index 1e776952..80da0670 100644 --- a/src/dimacs/Parser.mly +++ b/src/dimacs/Parser.mly @@ -25,14 +25,14 @@ prelude: | P CNF LIT LIT { () } | error { - Util.errorf "expected prelude %a" pp_pos ($startpos,$endpos) + Error.errorf "expected prelude %a" pp_pos ($startpos,$endpos) } clauses: | l=clause* { l } | error { - Util.errorf "expected list of clauses %a" + Error.errorf "expected list of clauses %a" pp_pos ($startpos,$endpos) } diff --git a/src/main/main.ml b/src/main/main.ml index 0b431522..7a0ad1c8 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -34,26 +34,6 @@ let p_progress = ref false let hyps : Ast.term list ref = ref [] -module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver) - -let check_model _state = - let check_clause _c = - true - (* FIXME - let l = - List.map - (fun a -> - Sidekick_sat.Log.debugf 99 - (fun k -> k "Checking value of %a" Term.pp (Sat.Atom.term a)); - Sat_solver.Sat_state.eval state a) - c - in - List.exists (fun x -> x) l - *) - in - let l = List.map check_clause !hyps in - List.for_all (fun x -> x) l - (* Arguments parsing *) let int_arg r arg = let l = String.length arg in @@ -170,7 +150,7 @@ let () = match main() with | exception e -> let b = Printexc.get_backtrace () in begin match e with - | Util.Error msg -> + | Error.Error msg -> Format.printf "@{Error@}: %s@." msg; ignore @@ exit 1 | Out_of_time -> diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index 819b9c86..973a6051 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -53,7 +53,7 @@ module Make (Th : Theory_intf.S) = struct and reason = | Decision | Bcp of clause - | Local + | Local of clause and premise = | Hyp @@ -352,7 +352,7 @@ module Make (Th : Theory_intf.S) = struct Format.fprintf fmt "%%" | n, None -> Format.fprintf fmt "%d" n - | n, Some Local -> + | n, Some Local _ -> Format.fprintf fmt "L%d" n | n, Some Decision -> Format.fprintf fmt "@@%d" n @@ -362,17 +362,17 @@ module Make (Th : Theory_intf.S) = struct let pp_level fmt a = debug_reason fmt (a.var.v_level, a.var.reason) - let debug_value fmt a = - if a.is_true then - Format.fprintf fmt "T%a" pp_level a - else if a.neg.is_true then - Format.fprintf fmt "F%a" pp_level a - else - Format.fprintf fmt "" + let debug_value out a = + if a.is_true then ( + Format.fprintf out "[T%a]" pp_level a + ) else if a.neg.is_true then ( + Format.fprintf out "[F%a]" pp_level a + ) else ( + CCFormat.string out "[?]" + ) let debug out a = - Format.fprintf out "@[%s%d[%a][@[%a@]]@]" - (sign a) (a.var.vid+1) debug_value a Th.Form.print a.lit + Format.fprintf out "@[@[%a@]%a@]" Th.Form.print a.lit debug_value a let debug_a out vec = Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec @@ -615,14 +615,14 @@ module Make (Th : Theory_intf.S) = struct let[@inline] conclusion (p:proof) : clause = p let expand conclusion = - Log.debugf 5 (fun k -> k "Expanding : @[%a@]" Clause.debug conclusion); + Log.debugf 5 (fun k -> k "(@[proof.expand@ @[%a@]@])" Clause.debug conclusion); match conclusion.c_premise with | Lemma l -> {conclusion; step = Lemma l; } | Hyp -> { conclusion; step = Hypothesis; } | History [] -> - Log.debugf 1 (fun k -> k "Empty history for clause: %a" Clause.debug conclusion); + Log.debugf 1 (fun k -> k "(@[proof.empty_history@ %a@]" Clause.debug conclusion); raise (Resolution_error "Empty history") | Simplified c -> let duplicates, res = analyze (list c) in @@ -974,7 +974,7 @@ module Make (Th : Theory_intf.S) = struct Wrapper function for adding a new propagated formula. *) let enqueue_bool st a reason : unit = if a.neg.is_true then ( - Util.errorf "(@[sat.enqueue_bool.1@ :false-literal %a@])" Atom.debug a + Error.errorf "(@[sat.enqueue_bool.1@ :false-literal %a@])" Atom.debug a ); let level = decision_level st in Log.debugf 5 @@ -1000,11 +1000,17 @@ module Make (Th : Theory_intf.S) = struct a.(j) <- tmp; ) - (* move atoms assigned at high levels first *) + (* move atoms that are not assigned first, + else put atoms assigned at high levels first *) let put_high_level_atoms_first (arr:atom array) : unit = + (* move [a] in front of [b]? *) + let[@inline] put_before a b = + if Atom.level a < 0 then Atom.level b >= 0 + else (Atom.level b >= 0 && Atom.level a > Atom.level b) + in Array.iteri (fun i a -> - if i>0 && Atom.level a > Atom.level arr.(0) then ( + if i>0 && put_before a arr.(0) then ( (* move first to second, [i]-th to first, second to [i] *) if i=1 then ( swap_arr arr 0 1; @@ -1014,7 +1020,7 @@ module Make (Th : Theory_intf.S) = struct arr.(0) <- arr.(i); arr.(i) <- tmp; ); - ) else if i>1 && Atom.level a > Atom.level arr.(1) then ( + ) else if i>1 && put_before a arr.(1) then ( swap_arr arr 1 i; )) arr @@ -1214,7 +1220,9 @@ module Make (Th : Theory_intf.S) = struct - report unsat if conflict at level 0 *) and add_boolean_conflict st (confl:clause): unit = - Log.debugf 3 (fun k -> k "(@[@{sat.boolean-conflict@}@ %a@])" Clause.debug confl); + Log.debugf 3 + (fun k -> k "(@[@{sat.boolean-conflict@}@ %a@ :decision-lvl %d@])" + Clause.debug confl (decision_level st)); st.next_decision <- None; assert (decision_level st >= base_level st); if decision_level st = base_level st || @@ -1336,7 +1344,7 @@ module Make (Th : Theory_intf.S) = struct enqueue_bool st p (Bcp c) ) ) else ( - Util.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ + Error.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ :1 all lits are not true@])" (Util.pp_list Atom.debug) l ) @@ -1502,21 +1510,20 @@ module Make (Th : Theory_intf.S) = struct let a = Atom.make st lit in Log.debugf 3 (fun k-> k "(@[sat.local_assumption@ %a@])" Atom.debug a); assert (decision_level st = base_level st); + let c = Clause.make [|a|] Hyp in if not a.is_true then ( if a.neg.is_true then ( (* conflict between assumptions: UNSAT *) - let c = Clause.make [|a|] Hyp in report_unsat st c; ) else ( (* make a decision, propagate *) - enqueue_bool st a Local; + enqueue_bool st a (Local c); ) ) in match st.unsat_conflict with | None -> Log.debug 3 "(sat.adding_local_assumptions)"; - cancel_until st (base_level st); List.iter add_lit assumptions | Some _ -> Log.debug 2 "(sat.local_assumptions.1: already unsat)" @@ -1568,7 +1575,9 @@ module Make (Th : Theory_intf.S) = struct end in try + cancel_until st 0; local st assumptions; + new_decision_level st; add_clauses() with Sat -> () @@ -1609,6 +1618,15 @@ module Make (Th : Theory_intf.S) = struct (* Unsafe access to internal data *) let trail st = st.trail + + let check_model st : unit = + Log.debug 5 "(sat.check-model)"; + Vec.iter + (fun c -> + if not (Array.exists Atom.is_true c.atoms) then ( + Error.errorf "(@[sat.check-model.invalid-model@ :clause %a@])" Clause.debug c + )) + st.clauses end [@@inline] diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 624313a1..9309b4fd 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -99,6 +99,8 @@ module Make (Th : Theory_intf.S) = struct let clauses = st.S.clauses in {clauses} + let check_model = S.check_model + module Atom = S.Atom module Clause = struct diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 84c94b5a..26fea6fd 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -138,6 +138,8 @@ module type S = sig val export : t -> clause export + val check_model : t -> unit + (** {2 Re-export some functions} *) type solver = t @@ -235,7 +237,7 @@ module type S = sig (** Check the contents of a proof. Mainly for internal use *) module Tbl : Hashtbl.S with type key = t - end + end module Clause : sig type t = clause diff --git a/src/smt/Ast.ml b/src/smt/Ast.ml index a0cbe71a..55f3731f 100644 --- a/src/smt/Ast.ml +++ b/src/smt/Ast.ml @@ -93,7 +93,7 @@ module Ty = struct end) let ill_typed fmt = - Util.errorf ("ill-typed: " ^^ fmt) + Error.errorf ("ill-typed: " ^^ fmt) end type var = Ty.t Var.t @@ -393,7 +393,7 @@ let num_z ty z = mk_ (Num_z z) ty let parse_num ~where (s:string) : [`Q of Q.t | `Z of Z.t] = let fail() = - Util.errorf "%sexpected number, got `%s`" (Lazy.force where) s + Error.errorf "%sexpected number, got `%s`" (Lazy.force where) s in begin match Z.of_string s with | n -> `Z n diff --git a/src/smt/Model.ml b/src/smt/Model.ml index b3ae3171..2844623b 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -18,6 +18,8 @@ type t = { (* constant -> its value *) } +let empty : t = { env=A.env_empty; domains=A.Ty.Map.empty; consts=ID.Map.empty} + let make ~env ~consts ~domains = (* also add domains to [env] *) let env = @@ -169,7 +171,7 @@ let rec eval_whnf (m:t) (st:term list) (subst:subst) (t:term): term = let st = t :: st in try eval_whnf_rec m st subst t - with Util.Error msg -> + with Error.Error msg -> errorf "@[<2>Model:@ internal type error `%s`@ in %a@]" msg pp_stack st and eval_whnf_rec m st subst t = match A.term_view t with | A.Num_q _ diff --git a/src/smt/Model.mli b/src/smt/Model.mli index 52b1f7ba..02cae326 100644 --- a/src/smt/Model.mli +++ b/src/smt/Model.mli @@ -16,6 +16,10 @@ type t = private { (* constant -> its value *) } +(* TODO: remove *) +(** Trivial model *) +val empty : t + val make : env:Ast.env -> consts:term ID.Map.t -> diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 8f05a745..51cff76a 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -19,6 +19,8 @@ let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t = module Proof = struct type t = Sat_solver.Proof.t + let check = Sat_solver.Proof.check + let pp out (p:t) : unit = let pp_step_res out p = let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in @@ -398,6 +400,8 @@ let[@inline] assume_eq self t u expl : unit = let[@inline] assume_distinct self l ~neq expl : unit = Congruence_closure.assert_distinct (cc self) l (E_lit expl) ~neq +let check_model (s:t) = Sat_solver.check_model s.solver + (* type unsat_core = Sat.clause list *) @@ -409,11 +413,13 @@ let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res = match r with | Sat_solver.Sat (Sidekick_sat.Sat_state _st) -> Log.debugf 0 (fun k->k "SAT"); - Unknown U_incomplete (* TODO *) + Sat Model.empty (* let env = Ast.env_empty in - let m = Model.make ~env - Sat m *) + let m = Model.make ~env in + … + Unknown U_incomplete (* TODO *) + *) | Sat_solver.Unsat (Sidekick_sat.Unsat_state us) -> let pr = us.get_proof () in Unsat pr diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index bb921ef7..71e4523a 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -17,6 +17,7 @@ type model = Model.t module Proof : sig type t = Sat_solver.Proof.t + val check : t -> unit val pp : t CCFormat.printer end @@ -63,6 +64,8 @@ val solve : @param check if true, the model is checked before returning @param on_exit functions to be run before this returns *) +val check_model : t -> unit + val pp_term_graph: t CCFormat.printer val pp_stats : t CCFormat.printer val pp_unknown : unknown CCFormat.printer diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml index a1521407..e606b0a6 100644 --- a/src/smt/th_bool/Sidekick_th_bool.ml +++ b/src/smt/th_bool/Sidekick_th_bool.ml @@ -264,7 +264,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = self.acts.Theory.propagate_distinct l ~neq:lit_t (Explanation.lit lit) ) else ( (* TODO: propagate pairwise equalities? *) - Util.errorf "cannot process negative distinct lit %a" Lit.pp lit; + Error.errorf "cannot process negative distinct lit %a" Lit.pp lit; ) | B_and subs -> if Lit.sign lit then ( diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 21e999b0..3ea89fba 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -9,6 +9,7 @@ module E = CCResult module A = Ast module Form = Sidekick_th_bool module Fmt = CCFormat +module Dot = Sidekick_backend.Dot.Simple(Solver.Sat_solver) module Subst = struct type 'a t = 'a ID.Map.t @@ -17,7 +18,7 @@ module Subst = struct let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out let add subst v t = if mem subst v then ( - Util.errorf "%a already bound" A.Var.pp v; + Error.errorf "%a already bound" A.Var.pp v; ); ID.Map.add (A.Var.id v) t subst let find subst v = ID.Map.get (A.Var.id v) subst @@ -33,9 +34,9 @@ module Conv = struct (* | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat *) | A.Ty.App (id, []) -> mk_ty id | A.Ty.App (_, _) -> - Util.errorf "cannot convert parametrized type %a" A.Ty.pp ty + Error.errorf "cannot convert parametrized type %a" A.Ty.pp ty | A.Ty.Arrow _ -> - Util.errorf "cannot convert arrow type `%a`" A.Ty.pp ty + Error.errorf "cannot convert arrow type `%a`" A.Ty.pp ty in aux_ty ty @@ -83,7 +84,7 @@ module Conv = struct begin match A.term_view t with | A.Var v -> begin match Subst.find subst v with - | None -> Util.errorf "variable %a not bound" A.Var.pp v + | None -> Error.errorf "variable %a not bound" A.Var.pp v | Some t -> t end | A.Const id -> @@ -94,7 +95,7 @@ module Conv = struct | A.Const id -> (* TODO: lookup definition of [f] *) mk_app (Cst.make_undef id (A.ty f |> conv_ty)) l - | _ -> Util.errorf "cannot process HO application %a" A.pp_term t + | _ -> Error.errorf "cannot process HO application %a" A.pp_term t end | A.If (a,b,c) -> let a = aux subst a in @@ -140,7 +141,7 @@ module Conv = struct begin match op, l with | A.Minus, [a] -> RLE.neg a |> ret_rat | _, [] | _, [_] -> - Util.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t + Error.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t | A.Leq, [a;b] -> let e = RLE.diff a b in mk_lra_pred Mc2_lra.Leq0 e |> ret_any @@ -154,7 +155,7 @@ module Conv = struct let e = RLE.diff b a in mk_lra_pred Mc2_lra.Lt0 e |> ret_any | (A.Leq | A.Lt | A.Geq | A.Gt), _ -> - Util.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t + Error.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t | A.Add, _ -> let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in mk_lra_expr e |> ret_t @@ -179,7 +180,7 @@ module Conv = struct | _, [t] -> List.fold_right RLE.mult coeffs t |> ret_rat | _ -> - Util.errorf "non-linear expr:@ `%a`" A.pp_term t + Error.errorf "non-linear expr:@ `%a`" A.pp_term t end | A.Div, (first::l) -> (* support t/a/b/c where only [t] is a rational *) @@ -187,7 +188,7 @@ module Conv = struct List.map (fun c -> match RLE.as_const c with | None -> - Util.errorf "non-linear expr:@ `%a`" A.pp_term t + Error.errorf "non-linear expr:@ `%a`" A.pp_term t | Some c -> Q.inv c) l in @@ -259,7 +260,7 @@ end let solve ?gc:_ ?restarts:_ - ?dot_proof:_ + ?dot_proof ?(pp_model=false) ?(check=false) ?time:_ ?memory:_ ?progress:_ @@ -275,17 +276,10 @@ let solve if pp_model then ( Format.printf "(@[model@ %a@])@." Model.pp m ); - if check then ( - (* TODO - if not (check_model m) then ( - Util.error "invalid model" - ) - *) - ); + if check then Solver.check_model s; let t3 = Sys.time () -. t2 in Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; - | Solver.Unsat _pr -> - (* + | Solver.Unsat p -> if check then ( Solver.Proof.check p; begin match dot_proof with @@ -299,7 +293,6 @@ let solve Format.pp_print_flush fmt (); flush oc) end ); - *) let t3 = Sys.time () -. t2 in Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; | Solver.Unknown reas -> @@ -365,11 +358,11 @@ let process_stmt Solver.assume solver (IArray.of_list c); E.return () | A.Goal (_, _) -> - Util.errorf "cannot deal with goals yet" + Error.errorf "cannot deal with goals yet" | A.Data _ -> - Util.errorf "cannot deal with datatypes yet" + Error.errorf "cannot deal with datatypes yet" | A.Define _ -> - Util.errorf "cannot deal with definitions yet" + Error.errorf "cannot deal with definitions yet" end @@ -403,7 +396,7 @@ end = struct | Ast.Ty.Prop -> Ty.prop | Ast.Ty.Const id -> begin try ID.Tbl.find ty_tbl_ id |> Lazy.force - with Not_found -> Util.errorf "type %a not in ty_tbl" ID.pp id + with Not_found -> Error.errorf "type %a not in ty_tbl" ID.pp id end | Ast.Ty.Arrow (a,b) -> Ty.arrow (conv_ty a) (conv_ty b) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index e9c9804b..aec2f0e1 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -78,15 +78,15 @@ module Ctx = struct let find_kind t (id:ID.t) : kind = try ID.Tbl.find t.kinds id - with Not_found -> Util.errorf "did not find kind of ID `%a`" ID.pp id + with Not_found -> Error.errorf "did not find kind of ID `%a`" ID.pp id let as_data t (ty:A.Ty.t) : (ID.t * A.Ty.t) list = match ty with | A.Ty.App (id,_) -> begin match ID.Tbl.get t.data id with | Some l -> l - | None -> Util.errorf "expected %a to be a datatype" A.Ty.pp ty + | None -> Error.errorf "expected %a to be a datatype" A.Ty.pp ty end - | _ -> Util.errorf "expected %a to be a constant type" A.Ty.pp ty + | _ -> Error.errorf "expected %a to be a constant type" A.Ty.pp ty let pp_kind out = function | K_ty _ -> Format.fprintf out "type" @@ -107,7 +107,7 @@ end let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx) let errorf_ctx ctx msg = - Util.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx) + Error.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx) let check_bool_ t = if not (A.Ty.equal (A.ty t) A.Ty.prop) then ( diff --git a/src/smtlib/jbuild b/src/smtlib/jbuild index 810b5e93..c041f14f 100644 --- a/src/smtlib/jbuild +++ b/src/smtlib/jbuild @@ -7,7 +7,8 @@ ((name sidekick_smtlib) (public_name sidekick.smtlib) (optional) ; only if deps present - (libraries (containers sidekick.smt sidekick.util sidekick.smt.th_bool zarith)) + (libraries (containers zarith sidekick.smt sidekick.util + sidekick.smt.th_bool sidekick.backend)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -color always -bin-annot diff --git a/src/util/Error.ml b/src/util/Error.ml new file mode 100644 index 00000000..007eb14a --- /dev/null +++ b/src/util/Error.ml @@ -0,0 +1,12 @@ + +module Fmt = CCFormat + +exception Error of string + +let () = Printexc.register_printer + (function + | Error msg -> Some ("internal error: " ^ msg) + | _ -> None) + +let errorf msg = Fmt.ksprintf msg ~f:(fun s -> raise (Error s)) + diff --git a/src/util/Error.mli b/src/util/Error.mli new file mode 100644 index 00000000..d94173bc --- /dev/null +++ b/src/util/Error.mli @@ -0,0 +1,6 @@ + + +exception Error of string + +val errorf : ('a, Format.formatter, unit, 'b) format4 -> 'a +(** @raise Error when called *) diff --git a/src/util/Util.ml b/src/util/Util.ml index 39ae1a16..f596a6db 100644 --- a/src/util/Util.ml +++ b/src/util/Util.ml @@ -24,15 +24,6 @@ let pp_array ?(sep=" ") pp out l = let pp_iarray ?(sep=" ") pp out a = Fmt.seq ~sep:(pp_sep sep) pp out (IArray.to_seq a) -exception Error of string - -let () = Printexc.register_printer - (function - | Error msg -> Some ("internal error: " ^ msg) - | _ -> None) - -let errorf msg = Fmt.ksprintf msg ~f:(fun s -> raise (Error s)) - let setup_gc () = let g = Gc.get () in g.Gc.space_overhead <- 3_000; (* major gc *) diff --git a/src/util/Util.mli b/src/util/Util.mli index 0bf0de87..66826a75 100644 --- a/src/util/Util.mli +++ b/src/util/Util.mli @@ -15,11 +15,6 @@ val pp_pair : ?sep:string -> 'a printer -> 'b printer -> ('a * 'b) printer val pp_iarray : ?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.printer -exception Error of string - -val errorf : ('a, Format.formatter, unit, 'b) format4 -> 'a -(** @raise Error when called *) - val setup_gc : unit -> unit (** Change parameters of the GC *)