Skip to content

Commit

Permalink
more fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
Gbury committed May 2, 2024
1 parent b267ef4 commit 2a13549
Show file tree
Hide file tree
Showing 5 changed files with 55 additions and 36 deletions.
19 changes: 12 additions & 7 deletions src/languages/smtlib2/poly/print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -672,7 +672,7 @@ module Make
| B.Fp_isSubnormal _ -> simple "fp.isSubnormal"
| B.Fp_isZero _ -> simple "fp.isZero"
| B.Fp_isInfinite _ -> simple "fp.isInfinite"
| B.Fp_isNaN _ -> simple "fp.isNan"
| B.Fp_isNaN _ -> simple "fp.isNaN"
| B.Fp_isNegative _ -> simple "fp.isNegative"
| B.Fp_isPositive _ -> simple "fp.isPositive"
| B.To_real _ -> simple "fp.to_real"
Expand Down Expand Up @@ -756,7 +756,7 @@ module Make
(* reset some env state *)
let env = set_omit_to_real env false in
(* actual printing *)
Format.fprintf fmt "@[<hv 2>(match@ @[<hov>%a@]@ (%a))"
Format.fprintf fmt "@[<hv 2>(match@ @[<hov>%a@]@ (%a))@]"
(term env) scrutinee
(list match_case env) cases

Expand Down Expand Up @@ -1023,10 +1023,15 @@ module Make
let define_fun_rec = define_fun_aux ~recursive:true

let define_funs_rec env fmt l =
let fun_body env fmt (_, _, _, body) = term env fmt body in
let fun_decl env fmt (f, vars, params, body) =
let env = List.fold_left Env.Ty_var.bind env vars in
let env = List.fold_left Env.Term_var.bind env params in
let l =
List.map (fun (f, vars, params, body) ->
let env = List.fold_left Env.Ty_var.bind env vars in
let env = List.fold_left Env.Term_var.bind env params in
(env, f, vars, params, body)
) l
in
let fun_body _env fmt (env, _, _, _, body) = term env fmt body in
let fun_decl _env fmt (env, f, vars, params, body) =
match vars with
| [] ->
Format.fprintf fmt "@[<hov 1>(%a@ (%a)@ %a)@]"
Expand All @@ -1041,7 +1046,7 @@ module Make
(ty env) (V.Term.ty body)
in
Format.fprintf fmt
"@[<v 2>(define-funs-rec@ @[<v 2>(%a)@]@ @[<v 2>(%a)@])@]"
"@[<v 2>(define-funs-rec@ @[<v 1>(%a)@]@ @[<v 1>(%a)@])@]"
(list fun_decl env) l
(list fun_body env) l

Expand Down
35 changes: 21 additions & 14 deletions src/languages/smtlib2/v2.6/script/print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -675,7 +675,7 @@ module Make
| B.Fp_isSubnormal _ -> simple "fp.isSubnormal"
| B.Fp_isZero _ -> simple "fp.isZero"
| B.Fp_isInfinite _ -> simple "fp.isInfinite"
| B.Fp_isNaN _ -> simple "fp.isNan"
| B.Fp_isNaN _ -> simple "fp.isNaN"
| B.Fp_isNegative _ -> simple "fp.isNegative"
| B.Fp_isPositive _ -> simple "fp.isPositive"
| B.To_real _ -> simple "fp.to_real"
Expand Down Expand Up @@ -759,7 +759,7 @@ module Make
(* reset some env state *)
let env = set_omit_to_real env false in
(* actual printing *)
Format.fprintf fmt "@[<hv 2>(match@ @[<hov>%a@]@ (%a))"
Format.fprintf fmt "@[<hv 2>(match@ @[<hov>%a@]@ (%a))@]"
(term env) scrutinee
(list match_case env) cases

Expand Down Expand Up @@ -1003,20 +1003,27 @@ module Make
let define_fun_rec = define_fun_aux ~recursive:true

let define_funs_rec env fmt l =
let fun_body env fmt (_, _, _, body) = term env fmt body in
let fun_decl env fmt (f, vars, params, body) =
let env = List.fold_left Env.Term_var.bind env params in
match (vars : V.Ty.Var.t list) with
| [] ->
Format.fprintf fmt "@[<hov 1>(%a@ (%a)@ %a)@]"
(term_cst env) f
(list sorted_var env) params
(ty env) (V.Term.ty body)
| _ :: _ ->
_cannot_print "polymorphic function definition"
let l =
List.map (fun (f, vars, params, body) ->
match vars with
| [] ->
let env = List.fold_left Env.Term_var.bind env params in
(env, f, params, body)
| _ :: _ ->
_cannot_print "polymorphic function definition"
) l
in
let fun_body _env fmt (env, _, _, body) =
term env fmt body
in
let fun_decl _env fmt (env, f, params, body) =
Format.fprintf fmt "@[<hov 1>(%a@ (%a)@ %a)@]"
(term_cst env) f
(list sorted_var env) params
(ty env) (V.Term.ty body)
in
Format.fprintf fmt
"@[<v 2>(define-funs-rec@ @[<v 2>(%a)@]@ @[<v 2>(%a)@])@]"
"@[<v 2>(define-funs-rec@ @[<v 1>(%a)@]@ @[<v 1>(%a)@])@]"
(list fun_decl env) l
(list fun_body env) l

Expand Down
7 changes: 4 additions & 3 deletions src/loop/transform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,9 +82,10 @@ module Make
}

let flush acc res set_logic tail =
let res = res @
List.rev_append acc.pre_logic_stmts (
set_logic :: List.rev_append acc.post_logic_stmts tail)
let res =
res @
List.rev_append acc.pre_logic_stmts (
set_logic :: List.rev_append acc.post_logic_stmts tail)
in
let acc = { acc with pre_logic_stmts = []; post_logic_stmts = []; } in
acc, res
Expand Down
19 changes: 13 additions & 6 deletions src/typecheck/logic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -608,10 +608,11 @@ module Smtlib2 = struct
scan_term acc body

and scan_app acc f ty_args t_args =
let aux_terms acc =
List.fold_left scan_term acc t_args
in
let aux acc =
List.fold_left scan_term
(List.fold_left scan_ty acc ty_args)
t_args
aux_terms (List.fold_left scan_ty acc ty_args)
in
match (V.Term.Cst.builtin f) with

Expand All @@ -634,11 +635,17 @@ module Smtlib2 = struct

(* Core *)
| B.True | B.False
| B.Neg | B.And | B.Or | B.Nor
| B.Xor | B.Imply | B.Implied | B.Ite
| B.Equiv | B.Equal | B.Distinct
| B.Neg | B.And | B.Or | B.Nor | B.Xor
| B.Imply | B.Implied | B.Ite | B.Equiv
-> aux acc

| B.Equal | B.Distinct
(* In this case, we don't really want the type of the values being
compared to influence the logics. In particular, the FP theory
can create and compare values of bitvector type without the
BV theory. *)
-> aux_terms acc

(* Arrays
for these, we try and accurately track exactly what kind
of arrays are used (e.g. only ints-ints, ints-reals, etc..).
Expand Down
11 changes: 5 additions & 6 deletions tools/gentests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -214,19 +214,19 @@ let typechecks dir =
let file = Filename.concat dir "flags.dune" in
not (contains "--type=false" file)

let already_has_flow_check dir =
let has_flow_check dir =
let file = Filename.concat dir "flags.dune" in
contains "--check-flow" file

let format_stanza ?(deps=[]) fmt (pb_file, out_file, need_flow) =
let format_stanza ?(deps=[]) fmt (pb_file, out_file) =
Format.fprintf fmt "
@[<v 2>(rule@ \
(target %s)@ \
(deps @[<hov>%a@])@ \
(package dolmen_bin)@ \
(action @[<hov 1>(chdir %%{workspace_root}@ \
@[<hov 1>(with-accepted-exit-codes 0@ \
@[<hov 1>(run dolmen %s %%{input} %%{target} %%{read-lines:flags.dune})@]\
@[<hov 1>(run dolmen %%{input} %%{target} %%{read-lines:flags.dune})@]\
)@]\
)@]\
))@]@\n\
Expand All @@ -236,7 +236,6 @@ let format_stanza ?(deps=[]) fmt (pb_file, out_file, need_flow) =
(action (diff %s %s))@])@\n"
out_file
pp_deps (pb_file, None, deps)
(if need_flow then "--check-flow=true" else "")
pb_file out_file


Expand Down Expand Up @@ -282,10 +281,10 @@ let gen_test fmt path pb =
if (exit_codes = Success) &&
(supports_formatting pb) &&
(typechecks path) &&
not (already_has_flow_check path)
not (has_flow_check path)
then begin
let out_f = formatted_of_problem pb in
format_stanza ~deps fmt (pb, out_f, true)
format_stanza ~deps fmt (pb, out_f)
end;
()

Expand Down

0 comments on commit 2a13549

Please sign in to comment.