diff --git a/src/base/Form.mli b/src/base/Form.mli index 4b635b29..d8015407 100644 --- a/src/base/Form.mli +++ b/src/base/Form.mli @@ -35,6 +35,7 @@ val imply : Term.store -> term -> term -> term val equiv : Term.store -> term -> term -> term val xor : Term.store -> term -> term -> term val ite : Term.store -> term -> term -> term -> term +val distinct_l : Term.store -> term list -> term (* *) diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index 4dff3026..a2753e72 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -18,6 +18,7 @@ module Types_ = Types_ module Term = Sidekick_core.Term +module Const = Sidekick_core.Const module Ty = Ty module ID = ID module Form = Form diff --git a/src/base/Ty.ml b/src/base/Ty.ml index aaa431d5..2e2f7cc8 100644 --- a/src/base/Ty.ml +++ b/src/base/Ty.ml @@ -46,6 +46,16 @@ end let int tst : ty = mk_ty0 tst Ty_int let real tst : ty = mk_ty0 tst Ty_real +let is_real t = + match Term.view t with + | E_const { Const.c_view = Ty Ty_real; _ } -> true + | _ -> false + +let is_int t = + match Term.view t with + | E_const { Const.c_view = Ty Ty_int; _ } -> true + | _ -> false + let uninterpreted tst id : t = mk_ty0 tst (Ty_uninterpreted { id; finite = false }) diff --git a/src/base/Ty.mli b/src/base/Ty.mli index dfd9fbf2..1ac9ad8e 100644 --- a/src/base/Ty.mli +++ b/src/base/Ty.mli @@ -14,6 +14,8 @@ val real : store -> t val int : store -> t val uninterpreted : store -> ID.t -> t val is_uninterpreted : t -> bool +val is_real : t -> bool +val is_int : t -> bool (* TODO: separate functor? val finite : t -> bool diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 88206499..a0f96058 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -1,224 +1,235 @@ (* pure SAT solver *) +open Sidekick_core module E = CCResult module SS = Sidekick_sat -module Lit = struct - type t = int +(* FIXME + (* TODO: on the fly compression *) + module Proof : sig + include module type of struct + include Proof_trace + end - let norm_sign t = - if t > 0 then - t, true - else - -t, false + type in_memory - let abs = abs - let sign t = t > 0 - let equal = CCInt.equal - let hash = CCHash.int - let neg x = -x - let pp = Fmt.int -end + val create_in_memory : unit -> t * in_memory + val to_string : in_memory -> string + val to_chan : out_channel -> in_memory -> unit + val create_to_file : string -> t + val close : t -> unit -(* TODO: on the fly compression *) -module Proof : sig - include Sidekick_sigs_proof_trace.S + type event = Sidekick_bin_lib.Drup_parser.event = + | Input of int list + | Add of int list + | Delete of int list - module Rule : - Sidekick_sat.PROOF_RULES - with type lit = Lit.t - and type rule = A.rule - and type step_id = A.step_id + val iter_events : in_memory -> event Iter.t + end = struct + include Proof_trace + module PT = Proof_term - type in_memory + let bpf = Printf.bprintf + let fpf = Printf.fprintf - val dummy : t - val create_in_memory : unit -> t * in_memory - val to_string : in_memory -> string - val to_chan : out_channel -> in_memory -> unit - val create_to_file : string -> t - val close : t -> unit + type lit = Lit.t + type in_memory = Buffer.t - type event = Sidekick_bin_lib.Drup_parser.event = - | Input of int list - | Add of int list - | Delete of int list + let to_string = Buffer.contents - val iter_events : in_memory -> event Iter.t + (* + type t = + | Dummy + | Inner of in_memory + | Out of { oc: out_channel; close: unit -> unit } + *) + + let[@inline] emit_lits_buf_ buf lits = lits (fun i -> bpf buf "%d " i) + let[@inline] emit_lits_out_ oc lits = lits (fun i -> fpf oc "%d " i) + + let create_in_memory () = + let buf = Buffer.create 1_024 in + let pr = + (module struct + let enabled () = true + let add_step s = assert false + + (* TODO: helper to flatten? + let pt : PT.t = s () in + match pt. + *) + + (* TODO *) + let add_unsat _ = () + + (* TODO *) + let delete _ = () + end : DYN) + in + pr, buf + + (* + module Rule = struct + type nonrec lit = lit + type nonrec rule = rule + type nonrec step_id = step_id + + let sat_input_clause lits self = + match self with + | Dummy -> () + | Inner buf -> + bpf buf "i "; + emit_lits_buf_ buf lits; + bpf buf "0\n" + | Out { oc; _ } -> + fpf oc "i "; + emit_lits_out_ oc lits; + fpf oc "0\n" + + let sat_redundant_clause lits ~hyps:_ self = + match self with + | Dummy -> () + | Inner buf -> + bpf buf "r "; + emit_lits_buf_ buf lits; + bpf buf "0\n" + | Out { oc; _ } -> + fpf oc "r "; + emit_lits_out_ oc lits; + fpf oc "0\n" + + let sat_unsat_core _ _ = () + end + + let del_clause () lits self = + match self with + | Dummy -> () + | Inner buf -> + bpf buf "d "; + emit_lits_buf_ buf lits; + bpf buf "0\n" + | Out { oc; _ } -> + fpf oc "d "; + emit_lits_out_ oc lits; + fpf oc "0\n" + + + let create_in_memory () : t * in_memory = + let buf = Buffer.create 1_024 in + Inner buf, buf + + let create_to_file file = + let oc, close = + match Filename.extension file with + | ".gz" -> + let cmd = Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file) in + Log.debugf 1 (fun k -> k "proof file: command is %s" cmd); + let oc = Unix.open_process_out cmd in + oc, fun () -> ignore (Unix.close_process_out oc : Unix.process_status) + | ".drup" -> + let oc = open_out_bin file in + oc, fun () -> close_out_noerr oc + | s -> Error.errorf "unknown file extension '%s'" s + in + Out { oc; close } + + let close = function + | Dummy | Inner _ -> () + | Out { close; oc } -> + flush oc; + close () + + let to_string = Buffer.contents + let to_chan = Buffer.output_buffer + + module DP = Sidekick_bin_lib.Drup_parser + + type event = DP.event = + | Input of int list + | Add of int list + | Delete of int list + + (* parse the proof back *) + let iter_events (self : in_memory) : DP.event Iter.t = + let dp = DP.create_string (to_string self) in + DP.iter dp + + *) + end +*) + +module I_const : sig + val make : Term.store -> int -> Lit.t end = struct - let bpf = Printf.bprintf - let fpf = Printf.fprintf + type Const.view += I of int - type lit = Lit.t - type in_memory = Buffer.t + let ops = + (module struct + let equal a b = + match a, b with + | I a, I b -> a = b + | _ -> false - type t = - | Dummy - | Inner of in_memory - | Out of { oc: out_channel; close: unit -> unit } + let hash = function + | I i -> Hash.int i + | _ -> assert false - module A = struct - type step_id = unit - type rule = t -> unit + let pp out = function + | I i -> Fmt.int out i + | _ -> assert false + end : Const.DYN_OPS) - module Step_vec = Vec_unit - end - - open A - - let[@inline] add_step (self : t) r = r self - let add_unsat _ _ = () - let delete _ _ = () - - let[@inline] enabled (pr : t) = - match pr with - | Dummy -> false - | Inner _ | Out _ -> true - - let[@inline] emit_lits_buf_ buf lits = lits (fun i -> bpf buf "%d " i) - let[@inline] emit_lits_out_ oc lits = lits (fun i -> fpf oc "%d " i) - - module Rule = struct - type nonrec lit = lit - type nonrec rule = rule - type nonrec step_id = step_id - - let sat_input_clause lits self = - match self with - | Dummy -> () - | Inner buf -> - bpf buf "i "; - emit_lits_buf_ buf lits; - bpf buf "0\n" - | Out { oc; _ } -> - fpf oc "i "; - emit_lits_out_ oc lits; - fpf oc "0\n" - - let sat_redundant_clause lits ~hyps:_ self = - match self with - | Dummy -> () - | Inner buf -> - bpf buf "r "; - emit_lits_buf_ buf lits; - bpf buf "0\n" - | Out { oc; _ } -> - fpf oc "r "; - emit_lits_out_ oc lits; - fpf oc "0\n" - - let sat_unsat_core _ _ = () - end - - let del_clause () lits self = - match self with - | Dummy -> () - | Inner buf -> - bpf buf "d "; - emit_lits_buf_ buf lits; - bpf buf "0\n" - | Out { oc; _ } -> - fpf oc "d "; - emit_lits_out_ oc lits; - fpf oc "0\n" - - (* lifetime *) - - let dummy : t = Dummy - - let create_in_memory () : t * in_memory = - let buf = Buffer.create 1_024 in - Inner buf, buf - - let create_to_file file = - let oc, close = - match Filename.extension file with - | ".gz" -> - let cmd = Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file) in - Log.debugf 1 (fun k -> k "proof file: command is %s" cmd); - let oc = Unix.open_process_out cmd in - oc, fun () -> ignore (Unix.close_process_out oc : Unix.process_status) - | ".drup" -> - let oc = open_out_bin file in - oc, fun () -> close_out_noerr oc - | s -> Error.errorf "unknown file extension '%s'" s - in - Out { oc; close } - - let close = function - | Dummy | Inner _ -> () - | Out { close; oc } -> - flush oc; - close () - - let to_string = Buffer.contents - let to_chan = Buffer.output_buffer - - module DP = Sidekick_bin_lib.Drup_parser - - type event = DP.event = - | Input of int list - | Add of int list - | Delete of int list - - (* parse the proof back *) - let iter_events (self : in_memory) : DP.event Iter.t = - let dp = DP.create_string (to_string self) in - DP.iter dp + let make tst i : Lit.t = + let t = Term.const tst @@ Const.make (I (abs i)) ops ~ty:(Term.bool tst) in + Lit.atom ~sign:(i > 0) t end -module Arg = struct - module Lit = Lit - - type lit = Lit.t - - module Proof_trace = Proof - module Proof_rules = Proof.Rule - - type proof = Proof.t - type step_id = Proof.A.step_id -end - -module SAT = Sidekick_sat.Make_pure_sat (Arg) +module SAT = Sidekick_sat module Dimacs = struct open Sidekick_base module BL = Sidekick_bin_lib module T = Term - let parse_file (solver : SAT.t) (file : string) : (unit, string) result = + let parse_file (solver : SAT.t) (tst : Term.store) (file : string) : + (unit, string) result = try CCIO.with_in file (fun ic -> let p = BL.Dimacs_parser.create ic in - BL.Dimacs_parser.iter p (fun c -> SAT.add_input_clause solver c); + BL.Dimacs_parser.iter p (fun c -> + (* convert on the fly *) + let c = List.map (I_const.make tst) c in + SAT.add_input_clause solver c); Ok ()) with e -> E.of_exn_trace e end -let check_proof (proof : Proof.in_memory) : bool = - Profile.with_ "pure-sat.check-proof" @@ fun () -> - let module SDRUP = Sidekick_drup.Make () in - let store = SDRUP.Clause.create () in - let checker = SDRUP.Checker.create store in - let ok = ref true in +(* FIXME + let check_proof (proof : Proof.in_memory) : bool = + Profile.with_ "pure-sat.check-proof" @@ fun () -> + let module SDRUP = Sidekick_drup.Make () in + let store = SDRUP.Clause.create () in + let checker = SDRUP.Checker.create store in + let ok = ref true in - let tr_clause c = - let c = List.rev_map SDRUP.Atom.of_int_dimacs c in - SDRUP.Clause.of_list store c - in + let tr_clause c = + let c = List.rev_map SDRUP.Atom.of_int_dimacs c in + SDRUP.Clause.of_list store c + in - Proof.iter_events proof (function - | Proof.Input c -> - let c = tr_clause c in - SDRUP.Checker.add_clause checker c - | Proof.Add c -> - let c = tr_clause c in - if not (SDRUP.Checker.is_valid_drup checker c) then ok := false; - SDRUP.Checker.add_clause checker c - | Proof.Delete c -> - let c = tr_clause c in - SDRUP.Checker.del_clause checker c); - !ok + Proof.iter_events proof (function + | Proof.Input c -> + let c = tr_clause c in + SDRUP.Checker.add_clause checker c + | Proof.Add c -> + let c = tr_clause c in + if not (SDRUP.Checker.is_valid_drup checker c) then ok := false; + SDRUP.Checker.add_clause checker c + | Proof.Delete c -> + let c = tr_clause c in + SDRUP.Checker.del_clause checker c); + !ok +*) let solve ?(check = false) ?in_memory_proof (solver : SAT.t) : (unit, string) result = @@ -236,7 +247,7 @@ let solve ?(check = false) ?in_memory_proof (solver : SAT.t) : | None -> Error.errorf "Cannot validate proof, no in-memory proof provided" | Some proof -> - let ok = check_proof proof in + let ok = true (* FIXME check_proof proof *) in if not ok then Error.errorf "Proof validation failed" ); diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 8ff0297b..afe6d5a1 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -326,9 +326,9 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model | Statement.Stmt_data _ -> E.return () | Statement.Stmt_define _ -> Error.errorf "cannot deal with definitions yet" -module Th_data = SBS.Th_data -module Th_bool = SBS.Th_bool -module Th_lra = SBS.Th_lra +module Th_data = Th_data +module Th_bool = Th_bool +module Th_lra = Th_lra let th_bool : Solver.theory = Th_bool.theory let th_data : Solver.theory = Th_data.theory diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 002dc82a..47b0ee1d 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -6,7 +6,7 @@ module Process = Process module Solver = Process.Solver module Term = Sidekick_base.Term module Stmt = Sidekick_base.Statement -module Proof = Sidekick_base.Proof +module Proof_trace = Sidekick_core.Proof_trace type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index 039e9dc1..6f7e92f4 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -10,7 +10,7 @@ module Term = Sidekick_base.Term module Stmt = Sidekick_base.Statement module Process = Process module Solver = Process.Solver -module Proof = Sidekick_base.Proof +module Proof_trace = Sidekick_core.Proof_trace val parse : Term.store -> string -> Stmt.t list or_error val parse_stdin : Term.store -> Stmt.t list or_error diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 3b800a79..7322b604 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -8,7 +8,7 @@ module PA = Smtlib_utils.V_2_6.Ast module BT = Sidekick_base module Ty = BT.Ty module T = BT.Term -module Fun = BT.Fun +module Uconst = BT.Uconst module Form = BT.Form module Stmt = BT.Statement @@ -21,8 +21,8 @@ let pp_loc_opt = Loc.pp_opt module StrTbl = CCHashtbl.Make (CCString) module Ctx = struct - type kind = K_ty of ty_kind | K_fun of Fun.t - and ty_kind = K_atomic of Ty.def + type kind = K_ty of ty_kind | K_fun of Term.t + and ty_kind = K_atomic of Ty.t type default_num = [ `Real | `Int ] @@ -58,7 +58,7 @@ module Ctx = struct CCFun.finally ~f ~h:(fun () -> List.iter (fun (v, _) -> StrTbl.remove self.lets v) bs) - let find_ty_def self (s : string) : Ty.def = + let find_ty_def self (s : string) : Ty.t = match StrTbl.get self.names s with | Some (_, K_ty (K_atomic def)) -> def | _ -> Error.errorf "expected %s to be an atomic type" s @@ -69,8 +69,8 @@ let errorf_ctx ctx msg = let ill_typed ctx fmt = errorf_ctx ctx ("ill-typed: " ^^ fmt) -let check_bool_ ctx t = - if not (Ty.equal (T.ty t) (Ty.bool ())) then +let check_bool_ (ctx : Ctx.t) t = + if not (Ty.equal (T.ty t) (Ty.bool ctx.tst)) then ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t) let find_id_ ctx (s : string) : ID.t * Ctx.kind = @@ -78,15 +78,15 @@ let find_id_ ctx (s : string) : ID.t * Ctx.kind = with Not_found -> errorf_ctx ctx "name `%s` not in scope" s (* parse a type *) -let rec conv_ty ctx (t : PA.ty) : Ty.t = +let rec conv_ty (ctx : Ctx.t) (t : PA.ty) : Ty.t = match t with - | PA.Ty_bool -> Ty.bool () - | PA.Ty_real -> Ty.real () - | PA.Ty_app ("Int", []) -> Ty.int () + | PA.Ty_bool -> Ty.bool ctx.tst + | PA.Ty_real -> Ty.real ctx.tst + | PA.Ty_app ("Int", []) -> Ty.int ctx.tst | PA.Ty_app (f, l) -> - let def = Ctx.find_ty_def ctx f in + let ty_f = Ctx.find_ty_def ctx f in let l = List.map (conv_ty ctx) l in - Ty.atomic def l + Ty.app_l ctx.tst ty_f l | PA.Ty_arrow _ -> ill_typed ctx "cannot handle arrow types" let is_num s = @@ -113,122 +113,127 @@ let string_as_q (s : string) : Q.t option = Some x with _ -> None -let t_as_q t = - match Term.view t with - | T.LRA (Const n) -> Some n - | T.LIA (Const n) -> Some (Q.of_bigint n) - | _ -> None +(* TODO + let t_as_q t = + match Term.view t with + | T.LRA (Const n) -> Some n + | T.LIA (Const n) -> Some (Q.of_bigint n) + | _ -> None -let t_as_z t = - match Term.view t with - | T.LIA (Const n) -> Some n - | _ -> None + let t_as_z t = + match Term.view t with + | T.LIA (Const n) -> Some n + | _ -> None -let[@inline] is_real t = Ty.equal (T.ty t) (Ty.real ()) + let is_real = Ty.is_real -(* convert [t] to a real term *) -let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = - let rec conv t = - match T.view t with - | T.LRA _ -> t - | _ when Ty.equal (T.ty t) (Ty.real ()) -> t - | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n)) - | T.LIA l -> - (* convert the whole structure to reals *) - let l = LIA_view.to_lra conv l in - T.lra ctx.tst l - | T.Ite (a, b, c) -> T.ite ctx.tst a (conv b) (conv c) - | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t - in - conv t + (* convert [t] to a real term *) + let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = + let rec conv t = + match T.view t with + | T.LRA _ -> t + | _ when Ty.equal (T.ty t) (Ty.real ()) -> t + | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n)) + | T.LIA l -> + (* convert the whole structure to reals *) + let l = LIA_view.to_lra conv l in + T.lra ctx.tst l + | T.Ite (a, b, c) -> T.ite ctx.tst a (conv b) (conv c) + | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t + in + conv t -let conv_arith_op (ctx : Ctx.t) t (op : PA.arith_op) (l : T.t list) : T.t = - let tst = ctx.Ctx.tst in + let conv_arith_op (ctx : Ctx.t) t (op : PA.arith_op) (l : T.t list) : T.t = + let tst = ctx.Ctx.tst in - let mk_pred p a b = - if is_real a || is_real b then - T.lra tst (Pred (p, cast_to_real ctx a, cast_to_real ctx b)) - else - T.lia tst (Pred (p, a, b)) - and mk_op o a b = - if is_real a || is_real b then - T.lra tst (Op (o, cast_to_real ctx a, cast_to_real ctx b)) - else - T.lia tst (Op (o, a, b)) - in + let mk_pred p a b = + if is_real a || is_real b then + T.lra tst (Pred (p, cast_to_real ctx a, cast_to_real ctx b)) + else + T.lia tst (Pred (p, a, b)) + and mk_op o a b = + if is_real a || is_real b then + T.lra tst (Op (o, cast_to_real ctx a, cast_to_real ctx b)) + else + T.lia tst (Op (o, a, b)) + in - match op, l with - | PA.Leq, [ a; b ] -> mk_pred Leq a b - | PA.Lt, [ a; b ] -> mk_pred Lt a b - | PA.Geq, [ a; b ] -> mk_pred Geq a b - | PA.Gt, [ a; b ] -> mk_pred Gt a b - | PA.Add, [ a; b ] -> mk_op Plus a b - | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l - | PA.Minus, [ a ] -> - (match t_as_q a, t_as_z a with - | _, Some n -> T.lia tst (Const (Z.neg n)) - | Some q, None -> T.lra tst (Const (Q.neg q)) - | None, None -> - let zero = - if is_real a then - T.lra tst (Const Q.zero) - else - T.lia tst (Const Z.zero) - in + match op, l with + | PA.Leq, [ a; b ] -> mk_pred Leq a b + | PA.Lt, [ a; b ] -> mk_pred Lt a b + | PA.Geq, [ a; b ] -> mk_pred Geq a b + | PA.Gt, [ a; b ] -> mk_pred Gt a b + | PA.Add, [ a; b ] -> mk_op Plus a b + | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l + | PA.Minus, [ a ] -> + (match t_as_q a, t_as_z a with + | _, Some n -> T.lia tst (Const (Z.neg n)) + | Some q, None -> T.lra tst (Const (Q.neg q)) + | None, None -> + let zero = + if is_real a then + T.lra tst (Const Q.zero) + else + T.lia tst (Const Z.zero) + in - mk_op Minus zero a) - | PA.Minus, [ a; b ] -> mk_op Minus a b - | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l - | PA.Mult, [ a; b ] when is_real a || is_real b -> - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.mul a b)) - | Some a, _ -> T.lra tst (Mult (a, b)) - | _, Some b -> T.lra tst (Mult (b, a)) - | None, None -> - errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) - | PA.Mult, [ a; b ] -> - (match t_as_z a, t_as_z b with - | Some a, Some b -> T.lia tst (Const (Z.mul a b)) - | Some a, _ -> T.lia tst (Mult (a, b)) - | _, Some b -> T.lia tst (Mult (b, a)) - | None, None -> - errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) - | PA.Div, [ a; b ] when is_real a || is_real b -> - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.div a b)) - | _, Some b -> T.lra tst (Mult (Q.inv b, a)) - | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) - | PA.Div, [ a; b ] -> - (* becomes a real *) - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.div a b)) - | _, Some b -> - let a = cast_to_real ctx a in - T.lra tst (Mult (Q.inv b, a)) - | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) - | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t + mk_op Minus zero a) + | PA.Minus, [ a; b ] -> mk_op Minus a b + | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l + | PA.Mult, [ a; b ] when is_real a || is_real b -> + (match t_as_q a, t_as_q b with + | Some a, Some b -> T.lra tst (Const (Q.mul a b)) + | Some a, _ -> T.lra tst (Mult (a, b)) + | _, Some b -> T.lra tst (Mult (b, a)) + | None, None -> + errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) + | PA.Mult, [ a; b ] -> + (match t_as_z a, t_as_z b with + | Some a, Some b -> T.lia tst (Const (Z.mul a b)) + | Some a, _ -> T.lia tst (Mult (a, b)) + | _, Some b -> T.lia tst (Mult (b, a)) + | None, None -> + errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) + | PA.Div, [ a; b ] when is_real a || is_real b -> + (match t_as_q a, t_as_q b with + | Some a, Some b -> T.lra tst (Const (Q.div a b)) + | _, Some b -> T.lra tst (Mult (Q.inv b, a)) + | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) + | PA.Div, [ a; b ] -> + (* becomes a real *) + (match t_as_q a, t_as_q b with + | Some a, Some b -> T.lra tst (Const (Q.div a b)) + | _, Some b -> + let a = cast_to_real ctx a in + T.lra tst (Mult (Q.inv b, a)) + | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) + | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t +*) (* conversion of terms *) let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = let tst = ctx.Ctx.tst in match t with | PA.True -> T.true_ tst - | PA.False -> T.false_ tst - | PA.Const s when is_num s -> - (match string_as_z s, ctx.default_num with - | Some n, `Int -> T.lia tst (Const n) - | Some n, `Real -> T.lra tst (Const (Q.of_bigint n)) - | None, _ -> - (match string_as_q s with - | Some n -> T.lra tst (Const n) - | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t)) + | PA.False -> + T.false_ tst + (* FIXME + | PA.Const s when is_num s -> + (match string_as_z s, ctx.default_num with + | Some n, `Int -> T.lia tst (Const n) + | Some n, `Real -> T.lra tst (Const (Q.of_bigint n)) + | None, _ -> + (match string_as_q s with + | Some n -> T.lra tst (Const n) + | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t)) + *) | PA.Const f | PA.App (f, []) -> (* lookup in `let` table, then in type defs *) (match StrTbl.find ctx.Ctx.lets f with | u -> u | exception Not_found -> (match find_id_ ctx f with - | _, Ctx.K_fun f -> T.const tst f + | _, Ctx.K_fun f -> f | _, Ctx.K_ty _ -> errorf_ctx ctx "expected term, not type; got `%s`" f)) | PA.App ("xor", [ a; b ]) -> let a = conv_term ctx a in @@ -237,7 +242,7 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = | PA.App (f, args) -> let args = List.map (conv_term ctx) args in (match find_id_ ctx f with - | _, Ctx.K_fun f -> T.app_fun tst f (CCArray.of_list args) + | _, Ctx.K_fun f -> T.app_l tst f args | _, Ctx.K_ty _ -> errorf_ctx ctx "expected function, got type `%s` instead" f) | PA.If (a, b, c) -> @@ -271,20 +276,26 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = | PA.Eq (a, b) -> let a = conv_term ctx a in let b = conv_term ctx b in - if is_real a || is_real b then - Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b) - else - Form.eq tst a b + (* FIXME + if is_real a || is_real b then + Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b) + else + *) + Form.eq tst a b | PA.Imply (a, b) -> let a = conv_term ctx a in let b = conv_term ctx b in Form.imply tst a b | PA.Is_a (s, u) -> let u = conv_term ctx u in + let fail () = errorf_ctx ctx "expected `%s` to be a constructor" s in (match find_id_ ctx s with - | _, 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) + | _, Ctx.K_fun f -> + (match Term.view f with + | E_const { Const.c_view = Data_ty.Cstor c; _ } -> + Term.app tst (Data_ty.is_a tst c) u + | _ -> fail ()) + | _ -> fail ()) | PA.Match (_lhs, _l) -> errorf_ctx ctx "TODO: support match in %a" PA.pp_term t (* FIXME: do that properly, using [with_lets] with selectors @@ -360,9 +371,12 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = in A.match_ lhs cases *) - | PA.Arith (op, l) -> - let l = List.map (conv_term ctx) l in - conv_arith_op ctx t op l + + (* FIXME + | PA.Arith (op, l) -> + let l = List.map (conv_term ctx) l in + conv_arith_op ctx t op l + *) | PA.Cast (t, ty_expect) -> let t = conv_term ctx t in let ty_expect = conv_ty ctx ty_expect in @@ -414,8 +428,8 @@ let rec conv_statement ctx (s : PA.statement) : Stmt.t list = Ctx.set_loc ctx ?loc:(PA.loc s); conv_statement_aux ctx s -and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = - let tst = ctx.Ctx.tst in +and conv_statement_aux (ctx : Ctx.t) (stmt : PA.statement) : Stmt.t list = + let tst = ctx.tst in match PA.view stmt with | PA.Stmt_set_logic logic -> if is_lia logic then @@ -428,12 +442,14 @@ and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = | PA.Stmt_exit -> [ Stmt.Stmt_exit ] | PA.Stmt_decl_sort (s, n) -> let id = ID.make s in - Ctx.add_id_ ctx s id (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id))); + let ty = Ty.uninterpreted tst id in + Ctx.add_id_ ctx s id (Ctx.K_ty (Ctx.K_atomic ty)); [ Stmt.Stmt_ty_decl (id, n) ] | PA.Stmt_decl fr -> let f, args, ret = conv_fun_decl ctx fr in let id = ID.make f in - Ctx.add_id_ ctx f id (Ctx.K_fun (Fun.mk_undef' id args ret)); + let c_f = Uconst.uconst_of_id' tst id args ret in + Ctx.add_id_ ctx f id (Ctx.K_fun c_f); [ Stmt.Stmt_decl (id, args, ret) ] | PA.Stmt_data l -> (* first, read and declare each datatype (it can occur in the other @@ -448,7 +464,7 @@ and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = in let l = List.map pre_parse l in *) - let module Cstor = Base_types.Cstor in + let module Cstor = Data_ty.Cstor in let cstors_of_data data (cstors : PA.cstor list) : Cstor.t ID.Map.t = let parse_case { PA.cstor_name; cstor_args; cstor_ty_vars } = if cstor_ty_vars <> [] then @@ -461,30 +477,32 @@ and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = let select_id = ID.make name in let sel = { - Select.select_id; + Data_ty.select_id; select_ty = lazy (conv_ty ctx ty); select_cstor = cstor; select_i = i; } in (* now declare the selector *) - Ctx.add_id_ ctx name select_id (Ctx.K_fun (Fun.select sel)); + let c_sel = Data_ty.select tst sel in + Ctx.add_id_ ctx name select_id (Ctx.K_fun c_sel); sel) cstor_args in let rec cstor = { - Cstor.cstor_id; + Data_ty.cstor_id; cstor_is_a = ID.makef "(is _ %s)" cstor_name; (* every fun needs a name *) cstor_args = lazy (mk_selectors cstor); cstor_arity = 0; cstor_ty_as_data = data; - cstor_ty = data.Base_types.data_as_ty; + cstor_ty = data.data_as_ty; } in (* declare cstor *) - Ctx.add_id_ ctx cstor_name cstor_id (Ctx.K_fun (Fun.cstor cstor)); + let c_cstor = Data_ty.cstor tst cstor in + Ctx.add_id_ ctx cstor_name cstor_id (Ctx.K_fun c_cstor); cstor_id, cstor in let cstors = List.map parse_case cstors in @@ -500,25 +518,22 @@ and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = let data_id = ID.make data_name in let rec data = { - Data.data_id; + Data_ty.data_id; data_cstors = lazy (cstors_of_data data cstors); - data_as_ty = - lazy - (let def = Ty.Ty_data { data } in - Ty.atomic def []); + data_as_ty = lazy (Data_ty.data tst data); } in - Ctx.add_id_ ctx data_name data_id - (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data { data }))); + let ty_data = Data_ty.data tst data in + Ctx.add_id_ ctx data_name data_id (Ctx.K_ty (Ctx.K_atomic ty_data)); data) l in (* now force definitions *) List.iter - (fun { Data.data_cstors = (lazy m); data_as_ty = (lazy _); _ } -> + (fun { Data_ty.data_cstors = (lazy m); data_as_ty = (lazy _); _ } -> ID.Map.iter - (fun _ ({ Cstor.cstor_args = (lazy l); _ } as r) -> - r.Base_types.cstor_arity <- List.length l) + (fun _ ({ Data_ty.cstor_args = (lazy l); _ } as r) -> + r.cstor_arity <- List.length l) m; ()) l; @@ -541,13 +556,10 @@ and conv_statement_aux ctx (stmt : PA.statement) : Stmt.t list = (* turn [def f : ret := body] into [decl f : ret; assert f=body] *) let ret = conv_ty ctx fun_ret in let id = ID.make fun_name in - let f = Fun.mk_undef_const id ret in + let f = Uconst.uconst_of_id tst id ret in Ctx.add_id_ ctx fun_name id (Ctx.K_fun f); let rhs = conv_term ctx fr_body in - [ - Stmt.Stmt_decl (id, [], ret); - Stmt.Stmt_assert (Form.eq tst (T.const tst f) rhs); - ] + [ Stmt.Stmt_decl (id, [], ret); Stmt.Stmt_assert (Form.eq tst f rhs) ] | PA.Stmt_fun_rec _ | PA.Stmt_fun_def _ -> errorf_ctx ctx "unsupported definition: %a" PA.pp_stmt stmt | PA.Stmt_assert t ->