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

debug

Browse source
This commit is contained in:
Simon Cruanes 2022-02-03 14:09:56 -05:00
parent a98132ed0c
commit 9cf9b025ab
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 6 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/lra/sidekick_arith_lra.ml
View file

@ -693,9 +693,10 @@ module Make(A : ARG) : S with module A = A = struct
(* help generating model *) (* help generating model *)
let model_complete_ (self:state) _si ~add : unit = let model_complete_ (self:state) _si ~add : unit =
Log.debugf 30 (fun k->k "lra: model complete");
begin match self.last_res with begin match self.last_res with
| Some (SimpSolver.Sat m) -> | Some (SimpSolver.Sat m) when not (Vec.is_empty self.in_model) ->
Log.debugf 50 (fun k->k "lra: model complete"); Log.debugf 50 (fun k->k "(@[lra.in_model@ %a@])" (Vec.pp T.pp) self.in_model);
let add_t t = let add_t t =
match SimpSolver.V_map.get t m with match SimpSolver.V_map.get t m with

30
src/proof-trace/proof_ser.ml
View file

@ -1,4 +1,3 @@
(* generated from "proof_ser.bare" using bare-codegen *)
[@@@ocaml.warning "-26-27"] [@@@ocaml.warning "-26-27"]
(* embedded runtime library *) (* embedded runtime library *)
@ -259,40 +258,17 @@ let of_string dec s = of_bytes dec (Bytes.unsafe_of_string s)
1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0])) 1 (let s = to_s Encode.int (-1209433446454112432L) in 0x1 land (Char.code s.[0]))
*) *)
(*$Q & ~count:1000 (*$Q
Q.(int64) (fun s -> \ Q.(int64) (fun s -> \
s = (of_s Decode.uint (to_s Encode.uint s))) s = (of_s Decode.uint (to_s Encode.uint s)))
Q.(small_nat) (fun n -> \
let n = Int64.of_int n in \
n = (of_s Decode.uint (to_s Encode.uint n)))
*) *)
(*$Q & ~count:1000 (*$Q
Q.(int64) (fun s -> \ Q.(int64) (fun s -> \
s = (of_s Decode.int (to_s Encode.int s))) s = (of_s Decode.int (to_s Encode.int s)))
Q.(small_signed_int) (fun n -> \
let n = Int64.of_int n in \
n = (of_s Decode.int (to_s Encode.int n)))
*) *)
(*$R (* TODO: some tests with qtest *)
for i=0 to 1_000 do
let i = Int64.of_int i in
assert_equal ~printer:Int64.to_string i (of_s Decode.int (to_s Encode.int i))
done
*)
(*$R
for i=0 to 1_000 do
let i = Int64.of_int i in
assert_equal ~printer:Int64.to_string i (of_s Decode.uint (to_s Encode.uint i))
done
*)
(*$Q & ~count:1000
Q.(string) (fun s -> \
s = (of_s Decode.string (to_s Encode.string s)))
*)
end end