mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Pretty printing

Browse source
This commit is contained in:
martin-neuhaeusser 2016-04-06 12:39:19 +02:00
parent 1662ba8353
commit bd9d13279a
2 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/ml/z3.ml
View file

@ -679,13 +679,13 @@ struct
| _ ->
let nopatterns_arr = Array.of_list nopatterns in
Z3native.mk_quantifier_ex ctx universal
(match weight with | None -> 1 | Some x -> x)
(match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
(match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
(Array.length patterns_arr) patterns_arr
(Array.length nopatterns_arr) nopatterns_arr
(Array.length sorts_arr) sorts_arr
names_arr body
(match weight with | None -> 1 | Some x -> x)
(match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
(match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
(Array.length patterns_arr) patterns_arr
(Array.length nopatterns_arr) nopatterns_arr
(Array.length sorts_arr) sorts_arr
names_arr body
let _internal_mk_quantifier_const ~universal ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id =
let patterns_arr = Array.of_list patterns in

12
src/api/ml/z3.mli
View file

@ -285,7 +285,7 @@ sig
sig
(** Parameters of func_decls *)
type parameter =
P_Int of int
P_Int of int
| P_Dbl of float
| P_Sym of Symbol.symbol
| P_Srt of Sort.sort
@ -3232,21 +3232,21 @@ sig
val add : optimize -> Expr.expr list -> unit
(** Asssert a soft constraint.
Supply integer weight and string that identifies a group
Supply integer weight and string that identifies a group
of soft constraints.
*)
*)
val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle
(** Add maximization objective.
*)
*)
val maximize : optimize -> Expr.expr -> handle
(** Add minimization objective.
*)
*)
val minimize : optimize -> Expr.expr -> handle
(** Checks whether the assertions in the context are satisfiable and solves objectives.
*)
*)
val check : optimize -> Solver.status
(** Retrieve model from satisfiable context *)