simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: refactor further

Browse source
This commit is contained in:
Simon Cruanes 2022-08-09 22:41:13 -04:00
parent fc5ce9bf87
commit 95dcb0ae74
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
9 changed files with 374 additions and 337 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base/Form.mli
View file

@ -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
(* *)

1
src/base/Sidekick_base.ml
View file

@ -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

10
src/base/Ty.ml
View file

@ -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 })

2
src/base/Ty.mli
View file

@ -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

385
src/main/pure_sat_solver.ml
View file

@ -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"
);

6
src/smtlib/Process.ml
View file

@ -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

2
src/smtlib/Sidekick_smtlib.ml
View file

@ -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

2
src/smtlib/Sidekick_smtlib.mli
View file

@ -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

302
src/smtlib/Typecheck.ml
View file

@ -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 ->