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

use sidekick-base.proof-trace in base

Browse source
This commit is contained in:
Simon Cruanes 2021-10-21 20:32:47 -04:00
parent 254d6a1906
commit 7e40851e1b
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
6 changed files with 3 additions and 679 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base/Base_types.ml
View file

@ -5,6 +5,7 @@ module Log = Sidekick_util.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
module Proof_ser = Sidekick_base_proof_trace.Proof_ser
type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type lra_op = Sidekick_arith_lra.op = Plus | Minus

2
src/base/Proof.ml
View file

@ -189,7 +189,7 @@ let rec emit_term_ (self:t) (t:Term.t) : term_id =
in
let id = alloc_id self in
emit_step_ self Proof_ser.({id; view});
emit_step_ self {id; view};
id
let emit_lit_ (self:t) (lit:Lit.t) : term_id =

1
src/base/Sidekick_base.ml
View file

@ -35,7 +35,6 @@ module Solver_arg = Solver_arg
module Lit = Lit
module Proof_dummy = Proof_dummy
module Proof_ser = Proof_ser
module Proof = Proof
module Proof_quip = Proof_quip

8
src/base/dune
View file

@ -3,14 +3,8 @@
(public_name sidekick-base)
(synopsis "Base term definitions for the standalone SMT solver and library")
(libraries containers iter sidekick.core sidekick.util sidekick.lit
sidekick-base.proof-trace
sidekick.arith-lra sidekick.th-bool-static sidekick.th-data
sidekick.zarith
zarith)
(flags :standard -w -32 -open Sidekick_util))
(rule
(targets proof_ser.ml)
(deps proof_ser.bare)
(mode promote) ; not required in releases
(action (run bare-codegen --standalone %{deps} -o %{targets})))

86
src/base/proof_ser.bare
View file

@ -1,86 +0,0 @@
type ID i32
type Lit ID
type Clause {
lits: []Lit
}
type Step_input {
c: Clause
}
# clause, RUP with previous steps
type Step_rup {
res: Clause
hyps: []ID
}
# TODO: remove?
# lit <-> expr
type Step_bridge_lit_expr {
lit: Lit
expr: ID
}
# prove congruence closure lemma `\/_{e\in eqns} e`
type Step_cc {
eqns: []ID
}
# prove t=u using some previous steps and unit equations,
# and add clause (t=u) with given ID
type Step_preprocess {
t: ID
u: ID
using: []ID
}
type Fun_decl {
f: string
}
type Expr_bool {
b: bool
}
type Expr_if {
cond: ID
then_: ID
else_: ID
}
type Expr_not {
f: ID
}
type Expr_eq {
lhs: ID
rhs: ID
}
type Expr_app {
f: ID
args: []ID
}
type Step_view
( Step_input
| Step_rup
| Step_bridge_lit_expr
| Step_cc
| Step_preprocess
| Fun_decl
| Expr_bool
| Expr_if
| Expr_not
| Expr_eq
| Expr_app
)
type Step {
id: ID
view: Step_view
}

584
src/base/proof_ser.ml
View file

@ -1,584 +0,0 @@
[@@@ocaml.warning "-26-27"]
(* embedded runtime library *)
module Bare = struct
module String_map = Map.Make(String)
let spf = Printf.sprintf
module Decode = struct
exception Error of string
type t = {
bs: bytes;
mutable off: int;
}
type 'a dec = t -> 'a
let fail_ e = raise (Error e)
let fail_eof_ what =
fail_ (spf "unexpected end of input, expected %s" what)
let uint (self:t) : int64 =
let rec loop () =
if self.off >= Bytes.length self.bs then fail_eof_ "uint";
let c = Char.code (Bytes.get self.bs self.off) in
self.off <- 1 + self.off; (* consume *)
if c land 0b1000_0000 <> 0 then (
let rest = loop() in
let c = Int64.of_int (c land 0b0111_1111) in
Int64.(logor (shift_left rest 7) c)
) else (
Int64.of_int c (* done *)
)
in
loop()
let int (self:t) : int64 =
let open Int64 in
let i = uint self in
let sign_bit = logand 0b1L i in (* true if negative *)
let sign = equal sign_bit 0L in
let res =
if sign then (
shift_right_logical i 1
) else (
(* put sign back *)
logor (shift_left 1L 63) (shift_right_logical (lognot i) 1)
)
in
res
let u8 self : char =
let x = Bytes.get self.bs self.off in
self.off <- self.off + 1;
x
let i8 = u8
let u16 self =
let x = Bytes.get_int16_le self.bs self.off in
self.off <- self.off + 2;
x
let i16 = u16
let u32 self =
let x = Bytes.get_int32_le self.bs self.off in
self.off <- self.off + 4;
x
let i32 = u32
let u64 self =
let i = Bytes.get_int64_le self.bs self.off in
self.off <- 8 + self.off;
i
let i64 = u64
let bool self : bool =
let c = Bytes.get self.bs self.off in
self.off <- 1 + self.off;
Char.code c <> 0
let f32 (self:t) : float =
let i = i32 self in
Int32.float_of_bits i
let f64 (self:t) : float =
let i = i64 self in
Int64.float_of_bits i
let data_of ~size self : bytes =
let s = Bytes.sub self.bs self.off size in
self.off <- self.off + size;
s
let data self : bytes =
let size = uint self in
if Int64.compare size (Int64.of_int Sys.max_string_length) > 0 then
fail_ "string too large";
let size = Int64.to_int size in (* fits, because of previous test *)
data_of ~size self
let string self : string =
Bytes.unsafe_to_string (data self)
let[@inline] optional dec self : _ option =
let c = u8 self in
if Char.code c = 0 then None else Some (dec self)
end
module Encode = struct
type t = Buffer.t
let of_buffer buf : t = buf
type 'a enc = t -> 'a -> unit
(* no need to check for overflow below *)
external unsafe_chr : int -> char = "%identity"
let uint (self:t) (i:int64) : unit =
let module I = Int64 in
let i = ref i in
let continue = ref true in
while !continue do
let j = I.logand 0b0111_1111L !i in
if !i = j then (
continue := false;
let j = I.to_int j in
Buffer.add_char self (unsafe_chr j)
) else (
(* set bit 8 to [1] *)
let lsb = I.to_int (I.logor 0b1000_0000L j) in
let lsb = (unsafe_chr lsb) in
Buffer.add_char self lsb;
i := I.shift_right_logical !i 7;
)
done
let[@inline] int (self:t) i =
let open Int64 in
let ui = logxor (shift_left i 1) (shift_right i 63) in
uint self ui
let u8 self x = Buffer.add_char self x
let i8 = u8
let u16 self x = Buffer.add_int16_le self x
let i16 = u16
let u32 self x = Buffer.add_int32_le self x
let i32 = u32
let u64 self x = Buffer.add_int64_le self x
let i64 = u64
let bool self x = Buffer.add_char self (if x then Char.chr 1 else Char.chr 0)
let f64 (self:t) x = Buffer.add_int64_le self (Int64.bits_of_float x)
let data_of ~size self x =
if size <> Bytes.length x then failwith "invalid length for Encode.data_of";
Buffer.add_bytes self x
let data self x =
uint self (Int64.of_int (Bytes.length x));
Buffer.add_bytes self x
let string self x = data self (Bytes.unsafe_of_string x)
let[@inline] optional enc self x : unit =
match x with
| None -> u8 self (Char.chr 0)
| Some x ->
u8 self (Char.chr 1);
enc self x
end
let to_string (e:'a Encode.enc) (x:'a) =
let buf = Buffer.create 32 in
e buf x;
Buffer.contents buf
let of_bytes_exn ?(off=0) dec bs =
let i = {Decode.bs; off} in
dec i
let of_bytes ?off dec bs =
try Ok (of_bytes_exn ?off dec bs)
with Decode.Error e -> Error e
let of_string_exn dec s = of_bytes_exn dec (Bytes.unsafe_of_string s)
let of_string dec s = of_bytes dec (Bytes.unsafe_of_string s)
(*$inject
let to_s f x =
let buf = Buffer.create 32 in
let out = Encode.of_buffer buf in
f out x;
Buffer.contents buf
let of_s f x =
let i = {Decode.off=0; bs=Bytes.unsafe_of_string x} in
f i
*)
(*$= & ~printer:Int64.to_string
37L (of_s Decode.uint (to_s Encode.uint 37L))
42L (of_s Decode.uint (to_s Encode.uint 42L))
0L (of_s Decode.uint (to_s Encode.uint 0L))
105542252L (of_s Decode.uint (to_s Encode.uint 105542252L))
Int64.max_int (of_s Decode.uint (to_s Encode.uint Int64.max_int))
*)
(*$= & ~printer:Int64.to_string
37L (of_s Decode.int (to_s Encode.int 37L))
42L (of_s Decode.int (to_s Encode.int 42L))
0L (of_s Decode.int (to_s Encode.int 0L))
105542252L (of_s Decode.int (to_s Encode.int 105542252L))
Int64.max_int (of_s Decode.int (to_s Encode.int Int64.max_int))
Int64.min_int (of_s Decode.int (to_s Encode.int Int64.min_int))
(-1209433446454112432L) (of_s Decode.int (to_s Encode.int (-1209433446454112432L)))
(-3112855215860398414L) (of_s Decode.int (to_s Encode.int (-3112855215860398414L)))
*)
(*$=
1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0]))
*)
(*$Q
Q.(int64) (fun s -> \
s = (of_s Decode.uint (to_s Encode.uint s)))
*)
(*$Q
Q.(int64) (fun s -> \
s = (of_s Decode.int (to_s Encode.int s)))
*)
(* TODO: some tests with qtest *)
end
module ID = struct
type t = int32
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
Bare.Decode.i32 dec
let encode (enc: Bare.Encode.t) (self: t) : unit =
Bare.Encode.i32 enc self
end
module Lit = struct
type t = ID.t
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
ID.decode dec
let encode (enc: Bare.Encode.t) (self: t) : unit =
ID.encode enc self
end
module Clause = struct
type t = {
lits: Lit.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lits =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> Lit.decode dec)) in
{lits; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
(let arr = self.lits in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> Lit.encode enc xi) arr);
end
end
module Step_input = struct
type t = {
c: Clause.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let c = Clause.decode dec in {c; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Clause.encode enc self.c; end
end
module Step_rup = struct
type t = {
res: Clause.t;
hyps: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let res = Clause.decode dec in
let hyps =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{res; hyps; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
Clause.encode enc self.res;
(let arr = self.hyps in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
end
module Step_bridge_lit_expr = struct
type t = {
lit: Lit.t;
expr: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lit = Lit.decode dec in let expr = ID.decode dec in {lit; expr; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Lit.encode enc self.lit; ID.encode enc self.expr; end
end
module Step_cc = struct
type t = {
eqns: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let eqns =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{eqns; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
(let arr = self.eqns in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
end
module Step_preprocess = struct
type t = {
t: ID.t;
u: ID.t;
using: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let t = ID.decode dec in
let u = ID.decode dec in
let using =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{t; u; using; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.t;
ID.encode enc self.u;
(let arr = self.using in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
end
module Fun_decl = struct
type t = {
f: string;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = Bare.Decode.string dec in {f; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Bare.Encode.string enc self.f; end
end
module Expr_bool = struct
type t = {
b: bool;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let b = Bare.Decode.bool dec in {b; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin Bare.Encode.bool enc self.b; end
end
module Expr_if = struct
type t = {
cond: ID.t;
then_: ID.t;
else_: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let cond = ID.decode dec in
let then_ = ID.decode dec in
let else_ = ID.decode dec in
{cond; then_; else_; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.cond;
ID.encode enc self.then_;
ID.encode enc self.else_;
end
end
module Expr_not = struct
type t = {
f: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = ID.decode dec in {f; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.f; end
end
module Expr_eq = struct
type t = {
lhs: ID.t;
rhs: ID.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let lhs = ID.decode dec in let rhs = ID.decode dec in {lhs; rhs; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.lhs; ID.encode enc self.rhs; end
end
module Expr_app = struct
type t = {
f: ID.t;
args: ID.t array;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let f = ID.decode dec in
let args =
(let len = Bare.Decode.uint dec in
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
{f; args; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin
ID.encode enc self.f;
(let arr = self.args in
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
Array.iter (fun xi -> ID.encode enc xi) arr);
end
end
module Step_view = struct
type t =
| Step_input of Step_input.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Fun_decl of Fun_decl.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let tag = Bare.Decode.uint dec in
match tag with
| 0L -> Step_input (Step_input.decode dec)
| 1L -> Step_rup (Step_rup.decode dec)
| 2L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
| 3L -> Step_cc (Step_cc.decode dec)
| 4L -> Step_preprocess (Step_preprocess.decode dec)
| 5L -> Fun_decl (Fun_decl.decode dec)
| 6L -> Expr_bool (Expr_bool.decode dec)
| 7L -> Expr_if (Expr_if.decode dec)
| 8L -> Expr_not (Expr_not.decode dec)
| 9L -> Expr_eq (Expr_eq.decode dec)
| 10L -> Expr_app (Expr_app.decode dec)
| _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
let encode (enc: Bare.Encode.t) (self: t) : unit =
match self with
| Step_input x ->
Bare.Encode.uint enc 0L;
Step_input.encode enc x
| Step_rup x ->
Bare.Encode.uint enc 1L;
Step_rup.encode enc x
| Step_bridge_lit_expr x ->
Bare.Encode.uint enc 2L;
Step_bridge_lit_expr.encode enc x
| Step_cc x ->
Bare.Encode.uint enc 3L;
Step_cc.encode enc x
| Step_preprocess x ->
Bare.Encode.uint enc 4L;
Step_preprocess.encode enc x
| Fun_decl x ->
Bare.Encode.uint enc 5L;
Fun_decl.encode enc x
| Expr_bool x ->
Bare.Encode.uint enc 6L;
Expr_bool.encode enc x
| Expr_if x ->
Bare.Encode.uint enc 7L;
Expr_if.encode enc x
| Expr_not x ->
Bare.Encode.uint enc 8L;
Expr_not.encode enc x
| Expr_eq x ->
Bare.Encode.uint enc 9L;
Expr_eq.encode enc x
| Expr_app x ->
Bare.Encode.uint enc 10L;
Expr_app.encode enc x
end
module Step = struct
type t = {
id: ID.t;
view: Step_view.t;
}
(** @raise Bare.Decode.Error in case of error. *)
let decode (dec: Bare.Decode.t) : t =
let id = ID.decode dec in let view = Step_view.decode dec in {id; view; }
let encode (enc: Bare.Encode.t) (self: t) : unit =
begin ID.encode enc self.id; Step_view.encode enc self.view; end
end